let Al be QC-alphabet ; :: thesis: for i, n being Nat
for p, q being Element of CQC-WFF Al
for L being PATH of q,p st QuantNbr p <= n & q is_subformula_of p & 1 <= i & i <= len L holds
ex r being Element of CQC-WFF Al st
( r = L . i & QuantNbr r <= n )

let i, n be Nat; :: thesis: for p, q being Element of CQC-WFF Al
for L being PATH of q,p st QuantNbr p <= n & q is_subformula_of p & 1 <= i & i <= len L holds
ex r being Element of CQC-WFF Al st
( r = L . i & QuantNbr r <= n )

let p, q be Element of CQC-WFF Al; :: thesis: for L being PATH of q,p st QuantNbr p <= n & q is_subformula_of p & 1 <= i & i <= len L holds
ex r being Element of CQC-WFF Al st
( r = L . i & QuantNbr r <= n )

let L be PATH of q,p; :: thesis: ( QuantNbr p <= n & q is_subformula_of p & 1 <= i & i <= len L implies ex r being Element of CQC-WFF Al st
( r = L . i & QuantNbr r <= n ) )

set m = len L;
assume that
A1: QuantNbr p <= n and
A2: q is_subformula_of p and
A3: 1 <= i and
A4: i <= len L ; :: thesis: ex r being Element of CQC-WFF Al st
( r = L . i & QuantNbr r <= n )

i + (- i) <= (len L) + (- i) by ;
then reconsider l = (len L) - i as Element of NAT by INT_1:3;
(len L) + 1 <= (len L) + i by ;
then ((len L) + 1) + (- 1) <= ((len L) + i) + (- 1) by XREAL_1:6;
then A5: (len L) + (- i) <= (((len L) - 1) + i) + (- i) by XREAL_1:6;
defpred S1[ Nat] means ( \$1 <= (len L) - 1 implies ex r being Element of CQC-WFF Al st
( r = L . ((len L) - \$1) & QuantNbr r <= n ) );
A6: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A7: S1[k] ; :: thesis: S1[k + 1]
assume A8: k + 1 <= (len L) - 1 ; :: thesis: ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

then (k + 1) + 1 <= ((len L) - 1) + 1 by XREAL_1:6;
then A9: (2 + k) + (- k) <= (len L) + (- k) by XREAL_1:6;
then reconsider j = (len L) - k as Element of NAT by INT_1:3;
A10: (1 + 1) + (- 1) <= j + (- 1) by ;
then reconsider j1 = j - 1 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 A11: j - 1 < len L by ;
j1 + 1 = j ;
then consider G1, H1 being Element of QC-WFF Al such that
A12: L . j1 = G1 and
A13: ( L . j = H1 & G1 is_immediate_constituent_of H1 ) by A2, A10, A11, Def5;
reconsider r = G1 as Element of CQC-WFF Al by A2, A10, A11, A12, Th28;
k < k + 1 by NAT_1:13;
then consider q being Element of CQC-WFF Al such that
A14: q = L . j and
A15: QuantNbr q <= n by ;
A16: now :: thesis: ( ex x being bound_QC-variable of Al st q = All (x,G1) implies ex r, r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) )
given x being bound_QC-variable of Al such that A17: q = All (x,G1) ; :: thesis: ex r, r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

take r = r; :: thesis: ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

(QuantNbr r) + 1 <= n by ;
then QuantNbr r <= n by NAT_1:13;
hence ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A12; :: thesis: verum
end;
A18: now :: thesis: ( ex F being Element of QC-WFF Al st q = F '&' G1 implies ex r, r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) )
given F being Element of QC-WFF Al such that A19: q = F '&' G1 ; :: thesis: ex r, r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

reconsider F = F as Element of CQC-WFF Al by ;
take r = r; :: thesis: ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

n <= n + () by NAT_1:11;
then A20: n + (- ()) <= (n + ()) + (- ()) by XREAL_1:6;
(QuantNbr r) + () <= n by ;
then ((QuantNbr r) + ()) + (- ()) <= n + (- ()) by XREAL_1:6;
hence ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by ; :: thesis: verum
end;
A21: now :: thesis: ( ex F being Element of QC-WFF Al st q = G1 '&' F implies ex r, r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) )
given F being Element of QC-WFF Al such that A22: q = G1 '&' F ; :: thesis: ex r, r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

reconsider F = F as Element of CQC-WFF Al by ;
take r = r; :: thesis: ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

n <= n + () by NAT_1:11;
then A23: n + (- ()) <= (n + ()) + (- ()) by XREAL_1:6;
(QuantNbr r) + () <= n by ;
then ((QuantNbr r) + ()) + (- ()) <= n + (- ()) by XREAL_1:6;
hence ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by ; :: thesis: verum
end;
now :: thesis: ( q = 'not' G1 implies ex r, r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) )
assume A24: q = 'not' G1 ; :: thesis: ex r, r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

take r = r; :: thesis: ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )

QuantNbr r <= n by ;
hence ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A12; :: thesis: verum
end;
hence ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by ; :: thesis: verum
end;
L . (len L) = p by ;
then A25: S1[ 0 ] by A1;
for k being Nat holds S1[k] from NAT_1:sch 2(A25, A6);
then ex r being Element of CQC-WFF Al st
( r = L . ((len L) - l) & QuantNbr r <= n ) by A5;
hence ex r being Element of CQC-WFF Al st
( r = L . i & QuantNbr r <= n ) ; :: thesis: verum