let n', m', j, i be Nat; :: thesis: for K being Field
for a being Element of
for M' being Matrix of the carrier of K,n', 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
for M' being Matrix of the carrier of K,n', 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 ; :: thesis: for M' being Matrix of the carrier of K,n', 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 the carrier of K,n',; :: 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 that
A1: j in Seg (len M') and
A2: 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 A3: i in Seg (len M') ; :: thesis: the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,(a * (Line M',j)))

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

end;

suppose A11: 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' by FINSEQ_3:113;
hence the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,(a * (Line M',j))) by A11, Th40; :: thesis: verum

end;

end;