let f, g be Function; :: thesis: for x being object st x in dom g holds
(f +* g) . x = g . x
let x be object ; :: 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