theorem :: REALSET2:8

for F being Field
for x, y being Element of F st x + y = 0. F holds
y = (comp F) . x