let K be Field; :: thesis: for m being Element of NAT
for A, C being Matrix of K st width A > 0 & len A > 0 holds
A * (0. K,(width A),m) = 0. K,(len A),m
let m be Element of NAT ; :: thesis: for A, C being Matrix of K st width A > 0 & len A > 0 holds
A * (0. K,(width A),m) = 0. K,(len A),m
let A, C be Matrix of K; :: thesis: ( width A > 0 & len A > 0 implies A * (0. K,(width A),m) = 0. K,(len A),m )
assume A1: ( width A > 0 & len A > 0 ) ; :: thesis: A * (0. K,(width A),m) = 0. K,(len A),m
A2: len (0. K,(width A),m) = width A by MATRIX_1:def 3;
then A3: width (0. K,(width A),m) = m by A1, MATRIX_1:20;
A4: ( m = width (0. K,(width A),m) & len (0. K,(width A),m) > 0 & width A > 0 & len A > 0 ) by A1, A2, MATRIX_1:20;
A5: len (A * (0. K,(width A),m)) = len A by A2, MATRIX_3:def 4;
A6: width (A * (0. K,(width A),m)) = m by A2, A4, MATRIX_3:def 4;
(A * (0. K,(width A),m)) + (A * (0. K,(width A),m)) = A * ((0. K,(width A),m) + (0. K,(width A),m)) by A1, A2, A3, MATRIX_4:62
.= A * (0. K,(width A),m) by MATRIX_3:6 ;
hence A * (0. K,(width A),m) = 0. K,(len A),m by A5, A6, MATRIX_4:6; :: thesis: verum