thus ( a in [#] K & b in [#] K implies the multF of K . (a,b) is Element of carr f ) :: thesis: ( ( ( a = 0. K or b = 0. K ) implies 0. K is Element of carr f ) & ( a in [#] K & a <> 0. K & not b in [#] K implies the multF of T . ((f . a),b) is Element of carr f ) & ( b in [#] K & b <> 0. K & not a in [#] K implies the multF of T . (a,(f . b)) is Element of carr f ) & ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies (f ") . ( the multF of T . (a,b)) is Element of carr f ) & ( ( a in [#] K & b in [#] K ) or a = 0. K or b = 0. K or ( a in [#] K & a <> 0. K & not b in [#] K ) or ( b in [#] K & b <> 0. K & not a in [#] K ) or ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f ) or the multF of T . (a,b) is Element of carr f ) )
proof
assume ( a in [#] K & b in [#] K ) ; :: thesis: the multF of K . (a,b) is Element of carr f
then reconsider x = a, y = b as Element of [#] K ;
the multF of K . (x,y) in (([#] T) \ (rng f)) \/ ([#] K) by XBOOLE_0:def 3;
hence the multF of K . (a,b) is Element of carr f ; :: thesis: verum
end;
thus ( ( a = 0. K or b = 0. K ) implies 0. K is Element of carr f ) ; :: thesis: ( ( a in [#] K & a <> 0. K & not b in [#] K implies the multF of T . ((f . a),b) is Element of carr f ) & ( b in [#] K & b <> 0. K & not a in [#] K implies the multF of T . (a,(f . b)) is Element of carr f ) & ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies (f ") . ( the multF of T . (a,b)) is Element of carr f ) & ( ( a in [#] K & b in [#] K ) or a = 0. K or b = 0. K or ( a in [#] K & a <> 0. K & not b in [#] K ) or ( b in [#] K & b <> 0. K & not a in [#] K ) or ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f ) or the multF of T . (a,b) is Element of carr f ) )
( a in [#] K & a <> 0. K & not b in [#] K implies the multF of T . ((f . a),b) in ([#] T) \ (rng f) ) by Lm5;
hence ( a in [#] K & a <> 0. K & not b in [#] K implies the multF of T . ((f . a),b) is Element of carr f ) by XBOOLE_0:def 3; :: thesis: ( ( b in [#] K & b <> 0. K & not a in [#] K implies the multF of T . (a,(f . b)) is Element of carr f ) & ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies (f ") . ( the multF of T . (a,b)) is Element of carr f ) & ( ( a in [#] K & b in [#] K ) or a = 0. K or b = 0. K or ( a in [#] K & a <> 0. K & not b in [#] K ) or ( b in [#] K & b <> 0. K & not a in [#] K ) or ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f ) or the multF of T . (a,b) is Element of carr f ) )
( b in [#] K & b <> 0. K & not a in [#] K implies the multF of T . (a,(f . b)) in ([#] T) \ (rng f) ) by Lm4;
hence ( b in [#] K & b <> 0. K & not a in [#] K implies the multF of T . (a,(f . b)) is Element of carr f ) by XBOOLE_0:def 3; :: thesis: ( ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies (f ") . ( the multF of T . (a,b)) is Element of carr f ) & ( ( a in [#] K & b in [#] K ) or a = 0. K or b = 0. K or ( a in [#] K & a <> 0. K & not b in [#] K ) or ( b in [#] K & b <> 0. K & not a in [#] K ) or ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f ) or the multF of T . (a,b) is Element of carr f ) )
thus ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies (f ") . ( the multF of T . (a,b)) is Element of carr f ) :: thesis: ( ( a in [#] K & b in [#] K ) or a = 0. K or b = 0. K or ( a in [#] K & a <> 0. K & not b in [#] K ) or ( b in [#] K & b <> 0. K & not a in [#] K ) or ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f ) or the multF of T . (a,b) is Element of carr f )
proof
assume A1: ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f ) ; :: thesis: (f ") . ( the multF of T . (a,b)) is Element of carr f
A2: rng (f ") = dom f by FUNCT_1:33
.= [#] K by FUNCT_2:def 1 ;
the multF of T . (a,b) in dom (f ") by A1, FUNCT_1:33;
then (f ") . ( the multF of T . (a,b)) in [#] K by A2, FUNCT_1:3;
hence (f ") . ( the multF of T . (a,b)) is Element of carr f by XBOOLE_0:def 3; :: thesis: verum
end;
( not a in [#] K & not b in [#] K & not the multF of T . (a,b) in rng f implies the multF of T . (a,b) is Element of carr f )
proof
assume A3: ( not a in [#] K & not b in [#] K & not the multF of T . (a,b) in rng f ) ; :: thesis: the multF of T . (a,b) is Element of carr f
then ( a in ([#] T) \ (rng f) & b in ([#] T) \ (rng f) ) by XBOOLE_0:def 3;
then reconsider a1 = a, b1 = b as Element of [#] T ;
the multF of T . (a1,b1) in ([#] T) \ (rng f) by A3, XBOOLE_0:def 5;
hence the multF of T . (a,b) is Element of carr f by XBOOLE_0:def 3; :: thesis: verum
end;
hence ( ( a in [#] K & b in [#] K ) or a = 0. K or b = 0. K or ( a in [#] K & a <> 0. K & not b in [#] K ) or ( b in [#] K & b <> 0. K & not a in [#] K ) or ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f ) or the multF of T . (a,b) is Element of carr f ) ; :: thesis: verum