let F be Field; :: thesis: for E being F -homomorphic Field
for K being Subfield of F
for EK being b₂ -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; :: thesis: for K being Subfield of F
for EK being b₁ -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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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; :: thesis: verum