theorem :: FINSEQ_4:73

for x being object
for f being Function st f is one-to-one & x in rng f holds
card (Coim (f,x)) = 1 by Th8, Def2;