:: deftheorem defines vSUB SUBSTUT1:def 1 :
for A being QC-alphabet holds vSUB A = PFuncs ((bound_QC-variables A),(bound_QC-variables A));