let x be object ; :: thesis: for f, g being Function st dom f misses dom g & x in dom f holds
(f +* g) . x = f . x
let f, g be Function; :: thesis: ( dom f misses dom g & x in dom f implies (f +* g) . x = f . x )
assume ( (dom f) /\ (dom g) = {} & x in dom f ) ; :: according to XBOOLE_0:def 7 :: thesis: (f +* g) . x = f . x
then not x in dom g by XBOOLE_0:def 4;
hence (f +* g) . x = f . x by Th11; :: thesis: verum