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

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