theorem :: AFINSQ_1:8

for p, q being XFinSequence st dom p = dom q & ( for k being Nat st k in dom p holds
p . k = q . k ) holds
p = q ;