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) )
A1: width (- (A * (0. K,(width A),(width A)))) = width (A * (0. K,(width A),(width A))) by MATRIX_3:def 2;
set B = A * (0. K,(width A),(width A));
assume A2: width A > 0 ; :: thesis: A * (0. K,(width A),(width A)) = 0. K,(len A),(width A)
then A3: len A > 0 by MATRIX_1:def 4;
A4: len (0. K,(width A),(width A)) = width A by MATRIX_1:def 3;
then A5: len (A * (0. K,(width A),(width A))) = len A by MATRIX_3:def 4;
A6: width (0. K,(width A),(width A)) = width A by A2, A4, MATRIX_1:20;
then A7: width (A * (0. K,(width A),(width A))) = width A by A4, MATRIX_3:def 4;
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 A2, A3, A4, A6, MATRIX_4:62 ;
then ( len (- (A * (0. K,(width A),(width A)))) = len (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, A7, MATRIX_3:def 2, 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 A1, MATRIX_3:5
.= A * (0. K,(width A),(width A)) by A5, A1, MATRIX_4:20 ;
hence A * (0. K,(width A),(width A)) = 0. K,(len A),(width A) ; :: thesis: verum