let A, B be non degenerated commutative Ring; :: thesis: for h being Function of A,B
for M0 being Ideal of B st h is RingHomomorphism holds
h " M0 is Ideal of A
let h be Function of A,B; :: thesis: for M0 being Ideal of B st h is RingHomomorphism holds
h " M0 is Ideal of A
let M0 be Ideal of B; :: thesis: ( h is RingHomomorphism implies h " M0 is Ideal of A )
assume A1: h is RingHomomorphism ; :: thesis: h " M0 is Ideal of A
then A2: h " M0 is add-closed by Lm48;
A3: h " M0 is left-ideal by A1, Lm49;
A6: dom h = the carrier of A by FUNCT_2:def 1;
h . (0. A) = 0. B by A1, RING_2:6;
then h . (0. A) in M0 by IDEAL_1:2;
then 0. A in h " M0 by A6, FUNCT_1:def 7;
hence h " M0 is Ideal of A by A2, A3; :: thesis: verum