let n, m be Nat; :: thesis: for M being Matrix of n,m,F_Real st the_rank_of M = n holds
M is OrdBasis of Lin (lines M)
let M be Matrix of n,m,F_Real; :: thesis: ( the_rank_of M = n implies M is OrdBasis of Lin (lines M) )
A1: lines M c= [#] (Lin (lines M)) by Lm4;
then reconsider L = lines M as Subset of (Lin (lines M)) ;
reconsider B = M as FinSequence of (Lin (lines M)) by A1, FINSEQ_1:def 4;
assume A2: the_rank_of M = n ; :: thesis: M is OrdBasis of Lin (lines M)
A3: M is one-to-one by A2, MATRIX13:121;
lines M is linearly-independent by A2, MATRIX13:121;
then A4: L is linearly-independent by VECTSP_9:12;
Lin L = Lin (lines M) by VECTSP_9:17;
then L is Basis of (Lin (lines M)) by A4, VECTSP_7:def 3;
then B is OrdBasis of Lin (lines M) by A3, MATRLIN:def 2;
hence M is OrdBasis of Lin (lines M) ; :: thesis: verum