theorem Th40:
for
S1,
S2 being non
empty non
void ManySortedSign for
X being
non-empty ManySortedSet of the
carrier of
S2 for
f being
Function of the
carrier of
S1, the
carrier of
S2 for
g being
Function st
f,
g form_morphism_between S1,
S2 holds
for
o being
OperSymbol of
S1 for
p being
Element of
Args (
o,
(FreeMSA (X * f)))
for
q being
FinSequence st
q = (hom (f,g,X,S1,S2)) # p holds
((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q