let f, g be Function; :: thesis: .: (g * f) = (.: g) * (.: f)
for x being set holds
( x in dom (.: (g * f)) iff x in dom ((.: g) * (.: f)) )

proof

let x be set ; :: thesis: ( x in dom (.: (g * f)) iff x in dom ((.: g) * (.: f)) )
thus ( x in dom (.: (g * f)) implies x in dom ((.: g) * (.: f)) ) :: thesis: ( x in dom ((.: g) * (.: f)) implies x in dom (.: (g * f)) )

proof

assume x in dom (.: (g * f)) ; :: thesis: x in dom ((.: g) * (.: f))
then A1: x in bool (dom (g * f)) by Def1;
dom (g * f) c= dom f by RELAT_1:25;
then A2: x c= dom f by A1, XBOOLE_1:1;
then x in bool (dom f) ;
then A3: x in dom (.: f) by Def1;
f .: x c= dom g by A1, Th2;
then f .: x in bool (dom g) ;
then f .: x in dom (.: g) by Def1;
then (.: f) . x in dom (.: g) by A2, Def1;
hence x in dom ((.: g) * (.: f)) by A3, FUNCT_1:11; :: thesis: verum

end;

assume A4: x in dom ((.: g) * (.: f)) ; :: thesis: x in dom (.: (g * f))
then A5: x in dom (.: f) by FUNCT_1:11;
(.: f) . x in dom (.: g) by A4, FUNCT_1:11;
then f .: x in dom (.: g) by A5, Th8;
then A6: f .: x in bool (dom g) by Def1;
x in bool (dom f) by A5, Def1;
then x c= dom (g * f) by A6, Th3;
then x in bool (dom (g * f)) ;
hence x in dom (.: (g * f)) by Def1; :: thesis: verum

end;

then A7: dom (.: (g * f)) = dom ((.: g) * (.: f)) by TARSKI:1;
for x being set st x in dom (.: (g * f)) holds
(.: (g * f)) . x = ((.: g) * (.: f)) . x

proof

let x be set ; :: thesis: ( x in dom (.: (g * f)) implies (.: (g * f)) . x = ((.: g) * (.: f)) . x )
assume A8: x in dom (.: (g * f)) ; :: thesis: (.: (g * f)) . x = ((.: g) * (.: f)) . x
then A9: x in bool (dom (g * f)) by Def1;
then A10: f .: x c= dom g by Th2;
dom (g * f) c= dom f by RELAT_1:25;
then A11: x c= dom f by A9, XBOOLE_1:1;
then x in bool (dom f) ;
then A12: x in dom (.: f) by Def1;
thus (.: (g * f)) . x = (g * f) .: x by A8, Th8
.= g .: (f .: x) by RELAT_1:126
.= (.: g) . (f .: x) by A10, Def1
.= (.: g) . ((.: f) . x) by A11, Def1
.= ((.: g) * (.: f)) . x by A12, FUNCT_1:13 ; :: thesis: verum

end;

hence .: (g * f) = (.: g) * (.: f) by A7, FUNCT_1:2; :: thesis: verum