let A, B be non degenerated commutative Ring; :: thesis: for M0 being Ideal of B
for r, x being Element of A
for h being Function of A,B st h is RingHomomorphism & x in h " M0 holds
r * x in h " M0
let M0 be Ideal of B; :: thesis: for r, x being Element of A
for h being Function of A,B st h is RingHomomorphism & x in h " M0 holds
r * x in h " M0
let r, x be Element of A; :: thesis: for h being Function of A,B st h is RingHomomorphism & x in h " M0 holds
r * x in h " M0
let h be Function of A,B; :: thesis: ( h is RingHomomorphism & x in h " M0 implies r * x in h " M0 )
assume that
A1: h is RingHomomorphism and
A2: x in h " M0 ; :: thesis: r * x in h " M0
h . x in M0 by A2, FUNCT_1:def 7;
then A5: (h . r) * (h . x) in M0 by IDEAL_1:def 2;
h is multiplicative by A1;
then A6: h . (r * x) in M0 by A5;
r * x in A ;
then r * x in dom h by FUNCT_2:def 1;
hence r * x in h " M0 by A6, FUNCT_1:def 7; :: thesis: verum