theorem Th6: :: FINSEQ_4:6

for f being Function
for y being object holds
( f just_once_values y iff ex x being object st {x} = f " {y} ) by CARD_2:42;