let K be Field; :: thesis: for A being Matrix of K st width A > 0 holds
A * (0. K,(width A),(width A)) = 0. K,(len A),(width A)
let A be Matrix of K; :: thesis: ( width A > 0 implies A * (0. K,(width A),(width A)) = 0. K,(len A),(width A) )
assume A1: width A > 0 ; :: thesis: A * (0. K,(width A),(width A)) = 0. K,(len A),(width A)
then A2: len A > 0 by MATRIX_1:def 4;
A3: ( len (0. K,(width A),(width A)) = width A & len (0. K,(len A),(width A)) = len A ) by MATRIX_1:def 3;
then A4: ( width (0. K,(width A),(width A)) = width A & width (0. K,(len A),(width A)) = width A ) by A1, A2, MATRIX_1:20;
A5: ( len (A * (0. K,(width A),(width A))) = len A & len (A * (0. K,(width A),(width A))) = len (0. K,(len A),(width A)) ) by A3, MATRIX_3:def 4;
A6: ( width (A * (0. K,(width A),(width A))) = width (0. K,(width A),(width A)) & width (A * (0. K,(width A),(width A))) = width A ) by A3, A4, MATRIX_3:def 4;
A7: len (- (A * (0. K,(width A),(width A)))) = len (A * (0. K,(width A),(width A))) by MATRIX_3:def 2;
A8: width (- (A * (0. K,(width A),(width A)))) = width (A * (0. K,(width A),(width A))) by MATRIX_3:def 2;
A9: A * (0. K,(width A),(width A)) = A * ((0. K,(width A),(width A)) + (0. K,(width A),(width A))) by MATRIX_3:6
.= (A * (0. K,(width A),(width A))) + (A * (0. K,(width A),(width A))) by A1, A2, A3, A4, MATRIX_4:62 ;
set B = 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 A5, A6, A9, 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 A7, A8, MATRIX_3:5
.= A * (0. K,(width A),(width A)) by A5, A8, MATRIX_4:20 ;
hence A * (0. K,(width A),(width A)) = 0. K,(len A),(width A) ; :: thesis: verum