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

now

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 Element of NAT such that
A16: ( k = n + 1 & n < len q1 ) by A15, Lm1;
thus q1 . k = p ^ <*n*> by A12, A16
.= q2 . k by A11, A13, A14, A16 ; :: thesis: verum

end;

hence q1 = q2 by A15, FINSEQ_1:17; :: thesis: verum