let S1, S2 be non empty non void ManySortedSign ; :: thesis: for X being V2() 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)) . ()) . t is CompoundTerm of S2,X iff t is CompoundTerm of S1,X * f )

let X be V2() 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)) . ()) . 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)) . ()) . 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)) . ()) . 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)) . ()) . 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)) . ()) . 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)) . ()) . t is CompoundTerm of S2,X )
assume ((hom (f,g,X,S1,S2)) . ()) . t is CompoundTerm of S2,X ; :: thesis: t is CompoundTerm of S1,X * f
then reconsider w = ((hom (f,g,X,S1,S2)) . ()) . 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 ;
then ( ((hom (f,g,X,S1,S2)) . s) . t = root-tree [v,(f . s)] & the_sort_of t = s ) by ;
then ( w . {} in [: the carrier' of S2,{ the carrier of S2}:] & w . {} = [v,(f . s)] ) by ;
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)) . ()) . 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 ;
then consider a being ArgumentSeq of Sym (o,(X * f)) such that
A7: t = [o, the carrier of S1] -tree a by ;
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),()) by ;
A8: ((hom (f,g,X,S1,S2)) . ) . ([o, the carrier of S1] -tree a) = [(g . o), the carrier of S2] -tree b by ;
t . {} = [o, the carrier of S1] by ;
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 ;
hence ((hom (f,g,X,S1,S2)) . ()) . t is CompoundTerm of S2,X by ; :: thesis: verum