let m be Nat; :: thesis: for K being Field
for A, B being Matrix of K st B = 0. (K,(len A),m) holds
the_rank_of A = the_rank_of (A ^^ B)
let K be Field; :: thesis: for A, B being Matrix of K st B = 0. (K,(len A),m) holds
the_rank_of A = the_rank_of (A ^^ B)
let A, B be Matrix of K; :: thesis: ( B = 0. (K,(len A),m) implies the_rank_of A = the_rank_of (A ^^ B) )
assume A1: B = 0. (K,(len A),m) ; :: thesis: the_rank_of A = the_rank_of (A ^^ B)
A2: len B = len A by A1, MATRIX_0:def 2;
set L = len A;
reconsider B9 = B as Matrix of len A, width B,K by A2, MATRIX_0:51;
reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;
set AB = A9 ^^ B9;

per cases ( width B = 0 or width B > 0 ) ;

suppose width B = 0 ; :: thesis: the_rank_of A = the_rank_of (A ^^ B)

hence the_rank_of A = the_rank_of (A ^^ B) by A2, Th22; :: thesis: verum

end;

suppose width B > 0 ; :: thesis: the_rank_of A = the_rank_of (A ^^ B)

then A3: len A > 0 by A2, MATRIX_0:def 3;
then A4: width (A9 ^^ B9) = (width A) + (width B) by MATRIX_0:23;
A5: len (A9 ^^ B9) = len A by A3, MATRIX_0:23;

A6: now :: thesis: for i being Nat st i in (Seg (width (A9 ^^ B9))) \ (Seg (width A)) holds
Col ((A9 ^^ B9),i) = (len (A9 ^^ B9)) |-> (0. K)

set L0 = (len (A9 ^^ B9)) |-> (0. K);
let i be Nat; :: thesis: ( i in (Seg (width (A9 ^^ B9))) \ (Seg (width A)) implies Col ((A9 ^^ B9),i) = (len (A9 ^^ B9)) |-> (0. K) )
assume A7: i in (Seg (width (A9 ^^ B9))) \ (Seg (width A)) ; :: thesis: Col ((A9 ^^ B9),i) = (len (A9 ^^ B9)) |-> (0. K)
A8: i in Seg (width (A9 ^^ B9)) by A7, XBOOLE_0:def 5;
not i in Seg (width A) by A7, XBOOLE_0:def 5;
then A9: ( i < 1 or i > width A ) ;
then reconsider n = i - (width A) as Element of NAT by A8, FINSEQ_1:1, NAT_1:21;
A10: i = n + (width A) ;
n <> 0 by A8, A9, FINSEQ_1:1;
then A11: n in Seg (width B) by A4, A8, A10, FINSEQ_1:61;

A12: now :: thesis: for i being Nat st 1 <= i & i <= len A holds
(Col (B9,n)) . i = ((len (A9 ^^ B9)) |-> (0. K)) . i

let i be Nat; :: thesis: ( 1 <= i & i <= len A implies (Col (B9,n)) . i = ((len (A9 ^^ B9)) |-> (0. K)) . i )
assume A13: ( 1 <= i & i <= len A ) ; :: thesis: (Col (B9,n)) . i = ((len (A9 ^^ B9)) |-> (0. K)) . i
A14: i in Seg (len A) by A13;
then A15: ((len (A9 ^^ B9)) |-> (0. K)) . i = 0. K by A5, FINSEQ_2:57;
Seg (len A) = dom B by A2, FINSEQ_1:def 3;
then ( (Col (B9,n)) . i = B9 * (i,n) & [i,n] in Indices B ) by A11, A14, MATRIX_0:def 8, ZFMISC_1:87;
hence (Col (B9,n)) . i = ((len (A9 ^^ B9)) |-> (0. K)) . i by A1, A15, MATRIX_3:1; :: thesis: verum

end;

A16: ( len (Col (B,n)) = len A & len ((len (A9 ^^ B9)) |-> (0. K)) = len A ) by A2, A5, CARD_1:def 7;
Col ((A9 ^^ B9),i) = Col (B9,n) by A10, A11, Th17;
hence Col ((A9 ^^ B9),i) = (len (A9 ^^ B9)) |-> (0. K) by A16, A12; :: thesis: verum

end;

width A <= width (A9 ^^ B9) by A4, NAT_1:11;
then Seg (width A) c= Seg (width (A9 ^^ B9)) by FINSEQ_1:5;
hence the_rank_of (A ^^ B) = the_rank_of (Segm ((A9 ^^ B9),(Seg (len (A9 ^^ B9))),(Seg (width A)))) by A6, Th12
.= the_rank_of A by A5, Th19 ;
:: thesis: verum

end;

end;