per cases ( D = {} or D <> {} ) ;

suppose D = {} ; :: thesis: f +* g is Function of A,B

then g = {} ;
hence f +* g is Function of A,B by FUNCT_4:21; :: thesis: verum

end;

suppose A0: D <> {} ; :: thesis: f +* g is Function of A,B

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

end;

end;