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)) . (the_sort_of t)) . 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)) . (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 )

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

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 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)) . (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
t is CompoundTerm of S1,X * f
; :: thesis: ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,Xassume
((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;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

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