let x be object ; :: according to FUNCT_1:def 14 :: thesis: ( x in dom (g | X) implies (g | X) . x in f . x )
A1: dom (g | X) c= dom g by RELAT_1:60;
assume A2: x in dom (g | X) ; :: thesis: (g | X) . x in f . x
then g . x in f . x by A1, Def14;
hence (g | X) . x in f . x by A2, Th46; :: thesis: verum