let K be Field; :: thesis: for m being 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 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_0:def 2;
then m = width (0. (K,(width A),m)) by A1, MATRIX_0: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_0: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:4 ;
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