theorem Th27: :: FINSEQ_4:27

for p being FinSequence
for x being object st x in rng p & ( for k being Nat st k in dom p & k <> x .. p holds
p . k <> x ) holds
p just_once_values x