let E, F be Field; :: thesis: for f being additive multiplicative Function of E,F holds
( f . (1. E) = 1. F iff f is monomorphism )
let f be additive multiplicative Function of E,F; :: thesis: ( f . (1. E) = 1. F iff f is monomorphism )
( ( f . (1. E) = 0. F & f = E --> (0. F) ) or ( f . (1. E) = 1. F & f is monomorphism ) ) by hom3;
hence ( f . (1. E) = 1. F iff f is monomorphism ) ; :: thesis: verum