theorem Th5: :: COMPLFLD:5

for x1 being Element of F_Complex
for x2 being Complex st x1 = x2 & x1 <> 0. F_Complex holds
x1 " = x2 "