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