let p be Element of CQC-WFF ; :: thesis:
A1: SepFunc . VERUM = [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):] --> VERUM by Def6;
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]);
A2: S₁[ VERUM ]

proof

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 A1, FUNCOP_1:13, QC_LANG3:7; :: thesis:

end;

A3: now

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

proof

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;
A4: (ATOMIC P,l) . m,f = P ! (f * l) by Def4;
A5: 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 ) }

proof

A6: 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:

proof

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
A7: ( 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
A8: ( y = l . i & 1 <= i & i <= len l & l . i in bound_QC-variables ) by A7;
i in dom l by A8, FINSEQ_3:27;
then A9: f . (l . i) = (f * l) . i by FUNCT_1:23;
(f * l) . i in bound_QC-variables by A6, A8, 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 A6, A7, A8, A9; :: 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
A10: ( x = (f * l) . i & 1 <= i & i <= len (f * l) & (f * l) . i in bound_QC-variables ) ;
A11: l . i in bound_QC-variables by A6, A10, Th13;
then A12: l . i in dom f by FUNCT_2:def 1;
i in dom l by A6, A10, FINSEQ_3:27;
then A13: (f * l) . i = f . (l . i) by FUNCT_1:23;
l . i in { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in bound_QC-variables ) } by A6, A10, A11;
hence x in f .: { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in bound_QC-variables ) } by A10, A12, A13, FUNCT_1:def 12; :: thesis:

end;

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 A5
.= still_not-bound_in (f * l) by QC_LANG3:6
.= still_not-bound_in (P ! (f * l)) by QC_LANG3:9 ;
hence f .: (still_not-bound_in (P ! l)) = still_not-bound_in ((SepFunc . (P ! l)) . [m,f]) by A4, Def6; :: thesis:

end;

A14: 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 ;
A15: SepFunc . ('not' r) = NEGATIVE g by Def6;
assume A16: S₁[r] ; :: thesis:
thus S₁[ 'not' r] :: thesis:

proof

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 A17: [('not' r),m,K,f] in SepQuadruples p ; :: thesis:
set mf = [m,f];
reconsider r' = g . [m,f] as Element of CQC-WFF ;
A18: ( still_not-bound_in r = still_not-bound_in ('not' r) & still_not-bound_in r' = still_not-bound_in ('not' r') ) by QC_LANG3:11;
( (NEGATIVE g) . [m,f] = 'not' r' & [r,m,K,f] in SepQuadruples p ) by A17, Def1, Th32;
hence f .: (still_not-bound_in ('not' r)) = still_not-bound_in ((SepFunc . ('not' r)) . [m,f]) by A15, A16, A18; :: thesis:

end;

A19: now

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

proof

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 A22: [(r '&' s),m,K,f] in SepQuadruples p ; :: thesis:
reconsider r' = g . m,f, s' = h . (m + (QuantNbr r)),f as Element of CQC-WFF ;
A23: (CON g,h,(QuantNbr r)) . m,f = r' '&' s' by Def2;
( [r,m,K,f] in SepQuadruples p & [s,(m + (QuantNbr r)),K,f] in SepQuadruples p ) by A22, Th33;
then A24: ( f .: (still_not-bound_in r) = still_not-bound_in r' & f .: (still_not-bound_in s) = still_not-bound_in s' ) by A20, A21;
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 r') \/ (still_not-bound_in s') by A24, RELAT_1:153
.= still_not-bound_in (r' '&' s') by QC_LANG3:14
.= still_not-bound_in ((SepFunc . (r '&' s)) . [m,f]) by A23, Def6 ; :: thesis:

end;

A25: now

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

proof

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 A27: [(All x,r),m,K,f] in SepQuadruples p ; :: thesis:
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 r'' = g . (m + 1),fm as Element of CQC-WFF ;
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 A27, Th43;
A30: (UNIVERSAL x,g) . m,f = All (x. m),r'' by Def3;
A31: [r,(m + 1),(K \/ {.x.}),(f +* (x .--> (x. m)))] in SepQuadruples p by A27, Th34;
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 r'') \ {(x. m)} by A26, A31
.= still_not-bound_in (All (x. m),r'') by QC_LANG3:16
.= still_not-bound_in ((SepFunc . (All x,r)) . [m,f]) by A30, Def6 ; :: thesis:

end;

A32: for q being Element of CQC-WFF holds S₁[q] from CQC_SIM1:sch 5(A2, A3, A14, A19, A25);
A33: [p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] in SepQuadruples p by Th31;
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 A32, A33 ; :: thesis: