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 that
A1: width A > 0 and
A2: len A > 0 ; :: thesis: A * (0. K,(width A),m) = 0. K,(len A),m
A3: len (0. K,(width A),m) = width A by MATRIX_1:def 3;
then m = width (0. K,(width A),m) by A1, MATRIX_1:20;
then A4: width (A * (0. K,(width A),m)) = m by A3, MATRIX_3:def 4;
width (0. K,(width A),m) = m by A1, A3, MATRIX_1:20;
then A5: (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 ;
len (A * (0. K,(width A),m)) = len A by A3, MATRIX_3:def 4;
hence A * (0. K,(width A),m) = 0. K,(len A),m by A4, A5, MATRIX_4:6; :: thesis: verum