theorem :: MSAFREE4:70

for S being non empty non void ManySortedSign
for X0, Y0 being non-empty countable ManySortedSet of S
for A being b₂,b₁ -terms all_vars_including inheriting_operations MSAlgebra over S
for h being ManySortedFunction of (Free (S,Y0)),A st h is_homomorphism Free (S,Y0),A holds
ex g being ManySortedFunction of (Free (S,Y0)),(Free (S,X0)) st
( g is_homomorphism Free (S,Y0), Free (S,X0) & h = (canonical_homomorphism A) ** g & ( for G being GeneratorSet of Free (S,Y0) st G = FreeGen Y0 holds
g || G = h || G ) )