let F be Field; :: thesis: for E being F -homomorphic Field
for K being Subfield of F holds E is K -homomorphic
let E be F -homomorphic Field; :: thesis: for K being Subfield of F holds E is K -homomorphic
let K be Subfield of F; :: thesis: E is K -homomorphic
consider f being Function of F,E such that
A1: f is RingHomomorphism by RING_2:def 4;
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;
take g ; :: according to RING_2:def 4 :: thesis: g is RingHomomorphism
thus g is RingHomomorphism by A1, Th53, Th54, Th55; :: thesis: verum