let x be set ; :: thesis: for g, f being Function st x in dom g holds
(f +* g) . x = g . x
let g, f be Function; :: thesis: ( x in dom g implies (f +* g) . x = g . x )
( x in dom g implies x in (dom f) \/ (dom g) ) by XBOOLE_0:def 3;
hence ( x in dom g implies (f +* g) . x = g . x ) by Def1; :: thesis: verum