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

now

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

proof

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

A4: now

given x being Element of bound_QC-variables , i being Element of NAT , h being Element of Funcs (bound_QC-variables,bound_QC-variables) such that i + 1 = k and
h +* ({x} --> (x. i)) = f and
A5: ( [(All (x,q)),i,K,h] in SepQuadruples (P ! l) or [(All (x,q)),i,(K \ {.x.}),h] in SepQuadruples (P ! l) ) ; :: thesis: contradiction
All (x,q) is_subformula_of P ! l by A5, Th36;
then All (x,q) = P ! l by QC_LANG2:80;
then P ! l is universal by QC_LANG1:def 19;
hence contradiction by A1, QC_LANG1:18; :: thesis: verum

end;

A6: now

given r being Element of CQC-WFF , i being Element of NAT such that k = i + (QuantNbr r) and
A7: [(r '&' q),i,K,f] in SepQuadruples (P ! l) ; :: thesis: contradiction
r '&' q is_subformula_of P ! l by A7, Th36;
then r '&' q = P ! l by QC_LANG2:80;
then P ! l is conjunctive by QC_LANG1:def 18;
hence contradiction by A1, QC_LANG1:18; :: thesis: verum

end;

A8: now

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

end;

now

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

end;

hence x = [(P ! l),(index (P ! l)),({}. bound_QC-variables),(id bound_QC-variables)] by A2, A3, A8, A6, A4, Th35; :: thesis: verum

end;

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

end;

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