let p, q be XFinSequence; :: thesis: ( len p = len q & ( for j being Nat st j in dom p holds
p . j = q . j ) implies p = q )
assume that
A1: len p = len q and
A2: for j being Nat st j in dom p holds
p . j = q . j ; :: thesis: p = q
for k being Element of NAT st k < len p holds
p . k = q . k

proof

let k be Element of NAT ; :: thesis: ( k < len p implies p . k = q . k )
assume k < len p ; :: thesis: p . k = q . k
then k in dom p by NAT_1:45;
hence p . k = q . k by A2; :: thesis: verum

end;

hence p = q by A1, AFINSQ_1:11; :: thesis: verum