let X, Y be set ; :: thesis: for f, g being PartFunc of , holds f +* g is PartFunc of ,
let f, g be PartFunc of ,; :: thesis: f +* g is PartFunc of ,
rng (f +* g) c= (rng f) \/ (rng g) by Th18;
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 , by A1, RELSET_1:11; :: thesis: verum