theorem Th2: :: JORDAN9:2

for D being non empty set
for f, g being FinSequence of D st ( for n being Nat holds f | n = g | n ) holds
f = g