let p, q be FinSequence; :: thesis: ( len p = len q & ( for k being Nat st 1 <= k & k <= len p holds
p . k = q . k ) implies p = q )
assume that
A1: len p = len q and
A2: for k being Nat st 1 <= k & k <= len p holds
p . k = q . k ; :: thesis: p = q
A3: dom p = Seg (len p) by Def3;
A4: dom q = Seg (len q) by Def3;

now

let x be set ; :: thesis: ( x in dom p implies p . x = q . x )
assume A5: x in dom p ; :: thesis: p . x = q . x
then reconsider k = x as Nat ;
( 1 <= k & k <= len p ) by A3, A5, Th3;
hence p . x = q . x by A2; :: thesis: verum

end;

hence p = q by A1, A3, A4, FUNCT_1:9; :: thesis: verum