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