theorem Th35: :: AOFA_A00:40

for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for A being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself vf-free VarMSAlgebra over S
for s being SortSymbol of S
for t being Element of A,s holds vf t is ManySortedSubset of FreeGen X