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 object st x in X holds
x in dom F by Th11;
hence X c= dom F ; :: thesis: F .: X c= dom G
let x be object ; :: 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 object st
( y in dom F & y in X & x = F . y ) by Def6;
hence x in dom G by A1, Th11; :: 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 object ; :: 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, Def6;
hence x in dom (G * F) by A2, A3, A4, Th11; :: thesis: verum