let R be Ring; :: thesis: for S being Subring of R holds R is S -monomorphic
let S be Subring of R; :: thesis: R is S -monomorphic
the carrier of S c= the carrier of R by C0SP1:def 3;
then reconsider f = id S as Function of S,R by FUNCT_2:7;

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

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

end;

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

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

end;

f . (1_ S) = 1_ R by C0SP1:def 3;
then f is RingHomomorphism by A1, A3, VECTSP_1:def 20, GROUP_1:def 13, GROUP_6:def 6;
hence R is S -monomorphic ; :: thesis: verum