let f, g be Function; :: thesis: for x, X being set st x nin X & x in dom g holds
(f,X +* g) . x = g . x
let x, X be set ; :: thesis: ( x nin X & x in dom g implies (f,X +* g) . x = g . x )
assume x nin X ; :: thesis: ( not x in dom g or (f,X +* g) . x = g . x )
then x nin (dom f) /\ X by XBOOLE_0:def 4;
then x nin dom (f | X) by RELAT_1:90;
hence ( not x in dom g or (f,X +* g) . x = g . x ) by FUNCT_4:12; :: thesis: verum