let x be set ; :: thesis: for f being Function st f is one-to-one & x in rng f holds
card (Coim (f,x)) = 1
let f be Function; :: thesis: ( f is one-to-one & x in rng f implies card (Coim (f,x)) = 1 )
assume ( f is one-to-one & x in rng f ) ; :: thesis: card (Coim (f,x)) = 1
then f just_once_values x by Th8;
hence card (Coim (f,x)) = 1 by Def2; :: thesis: verum