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

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

assume the addF of S . ((f . x),y) in rng f ; :: thesis: contradiction
then consider c being object such that
A4: ( c in dom f & f . c = the addF of S . ((f . x),y) ) by FUNCT_1:def 3;
reconsider z = c as Element of [#] R by A4;
(f . z) - fx = (fx + y) + (- fx) by A4
.= y + (fx + (- fx)) by RLVECT_1:def 3
.= y + (0. S) by RLVECT_1:5 ;
then A5: y = f . (z - x) 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 . ((f . a),b) in ([#] S) \ (rng f) by XBOOLE_0:def 5; :: thesis: verum