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:11;
A7: still_not-bound_in r = still_not-bound_in ('not' r) by QC_LANG3:11;
(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 FINSEQ_1:def 18
.= len l by FINSEQ_1:def 18 ;
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 12;
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:27;
then A15: f . (l . i) = (f * l) . i by FUNCT_1:23;
(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:27;
then A19: (f * l) . i = f . (l . i) by FUNCT_1:23;
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 12; :: thesis:

end;

A22: f .: (still_not-bound_in (P ! l)) = f .: (still_not-bound_in l) by QC_LANG3:9
.= f .: (variables_in l,bound_QC-variables ) by QC_LANG3:6
.= variables_in (f * l),bound_QC-variables by A9
.= still_not-bound_in (f * l) by QC_LANG3:6
.= still_not-bound_in (P ! (f * l)) by QC_LANG3:9 ;
(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:11;
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:16;
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:16
.= 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:14
.= (still_not-bound_in r9) \/ (still_not-bound_in s9) by A35, A36, RELAT_1:153
.= still_not-bound_in (r9 '&' s9) by QC_LANG3:14
.= 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:7, RELAT_1:149;
hence f .: (still_not-bound_in VERUM ) = still_not-bound_in ((SepFunc . VERUM ) . [k,f]) by A37, FUNCOP_1:13, QC_LANG3:7; :: 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:162
.= still_not-bound_in (SepVar p) by A39, A1 ; :: thesis: