let f, g be Function; 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 ; ( x in X & X c= dom f implies ((f,X) +* g) . x = f . x )
assume A1:
x in X
; ( not X c= dom f or ((f,X) +* g) . x = f . x )
assume A2:
X c= dom f
; ((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; verum