theorem :: COMPLFLD:25

for z being Element of F_Complex st z <> 0. F_Complex holds
(0. F_Complex) / z = 0. F_Complex ;