theorem :: COMPLFLD:50

for z being Element of F_Complex holds (z *') *' = z ;