let R be Ring; 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; 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; 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; ( 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 )
; 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 ;
hence
the addF of S . ((f . a),b) in ([#] S) \ (rng f)
by XBOOLE_0:def 5; verum