let n, m be Nat; :: thesis: for K being Field
for M being Matrix of m,n,K st the_rank_of M = m holds
M is without_repeated_line
let K be Field; :: thesis: for M being Matrix of m,n,K st the_rank_of M = m holds
M is without_repeated_line
let M be Matrix of m,n,K; :: thesis: ( the_rank_of M = m implies M is without_repeated_line )
assume A1: the_rank_of M = m ; :: thesis: M is without_repeated_line
assume not M is without_repeated_line ; :: thesis: contradiction
then consider x1, x2 being set such that
A2: ( x1 in dom M & x2 in dom M & M . x1 = M . x2 & x1 <> x2 ) by FUNCT_1:def 8;
A3: ( dom M = Seg (len M) & len M = m ) by FINSEQ_1:def 3, MATRIX_1:def 3;
reconsider x1 = x1, x2 = x2 as Element of NAT by A2;
consider k being Nat such that
A4: ( len M = k + 1 & len (Del M,x1) = k ) by A2, FINSEQ_3:113;
( M . x1 = Line M,x1 & M . x2 = Line M,x2 ) by A2, A3, MATRIX_2:10;
then M = RLine M,x1,(Line M,x2) by A2, MATRIX11:30
.= RLine M,x1,((1_ K) * (Line M,x2)) by FVSUM_1:70 ;
then m = the_rank_of (DelLine M,x1) by A1, A2, A3, Th93;
then m <= k by A4, Th74;
hence contradiction by A3, A4, NAT_1:13; :: thesis: verum