A1: now :: thesis: for x being object st x in A holds
(f +* g) . x in B

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

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

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

then (f +* g) . x = g . x by FUNCT_4:13;
hence (f +* g) . x in B by A3, PARTFUN1:4; :: thesis: verum

end;

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

then (f +* g) . x = f . x by FUNCT_4:11;
hence (f +* g) . x in B by A2, FUNCT_2:5; :: thesis: verum

end;

end;

end;

A4: ( dom f = A & dom g c= A ) by FUNCT_2:def 1, RELAT_1:def 18;
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