:: deftheorem Def18 defines args ABCMIZ_A:def 18 :
for l being FinSequence of Vars
for b₂ being FinSequence of QuasiTerms MaxConstrSign holds
( b₂ = args l iff ( len b₂ = len l & ( for i being Nat st i in dom l holds
b₂ . i = (l /. i) -term MaxConstrSign ) ) );