:: deftheorem Def4 defines pure AOFA_A01:def 4 :
for S being non empty non void ManySortedSign
for X being V3() ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations MSAlgebra over S
for G being GeneratorSet of T
for s being SortSymbol of S
for x being Element of G . s holds
( x is pure iff x in (FreeGen T) . s );