:: deftheorem defines = FINSEQ_1:def 17 :
for p, q being FinSequence holds
( p = q iff ( len p = len q & ( for k being Nat st 1 <= k & k <= len p holds
p . k = q . k ) ) );