let X, Y be set ; :: thesis: for f, g being PartFunc of X,Y holds f +* g is PartFunc of X,Y
let f, g be PartFunc of X,Y; :: thesis: f +* g is PartFunc of X,Y
rng (f +* g) c= (rng f) \/ (rng g) by Th17;
then A1: rng (f +* g) c= Y by XBOOLE_1:1;
dom (f +* g) = (dom f) \/ (dom g) by Def1;
hence f +* g is PartFunc of X,Y by A1, RELSET_1:4; :: thesis: verum