let F, G be Function; :: thesis: for X being set holds
( X c= dom (G * F) iff ( X c= dom F & F .: X c= dom G ) )
let X be set ; :: thesis: ( X c= dom (G * F) iff ( X c= dom F & F .: X c= dom G ) )
thus ( X c= dom (G * F) implies ( X c= dom F & F .: X c= dom G ) ) :: thesis: ( X c= dom F & F .: X c= dom G implies X c= dom (G * F) )

proof

assume A1: X c= dom (G * F) ; :: thesis: ( X c= dom F & F .: X c= dom G )
then for x being set st x in X holds
x in dom F by Th21;
hence X c= dom F by TARSKI:def 3; :: thesis: F .: X c= dom G
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F .: X or x in dom G )
assume x in F .: X ; :: thesis: x in dom G
then ex y being set st
( y in dom F & y in X & x = F . y ) by Def12;
hence x in dom G by A1, Th21; :: thesis: verum

end;

assume that
A2: X c= dom F and
A3: F .: X c= dom G ; :: thesis: X c= dom (G * F)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in dom (G * F) )
assume A4: x in X ; :: thesis: x in dom (G * F)
then F . x in F .: X by A2, Def12;
hence x in dom (G * F) by A2, A3, A4, Th21; :: thesis: verum