let n9, m9, i be Nat; :: thesis: for K being Field
for M9 being Matrix of n9,m9,K
for p being FinSequence of K st len p = width M9 holds
the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,((0. K) * p)))
let K be Field; :: thesis: for M9 being Matrix of n9,m9,K
for p being FinSequence of K st len p = width M9 holds
the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,((0. K) * p)))
let M9 be Matrix of n9,m9,K; :: thesis: for p being FinSequence of K st len p = width M9 holds
the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,((0. K) * p)))
let p be FinSequence of K; :: thesis: ( len p = width M9 implies the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,((0. K) * p))) )
assume A1: len p = width M9 ; :: thesis: the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,((0. K) * p)))
set R = RLine (M9,i,((0. K) * p));
A2: Seg (len M9) = dom M9 by FINSEQ_1:def 3;
A3: len M9 = n9 by MATRIX_1:def 3;

per cases ( not i in dom M9 or i in dom M9 ) ;

suppose A4: not i in dom M9 ; :: thesis: the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,((0. K) * p)))

then RLine (M9,i,((0. K) * p)) = M9 by A2, Th40;
hence the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,((0. K) * p))) by A4, FINSEQ_3:113; :: thesis: verum

end;

suppose A5: i in dom M9 ; :: thesis: the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,((0. K) * p)))

then B5: n9 <> 0 by A2, A3;
set KK = the carrier of K;
A6: p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:110;
A7: len ((0. K) * p) = len p by MATRIXR1:16;
then Line ((RLine (M9,i,((0. K) * p))),i) = (0. K) * p by A1, A2, A3, A5, MATRIX11:28;
then A8: Line ((RLine (M9,i,((0. K) * p))),i) = (len p) |-> (0. K) by A6, FVSUM_1:71;
reconsider 0p = (0. K) * p as Element of the carrier of K * by FINSEQ_1:def 11;
A9: i in NAT by ORDINAL1:def 13;
RLine (M9,i,((0. K) * p)) = Replace (M9,i,0p) by A1, A7, MATRIX11:29;
then A10: Replace ((RLine (M9,i,((0. K) * p))),i,0p) = Replace (M9,i,0p) by FUNCT_7:36;
A11: width (RLine (M9,i,((0. K) * p))) = m9 by Th1, B5;
width M9 = m9 by Th1, B5;
then the_rank_of (RLine (M9,i,((0. K) * p))) = the_rank_of (DelLine ((RLine (M9,i,((0. K) * p))),i)) by A1, A11, A8, Th90;
hence the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,((0. K) * p))) by A10, A9, COMPUT_1:7; :: thesis: verum

end;

end;