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) )
assume A1: ( width M1 = len M2 & len M1 > 0 & len M2 > 0 ) ; :: thesis: (0_Cx (len M1),(width M1)) * M2 = 0_Cx (len M1),(width M2)
( len M1 = len (COMPLEX2Field M1) & width M1 = width (COMPLEX2Field M1) ) ;
hence (0_Cx (len M1),(width M1)) * M2 = 0_Cx (len M1),(width M2) by A1, Th38; :: thesis: verum