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 ;