let M1, M2 be Matrix of COMPLEX; :: thesis: ( width M1 = len M2 & len M1 > 0 & len M2 > 0 implies (0_Cx ((len M1),(width M1))) * M2 = 0_Cx ((len M1),(width M2)) )
A1: len M1 = len (COMPLEX2Field M1) ;
assume ( width M1 = len M2 & len M1 > 0 & len M2 > 0 ) ; :: thesis: (0_Cx ((len M1),(width M1))) * M2 = 0_Cx ((len M1),(width M2))
hence (0_Cx ((len M1),(width M1))) * M2 = 0_Cx ((len M1),(width M2)) by A1, Th22; :: thesis: verum