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:93;
B0 is Basis of RealVectSpace (Seg n) by Th49;
hence card B = n by Th46; :: thesis: verum