let R, S be Ring; :: thesis:

A1: now :: thesis:

assume S is R -monomorphic ; :: thesis:
then reconsider T = S as R -monomorphic Ring ;
set f = the Monomorphism of R,T;
ker the Monomorphism of R,T = {(0. R)} by RING_2:12;
then A2: R / (ker the Monomorphism of R,T),R are_isomorphic by RING_2:17;
R / (ker the Monomorphism of R,T), Image the Monomorphism of R,T are_isomorphic by RING_2:15;
hence S includes R by Th43, A2; :: thesis:

end;

now :: thesis:

assume S includes R ; :: thesis:
then consider T being Subring of S such that
A3: T,R are_isomorphic ;
consider f being Function of R,T such that
A4: f is isomorphism by A3, QUOFIELD:def 23;
A5: ( f is additive & f is multiplicative & f is unity-preserving & f is one-to-one ) by A4;
the carrier of T c= the carrier of S by C0SP1:def 3;
then reconsider g = f as Function of R,S by FUNCT_2:7;

now :: thesis:

let x, y be Element of R; :: thesis:
A6: [(f . x),(f . y)] in [: the carrier of T, the carrier of T:] ;
thus g . (x + y) = (f . x) + (f . y) by A5
.= ( the addF of S || the carrier of T) . ((f . x),(f . y)) by C0SP1:def 3
.= (g . x) + (g . y) by A6, FUNCT_1:49 ; :: thesis:

end;

then A7: g is additive ;

now :: thesis:

let x, y be Element of R; :: thesis:
A8: [(f . x),(f . y)] in [: the carrier of T, the carrier of T:] ;
thus g . (x * y) = (f . x) * (f . y) by A5
.= ( the multF of S || the carrier of T) . ((f . x),(f . y)) by C0SP1:def 3
.= (g . x) * (g . y) by A8, FUNCT_1:49 ; :: thesis:

end;

then A9: g is multiplicative ;
g is unity-preserving by A5, C0SP1:def 3;
hence S is R -monomorphic by A7, A9, A4; :: thesis:

end;

hence ( S is R -monomorphic Ring iff S includes R ) by A1; :: thesis: