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_0:def 3;
A4: len (0. (K,(width A),(width A))) = width A by MATRIX_0:def 2;
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_0: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:4
.= (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:3
.= 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