let x be set ; :: thesis: for f being Function st f is one-to-one & x in rng f holds
card (f " {x}) = 1
let f be Function; :: thesis: ( f is one-to-one & x in rng f implies card (f " {x}) = 1 )
assume ( f is one-to-one & x in rng f ) ; :: thesis: card (f " {x}) = 1
then f just_once_values x by Th10;
then ex B being finite set st
( B = f " {x} & card B = 1 ) by Def2;
hence card (f " {x}) = 1 ; :: thesis: verum