Theorem orthonormal_empty

Modification history