theorem Th5: :: FIELD_2:6
for K being Field
for F being b1 -monomorphic Field
for f being Monomorphism of K,F
for a being Element of K st a <> 0. K holds
f . (a ") = (f . a) "