theorem Th2: :: SIN_COS6:2
for f being Function
for X, Y being set st f | X is one-to-one & Y c= X holds
f | Y is one-to-one