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 b in [#] K & a in [#] K & a <> 0. K holds
the multF of T . ((f . a),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 b in [#] K & a in [#] K & a <> 0. K holds
the multF of T . ((f . a),b) in ([#] T) \ (rng f)
let f be Monomorphism of K,T; :: thesis: for a, b being Element of carr f st not b in [#] K & a in [#] K & a <> 0. K holds
the multF of T . ((f . a),b) in ([#] T) \ (rng f)
let a, b be Element of carr f; :: thesis: ( not b in [#] K & a in [#] K & a <> 0. K implies the multF of T . ((f . a),b) in ([#] T) \ (rng f) )
assume A1: ( not b in [#] K & a in [#] K & a <> 0. K ) ; :: thesis: the multF of T . ((f . a),b) in ([#] T) \ (rng f)
then reconsider x = a as Element of [#] K ;
reconsider fx1 = f . (x ") as Element of T ;
A2: b in ([#] T) \ (rng f) by A1, XBOOLE_0:def 3;
then A3: ( b in [#] T & not b in rng f ) by XBOOLE_0:def 5;
reconsider y = b as Element of [#] T by A2;
reconsider fx = f . x as Element of [#] T ;

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

assume the multF of T . ((f . x),y) in rng f ; :: thesis: contradiction
then consider c being object such that
A4: ( c in dom f & f . c = the multF of T . ((f . x),y) ) by FUNCT_1:def 3;
reconsider z = c as Element of [#] K by A4;
(f . z) * fx1 = ((f . x) * y) * fx1 by A4
.= (y * (f . x)) * fx1 by GROUP_1:def 12
.= y * (fx * fx1) by GROUP_1:def 3
.= y * (f . (x * (x "))) by GROUP_6:def 6
.= y * (f . ((x ") * x)) by GROUP_1:def 12
.= y * (f . (1_ K)) by A1, VECTSP_1:def 10
.= y * (1_ T) by GROUP_1:def 13
.= y ;
then A5: y = f . (z * (x ")) 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 . ((f . a),b) in ([#] T) \ (rng f) by XBOOLE_0:def 5; :: thesis: verum