:: deftheorem Def2 defines just_once_values FINSEQ_4:def 2 :
for R being Relation
for y being object holds
( R just_once_values y iff card (Coim (R,y)) = 1 );