:: deftheorem Def29 defines Sub_the_arguments_of SUBSTUT1:def 29 :
for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_atomic holds
for b₃ being FinSequence of QC-variables A holds
( b₃ = Sub_the_arguments_of S iff ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st
( b₃ = ll & S = Sub_P (P,ll,e) ) );