theorem Th41:
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
t being
Term of
S1,
(X * f) holds
(
((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is
CompoundTerm of
S2,
X iff
t is
CompoundTerm of
S1,
X * f )