for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being Element of bound_QC-variables A
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 [(All (x,q)),t,K,f] in SepQuadruples p holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in SepQuadruples p