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, Th38; :: thesis: verum