let Al be QC-alphabet ; :: thesis:
let i be Nat; :: thesis:
let F1, F2 be QC-formula of Al; :: thesis:
let L be PATH of F1,F2; :: thesis:
set n = len L;
assume that
A1: F1 is_subformula_of F2 and
A2: 1 <= i and
A3: i <= len L ; :: thesis:
(len L) + 1 <= (len L) + i by A2, XREAL_1:6;
then ((len L) + 1) + (- 1) <= ((len L) + i) + (- 1) by XREAL_1:6;
then A4: (len L) + (- i) <= (((len L) - 1) + i) + (- i) by XREAL_1:6;
i + (- i) <= (len L) + (- i) by A3, XREAL_1:6;
then reconsider l = (len L) - i as Element of NAT by INT_1:3;
defpred S₁[ Nat] means ( $1 <= (len L) - 1 implies ex F3 being QC-formula of Al st
( F3 = L . ((len L) - $1) & F3 is_subformula_of F2 ) );
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume A6: S₁[k] ; :: thesis:
assume A7: k + 1 <= (len L) - 1 ; :: thesis:
then (k + 1) + 1 <= ((len L) - 1) + 1 by XREAL_1:6;
then A8: (2 + k) + (- k) <= (len L) + (- k) by XREAL_1:6;
then reconsider j = (len L) - k as Element of NAT by INT_1:3;
len L <= (len L) + k by NAT_1:11;
then (len L) + (- k) <= ((len L) + k) + (- k) by XREAL_1:6;
then A9: j - 1 < len L by XREAL_1:146, XXREAL_0:2;
A10: (1 + 1) + (- 1) <= j + (- 1) by A8, XREAL_1:6;
then reconsider j1 = j - 1 as Element of NAT by INT_1:3;
j1 + 1 = j ;
then A11: ex G1, H1 being Element of QC-WFF Al st
( L . j1 = G1 & L . j = H1 & G1 is_immediate_constituent_of H1 ) by A1, A10, A9, Def5;
then reconsider F3 = L . j1 as QC-formula of Al ;
take F3 ; :: thesis:
k < k + 1 by NAT_1:13;
then F3 is_proper_subformula_of F2 by A6, A7, A11, QC_LANG2:63, XXREAL_0:2;
hence ( F3 = L . ((len L) - (k + 1)) & F3 is_subformula_of F2 ) by QC_LANG2:def 21; :: thesis:

end;

L . (len L) = F2 by A1, Def5;
then A12: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A12, A5);
then ex F3 being QC-formula of Al st
( F3 = L . ((len L) - l) & F3 is_subformula_of F2 ) by A4;
hence ex F3 being QC-formula of Al st
( F3 = L . i & F3 is_subformula_of F2 ) ; :: thesis: