theorem :: FINSEQ_4:28

for p being FinSequence
for x being object holds
( p just_once_values x iff ( x in rng p & {(x .. p)} = p " {x} ) )