theorem Th86: :: MSAFREE5:126

for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being Endomorphism of Free (S,X) ex g being Endomorphism of T st
( (canonical_homomorphism T) ** h = g ** (canonical_homomorphism T) & ( for t being Element of T holds g . t = (canonical_homomorphism T) . (h . (@ t)) ) )