A1: dom f = A by FUNCT_2:def 1;
A2: dom g c= A by RELAT_1:def 18;
A3: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1
.= A by A1, A2, XBOOLE_1:12 ;

now

let x be set ; :: thesis: ( x in A implies (f +* g) . b₁ in B )
assume A4: x in A ; :: thesis: (f +* g) . b₁ in B

per cases ( x in dom g or not x in dom g ) ;

suppose A5: x in dom g ; :: thesis: (f +* g) . b₁ in B

then (f +* g) . x = g . x by FUNCT_4:14;
hence (f +* g) . x in B by A5, PARTFUN1:27; :: thesis: verum

end;

suppose not x in dom g ; :: thesis: (f +* g) . b₁ in B

then (f +* g) . x = f . x by FUNCT_4:12;
hence (f +* g) . x in B by A4, FUNCT_2:7; :: thesis: verum

end;

end;

end;

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