theorem :: MSAFREE5:93

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for Z being non-trivial ManySortedSet of the carrier of S
for z being Element of Z . s
for R being b₃,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for C9 being context of z
for t being Element of (Free (S,Z)) st the_sort_of t = s holds
(canonical_homomorphism R) . (C9 -sub t) = (canonical_homomorphism R) . (C9 -sub (@ ((canonical_homomorphism R) . t)))