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