let T be RingExtension of R; :: thesis: ( T is R -homomorphic & T is R -monomorphic )
set S = R;
H: R is Subring of T by FIELD_4:def 1;
then rng (id R) c= the carrier of T by C0SP1:def 3;
then reconsider h = id R as Function of the carrier of R, the carrier of T by FUNCT_2:6;
A: ( h is additive & h is multiplicative & h is unity-preserving )

proof

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

let a, b be Element of R; :: thesis: h . (a + b) = (h . a) + (h . b)
I: [a,b] in [: the carrier of R, the carrier of R:] ;
thus h . (a + b) = ( the addF of T || the carrier of R) . (a,b) by H, C0SP1:def 3
.= (h . a) + (h . b) by I, FUNCT_1:49 ; :: thesis: verum

end;

hence h is additive ; :: thesis: ( h is multiplicative & h is unity-preserving )

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

let a, b be Element of R; :: thesis: h . (a * b) = (h . a) * (h . b)
I: [a,b] in [: the carrier of R, the carrier of R:] ;
thus h . (a * b) = ( the multF of T || the carrier of R) . (a,b) by H, C0SP1:def 3
.= (h . a) * (h . b) by I, FUNCT_1:49 ; :: thesis: verum

end;

hence h is multiplicative ; :: thesis: h is unity-preserving
thus h is unity-preserving by H, C0SP1:def 3; :: thesis: verum

end;

hence T is R -homomorphic ; :: thesis: T is R -monomorphic
thus T is R -monomorphic by A, RING_3:def 3; :: thesis: verum