let X be set ; :: thesis: for f, g being Function st X c= dom (g * f) holds
f .: X c= dom g
let f, g be Function; :: thesis: ( X c= dom (g * f) implies f .: X c= dom g )
assume A1: X c= dom (g * f) ; :: thesis: f .: X c= dom g
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: X or y in dom g )
assume y in f .: X ; :: thesis: y in dom g
then ex x being object st
( x in dom f & x in X & y = f . x ) by FUNCT_1:def 6;
hence y in dom g by A1, FUNCT_1:11; :: thesis: verum