let F be Field; for E being F -homomorphic Field
for K being Subfield of F
for EK being b2 -homomorphic Field
for f being Homomorphism of F,E st E = EK holds
f | K is Homomorphism of K,EK
let E be F -homomorphic Field; for K being Subfield of F
for EK being b1 -homomorphic Field
for f being Homomorphism of F,E st E = EK holds
f | K is Homomorphism of K,EK
let K be Subfield of F; for EK being K -homomorphic Field
for f being Homomorphism of F,E st E = EK holds
f | K is Homomorphism of K,EK
let EK be K -homomorphic Field; for f being Homomorphism of F,E st E = EK holds
f | K is Homomorphism of K,EK
let f be Homomorphism of F,E; ( E = EK implies f | K is Homomorphism of K,EK )
the carrier of K c= the carrier of F
by EC_PF_1:def 1;
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 Th53, Th54, Th55; verum