for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for T being non-empty b₂,b₁ -terms free_in_itself MSAlgebra over S
for A being image of T
for G being GeneratorSet of T st G = FreeGen X holds
for f being ManySortedFunction of G, the Sorts of A ex h being ManySortedFunction of T,A st
( h is_homomorphism T,A & f = h || G )