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

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

then A1: g = {} ;
thus f +* g is Function of A,B by A1; :: thesis: verum

end;

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

A3: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1
.= A \/ (dom g) by FUNCT_2:def 1
.= A \/ C by A2, FUNCT_2:def 1
.= A by XBOOLE_1:12 ;
A4: 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 A3, A4, FUNCT_2:2, XBOOLE_1:1; :: thesis: verum

end;

end;