theorem :: MATRIX_5:23

for M1, M2 being Matrix of COMPLEX st width M1 = len M2 & len M1 > 0 & len M2 > 0 holds
(0_Cx ((len M1),(width M1))) * M2 = 0_Cx ((len M1),(width M2))