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:61;
hence ( not x in dom g or ((f,X) +* g) . x = g . x ) by FUNCT_4:11; :: thesis: verum