let A be QC-alphabet ; :: thesis: for k being Nat
for l being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds SepQuadruples (P ! l) = {[(P ! l),(index (P ! l)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))]}
let k be Nat; :: thesis: for l being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds SepQuadruples (P ! l) = {[(P ! l),(index (P ! l)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))]}
let l be CQC-variable_list of k,A; :: thesis: for P being QC-pred_symbol of k,A holds SepQuadruples (P ! l) = {[(P ! l),(index (P ! l)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))]}
let P be QC-pred_symbol of k,A; :: thesis: SepQuadruples (P ! l) = {[(P ! l),(index (P ! l)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))]}
A1: P ! l is atomic by QC_LANG1:def 18;

now :: thesis: for x being object holds
( ( x in SepQuadruples (P ! l) implies x = [(P ! l),(index (P ! l)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] ) & ( x = [(P ! l),(index (P ! l)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] implies x in SepQuadruples (P ! l) ) )

let x be object ; :: thesis: ( ( x in SepQuadruples (P ! l) implies x = [(P ! l),(index (P ! l)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] ) & ( x = [(P ! l),(index (P ! l)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] implies x in SepQuadruples (P ! l) ) )
thus ( x in SepQuadruples (P ! l) implies x = [(P ! l),(index (P ! l)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] ) :: thesis: ( x = [(P ! l),(index (P ! l)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] implies x in SepQuadruples (P ! l) )

proof

assume A2: x in SepQuadruples (P ! l) ; :: thesis: x = [(P ! l),(index (P ! l)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))]
then consider q being Element of CQC-WFF A, t being QC-symbol of A, K being Element of Fin (bound_QC-variables A), f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) such that
A3: x = [q,t,K,f] by DOMAIN_1:10;

A4: now :: thesis: for x being Element of bound_QC-variables A
for u being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds
( not u ++ = t or not h +* ({x} --> (x. u)) = f or ( not [(All (x,q)),u,K,h] in SepQuadruples (P ! l) & not [(All (x,q)),u,(K \ {.x.}),h] in SepQuadruples (P ! l) ) )

given x being Element of bound_QC-variables A, u being QC-symbol of A, h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) such that u ++ = t and
h +* ({x} --> (x. u)) = f and
A5: ( [(All (x,q)),u,K,h] in SepQuadruples (P ! l) or [(All (x,q)),u,(K \ {.x.}),h] in SepQuadruples (P ! l) ) ; :: thesis: contradiction
All (x,q) is_subformula_of P ! l by A5, Th35;
then All (x,q) = P ! l by QC_LANG2:80;
then P ! l is universal by QC_LANG1:def 21;
hence contradiction by A1, QC_LANG1:20; :: thesis: verum

end;

A6: now :: thesis: for r being Element of CQC-WFF A
for u being QC-symbol of A holds
( not t = u + (QuantNbr r) or not [(r '&' q),u,K,f] in SepQuadruples (P ! l) )

given r being Element of CQC-WFF A, u being QC-symbol of A such that t = u + (QuantNbr r) and
A7: [(r '&' q),u,K,f] in SepQuadruples (P ! l) ; :: thesis: contradiction
r '&' q is_subformula_of P ! l by A7, Th35;
then r '&' q = P ! l by QC_LANG2:80;
then P ! l is conjunctive by QC_LANG1:def 20;
hence contradiction by A1, QC_LANG1:20; :: thesis: verum

end;

A8: now :: thesis: for r being Element of CQC-WFF A holds not [(q '&' r),t,K,f] in SepQuadruples (P ! l)

given r being Element of CQC-WFF A such that A9: [(q '&' r),t,K,f] in SepQuadruples (P ! l) ; :: thesis: contradiction
q '&' r is_subformula_of P ! l by A9, Th35;
then q '&' r = P ! l by QC_LANG2:80;
then P ! l is conjunctive by QC_LANG1:def 20;
hence contradiction by A1, QC_LANG1:20; :: thesis: verum

end;

A10: now :: thesis: not [('not' q),t,K,f] in SepQuadruples (P ! l)

assume [('not' q),t,K,f] in SepQuadruples (P ! l) ; :: thesis: contradiction
then 'not' q is_subformula_of P ! l by Th35;
then 'not' q = P ! l by QC_LANG2:80;
then P ! l is negative by QC_LANG1:def 19;
hence contradiction by A1, QC_LANG1:20; :: thesis: verum

end;

set p = P ! l;
( [q,t,K,f] = [(P ! l),(index (P ! l)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples (P ! l) or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples (P ! l) or ex r being Element of CQC-WFF A ex u being QC-symbol of A st
( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples (P ! l) ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st
( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples (P ! l) or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples (P ! l) ) ) ) by A2, Th34, A3;
hence x = [(P ! l),(index (P ! l)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] by A3, A8, A6, A4, A10; :: thesis: verum

end;

thus ( x = [(P ! l),(index (P ! l)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] implies x in SepQuadruples (P ! l) ) by Th30; :: thesis: verum

end;

hence SepQuadruples (P ! l) = {[(P ! l),(index (P ! l)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))]} by TARSKI:def 1; :: thesis: verum