let K be Field; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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 ;

now :: thesis: not the multF of T . (x,(f . y)) in rng f

assume the multF of T . (x,(f . y)) in rng f ; :: thesis: contradiction
then consider c being object such that
A4: ( c in dom f & f . c = the multF of T . (x,(f . y)) ) by FUNCT_1:def 3;
reconsider z = c as Element of [#] K by A4;
(f . z) * fy1 = (x * fy) * fy1 by A4
.= x * (fy * fy1) by GROUP_1:def 3
.= x * (f . (y * (y "))) by GROUP_6:def 6
.= x * (f . ((y ") * y)) by GROUP_1:def 12
.= x * (f . (1_ K)) by A1, VECTSP_1:def 10
.= x * (1_ T) by GROUP_1:def 13
.= x ;
then A5: x = f . (z * (y ")) by GROUP_6:def 6;
dom f = [#] K by FUNCT_2:def 1;
hence contradiction by A3, A5, FUNCT_1:def 3; :: thesis: verum

end;

hence the multF of T . (a,(f . b)) in ([#] T) \ (rng f) by XBOOLE_0:def 5; :: thesis: verum