let i, m9, n9 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_0:def 2;

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:104; :: 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 A6: n9 <> 0 by A2, A3;
set KK = the carrier of K;
A7: p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
A8: 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 A9: Line ((RLine (M9,i,((0. K) * p))),i) = (len p) |-> (0. K) by A7, FVSUM_1:58;
reconsider 0p = (0. K) * p as Element of the carrier of K * by FINSEQ_1:def 11;
RLine (M9,i,((0. K) * p)) = Replace (M9,i,0p) by A1, A8, MATRIX11:29;
then A11: Replace ((RLine (M9,i,((0. K) * p))),i,0p) = Replace (M9,i,0p) by FUNCT_7:34;
A12: width (RLine (M9,i,((0. K) * p))) = m9 by Th1, A6;
width M9 = m9 by Th1, A6;
then the_rank_of (RLine (M9,i,((0. K) * p))) = the_rank_of (DelLine ((RLine (M9,i,((0. K) * p))),i)) by A1, A12, A9, Th90;
hence the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,((0. K) * p))) by A11, COMPUT_1:4; :: thesis: verum

end;

end;