let f, g be Function; :: thesis: for X being set st dom f = dom g & ( for x being set st x in X holds
f . x = g . x ) holds
f | X = g | X
let X be set ; :: thesis: ( dom f = dom g & ( for x being set st x in X holds
f . x = g . x ) implies f | X = g | X )
assume that
A1: dom f = dom g and
A2: for x being set st x in X holds
f . x = g . x ; :: thesis: f | X = g | X
A3: dom (f | X) = (dom f) /\ X by RELAT_1:61;
then A4: dom (f | X) = dom (g | X) by A1, RELAT_1:61;

now :: thesis: for x being object st x in dom (f | X) holds
(f | X) . x = (g | X) . x

let x be object ; :: thesis: ( x in dom (f | X) implies (f | X) . x = (g | X) . x )
assume A5: x in dom (f | X) ; :: thesis: (f | X) . x = (g | X) . x
then A6: x in X by A3, XBOOLE_0:def 4;
( (f | X) . x = f . x & (g | X) . x = g . x ) by A4, A5, Th46;
hence (f | X) . x = (g | X) . x by A2, A6; :: thesis: verum

end;

hence f | X = g | X by A4; :: thesis: verum