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

proof

let x be object ; :: thesis: ( x in dom (.: (g * f)) iff x in dom ((.: g) * (.: f)) )
reconsider xx = x as set by TARSKI:1;
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: xx c= dom f by A1;
then x in bool (dom f) ;
then A3: x in dom (.: f) by Def1;
f .: xx c= dom g by A1, Th2;
then f .: xx in bool (dom g) ;
then f .: xx 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 .: xx in dom (.: g) by A5, Th7;
then A6: f .: xx in bool (dom g) by Def1;
x in bool (dom f) by A5, Def1;
then xx 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:2;
for x being object st x in dom (.: (g * f)) holds
(.: (g * f)) . x = ((.: g) * (.: f)) . x

proof

let x be object ; :: 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;
reconsider xx = x as set by TARSKI:1;
A10: f .: xx c= dom g by Th2, A9;
dom (g * f) c= dom f by RELAT_1:25;
then A11: xx c= dom f by A9;
then x in bool (dom f) ;
then A12: x in dom (.: f) by Def1;
thus (.: (g * f)) . x = (g * f) .: xx by A8, Th7
.= g .: (f .: xx) by RELAT_1:126
.= (.: g) . (f .: xx) 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; :: thesis: verum