let f, g be Function; :: thesis: for x, X being set st x in X & X c= dom f holds
((f,X) +* g) . x = f . x
let x, X be set ; :: thesis: ( x in X & X c= dom f implies ((f,X) +* g) . x = f . x )
assume A1: x in X ; :: thesis: ( not X c= dom f or ((f,X) +* g) . x = f . x )
assume A2: X c= dom f ; :: thesis: ((f,X) +* g) . x = f . x
dom (f | X) = (dom f) /\ X by RELAT_1:61;
then A3: x in dom (f | X) by A1, A2, XBOOLE_0:def 4;
then (f | X) . x = f . x by FUNCT_1:47;
hence ((f,X) +* g) . x = f . x by A3, FUNCT_4:13; :: thesis: verum