theorem :: AOFA_A01:9

for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations MSAlgebra over S
for G being basic GeneratorSet of T
for s being SortSymbol of S
for a being set holds
( a is pure Element of G . s iff a in (FreeGen T) . s )