thus for p1, p2 being XFinSequence of D 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 D; :: 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 that
A9: len p1 = len q and
A10: for i being Nat st i < len q holds
q . (i + 1) = p1 . i and
A11: len p2 = len q and
A12: for i being Nat st i < len q holds
q . (i + 1) = p2 . i ; :: thesis: p1 = p2
for i being Nat st i < len p1 holds
p1 . i = p2 . i

proof

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

end;

hence p1 = p2 by A9, A11, Th8; :: thesis: verum

end;