let p be Element of CQC-WFF ; :: thesis:
defpred S₁[ Element of CQC-WFF ] means 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 [$1,k,K,f] in SepQuadruples p holds
f .: (still_not-bound_in $1) = still_not-bound_in ((SepFunc . $1) . [k,f]);
A1: [p,(index p),({}. bound_QC-variables),(id bound_QC-variables)] in SepQuadruples p by Th31;

A2: now

let r be Element of CQC-WFF ; :: thesis:
reconsider g = SepFunc . r as Function of [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF ;
assume A3: S₁[r] ; :: thesis:
A4: SepFunc . ('not' r) = NEGATIVE g by Def6;
thus S₁[ 'not' r] :: thesis:

let m be Element of NAT ; :: thesis:
let K be Finite_Subset of bound_QC-variables; :: thesis:
let f be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis:
assume [('not' r),m,K,f] in SepQuadruples p ; :: thesis:
then A5: [r,m,K,f] in SepQuadruples p by Th32;
set mf = [m,f];
reconsider r9 = g . [m,f] as Element of CQC-WFF ;
A6: still_not-bound_in r9 = still_not-bound_in ('not' r9) by QC_LANG3:7;
A7: still_not-bound_in r = still_not-bound_in ('not' r) by QC_LANG3:7;
(NEGATIVE g) . [m,f] = 'not' r9 by Def1;
hence f .: (still_not-bound_in ('not' r)) = still_not-bound_in ((SepFunc . ('not' r)) . [m,f]) by A4, A3, A7, A6, A5; :: thesis:

end;

end;

A8: now

let k be Element of NAT ; :: thesis:
let l be CQC-variable_list of k; :: thesis:
let P be QC-pred_symbol of k; :: thesis:
thus S₁[P ! l] :: thesis:

let m be Element of NAT ; :: thesis:
let K be Finite_Subset of bound_QC-variables; :: thesis:
let f be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis:
assume [(P ! l),m,K,f] in SepQuadruples p ; :: thesis:
set fl = f * l;
A9: f .: { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in bound_QC-variables ) } = { ((f * l) . j) where j is Element of NAT : ( 1 <= j & j <= len (f * l) & (f * l) . j in bound_QC-variables ) }

A10: len (f * l) = k by CARD_1:def 7
.= len l by CARD_1:def 7 ;
thus f .: { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in bound_QC-variables ) } c= { ((f * l) . j) where j is Element of NAT : ( 1 <= j & j <= len (f * l) & (f * l) . j in bound_QC-variables ) } :: according to XBOOLE_0:def 10 :: thesis:

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in f .: { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in bound_QC-variables ) } ; :: thesis:
then consider y being set such that
A11: ( y in dom f & y in { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in bound_QC-variables ) } & x = f . y ) by FUNCT_1:def 6;
consider i being Element of NAT such that
A12: y = l . i and
A13: 1 <= i and
A14: i <= len l and
l . i in bound_QC-variables by A11;
i in dom l by A13, A14, FINSEQ_3:25;
then A15: f . (l . i) = (f * l) . i by FUNCT_1:13;
(f * l) . i in bound_QC-variables by A10, A13, A14, Th13;
hence x in { ((f * l) . j) where j is Element of NAT : ( 1 <= j & j <= len (f * l) & (f * l) . j in bound_QC-variables ) } by A10, A11, A12, A13, A14, A15; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { ((f * l) . i) where i is Element of NAT : ( 1 <= i & i <= len (f * l) & (f * l) . i in bound_QC-variables ) } ; :: thesis:
then consider i being Element of NAT such that
A16: x = (f * l) . i and
A17: 1 <= i and
A18: i <= len (f * l) and
(f * l) . i in bound_QC-variables ;
i in dom l by A10, A17, A18, FINSEQ_3:25;
then A19: (f * l) . i = f . (l . i) by FUNCT_1:13;
A20: l . i in bound_QC-variables by A10, A17, A18, Th13;
then A21: l . i in dom f by FUNCT_2:def 1;
l . i in { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in bound_QC-variables ) } by A10, A17, A18, A20;
hence x in f .: { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in bound_QC-variables ) } by A16, A21, A19, FUNCT_1:def 6; :: thesis:

end;

A22: f .: (still_not-bound_in (P ! l)) = f .: (still_not-bound_in l) by QC_LANG3:5
.= f .: (variables_in (l,bound_QC-variables)) by QC_LANG3:2
.= variables_in ((f * l),bound_QC-variables) by A9
.= still_not-bound_in (f * l) by QC_LANG3:2
.= still_not-bound_in (P ! (f * l)) by QC_LANG3:5 ;
(ATOMIC (P,l)) . (m,f) = P ! (f * l) by Def4;
hence f .: (still_not-bound_in (P ! l)) = still_not-bound_in ((SepFunc . (P ! l)) . [m,f]) by A22, Def6; :: thesis:

end;

end;

A23: now

let r be Element of CQC-WFF ; :: thesis:
let x be Element of bound_QC-variables ; :: thesis:
assume A24: S₁[r] ; :: thesis:
thus S₁[ All (x,r)] :: thesis:

reconsider g = SepFunc . r as Function of [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF ;
let m be Element of NAT ; :: thesis:
let K be Finite_Subset of bound_QC-variables; :: thesis:
let f be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis:
assume A25: [(All (x,r)),m,K,f] in SepQuadruples p ; :: thesis:
A26: [r,(m + 1),(K \/ {.x.}),(f +* (x .--> (x. m)))] in SepQuadruples p by A25, Th34;
f +* (x .--> (x. m)) is Function of bound_QC-variables,bound_QC-variables by Lm1;
then reconsider fm = f +* (x .--> (x. m)) as Element of Funcs (bound_QC-variables,bound_QC-variables) by FUNCT_2:8;
reconsider r99 = g . ((m + 1),fm) as Element of CQC-WFF ;
A27: (UNIVERSAL (x,g)) . (m,f) = All ((x. m),r99) by Def3;
A28: still_not-bound_in (All (x,r)) = (still_not-bound_in r) \ {x} by QC_LANG3:12;
then A29: not x. m in f .: ((still_not-bound_in r) \ {x}) by A25, Th43;
thus f .: (still_not-bound_in (All (x,r))) = fm .: ((still_not-bound_in r) \ {x}) by A28, Th3
.= (fm .: (still_not-bound_in r)) \ {(x. m)} by A29, Th4
.= (still_not-bound_in r99) \ {(x. m)} by A24, A26
.= still_not-bound_in (All ((x. m),r99)) by QC_LANG3:12
.= still_not-bound_in ((SepFunc . (All (x,r))) . [m,f]) by A27, Def6 ; :: thesis:

end;

end;

A30: now

let r, s be Element of CQC-WFF ; :: thesis:
assume that
A31: S₁[r] and
A32: S₁[s] ; :: thesis:
thus S₁[r '&' s] :: thesis:

reconsider g = SepFunc . r, h = SepFunc . s as Function of [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF ;
let m be Element of NAT ; :: thesis:
let K be Finite_Subset of bound_QC-variables; :: thesis:
let f be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis:
assume A33: [(r '&' s),m,K,f] in SepQuadruples p ; :: thesis:
reconsider r9 = g . (m,f), s9 = h . ((m + (QuantNbr r)),f) as Element of CQC-WFF ;
A34: (CON (g,h,(QuantNbr r))) . (m,f) = r9 '&' s9 by Def2;
[r,m,K,f] in SepQuadruples p by A33, Th33;
then A35: f .: (still_not-bound_in r) = still_not-bound_in r9 by A31;
[s,(m + (QuantNbr r)),K,f] in SepQuadruples p by A33, Th33;
then A36: f .: (still_not-bound_in s) = still_not-bound_in s9 by A32;
thus f .: (still_not-bound_in (r '&' s)) = f .: ((still_not-bound_in r) \/ (still_not-bound_in s)) by QC_LANG3:10
.= (still_not-bound_in r9) \/ (still_not-bound_in s9) by A35, A36, RELAT_1:120
.= still_not-bound_in (r9 '&' s9) by QC_LANG3:10
.= still_not-bound_in ((SepFunc . (r '&' s)) . [m,f]) by A34, Def6 ; :: thesis:

end;

end;

A37: SepFunc . VERUM = [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):] --> VERUM by Def6;
A38: S₁[ VERUM ]

let k be Element of NAT ; :: thesis:
let K be Finite_Subset of bound_QC-variables; :: thesis:
let f be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis:
assume [VERUM,k,K,f] in SepQuadruples p ; :: thesis:
f .: (still_not-bound_in VERUM) = {} by QC_LANG3:3, RELAT_1:116;
hence f .: (still_not-bound_in VERUM) = still_not-bound_in ((SepFunc . VERUM) . [k,f]) by A37, FUNCOP_1:7, QC_LANG3:3; :: thesis:

end;

A39: for q being Element of CQC-WFF holds S₁[q] from CQC_SIM1:sch 5(A38, A8, A2, A30, A23);
thus still_not-bound_in p = (id bound_QC-variables) .: (still_not-bound_in p) by FUNCT_1:92
.= still_not-bound_in (SepVar p) by A39, A1 ; :: thesis: