let f, g, h be Function; :: thesis: ( dom f c= rng g & dom f misses rng h & g .: (dom h) misses dom f implies f * (g +* h) = f * g )
assume A1: ( dom f c= rng g & dom f misses rng h & g .: (dom h) misses dom f ) ; :: thesis: f * (g +* h) = f * g
A2: dom (f * g) = dom (f * (g +* h))
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: dom (f * (g +* h)) c= dom (f * g)
let x be set ; :: thesis: ( x in dom (f * g) implies x in dom (f * (g +* h)) )
assume x in dom (f * g) ; :: thesis: x in dom (f * (g +* h))
then A3: ( x in dom g & g . x in dom f ) by FUNCT_1:21;
then ( x in dom (g +* h) & g . x = (g +* h) . x ) by A3, FUNCT_4:12, FUNCT_4:13;
hence x in dom (f * (g +* h)) by A3, FUNCT_1:21; :: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (f * (g +* h)) or x in dom (f * g) )
assume x in dom (f * (g +* h)) ; :: thesis: x in dom (f * g)
then A4: ( x in dom (g +* h) & (g +* h) . x in dom f ) by FUNCT_1:21;
then ( ( x in dom g & not x in dom h ) or x in dom h ) by FUNCT_4:13;
then ( ( x in dom g & (g +* h) . x = g . x ) or ( (g +* h) . x = h . x & h . x in rng h ) ) by FUNCT_1:def 5, FUNCT_4:12, FUNCT_4:14;
hence x in dom (f * g) by A1, A4, FUNCT_1:21, XBOOLE_0:3; :: thesis: verum
end;
now
let x be set ; :: thesis: ( x in dom (f * g) implies (f * (g +* h)) . x = (f * g) . x )
assume x in dom (f * g) ; :: thesis: (f * (g +* h)) . x = (f * g) . x
then A5: ( x in dom g & g . x in dom f ) by FUNCT_1:21;
now
assume x in dom h ; :: thesis: contradiction
then g . x in g .: (dom h) by A5, FUNCT_1:def 12;
hence contradiction by A1, A5, XBOOLE_0:3; :: thesis: verum
end;
then ( x in dom (g +* h) & g . x = (g +* h) . x ) by A5, FUNCT_4:12, FUNCT_4:13;
hence (f * (g +* h)) . x = f . (g . x) by FUNCT_1:23
.= (f * g) . x by A5, FUNCT_1:23 ;
:: thesis: verum
end;
hence f * (g +* h) = f * g by A2, FUNCT_1:9; :: thesis: verum