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 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 L . ((len L) - $1) is Element of CQC-WFF Al );
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[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 A6, A7, XXREAL_0:2;
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 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 A11, CQC_LANG:9;
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 A11, CQC_LANG:13;
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 A11, CQC_LANG:9;
( q = 'not' G1 implies L . ((len L) - (k + 1)) is Element of CQC-WFF Al ) by A11, CQC_LANG:8;
hence L . ((len L) - (k + 1)) is Element of CQC-WFF Al by A12, A13, A15, A14, QC_LANG2:def 19; :: thesis: verum

end;

A16: S₁[ 0 ] by A1, Def5;
for k being Nat holds S₁[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