let q1, q2 be FinSequence; :: thesis: ( len q1 = (len p) + 1 & q1 . 1 = x & ( for i being Element of 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 Element of 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 & q1 . 1 = x ) and
A7: for i being Element of NAT
for f being Function st i in dom p & f = p . i holds
q1 . (i + 1) = f . (q1 . i) and
A8: ( len q2 = (len p) + 1 & q2 . 1 = x ) and
A9: for i being Element of NAT
for f being Function st i in dom p & f = p . i holds
q2 . (i + 1) = f . (q2 . i) ; :: thesis: q1 = q2
A10: dom q1 = dom q2 by A6, A8, FINSEQ_3:31;
defpred S₁[ Nat] means ( $1 in dom q1 implies q1 . $1 = q2 . $1 );
A11: S₁[ 0 ] by FINSEQ_3:27;
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:27;
then A15: i <= len p by A6, XREAL_1:8;

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 A6, A8; :: thesis: verum

end;

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

then i >= 0 + 1 by NAT_1:13;
then A16: i in dom p by A15, FINSEQ_3:27;
reconsider f = p . i as Function ;
thus q1 . (i + 1) = f . (q2 . i) by A6, A7, A13, A16, Th24
.= q2 . (i + 1) by A9, A16 ; :: thesis: verum

end;

end;

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A11, A12);
hence q1 = q2 by A10, FINSEQ_1:17; :: thesis: verum