let X be set ; :: thesis: for f, g being Function st X c= dom f & f .: X c= dom g holds
X c= dom (g * f)
let f, g be Function; :: thesis: ( X c= dom f & f .: X c= dom g implies X c= dom (g * f) )
assume that
A1: X c= dom f and
A2: 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 A3: x in X ; :: thesis: x in dom (g * f)
then f . x in f .: X by A1, FUNCT_1:def 6;
hence x in dom (g * f) by A1, A2, A3, FUNCT_1:11; :: thesis: verum