let K be Field; for T being K -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of carr f st not a in [#] K & b in [#] K & b <> 0. K holds
the multF of T . (a,(f . b)) in ([#] T) \ (rng f)
let T be K -monomorphic comRing; for f being Monomorphism of K,T
for a, b being Element of carr f st not a in [#] K & b in [#] K & b <> 0. K holds
the multF of T . (a,(f . b)) in ([#] T) \ (rng f)
let f be Monomorphism of K,T; for a, b being Element of carr f st not a in [#] K & b in [#] K & b <> 0. K holds
the multF of T . (a,(f . b)) in ([#] T) \ (rng f)
let a, b be Element of carr f; ( not a in [#] K & b in [#] K & b <> 0. K implies the multF of T . (a,(f . b)) in ([#] T) \ (rng f) )
assume A1:
( not a in [#] K & b in [#] K & b <> 0. K )
; the multF of T . (a,(f . b)) in ([#] T) \ (rng f)
then reconsider y = b as Element of [#] K ;
reconsider fy1 = f . (y ") as Element of T ;
A2:
a in ([#] T) \ (rng f)
by A1, XBOOLE_0:def 3;
then A3:
( a in [#] T & not a in rng f )
by XBOOLE_0:def 5;
reconsider x = a as Element of [#] T by A2;
reconsider fy = f . y as Element of [#] T ;
hence
the multF of T . (a,(f . b)) in ([#] T) \ (rng f)
by XBOOLE_0:def 5; verum