let f, g be Function; :: thesis: ( dom (g * f) = dom f implies rng f c= dom g )
assume A1: dom (g * f) = dom f ; :: thesis: rng f c= dom g
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in dom g )
assume y in rng f ; :: thesis: y in dom g
then ex x being object st
( x in dom f & y = f . x ) by Def3;
hence y in dom g by A1, Th11; :: thesis: verum