let x be set ; :: according to FUNCT_1:def 20 :: thesis: ( x in dom (g | X) implies (g | X) . x in f . x )
F: dom (g | X) c= dom g by RELAT_1:89;
assume Z: x in dom (g | X) ; :: thesis: (g | X) . x in f . x
then x in dom g by F;
then g . x in f . x by Def20;
hence (g | X) . x in f . x by Z, Th70; :: thesis: verum