:: deftheorem defines SepFunc CQC_SIM1:def 8 :
for A being QC-alphabet
for p being Element of CQC-WFF A
for t being QC-symbol of A
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds SepFunc (p,t,f) = ((SepFunc A) . p) . [t,f];