let n be Nat; :: thesis: for B being Orthogonal_Basis of n holds card B = n
let B be Orthogonal_Basis of n; :: thesis: card B = n
reconsider B0 = B as Subset of (RealVectSpace (Seg n)) by FINSEQ_2:111;
B0 is Basis of RealVectSpace (Seg n) by Th59;
hence card B = n by Th56; :: thesis: verum