A1: now :: thesis: for x being object st x in A holds

(f +* g) . x in B

A4:
( dom f = A & dom g c= A )
by FUNCT_2:def 1, RELAT_1:def 18;(f +* g) . x in B

let x be object ; :: thesis: ( x in A implies (f +* g) . b_{1} in B )

assume A2: x in A ; :: thesis: (f +* g) . b_{1} in B

end;assume A2: x in A ; :: thesis: (f +* g) . b

dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1

.= A by A4, XBOOLE_1:12 ;

hence f +* g is Function of A,B by A1, FUNCT_2:3; :: thesis: verum