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 X c= dom f ; :: thesis: (f,X +* g) . x = f . x
then ( x in dom f & dom (f | X) = (dom f) /\ X ) by A1, RELAT_1:90;
then A2: x in dom (f | X) by A1, XBOOLE_0:def 4;
then (f | X) . x = f . x by FUNCT_1:70;
hence (f,X +* g) . x = f . x by A2, FUNCT_4:14; :: thesis: verum