theorem Th7: :: FINSEQ_4:7

for f being Function
for y being object holds
( f just_once_values y iff ex x being object st
( x in dom f & y = f . x & ( for z being object st z in dom f & z <> x holds
f . z <> y ) ) )