let S1, S2 be non empty non void ManySortedSign ; 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; 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; 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; ( 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
; 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); ( ((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 ( 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
;
t is CompoundTerm of S1,X * fthen 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
;
contradictionthen
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;
verum
end;
assume
t is CompoundTerm of S1,X * f
; ((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; verum