let K be Ring; :: thesis: for A being Matrix of K holds (0. (K,(len A),(len A))) * A = 0. (K,(len A),(width A))
let A be Matrix of K; :: thesis: (0. (K,(len A),(len A))) * A = 0. (K,(len A),(width A))

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

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

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

end;

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

then len (0. (K,(len A),(len A))) = 0 by MATRIX_0:def 2;
then width (0. (K,(len A),(len A))) = len A by A7, MATRIX_0:def 3;
then A8: len ((0. (K,(len A),(len A))) * A) = len (0. (K,(len A),(len A))) by MATRIX_3:def 4;
( len (0. (K,(len A),(len A))) = len A & len (0. (K,(len A),(width A))) = len A ) by MATRIX_0:def 2;
hence (0. (K,(len A),(len A))) * A = 0. (K,(len A),(width A)) by A7, A8, CARD_2:64; :: thesis: verum

end;

end;