let S1, S2 be non empty non void ManySortedSign ; :: thesis: 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 )
let X be non-empty ManySortedSet of the carrier of S2; :: thesis: 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 )
let f be Function of the carrier of S1, the carrier of S2; :: thesis: 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 )
let g be Function; :: thesis: ( f,g form_morphism_between S1,S2 implies 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 ) )
assume A1: f,g form_morphism_between S1,S2 ; :: thesis: 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 )
then reconsider h = g as Function of the carrier' of S1, the carrier' of S2 by Th9;
let t be Term of S1,(X * f); :: thesis: ( ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X iff t is CompoundTerm of S1,X * f )

hereby :: thesis: ( t is CompoundTerm of S1,X * f implies ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X )

assume ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X ; :: thesis: t is CompoundTerm of S1,X * f
then reconsider w = ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t as CompoundTerm of S2,X ;
assume t is not CompoundTerm of S1,X * f ; :: thesis: contradiction
then not t . {} in [: the carrier' of S1,{ the carrier of S1}:] by MSATERM:def 6;
then consider s being SortSymbol of S1, v being Element of (X * f) . s such that
A2: t . {} = [v,s] by MSATERM:2;
t = root-tree [v,s] by A2, MSATERM:5;
then ( ((hom (f,g,X,S1,S2)) . s) . t = root-tree [v,(f . s)] & the_sort_of t = s ) by A1, Def5, MSATERM:14;
then ( w . {} in [: the carrier' of S2,{ the carrier of S2}:] & w . {} = [v,(f . s)] ) by MSATERM:def 6, TREES_4:3;
then A3: f . s = the carrier of S2 by ZFMISC_1:106;
f . s in the carrier of S2 ;
hence contradiction by A3; :: thesis: verum

end;

assume t is CompoundTerm of S1,X * f ; :: thesis: ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X
then reconsider t = t as CompoundTerm of S1,X * f ;
t . {} in [: the carrier' of S1,{ the carrier of S1}:] by MSATERM:def 6;
then consider o, r being object such that
A4: o in the carrier' of S1 and
A5: r in { the carrier of S1} and
A6: t . {} = [o,r] by ZFMISC_1:def 2;
reconsider o = o as OperSymbol of S1 by A4;
r = the carrier of S1 by A5, TARSKI:def 1;
then consider a being ArgumentSeq of Sym (o,(X * f)) such that
A7: t = [o, the carrier of S1] -tree a by A6, MSATERM:10;
reconsider a = a as Element of Args (o,(FreeMSA (X * f))) by Th1;
reconsider b = (hom (f,g,X,S1,S2)) # a as Element of Args ((h . o),(FreeMSA X)) by A1, Th24;
A8: ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree a) = [(g . o), the carrier of S2] -tree b by A1, Th40;
t . {} = [o, the carrier of S1] by A7, TREES_4:def 4;
then A9: the_sort_of t = the_result_sort_of o by MSATERM:17;
reconsider b = b as ArgumentSeq of Sym ((h . o),X) by Th1;
(Sym ((h . o),X)) -tree b = [(h . o), the carrier of S2] -tree b by MSAFREE:def 9;
then reconsider T = [(h . o), the carrier of S2] -tree b as Term of S2,X ;
( T . {} = [(g . o), the carrier of S2] & [(h . o), the carrier of S2] in [: the carrier' of S2,{ the carrier of S2}:] ) by TREES_4:def 4, ZFMISC_1:106;
hence ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X by A7, A9, A8, MSATERM:def 6; :: thesis: verum