theorem Th1: :: FRAENKEL:1

for A, B being set
for F, G being Function of A,B
for X being set st F | X = G | X holds
for x being Element of A st x in X holds
F . x = G . x