dom g = X by FUNCT_2:169;
then (dom g) \/ (dom (f | A)) = X by XBOOLE_1:12;
then A1: dom (f,A +* g) = X by FUNCT_4:def 1;
rng (f,A +* g) c= (rng g) \/ (rng (f | A)) by FUNCT_4:18;
then rng (f,A +* g) c= Y by XBOOLE_1:1;
hence f,A +* g is Element of Funcs X,Y by A1, FUNCT_2:def 2; :: thesis: verum