let K be Field; :: 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_1:def 3;
then A4: width (0. K,(len A),(len A)) = len A by A1, MATRIX_1: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:6
.= ((0. K,(len A),(len A)) * A) + ((0. K,(len A),(len A)) * A) by A1, 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:5
.= (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_1:def 3;
then width (0. K,(len A),(len A)) = len A by A7, MATRIX_1:def 4;
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_1:def 3;
hence (0. K,(len A),(len A)) * A = 0. K,(len A),(width A) by A7, A8, CARD_2:83; :: thesis: verum

end;

end;