let n be Nat; :: thesis: for B being Subset of (RealVectSpace (Seg n)) st B is Basis of RealVectSpace (Seg n) holds
card B = n
let B be Subset of (RealVectSpace (Seg n)); :: thesis: ( B is Basis of RealVectSpace (Seg n) implies card B = n )
assume A1: B is Basis of RealVectSpace (Seg n) ; :: thesis: card B = n
reconsider Br = RN_Base n as Subset of (RealVectSpace (Seg n)) by FINSEQ_2:93;
Br is Basis of RealVectSpace (Seg n) by Th44;
then card Br = card B by A1, RLVECT_5:25;
hence card B = n by Lm5; :: thesis: verum