:: deftheorem defines 0_Cx MATRIX_5:def 8 :
for n, m being Nat holds 0_Cx (n,m) = Field2COMPLEX (0. (F_Complex,n,m));