let E be FieldExtension of F; :: thesis: ( E is F -monomorphic & E is F -homomorphic )
H: F is Subring of E by FIELD_4:def 1;
then rng (id F) c= the carrier of E by C0SP1:def 3;
then reconsider f = id F as Function of F,E by FUNCT_2:6;

B: now :: thesis: for x, y being Element of F holds f . (x + y) = (f . x) + (f . y)

let x, y be Element of F; :: thesis: f . (x + y) = (f . x) + (f . y)
reconsider a = f . x, b = f . y as Element of E ;
B1: [a,b] in [: the carrier of F, the carrier of F:] by ZFMISC_1:def 2;
thus f . (x + y) = ( the addF of E || the carrier of F) . (a,b) by H, C0SP1:def 3
.= (f . x) + (f . y) by B1, FUNCT_1:49 ; :: thesis: verum

end;

C: now :: thesis: for x, y being Element of F holds f . (x * y) = (f . x) * (f . y)

let x, y be Element of F; :: thesis: f . (x * y) = (f . x) * (f . y)
reconsider a = f . x, b = f . y as Element of E ;
B1: [a,b] in [: the carrier of F, the carrier of F:] by ZFMISC_1:def 2;
thus f . (x * y) = ( the multF of E || the carrier of F) . (a,b) by H, C0SP1:def 3
.= (f . x) * (f . y) by B1, FUNCT_1:49 ; :: thesis: verum

end;

( f is additive & f is multiplicative & f is unity-preserving ) by B, C, H, C0SP1:def 3;
hence ( E is F -monomorphic & E is F -homomorphic ) by RING_3:def 3; :: thesis: verum