theorem Th6: :: DIST_1:8

for S being finite set
for s being FinSequence of S holds s in Finseq-EQclass s ;