let p, q be XFinSequence; :: thesis: ( len p = len q & ( for k being Element of NAT st k < len p holds
p . k = q . k ) implies p = q )
assume A1: ( len p = len q & ( for k being Element of NAT st k < len p holds
p . k = q . k ) ) ; :: thesis: p = q

now

let x be set ; :: thesis: ( x in dom p implies p . x = q . x )
assume A3: x in dom p ; :: thesis: p . x = q . x
then reconsider k = x as Element of NAT ;
k < len p by A3, NAT_1:45;
hence p . x = q . x by A1; :: thesis: verum

end;

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