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_1:def 3;
set L = len A;
reconsider B9 = B as Matrix of len A, width B,K by A2, MATRIX_2:7;
reconsider A9 = A as Matrix of len A, width A,K by MATRIX_2:7;
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_1:def 4;
then A4: width (A9 ^^ B9) = (width A) + (width B) by MATRIX_1:24;
A5: len (A9 ^^ B9) = len A by A3, MATRIX_1:24;

A6: now

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 ) by A7;
then reconsider n = i - (width A) as Element of NAT by A8, FINSEQ_1:3, NAT_1:21;
A10: i = n + (width A) ;
n <> 0 by A8, A9, FINSEQ_1:3;
then A11: n in Seg (width B) by A4, A8, A10, FINSEQ_1:82;

A12: now

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
i in NAT by ORDINAL1:def 13;
then A14: i in Seg (len A) by A13;
then A15: ((len (A9 ^^ B9)) |-> (0. K)) . i = 0. K by A5, FINSEQ_2:71;
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_1:def 9, ZFMISC_1:106;
hence (Col B9,n) . i = ((len (A9 ^^ B9)) |-> (0. K)) . i by A1, A15, MATRIX_3:3; :: thesis: verum

end;

A16: ( len (Col B,n) = len A & len ((len (A9 ^^ B9)) |-> (0. K)) = len A ) by A2, A5, FINSEQ_1:def 18;
Col (A9 ^^ B9),i = Col B9,n by A10, A11, Th17;
hence Col (A9 ^^ B9),i = (len (A9 ^^ B9)) |-> (0. K) by A16, A12, FINSEQ_1:18; :: 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:7;
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;