let n', m', j, i be Nat; :: thesis: for K being Field
for a being Element of K
for M' being Matrix of n',m',K st j in Seg (len M') & j <> i holds
the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,(a * (Line M',j)))
let K be Field; :: thesis: for a being Element of K
for M' being Matrix of n',m',K st j in Seg (len M') & j <> i holds
the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,(a * (Line M',j)))
let a be Element of K; :: thesis: for M' being Matrix of n',m',K st j in Seg (len M') & j <> i holds
the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,(a * (Line M',j)))
let M' be Matrix of n',m',K; :: thesis: ( j in Seg (len M') & j <> i implies the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,(a * (Line M',j))) )
assume A1: ( j in Seg (len M') & i <> j ) ; :: thesis: the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,(a * (Line M',j)))

per cases ( i in Seg (len M') or not i in Seg (len M') ) ;

suppose A2: i in Seg (len M') ; :: thesis: the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,(a * (Line M',j)))

set W = width M';
set Li = Line M',i;
set Lj = Line M',j;
set R = RLine M',i,((0. K) * (Line M',i));
A3: ( width M' = len (Line M',i) & width M' = len ((0. K) * (Line M',i)) & width M' = len (a * (Line M',j)) ) by FINSEQ_1:def 18;
then A4: ( len (RLine M',i,((0. K) * (Line M',i))) = len M' & width (RLine M',i,((0. K) * (Line M',i))) = width M' & len M' = n' ) by MATRIX11:def 3, MATRIX_1:def 3;
reconsider 0Li = (0. K) * (Line M',i), aLj = a * (Line M',j) as Element of the carrier of K * by FINSEQ_1:def 11;
( Line (RLine M',i,((0. K) * (Line M',i))),i = (0. K) * (Line M',i) & Line (RLine M',i,((0. K) * (Line M',i))),j = Line M',j ) by A1, A2, A3, A4, MATRIX11:28;
then A5: (Line (RLine M',i,((0. K) * (Line M',i))),i) + (a * (Line (RLine M',i,((0. K) * (Line M',i))),j)) = ((width M') |-> (0. K)) + (a * (Line M',j)) by FVSUM_1:71
.= a * (Line M',j) by FVSUM_1:28 ;
A6: RLine (RLine M',i,((0. K) * (Line M',i))),i,aLj = Replace (RLine M',i,((0. K) * (Line M',i))),i,aLj by A3, A4, MATRIX11:29
.= Replace (Replace M',i,0Li),i,aLj by A3, MATRIX11:29
.= Replace M',i,aLj by FUNCT_7:36
.= RLine M',i,aLj by A3, MATRIX11:29 ;
thus the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,((0. K) * (Line M',i))) by A3, Th91
.= the_rank_of (RLine M',i,(a * (Line M',j))) by A1, A4, A5, A6, Th92 ; :: thesis: verum

end;

suppose A7: not i in Seg (len M') ; :: thesis: the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,(a * (Line M',j)))

then not i in dom M' by FINSEQ_1:def 3;
then ( DelLine M',i = M' & RLine M',i,(a * (Line M',j)) = M' ) by A7, Th40, FINSEQ_3:113;
hence the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,(a * (Line M',j))) ; :: thesis: verum

end;

end;