let q, p be Element of CQC-WFF ; :: thesis: for m, i being Element of NAT
for f being Element of Funcs bound_QC-variables ,bound_QC-variables
for K being Finite_Subset of bound_QC-variables st [q,m,K,f] in SepQuadruples p & x. i in f .: (still_not-bound_in p) holds
i < m
let m, i be Element of NAT ; :: thesis: for f being Element of Funcs bound_QC-variables ,bound_QC-variables
for K being Finite_Subset of bound_QC-variables st [q,m,K,f] in SepQuadruples p & x. i in f .: (still_not-bound_in p) holds
i < m
let f be Element of Funcs bound_QC-variables ,bound_QC-variables ; :: thesis: for K being Finite_Subset of bound_QC-variables st [q,m,K,f] in SepQuadruples p & x. i in f .: (still_not-bound_in p) holds
i < m
let K be Finite_Subset of bound_QC-variables ; :: thesis: ( [q,m,K,f] in SepQuadruples p & x. i in f .: (still_not-bound_in p) implies i < m )
defpred S₁[ Element of CQC-WFF , Element of NAT , Finite_Subset of bound_QC-variables , Function] means for i being Element of NAT st x. i in $4 .: (still_not-bound_in p) holds
i < $2;

A1: now

let q, r be Element of CQC-WFF ; :: thesis: for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(q '&' r),k,K,f] in SepQuadruples p & S₁[q '&' r,k,K,f] holds
( S₁[q,k,K,f] & S₁[r,k + (QuantNbr q),K,f] )
let k be Element of NAT ; :: thesis: for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(q '&' r),k,K,f] in SepQuadruples p & S₁[q '&' r,k,K,f] holds
( S₁[q,k,K,f] & S₁[r,k + (QuantNbr q),K,f] )
let K be Finite_Subset of bound_QC-variables ; :: thesis: for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(q '&' r),k,K,f] in SepQuadruples p & S₁[q '&' r,k,K,f] holds
( S₁[q,k,K,f] & S₁[r,k + (QuantNbr q),K,f] )
let f be Element of Funcs bound_QC-variables ,bound_QC-variables ; :: thesis: ( [(q '&' r),k,K,f] in SepQuadruples p & S₁[q '&' r,k,K,f] implies ( S₁[q,k,K,f] & S₁[r,k + (QuantNbr q),K,f] ) )
assume [(q '&' r),k,K,f] in SepQuadruples p ; :: thesis: ( S₁[q '&' r,k,K,f] implies ( S₁[q,k,K,f] & S₁[r,k + (QuantNbr q),K,f] ) )
assume A2: S₁[q '&' r,k,K,f] ; :: thesis: ( S₁[q,k,K,f] & S₁[r,k + (QuantNbr q),K,f] )
hence S₁[q,k,K,f] ; :: thesis: S₁[r,k + (QuantNbr q),K,f]
thus S₁[r,k + (QuantNbr q),K,f] :: thesis: verum

proof

let i be Element of NAT ; :: thesis: ( x. i in f .: (still_not-bound_in p) implies i < k + (QuantNbr q) )
A3: k <= k + (QuantNbr q) by NAT_1:11;
assume x. i in f .: (still_not-bound_in p) ; :: thesis: i < k + (QuantNbr q)
hence i < k + (QuantNbr q) by A2, A3, XXREAL_0:2; :: thesis: verum

end;

end;

A4: S₁[p, index p, {}. bound_QC-variables , id bound_QC-variables ]

proof

let i be Element of NAT ; :: thesis: ( x. i in (id bound_QC-variables ) .: (still_not-bound_in p) implies i < index p )
assume A5: x. i in (id bound_QC-variables ) .: (still_not-bound_in p) ; :: thesis: i < index p
(id bound_QC-variables ) .: (still_not-bound_in p) = still_not-bound_in p by FUNCT_1:162;
hence i < index p by A5, Th22; :: thesis: verum

end;

A6: now

let q be Element of CQC-WFF ; :: thesis: for x being Element of bound_QC-variables
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in SepQuadruples p & S₁[ All x,q,k,K,f] holds
S₁[q,k + 1,K \/ {.x.},f +* (x .--> (x. k))]
let x be Element of bound_QC-variables ; :: thesis: for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in SepQuadruples p & S₁[ All x,q,k,K,f] holds
S₁[q,k + 1,K \/ {.x.},f +* (x .--> (x. k))]
let k be Element of NAT ; :: thesis: for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in SepQuadruples p & S₁[ All x,q,k,K,f] holds
S₁[q,k + 1,K \/ {.x.},f +* (x .--> (x. k))]
let K be Finite_Subset of bound_QC-variables ; :: thesis: for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in SepQuadruples p & S₁[ All x,q,k,K,f] holds
S₁[q,k + 1,K \/ {.x.},f +* (x .--> (x. k))]
let f be Element of Funcs bound_QC-variables ,bound_QC-variables ; :: thesis: ( [(All x,q),k,K,f] in SepQuadruples p & S₁[ All x,q,k,K,f] implies S₁[q,k + 1,K \/ {.x.},f +* (x .--> (x. k))] )
assume [(All x,q),k,K,f] in SepQuadruples p ; :: thesis: ( S₁[ All x,q,k,K,f] implies S₁[q,k + 1,K \/ {.x.},f +* (x .--> (x. k))] )
assume A7: S₁[ All x,q,k,K,f] ; :: thesis: S₁[q,k + 1,K \/ {.x.},f +* (x .--> (x. k))]
thus S₁[q,k + 1,K \/ {.x.},f +* (x .--> (x. k))] :: thesis: verum

proof

let i be Element of NAT ; :: thesis: ( x. i in (f +* (x .--> (x. k))) .: (still_not-bound_in p) implies i < k + 1 )
assume A8: x. i in (f +* (x .--> (x. k))) .: (still_not-bound_in p) ; :: thesis: i < k + 1
(f +* (x .--> (x. k))) .: (still_not-bound_in p) c= (f .: (still_not-bound_in p)) \/ {(x. k)} by Th2;
then ( x. i in f .: (still_not-bound_in p) or x. i in {(x. k)} ) by A8, XBOOLE_0:def 3;
then ( i < k or x. i = x. k ) by A7, TARSKI:def 1;
then i <= k by ZFMISC_1:33;
hence i < k + 1 by NAT_1:13; :: thesis: verum

end;

end;

A9: for q being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [('not' q),k,K,f] in SepQuadruples p & S₁[ 'not' q,k,K,f] holds
S₁[q,k,K,f] ;
for q being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [q,k,K,f] in SepQuadruples p holds
S₁[q,k,K,f] from CQC_SIM1:sch 6(A4, A9, A1, A6);
hence ( [q,m,K,f] in SepQuadruples p & x. i in f .: (still_not-bound_in p) implies i < m ) ; :: thesis: verum