theorem :: MATRIX_5:15

for n, m being Nat holds COMPLEX2Field (0_Cx (n,m)) = 0. (F_Complex,n,m) ;