let q1, q2 be one-to-one FinSequence of t; :: thesis: ( len q1 = card (succ p) & rng q1 = succ p & ( for i being Nat st i < len q1 holds
q1 . (i + 1) = p ^ <*i*> ) & len q2 = card (succ p) & rng q2 = succ p & ( for i being Nat st i < len q2 holds
q2 . (i + 1) = p ^ <*i*> ) implies q1 = q2 )
assume that
A12: len q1 = card (succ p) and
rng q1 = succ p and
A13: for i being Nat st i < len q1 holds
q1 . (i + 1) = p ^ <*i*> and
A14: len q2 = card (succ p) and
rng q2 = succ p and
A15: for i being Nat st i < len q2 holds
q2 . (i + 1) = p ^ <*i*> ; :: thesis: q1 = q2
A16: dom q1 = Seg (card (succ p)) by A12, FINSEQ_1:def 3;

A17: now :: thesis: for k being Nat st k in Seg (card (succ p)) holds
q1 . k = q2 . k

let k be Nat; :: thesis: ( k in Seg (card (succ p)) implies q1 . k = q2 . k )
assume k in Seg (card (succ p)) ; :: thesis: q1 . k = q2 . k
then consider n being Nat such that
A18: ( k = n + 1 & n < len q1 ) by A16, Lm1;
thus q1 . k = p ^ <*n*> by A13, A18
.= q2 . k by A12, A14, A15, A18 ; :: thesis: verum

end;

dom q2 = Seg (card (succ p)) by A14, FINSEQ_1:def 3;
hence q1 = q2 by A16, A17; :: thesis: verum