let A be QC-alphabet ; :: thesis:
let p be Element of CQC-WFF A; :: thesis:
defpred S₁[ Element of CQC-WFF A] means for t being QC-symbol of A
for K being Element of Fin (bound_QC-variables A)
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [$1,t,K,f] in SepQuadruples p holds
f .: (still_not-bound_in $1) = still_not-bound_in (((SepFunc A) . $1) . [t,f]);
A1: [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] in SepQuadruples p by Th30;

A2: now :: thesis:

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

proof

let u be QC-symbol of A; :: thesis:
let K be Element of Fin (bound_QC-variables A); :: thesis:
let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis:
assume [('not' r),u,K,f] in SepQuadruples p ; :: thesis:
then A5: [r,u,K,f] in SepQuadruples p by Th31;
set uf = [u,f];
reconsider r9 = g . [u,f] as Element of CQC-WFF A ;
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) . [u,f] = 'not' r9 by Def2;
hence f .: (still_not-bound_in ('not' r)) = still_not-bound_in (((SepFunc A) . ('not' r)) . [u,f]) by A4, A3, A7, A6, A5; :: thesis:

end;

A8: now :: thesis:

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

proof

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

proof

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in f .: { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables A ) } ; :: thesis:
then consider y being object such that
A11: ( y in dom f & y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables A ) } & x = f . y ) by FUNCT_1:def 6;
consider i being Nat such that
A12: y = l . i and
A13: 1 <= i and
A14: i <= len l and
l . i in bound_QC-variables A 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 A by A10, A13, A14, Th13;
hence x in { ((f * l) . j) where j is Nat : ( 1 <= j & j <= len (f * l) & (f * l) . j in bound_QC-variables A ) } by A10, A11, A12, A13, A14, A15; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { ((f * l) . i) where i is Nat : ( 1 <= i & i <= len (f * l) & (f * l) . i in bound_QC-variables A ) } ; :: thesis:
then consider i being 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 A ;
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 A 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 Nat : ( 1 <= j & j <= len l & l . j in bound_QC-variables A ) } by A10, A17, A18, A20;
hence x in f .: { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in bound_QC-variables A ) } 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 A))) by QC_LANG3:2
.= variables_in ((f * l),(bound_QC-variables A)) 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)) . (u,f) = P ! (f * l) by Def5;
hence f .: (still_not-bound_in (P ! l)) = still_not-bound_in (((SepFunc A) . (P ! l)) . [u,f]) by A22, Def7; :: thesis:

end;

A23: now :: thesis:

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

proof

reconsider g = (SepFunc A) . r as Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A) ;
let u be QC-symbol of A; :: thesis:
let K be Element of Fin (bound_QC-variables A); :: thesis:
let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis:
assume A25: [(All (x,r)),u,K,f] in SepQuadruples p ; :: thesis:
A26: [r,(u ++),(K \/ {.x.}),(f +* (x .--> (x. u)))] in SepQuadruples p by A25, Th33;
f +* (x .--> (x. u)) is Function of (bound_QC-variables A),(bound_QC-variables A) by Lm1;
then reconsider fu = f +* (x .--> (x. u)) as Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) by FUNCT_2:8;
reconsider r99 = g . ((u ++),fu) as Element of CQC-WFF A ;
A27: (UNIVERSAL (x,g)) . (u,f) = All ((x. u),r99) by Def4;
A28: still_not-bound_in (All (x,r)) = (still_not-bound_in r) \ {x} by QC_LANG3:12;
then A29: not x. u in f .: ((still_not-bound_in r) \ {x}) by A25, Th43;
thus f .: (still_not-bound_in (All (x,r))) = fu .: ((still_not-bound_in r) \ {x}) by A28, Th3
.= (fu .: (still_not-bound_in r)) \ {(x. u)} by A29, Th4
.= (still_not-bound_in r99) \ {(x. u)} by A24, A26
.= still_not-bound_in (All ((x. u),r99)) by QC_LANG3:12
.= still_not-bound_in (((SepFunc A) . (All (x,r))) . [u,f]) by A27, Def7 ; :: thesis:

end;

A30: now :: thesis:

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

proof

reconsider g = (SepFunc A) . r, h = (SepFunc A) . s as Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A) ;
let u be QC-symbol of A; :: thesis:
let K be Element of Fin (bound_QC-variables A); :: thesis:
let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis:
assume A33: [(r '&' s),u,K,f] in SepQuadruples p ; :: thesis:
reconsider r9 = g . (u,f), s9 = h . ((u + (QuantNbr r)),f) as Element of CQC-WFF A ;
A34: (CON (g,h,(QuantNbr r))) . (u,f) = r9 '&' s9 by Def3;
[r,u,K,f] in SepQuadruples p by A33, Th32;
then A35: f .: (still_not-bound_in r) = still_not-bound_in r9 by A31;
[s,(u + (QuantNbr r)),K,f] in SepQuadruples p by A33, Th32;
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 A) . (r '&' s)) . [u,f]) by A34, Def7 ; :: thesis:

end;

A37: (SepFunc A) . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) by Def7;
A38: S₁[ VERUM A]

proof

let v be QC-symbol of A; :: thesis:
let K be Element of Fin (bound_QC-variables A); :: thesis:
let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis:
assume [(VERUM A),v,K,f] in SepQuadruples p ; :: thesis:
A39: still_not-bound_in (VERUM A) = {} by QC_LANG3:3;
thus f .: (still_not-bound_in (VERUM A)) = still_not-bound_in (((SepFunc A) . (VERUM A)) . [v,f]) by A39, A37; :: thesis:

end;

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