let X, Y be set ; :: thesis: for f, g being PartFunc of X,Y st g is total holds
f +* g = g
let f, g be PartFunc of X,Y; :: thesis: ( g is total implies f +* g = g )
assume dom g = X ; :: according to PARTFUN1:def 2 :: thesis: f +* g = g
then dom f c= dom g ;
hence f +* g = g by Th19; :: thesis: verum