let n be Nat; :: thesis: for R being Ring
for A being Matrix of R st n = width (0. (R,(width A),n)) holds
A * (0. (R,(width A),n)) = 0. (R,(len A),n)
let R be Ring; :: thesis: for A being Matrix of R st n = width (0. (R,(width A),n)) holds
A * (0. (R,(width A),n)) = 0. (R,(len A),n)
let A be Matrix of R; :: thesis: ( n = width (0. (R,(width A),n)) implies A * (0. (R,(width A),n)) = 0. (R,(len A),n) )
assume A1: n = width (0. (R,(width A),n)) ; :: thesis: A * (0. (R,(width A),n)) = 0. (R,(len A),n)
set B = A * (0. (R,(width A),n));

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

suppose A3: width A > 0 ; :: thesis: A * (0. (R,(width A),n)) = 0. (R,(len A),n)

A4: len (0. (R,(width A),n)) = width A by MATRIX_0:def 2;
then A5: len (A * (0. (R,(width A),n))) = len A by MATRIX_3:def 4;
width (0. (R,(width A),n)) = n by A3, A4, MATRIX_0:20;
then A7: width (A * (0. (R,(width A),n))) = n by A4, MATRIX_3:def 4;

per cases ( len A = 0 or len A > 0 ) ;

suppose len A = 0 ; :: thesis: A * (0. (R,(width A),n)) = 0. (R,(len A),n)

hence A * (0. (R,(width A),n)) = 0. (R,(len A),n) by A3, MATRIX_0:def 3; :: thesis: verum

end;

suppose len A > 0 ; :: thesis: A * (0. (R,(width A),n)) = 0. (R,(len A),n)

then reconsider LHS = A * (0. (R,(width A),n)) as Matrix of len A,n,R by A5, A7, MATRIX_0:20;
A * (0. (R,(width A),n)) = A * ((0. (R,(width A),n)) + (0. (R,(width A),n))) by MATRIX_3:4
.= (A * (0. (R,(width A),n))) + (A * (0. (R,(width A),n))) by A4, MATRIX_4:62 ;
then ( len (- (A * (0. (R,(width A),n)))) = len (A * (0. (R,(width A),n))) & 0. (R,(len A),n) = ((A * (0. (R,(width A),n))) + (A * (0. (R,(width A),n)))) + (- (A * (0. (R,(width A),n)))) ) by A5, A7, MATRIX_1:def 4, MATRIX_4:2;
then 0. (R,(len A),n) = (A * (0. (R,(width A),n))) + ((A * (0. (R,(width A),n))) - (A * (0. (R,(width A),n)))) by MATRIX_3:3
.= A * (0. (R,(width A),n)) by MATRIX_4:20 ;
hence A * (0. (R,(width A),n)) = 0. (R,(len A),n) ; :: thesis: verum

end;

end;

end;

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

then A10: ( len (0. (R,(width A),n)) = 0 & width (0. (R,(width A),n)) = 0 ) by MATRIX_0:22;
set LHS = A * (0. (R,(width A),n));
set RHS = 0. (R,(len A),n);
A11: ( len (A * (0. (R,(width A),n))) = len A & width (A * (0. (R,(width A),n))) = width (0. (R,(width A),n)) ) by A8, A10, MATRIX_3:def 4;
then Seg (width (A * (0. (R,(width A),n)))) = {} by A10;
then {} = [:(dom (A * (0. (R,(width A),n)))),(Seg (width (A * (0. (R,(width A),n))))):] by ZFMISC_1:90
.= Indices (A * (0. (R,(width A),n))) by MATRIX_0:def 4 ;
then A12: for i, j being Nat st [i,j] in Indices (A * (0. (R,(width A),n))) holds
(A * (0. (R,(width A),n))) * (i,j) = (0. (R,(len A),n)) * (i,j) ;
len (0. (R,(width A),n)) = width A by A8;
then A15: ( len (A * (0. (R,(width A),n))) = len A & width (A * (0. (R,(width A),n))) = width (0. (R,(width A),n)) ) by MATRIX_3:def 4;

per cases ( len A = 0 or len A > 0 ) ;

suppose len A = 0 ; :: thesis: A * (0. (R,(width A),n)) = 0. (R,(len A),n)

then ( len (A * (0. (R,(width A),n))) = len (0. (R,(len A),n)) & width (A * (0. (R,(width A),n))) = width (0. (R,(len A),n)) ) by A10, A11, MATRIX_0:22;
hence A * (0. (R,(width A),n)) = 0. (R,(len A),n) by A12, MATRIX_0:21; :: thesis: verum

end;

suppose len A > 0 ; :: thesis: A * (0. (R,(width A),n)) = 0. (R,(len A),n)

then ( len (A * (0. (R,(width A),n))) = len (0. (R,(len A),n)) & width (A * (0. (R,(width A),n))) = width (0. (R,(len A),n)) ) by A1, A15, MATRIX_0:23;
hence A * (0. (R,(width A),n)) = 0. (R,(len A),n) by A12, MATRIX_0:21; :: thesis: verum

end;

end;

end;

end;