:: deftheorem Def23 defines the_arguments_of QC_LANG1:def 23 :
for A being QC-alphabet
for F being Element of QC-WFF A st F is atomic holds
for b₃ being FinSequence of QC-variables A holds
( b₃ = the_arguments_of F iff ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st
( b₃ = ll & F = P ! ll ) );