theorem Th92: :: MSAFREE5:69

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for T being b₃,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T st x nin vf r holds
r is x -omitting