theorem Th25: :: FINSEQ_4:25

for p being FinSequence
for x being object st p just_once_values x holds
p <- x = x .. p