consider r being non empty FinSequence of F₄() such that
A5: r . 1 = F₇() . (F₅(),F₂()) and
A6: r . (len r) nin F₆() and
A7: for i being Nat st 1 <= i & i < len r holds
( r . i in F₆() & r . (i + 1) = F₇() . ((r . i),(F₃() \; F₂())) ) by A2;
defpred S₁[ Nat] means ( (len r) - $1 in dom r implies P₁[r . ((len r) - $1)] );
defpred S₂[ Nat] means ( $1 + 1 in dom r implies ex q being Element of F₄() st r . ($1 + 1) = F₇() . (q,F₂()) );
A8: S₂[ 0 ] by A5;
A9: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume S₂[n] ; :: thesis: S₂[n + 1]
assume (n + 1) + 1 in dom r ; :: thesis: ex q being Element of F₄() st r . ((n + 1) + 1) = F₇() . (q,F₂())
then A10: (n + 1) + 1 <= len r by FINSEQ_3:25;
A11: n + 1 >= 1 by NAT_1:11;
A12: n + 1 < len r by A10, NAT_1:13;
then A13: r . (n + 1) in F₆() by A7, A11;
A14: r . ((n + 1) + 1) = F₇() . ((r . (n + 1)),(F₃() \; F₂())) by A7, A11, A12;
reconsider q1 = r . (n + 1) as Element of F₄() by A13;
reconsider q3 = F₇() . (q1,F₃()) as Element of F₄() ;
take q3 ; :: thesis: r . ((n + 1) + 1) = F₇() . (q3,F₂())
thus r . ((n + 1) + 1) = F₇() . (q3,F₂()) by A14, Def29; :: thesis: verum

end;

A15: S₁[ 0 ] by A1, A5, A6, A7, Th86;
A16: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A17: S₁[n] ; :: thesis: S₁[n + 1]
assume A18: (len r) - (n + 1) in dom r ; :: thesis: P₁[r . ((len r) - (n + 1))]
then reconsider j = (len r) - (n + 1) as Element of NAT ;
A19: j >= 1 by A18, FINSEQ_3:25;
n + 1 >= 0 + 1 by NAT_1:13;
then j <= (len r) - 1 by XREAL_1:10;
then A20: j + 1 <= ((len r) - 1) + 1 by XREAL_1:6;
A21: 1 <= 1 + j by NAT_1:11;
A22: j < len r by A20, NAT_1:13;
A23: j + 1 in dom r by A20, A21, FINSEQ_3:25;
A24: r . j in F₆() by A7, A19, A22;
A25: r . (j + 1) = F₇() . ((r . j),(F₃() \; F₂())) by A7, A19, A22;
reconsider q1 = r . j, q2 = r . (j + 1) as Element of F₄() by A23, A24, DTCONSTR:2;
reconsider q9 = F₇() . (q1,F₃()) as Element of F₄() ;
consider j9 being Nat such that
A26: j = 1 + j9 by A19, NAT_1:10;
for n being Nat holds S₂[n] from NAT_1:sch 2(A8, A9);
then consider qq being Element of F₄() such that
A27: r . (j9 + 1) = F₇() . (qq,F₂()) by A18, A26;
q2 = F₇() . (q9,F₂()) by A25, Def29;
then P₁[F₇() . ((F₇() . (qq,F₂())),F₃())] by A4, A17, A20, A21, A26, A27, FINSEQ_3:25;
hence P₁[r . ((len r) - (n + 1))] by A3, A7, A19, A22, A26, A27; :: thesis: verum

end;

A28: for n being Nat holds S₁[n] from NAT_1:sch 2(A15, A16);
A29: len r >= 0 + 1 by NAT_1:13;
then consider j being Nat such that
A30: len r = 1 + j by NAT_1:10;
(len r) - j in dom r by A29, A30, FINSEQ_3:25;
hence P₁[F₅()] by A4, A5, A28, A30; :: thesis: verum