:: deftheorem Def18 defines Sub_P SUBSTUT1:def 18 :
for A being QC-alphabet
for P being QC-pred_symbol of A
for l being FinSequence of QC-variables A
for e being Element of vSUB A st the_arity_of P = len l holds
Sub_P (P,l,e) = [(P ! l),e];