theorem Th8: :: AFINSQ_1:9

for p, q being XFinSequence st len p = len q & ( for k being Nat st k < len p holds
p . k = q . k ) holds
p = q