theorem :: FLEXARY1:32

for f being Function-yielding Function holds
( f is double-one-to-one iff ( ( for x being object holds f . x is one-to-one ) & ( for x, y being object st x <> y holds
rng (f . x) misses rng (f . y) ) ) )