theorem Th15: :: FIELD_3:18

for F being non almost_trivial Field
for x being non trivial Element of F
for u being object st not u in [#] F holds
( isoR (x,u) is additive & isoR (x,u) is multiplicative & isoR (x,u) is unity-preserving )