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;
A8: F₇() . (F₅(),(while (F₂(),F₃()))) = r . (len r) by A5, A6, A7, Th86;
defpred S₁[ Nat] means ( $1 + 1 in dom r implies ( P₁[r . ($1 + 1)] & ( $1 + 1 < len r implies P₂[r . ($1 + 1)] ) & ex q being Element of F₄() st
( P₁[q] & r . ($1 + 1) = F₇() . (q,F₂()) ) ) );
( 0 + 1 < len r implies r . (0 + 1) in F₆() ) by A7;
then A9: S₁[ 0 ] by A1, A4, A5;
A10: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A11: S₁[n] ; :: thesis: S₁[n + 1]
assume A12: (n + 1) + 1 in dom r ; :: thesis: ( P₁[r . ((n + 1) + 1)] & ( (n + 1) + 1 < len r implies P₂[r . ((n + 1) + 1)] ) & ex q being Element of F₄() st
( P₁[q] & r . ((n + 1) + 1) = F₇() . (q,F₂()) ) )
then A13: (n + 1) + 1 <= len r by FINSEQ_3:25;
A14: (n + 1) + 1 >= 1 by NAT_1:11;
A15: n + 1 >= 1 by NAT_1:11;
A16: n + 1 < len r by A13, NAT_1:13;
then A17: n + 1 in dom r by A15, FINSEQ_3:25;
A18: r . (n + 1) in F₆() by A7, A15, A16;
A19: r . ((n + 1) + 1) = F₇() . ((r . (n + 1)),(F₃() \; F₂())) by A7, A15, A16;
reconsider q1 = r . (n + 1), q2 = r . ((n + 1) + 1) as Element of F₄() by A12, A17, DTCONSTR:2;
reconsider q3 = F₇() . (q1,F₃()) as Element of F₄() ;
A20: q2 = F₇() . (q3,F₂()) by A19, Def29;
A21: P₁[q3] by A3, A11, A15, A16, A18, FINSEQ_3:25;
hence P₁[r . ((n + 1) + 1)] by A4, A20; :: thesis: ( ( (n + 1) + 1 < len r implies P₂[r . ((n + 1) + 1)] ) & ex q being Element of F₄() st
( P₁[q] & r . ((n + 1) + 1) = F₇() . (q,F₂()) ) )

hereby :: thesis: ex q being Element of F₄() st
( P₁[q] & r . ((n + 1) + 1) = F₇() . (q,F₂()) )

assume (n + 1) + 1 < len r ; :: thesis: P₂[r . ((n + 1) + 1)]
then r . ((n + 1) + 1) in F₆() by A7, A14;
hence P₂[r . ((n + 1) + 1)] by A4, A20, A21; :: thesis: verum

end;

take q3 ; :: thesis: ( P₁[q3] & r . ((n + 1) + 1) = F₇() . (q3,F₂()) )
thus ( P₁[q3] & r . ((n + 1) + 1) = F₇() . (q3,F₂()) ) by A3, A11, A15, A16, A18, A19, Def29, FINSEQ_3:25; :: thesis: verum

end;

A22: for n being Nat holds S₁[n] from NAT_1:sch 2(A9, A10);
A23: len r >= 0 + 1 by NAT_1:13;
then consider j being Nat such that
A24: len r = 1 + j by NAT_1:10;
A25: j + 1 in dom r by A23, A24, FINSEQ_3:25;
hence P₁[F₇() . (F₅(),(while (F₂(),F₃())))] by A8, A22, A24; :: thesis: P₂[F₇() . (F₅(),(while (F₂(),F₃())))]
ex q being Element of F₄() st
( P₁[q] & r . (j + 1) = F₇() . (q,F₂()) ) by A22, A25;
hence P₂[F₇() . (F₅(),(while (F₂(),F₃())))] by A4, A6, A8, A24; :: thesis: verum