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

per cases ( m > 0 or m = 0 ) ;

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

set B = (0. (R,m,(len A))) * A;
A4: len (0. (R,m,(len A))) = m by MATRIX_0:def 2;
then A5: width (0. (R,m,(len A))) = len A by A2, MATRIX_0:20;
then A6: len ((0. (R,m,(len A))) * A) = m by A4, MATRIX_3:def 4;
A7: width ((0. (R,m,(len A))) * A) = width A by A5, MATRIX_3:def 4;
(0. (R,m,(len A))) * A = ((0. (R,m,(len A))) + (0. (R,m,(len A)))) * A by MATRIX_3:4
.= ((0. (R,m,(len A))) * A) + ((0. (R,m,(len A))) * A) by A5, MATRIX_4:63 ;
then ( len (- ((0. (R,m,(len A))) * A)) = len ((0. (R,m,(len A))) * A) & 0. (R,m,(width A)) = (((0. (R,m,(len A))) * A) + ((0. (R,m,(len A))) * A)) + (- ((0. (R,m,(len A))) * A)) ) by A6, A7, MATRIX_1:def 4, MATRIX_4:2;
then 0. (R,m,(width A)) = ((0. (R,m,(len A))) * A) + (((0. (R,m,(len A))) * A) - ((0. (R,m,(len A))) * A)) by MATRIX_3:3
.= (0. (R,m,(len A))) * A by MATRIX_4:20 ;
hence (0. (R,m,(len A))) * A = 0. (R,m,(width A)) ; :: thesis: verum

end;

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

set LHS = (0. (R,m,(len A))) * A;
set RHS = 0. (R,m,(width A));
A9: len ((0. (R,m,(len A))) * A) = len (0. (R,m,(len A))) by A1, MATRIX_3:def 4
.= 0 by A8 ;
then {} = Seg (len ((0. (R,m,(len A))) * A))
.= dom ((0. (R,m,(len A))) * A) by FINSEQ_1:def 3 ;
then {} = [:(dom ((0. (R,m,(len A))) * A)),(Seg (width ((0. (R,m,(len A))) * A))):] by ZFMISC_1:90
.= Indices ((0. (R,m,(len A))) * A) by MATRIX_0:def 4 ;
then A10: for i, j being Nat st [i,j] in Indices ((0. (R,m,(len A))) * A) holds
((0. (R,m,(len A))) * A) * (i,j) = (0. (R,m,(width A))) * (i,j) ;
( width ((0. (R,m,(len A))) * A) = 0 & len ((0. (R,m,(len A))) * A) = 0 & len (0. (R,m,(width A))) = 0 & width (0. (R,m,(width A))) = 0 ) by A8, A9, MATRIX_0:22, MATRIX_0:def 3;
hence (0. (R,m,(len A))) * A = 0. (R,m,(width A)) by A10, MATRIX_0:21; :: thesis: verum

end;

end;