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 3;
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:6 ;
hence (0. K,n,(len A)) * A = 0. K,n,(width A) by A5, A6, MATRIX_4:6; :: thesis: verum