let K be Ring; :: thesis: for A being Matrix of K holds A * (0. (K,(width A),(width A))) = 0. (K,(len A),(width A))
let A be Matrix of K; :: thesis: A * (0. (K,(width A),(width A))) = 0. (K,(len A),(width A))
A1: width (- (A * (0. (K,(width A),(width A))))) = width (A * (0. (K,(width A),(width A)))) by MATRIX_3:def 2;
set B = A * (0. (K,(width A),(width A)));

per cases ( width A > 0 or width A = 0 ) by NAT_1:3;

suppose A2: width A > 0 ; :: thesis: A * (0. (K,(width A),(width A))) = 0. (K,(len A),(width A))

A3: len (0. (K,(width A),(width A))) = width A by MATRIX_0:def 2;
then A4: len (A * (0. (K,(width A),(width A)))) = len A by MATRIX_3:def 4;
A5: width (0. (K,(width A),(width A))) = width A by A2, A3, MATRIX_0:20;
then A6: width (A * (0. (K,(width A),(width A)))) = width A by A3, MATRIX_3:def 4;
A * (0. (K,(width A),(width A))) = A * ((0. (K,(width A),(width A))) + (0. (K,(width A),(width A)))) by MATRIX_3:4
.= (A * (0. (K,(width A),(width A)))) + (A * (0. (K,(width A),(width A)))) by A3, A5, MATRIX_4:62 ;
then ( len (- (A * (0. (K,(width A),(width A))))) = len (A * (0. (K,(width A),(width A)))) & 0. (K,(len A),(width A)) = ((A * (0. (K,(width A),(width A)))) + (A * (0. (K,(width A),(width A))))) + (- (A * (0. (K,(width A),(width A))))) ) by A4, A6, MATRIX_3:def 2, MATRIX_4:2;
then 0. (K,(len A),(width A)) = (A * (0. (K,(width A),(width A)))) + ((A * (0. (K,(width A),(width A)))) - (A * (0. (K,(width A),(width A))))) by A1, MATRIX_3:3
.= A * (0. (K,(width A),(width A))) by A4, A1, MATRIX_4:20 ;
hence A * (0. (K,(width A),(width A))) = 0. (K,(len A),(width A)) ; :: thesis: verum

end;

suppose A7: width A = 0 ; :: thesis: A * (0. (K,(width A),(width A))) = 0. (K,(len A),(width A))

set LHS = A * (0. (K,(width A),(width A)));
set RHS = 0. (K,(len A),(width A));

per cases ( len A = 0 or len A > 0 ) by NAT_1:3;

suppose A8: len A = 0 ; :: thesis: A * (0. (K,(width A),(width A))) = 0. (K,(len A),(width A))

A9: len (0. (K,(width A),(width A))) = 0 by A7, MATRIX_0:22;
A10: width (0. (K,(width A),(width A))) = 0 by A7, MATRIX_0:22;
A11: ( len (A * (0. (K,(width A),(width A)))) = len A & width (A * (0. (K,(width A),(width A)))) = width (0. (K,(width A),(width A))) ) by A7, A9, MATRIX_3:def 4;
then width (A * (0. (K,(width A),(width A)))) = 0 by A10;
then Seg (width (A * (0. (K,(width A),(width A))))) = {} ;
then {} = [:(dom (A * (0. (K,(width A),(width A))))),(Seg (width (A * (0. (K,(width A),(width A)))))):] by ZFMISC_1:90
.= Indices (A * (0. (K,(width A),(width A)))) by MATRIX_0:def 4 ;
then A12: for i, j being Nat st [i,j] in Indices (A * (0. (K,(width A),(width A)))) holds
(A * (0. (K,(width A),(width A)))) * (i,j) = (0. (K,(len A),(width A))) * (i,j) ;
( len (A * (0. (K,(width A),(width A)))) = len (0. (K,(len A),(width A))) & width (A * (0. (K,(width A),(width A)))) = width (0. (K,(len A),(width A))) ) by A8, A10, A11, MATRIX_0:22;
hence A * (0. (K,(width A),(width A))) = 0. (K,(len A),(width A)) by A12, MATRIX_0:21; :: thesis: verum

end;

suppose A13: len A > 0 ; :: thesis: A * (0. (K,(width A),(width A))) = 0. (K,(len A),(width A))

A14: width (0. (K,(width A),(width A))) = 0 by A7, MATRIX_0:22;
len (0. (K,(width A),(width A))) = width A by A7, MATRIX_0:22;
then A15: ( len (A * (0. (K,(width A),(width A)))) = len A & width (A * (0. (K,(width A),(width A)))) = width (0. (K,(width A),(width A))) ) by MATRIX_3:def 4;
Seg (width (A * (0. (K,(width A),(width A))))) = {} by A14, A15;
then {} = [:(dom (A * (0. (K,(width A),(width A))))),(Seg (width (A * (0. (K,(width A),(width A)))))):] by ZFMISC_1:90
.= Indices (A * (0. (K,(width A),(width A)))) by MATRIX_0:def 4 ;
then A16: for i, j being Nat st [i,j] in Indices (A * (0. (K,(width A),(width A)))) holds
(A * (0. (K,(width A),(width A)))) * (i,j) = (0. (K,(len A),(width A))) * (i,j) ;
( len (A * (0. (K,(width A),(width A)))) = len (0. (K,(len A),(width A))) & width (A * (0. (K,(width A),(width A)))) = width (0. (K,(len A),(width A))) ) by A7, A14, A15, A13, MATRIX_0:23;
hence A * (0. (K,(width A),(width A))) = 0. (K,(len A),(width A)) by A16, MATRIX_0:21; :: thesis: verum

end;

end;

end;

end;