A1: ( dom g c= A & rng g c= B & dom f = A & rng f c= B ) by RELAT_1:def 19, FUNCT_2:def 1;
then A2: ( dom (f +* g) = (dom f) \/ (dom g) & (dom f) \/ (dom g) = A ) by XBOOLE_1:12, FUNCT_4:def 1;
( rng (f +* g) c= (rng f) \/ (rng g) & (rng f) \/ (rng g) c= B \/ B ) by A1, XBOOLE_1:13, FUNCT_4:17;
then rng (f +* g) c= B ;
hence f +* g is Function of A,B by A2, FUNCT_2:2; :: thesis: verum