let f, g be Function; for x, y being set st dom f = dom g & f . x = g . x & f . y = g . y holds
f | {x,y} = g | {x,y}
let x, y be set ; ( dom f = dom g & f . x = g . x & f . y = g . y implies f | {x,y} = g | {x,y} )
assume
( dom f = dom g & f . x = g . x & f . y = g . y )
; f | {x,y} = g | {x,y}
then A1:
( f | {x} = g | {x} & f | {y} = g | {y} )
by Th27;
{x,y} = {x} \/ {y}
by ENUMSET1:1;
hence
f | {x,y} = g | {x,y}
by A1, RELAT_1:150; verum