:: deftheorem defines \2 AOFA_A01:def 10 :
for S being non empty non void bool-correct 4,1 integer BoolSignature
for X being V3() ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for I being integer SortSymbol of S holds \2 (T,I) = (\1 (T,I)) + (\1 (T,I));