let R be Ring; :: thesis: for E being R -homomorphic Ring
for K being Subring of R
for EK being b₂ -homomorphic Ring
for f being Homomorphism of R,E st E = EK holds
f | K is Homomorphism of K,EK
let E be R -homomorphic Ring; :: thesis: for K being Subring of R
for EK being b₁ -homomorphic Ring
for f being Homomorphism of R,E st E = EK holds
f | K is Homomorphism of K,EK
let K be Subring of R; :: thesis: for EK being K -homomorphic Ring
for f being Homomorphism of R,E st E = EK holds
f | K is Homomorphism of K,EK
let EK be K -homomorphic Ring; :: thesis: for f being Homomorphism of R,E st E = EK holds
f | K is Homomorphism of K,EK
let f be Homomorphism of R,E; :: thesis: ( E = EK implies f | K is Homomorphism of K,EK )
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;
g = f | K ;
hence ( E = EK implies f | K is Homomorphism of K,EK ) by Th48, Th49, Th50; :: thesis: verum