dom g = X by FUNCT_2:92;
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:17;
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