let A, B be non degenerated commutative Ring; :: thesis: for M0 being Ideal of B
for x, y being Element of the carrier of A
for h being Function of A,B st h is RingHomomorphism & x in h " M0 & y in h " M0 holds
x + y in h " M0
let M0 be Ideal of B; :: thesis: for x, y being Element of the carrier of A
for h being Function of A,B st h is RingHomomorphism & x in h " M0 & y in h " M0 holds
x + y in h " M0
let x, y be Element of the carrier of A; :: thesis: for h being Function of A,B st h is RingHomomorphism & x in h " M0 & y in h " M0 holds
x + y in h " M0
let h be Function of A,B; :: thesis: ( h is RingHomomorphism & x in h " M0 & y in h " M0 implies x + y in h " M0 )
assume that
A1: h is RingHomomorphism and
A2: x in h " M0 and
A3: y in h " M0 ; :: thesis: x + y in h " M0
A4: h . x in M0 by A2, FUNCT_1:def 7;
A5: h . y in M0 by A3, FUNCT_1:def 7;
reconsider a = x, b = y as Element of A ;
A6: h is additive by A1;
(h . x) + (h . y) in M0 by A4, A5, IDEAL_1:def 1;
then A8: h . (x + y) in M0 by A6;
x + y in A ;
then x + y in dom h by FUNCT_2:def 1;
hence x + y in h " M0 by A8, FUNCT_1:def 7; :: thesis: verum