set H = f1 +* f2;
rng (f1 +* f2) c= (rng f1) \/ (rng f2) by FUNCT_4:17;
then A2: rng (f1 +* f2) c= B by XBOOLE_1:1;
( dom f1 = A1 & dom f2 = A2 ) by FUNCT_2:def 1;
then dom (f1 +* f2) = A1 \/ A2 by FUNCT_4:def 1;
hence f1 +* f2 is Function of (A1 \/ A2),B by A2, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum