let n be Nat; :: thesis: for K being Ring
for A being Matrix of K st n > 0 holds
(0. (K,n,(len A))) * A = 0. (K,n,(width A))
let K be Ring; :: thesis: for A being Matrix of K st n > 0 holds
(0. (K,n,(len A))) * A = 0. (K,n,(width A))
let A be Matrix of K; :: thesis: ( n > 0 implies (0. (K,n,(len A))) * A = 0. (K,n,(width A)) )
assume A1: n > 0 ; :: thesis: (0. (K,n,(len A))) * A = 0. (K,n,(width A))
A3: len (0. (K,n,(len A))) = n by MATRIX_0:def 2;
then A4: width (0. (K,n,(len A))) = len A by A1, MATRIX_0: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 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