let x be object ; :: thesis: for f, g being Function st x in (dom f) \ (dom g) holds
(f \ g) . x = f . x
let f, g be Function; :: thesis: ( x in (dom f) \ (dom g) implies (f \ g) . x = f . x )
assume A1: x in (dom f) \ (dom g) ; :: thesis: (f \ g) . x = f . x
( f \ g c= f & (dom f) \ (dom g) c= dom (f \ g) ) by XTUPLE_0:25;
hence (f \ g) . x = f . x by A1, Th2; :: thesis: verum