theorem Th54: :: FINSEQ_4:54

for p being FinSequence
for x being object holds
( p just_once_values x iff ( x in rng p & p - {x} = (p -| x) ^ (p |-- x) ) )