for f being Function st rng f = dom f holds
f is onto Function of (dom f),(dom f) by Lm64;