let Al be QC-alphabet ; :: thesis: for i being Nat
for p being Element of CQC-WFF Al
for F1 being QC-formula of Al
for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i <= len L holds
L . i is Element of CQC-WFF Al

let i be Nat; :: thesis: for p being Element of CQC-WFF Al
for F1 being QC-formula of Al
for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i <= len L holds
L . i is Element of CQC-WFF Al

let p be Element of CQC-WFF Al; :: thesis: for F1 being QC-formula of Al
for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i <= len L holds
L . i is Element of CQC-WFF Al

let F1 be QC-formula of Al; :: thesis: for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i <= len L holds
L . i is Element of CQC-WFF Al

let L be PATH of F1,p; :: thesis: ( F1 is_subformula_of p & 1 <= i & i <= len L implies L . i is Element of CQC-WFF Al )
set n = len L;
assume that
A1: F1 is_subformula_of p and
A2: 1 <= i and
A3: i <= len L ; :: thesis: L . i is Element of CQC-WFF Al
(len L) + 1 <= (len L) + i by ;
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 ;
then reconsider l = (len L) - i as Element of NAT by INT_1:3;
defpred S1[ Nat] means ( \$1 <= (len L) - 1 implies L . ((len L) - \$1) is Element of CQC-WFF Al );
A5: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; :: thesis: S1[k + 1]
assume A7: k + 1 <= (len L) - 1 ; :: thesis: L . ((len L) - (k + 1)) is Element of CQC-WFF Al
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;
k < k + 1 by NAT_1:13;
then reconsider q = L . j as Element of CQC-WFF Al by ;
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 ;
A10: (1 + 1) + (- 1) <= j + (- 1) by ;
then reconsider j1 = j - 1 as Element of NAT by INT_1:3;
j1 + 1 = j ;
then consider G1, H1 being Element of QC-WFF Al such that
A11: L . j1 = G1 and
A12: ( q = H1 & G1 is_immediate_constituent_of H1 ) by A1, A10, A9, Def5;
A13: ( ex F being Element of QC-WFF Al st q = G1 '&' F implies L . ((len L) - (k + 1)) is Element of CQC-WFF Al ) by ;
A14: ( ex x being bound_QC-variable of Al st q = All (x,G1) implies L . ((len L) - (k + 1)) is Element of CQC-WFF Al ) by ;
A15: ( ex F being Element of QC-WFF Al st q = F '&' G1 implies L . ((len L) - (k + 1)) is Element of CQC-WFF Al ) by ;
( q = 'not' G1 implies L . ((len L) - (k + 1)) is Element of CQC-WFF Al ) by ;
hence L . ((len L) - (k + 1)) is Element of CQC-WFF Al by ; :: thesis: verum
end;
A16: S1[ 0 ] by ;
for k being Nat holds S1[k] from NAT_1:sch 2(A16, A5);
then L . ((len L) - l) is Element of CQC-WFF Al by A4;
hence L . i is Element of CQC-WFF Al ; :: thesis: verum