let q1, q2 be FinSequence; :: thesis: ( len q1 = (len p) + 1 & q1 . 1 = x & ( for i being Nat
for f being Function st i in dom p & f = p . i holds
q1 . (i + 1) = f . (q1 . i) ) & len q2 = (len p) + 1 & q2 . 1 = x & ( for i being Nat
for f being Function st i in dom p & f = p . i holds
q2 . (i + 1) = f . (q2 . i) ) implies q1 = q2 )
assume that
A6: len q1 = (len p) + 1 and
A7: q1 . 1 = x and
A8: for i being Nat
for f being Function st i in dom p & f = p . i holds
q1 . (i + 1) = f . (q1 . i) and
A9: len q2 = (len p) + 1 and
A10: q2 . 1 = x and
A11: for i being Nat
for f being Function st i in dom p & f = p . i holds
q2 . (i + 1) = f . (q2 . i) ; :: thesis: q1 = q2
defpred S₁[ Nat] means ( $1 in dom q1 implies q1 . $1 = q2 . $1 );
A12: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume that
A13: ( i in dom q1 implies q1 . i = q2 . i ) and
A14: i + 1 in dom q1 ; :: thesis: q1 . (i + 1) = q2 . (i + 1)
i + 1 <= len q1 by A14, FINSEQ_3:25;
then A15: i <= len p by A6, XREAL_1:6;

per cases ( i = 0 or i > 0 ) ;

suppose i = 0 ; :: thesis: q1 . (i + 1) = q2 . (i + 1)

hence q1 . (i + 1) = q2 . (i + 1) by A7, A10; :: thesis: verum

end;

suppose A16: i > 0 ; :: thesis: q1 . (i + 1) = q2 . (i + 1)

reconsider f = p . i as Function ;
i >= 0 + 1 by A16, NAT_1:13;
then A17: i in dom p by A15, FINSEQ_3:25;
hence q1 . (i + 1) = f . (q2 . i) by A6, A8, A13, Th22
.= q2 . (i + 1) by A11, A17 ;
:: thesis: verum

end;

end;

end;

A18: S₁[ 0 ] by FINSEQ_3:25;
A19: for i being Nat holds S₁[i] from NAT_1:sch 2(A18, A12);
dom q1 = dom q2 by A6, A9, FINSEQ_3:29;
hence q1 = q2 by A19; :: thesis: verum