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
( dom f c= X & dom g c= X & dom (f +* g) = (dom f) \/ (dom g) & rng (f +* g) c= (rng f) \/ (rng g) & (rng f) \/ (rng g) c= Y ) by Def1, Th18;
then ( dom (f +* g) c= X & rng (f +* g) c= Y ) by XBOOLE_1:1;
hence f +* g is PartFunc of X,Y by RELSET_1:11; :: thesis: verum