let R be Ring; :: thesis: for S being R -monomorphic Ring
for f being Monomorphism of R,S
for a being Element of carr f st not a in [#] R holds
( a in [#] S & not a in rng f )
let S be R -monomorphic Ring; :: thesis: for f being Monomorphism of R,S
for a being Element of carr f st not a in [#] R holds
( a in [#] S & not a in rng f )
let f be Monomorphism of R,S; :: thesis: for a being Element of carr f st not a in [#] R holds
( a in [#] S & not a in rng f )
let a be Element of carr f; :: thesis: ( not a in [#] R implies ( a in [#] S & not a in rng f ) )
assume not a in [#] R ; :: thesis: ( a in [#] S & not a in rng f )
then a in ([#] S) \ (rng f) by XBOOLE_0:def 3;
hence ( a in [#] S & not a in rng f ) by XBOOLE_0:def 5; :: thesis: verum