:: deftheorem defines NSub SUBSTUT1:def 11 :
for A being QC-alphabet
for p being QC-formula of A
for finSub being finite CQC_Substitution of A holds NSub (p,finSub) = NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub));