let R be Ring; :: thesis: for E being R -homomorphic Ring
for K being Subring of R holds E is K -homomorphic
let E be R -homomorphic Ring; :: thesis: for K being Subring of R holds E is K -homomorphic
let K be Subring of R; :: thesis: E is K -homomorphic
consider f being Function of R,E such that
A1: f is RingHomomorphism by RING_2:def 4;
the carrier of K c= the carrier of R by C0SP1:def 3;
then reconsider g = f | the carrier of K as Function of K,E by FUNCT_2:32;
take g ; :: according to RING_2:def 4 :: thesis: g is RingHomomorphism
thus g is RingHomomorphism by A1, Th48, Th49, Th50; :: thesis: verum