let R be Ring; :: thesis: for S being R -monomorphic Ring
for f being Monomorphism of R,S holds
( (f ") . (1. S) = 1. R & (f ") . (0. S) = 0. R )
let S be R -monomorphic Ring; :: thesis: for f being Monomorphism of R,S holds
( (f ") . (1. S) = 1. R & (f ") . (0. S) = 0. R )
let f be Monomorphism of R,S; :: thesis: ( (f ") . (1. S) = 1. R & (f ") . (0. S) = 0. R )
A1: [#] R = dom f by FUNCT_2:def 1;
f . (1_ R) = 1_ S by GROUP_1:def 13;
hence (f ") . (1. S) = 1. R by A1, FUNCT_1:34; :: thesis: (f ") . (0. S) = 0. R
f . (0. R) = 0. S by RING_2:6;
then reconsider o = 0. S as Element of rng f by FUNCT_2:4;
( (f ") . (0. S) = (f ") . (o + o) & (f ") . (o + o) = ((f ") . o) + ((f ") . o) ) by Th1;
hence (f ") . (0. S) = 0. R by RLVECT_1:9; :: thesis: verum