let F be Field; :: thesis: for E being FieldExtension of F holds id F is Monomorphism of F,E
let E be FieldExtension of F; :: thesis: id F is Monomorphism of F,E
I: F is Subfield of E by FIELD_4:7;
then H: the carrier of F c= the carrier of E by EC_PF_1:def 1;
rng (id F) c= the carrier of E by I, EC_PF_1:def 1;
then reconsider f = id F as Function of F,E by FUNCT_2:6;
( f is additive & f is multiplicative & f is unity-preserving & f is monomorphism )

proof

now :: thesis: for a, b being Element of F holds f . (a + b) = (f . a) + (f . b)

let a, b be Element of F; :: thesis: f . (a + b) = (f . a) + (f . b)
reconsider a1 = a, b1 = b as Element of E by H;
K: [a,b] in [: the carrier of F, the carrier of F:] by ZFMISC_1:def 2;
thus f . (a + b) = ( the addF of E || the carrier of F) . (a,b) by I, EC_PF_1:def 1
.= (f . a) + (f . b) by K, FUNCT_1:49 ; :: thesis: verum

end;

hence K1: f is additive ; :: thesis: ( f is multiplicative & f is unity-preserving & f is monomorphism )

now :: thesis: for a, b being Element of F holds f . (a * b) = (f . a) * (f . b)

let a, b be Element of F; :: thesis: f . (a * b) = (f . a) * (f . b)
reconsider a1 = a, b1 = b as Element of E by H;
K: [a,b] in [: the carrier of F, the carrier of F:] by ZFMISC_1:def 2;
thus f . (a * b) = ( the multF of E || the carrier of F) . (a,b) by I, EC_PF_1:def 1
.= (f . a) * (f . b) by K, FUNCT_1:49 ; :: thesis: verum

end;

hence K2: f is multiplicative ; :: thesis: ( f is unity-preserving & f is monomorphism )
thus f is unity-preserving by I, EC_PF_1:def 1; :: thesis: f is monomorphism
hence f is monomorphism by K1, K2; :: thesis: verum

end;

hence id F is Monomorphism of F,E ; :: thesis: verum