let f, g be Function-yielding Function; :: thesis: doms (f * g) = (doms f) * g
A1: ( dom (doms (f * g)) = dom (f * g) & dom (doms f) = dom f ) by FUNCT_6:def 2;
A2: dom (doms (f * g)) = dom ((doms f) * g)
proof
thus dom (doms (f * g)) c= dom ((doms f) * g) :: according to XBOOLE_0:def 10 :: thesis: dom ((doms f) * g) c= dom (doms (f * g))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (doms (f * g)) or x in dom ((doms f) * g) )
assume x in dom (doms (f * g)) ; :: thesis: x in dom ((doms f) * g)
then ( x in dom (f * g) & (f * g) . x is Function ) by A1;
then A3: ( x in dom g & g . x in dom f & (f * g) . x = f . (g . x) ) by FUNCT_1:11, FUNCT_1:12;
then g . x in dom (doms f) by FUNCT_6:22;
hence x in dom ((doms f) * g) by A3, FUNCT_1:11; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((doms f) * g) or x in dom (doms (f * g)) )
assume x in dom ((doms f) * g) ; :: thesis: x in dom (doms (f * g))
then A4: ( x in dom g & g . x in dom (doms f) ) by FUNCT_1:11;
then A5: ( g . x in dom f & f . (g . x) is Function & f . (g . x) = (f * g) . x ) by A1, FUNCT_1:13;
then x in dom (f * g) by A4, FUNCT_1:11;
hence x in dom (doms (f * g)) by A5, FUNCT_6:22; :: thesis: verum
end;
now :: thesis: for x being object st x in dom (doms (f * g)) holds
(doms (f * g)) . x = ((doms f) * g) . x
let x be object ; :: thesis: ( x in dom (doms (f * g)) implies (doms (f * g)) . x = ((doms f) * g) . x )
assume x in dom (doms (f * g)) ; :: thesis: (doms (f * g)) . x = ((doms f) * g) . x
then A6: ( x in dom g & g . x in dom (doms f) & (doms (f * g)) . x = proj1 ((f * g) . x) ) by A1, FUNCT_1:11, FUNCT_6:def 2;
then A7: (doms f) . (g . x) = proj1 (f . (g . x)) by A1, FUNCT_6:def 2;
thus (doms (f * g)) . x = (doms f) . (g . x) by A6, A7, FUNCT_1:13
.= ((doms f) * g) . x by A6, FUNCT_1:13 ; :: thesis: verum
end;
hence doms (f * g) = (doms f) * g by A2; :: thesis: verum