theorem :: MATRTOP1:6

for F being Function ex X being set st
( X c= dom F & rng F = rng (F | X) & F | X is one-to-one )