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 (REAL-L n) ;
B0 is Basis of REAL-L n by Th59;
hence card B = n by Th56; :: thesis: verum