theorem :: COMPLFLD:24

for z being Element of F_Complex st z <> 0. F_Complex holds
z / z = 1. F_Complex