theorem :: GLIBPRE1:4

for f being one-to-one Function
for y being object st rng f = {y} holds
ex x being object st f = x .--> y