let f, g be Function; :: thesis: f +* g = (f \ [:(dom g),(rng f):]) \/ g
set df = dom f;
set dg = dom g;
set rf = rng f;
(f | (dom f)) +* g = (f | ((dom f) \ (dom g))) \/ g by Th57
.= ((f | (dom f)) \ [:(dom g),(rng f):]) \/ g by Lm55 ;
hence f +* g = (f \ [:(dom g),(rng f):]) \/ g ; :: thesis: verum