let R be Ring; :: thesis: for S being R -monomorphic Ring
for f being Monomorphism of R,S
for a, b being Element of carr f st not a in [#] R & b in [#] R holds
the addF of S . (a,(f . b)) in ([#] S) \ (rng f)
let S be R -monomorphic Ring; :: thesis: for f being Monomorphism of R,S
for a, b being Element of carr f st not a in [#] R & b in [#] R holds
the addF of S . (a,(f . b)) in ([#] S) \ (rng f)
let f be Monomorphism of R,S; :: thesis: for a, b being Element of carr f st not a in [#] R & b in [#] R holds
the addF of S . (a,(f . b)) in ([#] S) \ (rng f)
let a, b be Element of carr f; :: thesis: ( not a in [#] R & b in [#] R implies the addF of S . (a,(f . b)) in ([#] S) \ (rng f) )
assume A1: ( not a in [#] R & b in [#] R ) ; :: thesis: the addF of S . (a,(f . b)) in ([#] S) \ (rng f)
then reconsider y = b as Element of [#] R ;
A2: a in ([#] S) \ (rng f) by A1, XBOOLE_0:def 3;
then A3: ( a in [#] S & not a in rng f ) by XBOOLE_0:def 5;
reconsider x = a as Element of [#] S by A2;
reconsider fy = f . y as Element of [#] S ;

now :: thesis: not the addF of S . (x,(f . y)) in rng f

assume the addF of S . (x,(f . y)) in rng f ; :: thesis: contradiction
then consider c being object such that
A4: ( c in dom f & f . c = the addF of S . (x,(f . y)) ) by FUNCT_1:def 3;
reconsider z = c as Element of [#] R by A4;
(f . z) - fy = (x + fy) + (- fy) by A4
.= x + (fy + (- fy)) by RLVECT_1:def 3
.= x + (0. S) by RLVECT_1:5 ;
then A5: x = f . (z - y) by RING_2:8;
dom f = [#] R by FUNCT_2:def 1;
hence contradiction by A3, A5, FUNCT_1:def 3; :: thesis: verum

end;

hence the addF of S . (a,(f . b)) in ([#] S) \ (rng f) by XBOOLE_0:def 5; :: thesis: verum