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