theorem Th45: :: MSAFREE4:45
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A2 being b2,b1 -terms all_vars_including inheriting_operations MSAlgebra over S holds FreeGen X is GeneratorSet of A2