let n9, m9, j, i be Nat; :: thesis: for K being Field
for a being Element of K
for M9 being Matrix of n9,m9,K st j in Seg (len M9) & j <> i holds
the_rank_of (DelLine M9,i) = the_rank_of (RLine M9,i,(a * (Line M9,j)))
let K be Field; :: thesis: for a being Element of K
for M9 being Matrix of n9,m9,K st j in Seg (len M9) & j <> i holds
the_rank_of (DelLine M9,i) = the_rank_of (RLine M9,i,(a * (Line M9,j)))
let a be Element of K; :: thesis: for M9 being Matrix of n9,m9,K st j in Seg (len M9) & j <> i holds
the_rank_of (DelLine M9,i) = the_rank_of (RLine M9,i,(a * (Line M9,j)))
let M9 be Matrix of n9,m9,K; :: thesis: ( j in Seg (len M9) & j <> i implies the_rank_of (DelLine M9,i) = the_rank_of (RLine M9,i,(a * (Line M9,j))) )
assume that
A1: j in Seg (len M9) and
A2: i <> j ; :: thesis: the_rank_of (DelLine M9,i) = the_rank_of (RLine M9,i,(a * (Line M9,j)))

per cases ( i in Seg (len M9) or not i in Seg (len M9) ) ;

suppose A3: i in Seg (len M9) ; :: thesis: the_rank_of (DelLine M9,i) = the_rank_of (RLine M9,i,(a * (Line M9,j)))

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

end;

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

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

end;

end;