theorem :: REALSET2:9

for F being Field
for x being Element of F holds x = (comp F) . ((comp F) . x)