thus for p1, p2 being XFinSequence of st len p1 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = p1 . i ) & len p2 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = p2 . i ) holds
p1 = p2 :: thesis: verum

proof

let p1, p2 be XFinSequence of ; :: thesis: ( len p1 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = p1 . i ) & len p2 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = p2 . i ) implies p1 = p2 )
assume A9: ( len p1 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = p1 . i ) & len p2 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = p2 . i ) ) ; :: thesis: p1 = p2
for i being Element of NAT st i < len p1 holds
p1 . i = p2 . i

proof

let i be Element of NAT ; :: thesis: ( i < len p1 implies p1 . i = p2 . i )
assume A10: i < len p1 ; :: thesis: p1 . i = p2 . i
then q . (i + 1) = p1 . i by A9;
hence p1 . i = p2 . i by A9, A10; :: thesis: verum

end;

hence p1 = p2 by A9, AFINSQ_1:11; :: thesis: verum

end;