:: deftheorem Def16 defines -Sub-closed SUBSTUT1:def 16 :
for A being QC-alphabet
for IT being set holds
( IT is A -Sub-closed iff ( IT is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds [(<*p*> ^ ll),e] in IT ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in IT ) & ( for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in IT holds
[(<*[1,0]*> ^ p),e] in IT ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,e] in IT & [q,e] in IT holds
[((<*[2,0]*> ^ p) ^ q),e] in IT ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):]
for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in IT holds
[((<*[3,0]*> ^ <*x*>) ^ p),e] in IT ) ) );