reconsider ea = 0 as Element of F_Complex by COMPLFLD:def 1;
let M1 be Matrix of COMPLEX; :: thesis: ( len M1 > 0 implies 0 * M1 = 0_Cx ((len M1),(width M1)) )
assume A1: len M1 > 0 ; :: thesis: 0 * M1 = 0_Cx ((len M1),(width M1))
0 * M1 = Field2COMPLEX (ea * (COMPLEX2Field M1)) by Def7
.= 0_Cx ((len M1),(width M1)) by A1, Th24, COMPLFLD:7 ;
hence 0 * M1 = 0_Cx ((len M1),(width M1)) ; :: thesis: verum