consider F being ManySortedSet of S -Terms X such that
A2: for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = H2(x,s) and
A3: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = H3(o,F * p) from MSAFREE4:sch 3();
 set Y = the carrier of S --> NAT;
defpred S1[ set ] means ex t being Term of S,( the carrier of S --> NAT) ex q being Term of S,X st
( t = F . $1 & q = $1 & the_sort_of t = the_sort_of q );
A4: now :: thesis: for s being SortSymbol of S
for x being Element of X . s holds S1[ root-tree [x,s]]
let s be SortSymbol of S; :: thesis: for x being Element of X . s holds S1[ root-tree [x,s]]
let x be Element of X . s; :: thesis: S1[ root-tree [x,s]]
A5: ( (w . s) . x in NAT & F . (root-tree [x,s]) = H2(x,s) ) by A2;
then reconsider t = F . (root-tree [x,s]) as Term of S,( the carrier of S --> NAT) by MSATERM:4;
reconsider q = root-tree [x,s] as Term of S,X by MSATERM:4;
thus S1[ root-tree [x,s]] :: thesis: verum
proof
take t ; :: thesis: ex q being Term of S,X st
( t = F . (root-tree [x,s]) & q = root-tree [x,s] & the_sort_of t = the_sort_of q )
take q ; :: thesis: ( t = F . (root-tree [x,s]) & q = root-tree [x,s] & the_sort_of t = the_sort_of q )
the_sort_of t = s by A5, MSATERM:14;
hence ( t = F . (root-tree [x,s]) & q = root-tree [x,s] & the_sort_of t = the_sort_of q ) by MSATERM:14; :: thesis: verum
end;
end;
A6: now :: thesis: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st ( for t being Term of S,X st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
let o be OperSymbol of S; :: thesis: for p being ArgumentSeq of Sym (o,X) st ( for t being Term of S,X st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
let p be ArgumentSeq of Sym (o,X); :: thesis: ( ( for t being Term of S,X st t in rng p holds
S1[t] ) implies S1[[o, the carrier of S] -tree p] )
assume A7: for t being Term of S,X st t in rng p holds
S1[t] ; :: thesis: S1[[o, the carrier of S] -tree p]
A8: ( dom (F * p) = dom p & dom p = dom (the_arity_of o) ) by MSATERM:22, PARTFUN1:def 2;
now :: thesis: for i being Nat st i in dom p holds
ex t being Term of S,( the carrier of S --> NAT) st
( t = (F * p) . i & the_sort_of t = (the_arity_of o) . i )
let i be Nat; :: thesis: ( i in dom p implies ex t being Term of S,( the carrier of S --> NAT) st
( t = (F * p) . i & the_sort_of t = (the_arity_of o) . i ) )
assume A9: i in dom p ; :: thesis: ex t being Term of S,( the carrier of S --> NAT) st
( t = (F * p) . i & the_sort_of t = (the_arity_of o) . i )
then reconsider q = p . i as Term of S,X by PARTFUN1:4;
A10: ( (F * p) . i = F . (p . i) & p . i in rng p & p . i in S -Terms X ) by A9, FUNCT_1:def 3, FUNCT_1:13, PARTFUN1:4;
then A11: S1[p . i] by A7;
then reconsider t = (F * p) . i as Term of S,( the carrier of S --> NAT) by A9, FUNCT_1:13;
reconsider q = p . i as Term of S,X by A9, PARTFUN1:4;
take t = t; :: thesis: ( t = (F * p) . i & the_sort_of t = (the_arity_of o) . i )
thus t = (F * p) . i ; :: thesis: the_sort_of t = (the_arity_of o) . i
thus the_sort_of t = (the_arity_of o) . i by A9, A10, A11, MSATERM:23; :: thesis: verum
end;
then reconsider Fp = F * p as ArgumentSeq of Sym (o,( the carrier of S --> NAT)) by A8, MSATERM:24;
reconsider q = (Sym (o,X)) -tree p as Term of S,X ;
reconsider t = (Sym (o,( the carrier of S --> NAT))) -tree Fp as Term of S,( the carrier of S --> NAT) ;
thus S1[[o, the carrier of S] -tree p] :: thesis: verum
proof
take t ; :: thesis: ex q being Term of S,X st
( t = F . ([o, the carrier of S] -tree p) & q = [o, the carrier of S] -tree p & the_sort_of t = the_sort_of q )
take q ; :: thesis: ( t = F . ([o, the carrier of S] -tree p) & q = [o, the carrier of S] -tree p & the_sort_of t = the_sort_of q )
thus ( t = F . ([o, the carrier of S] -tree p) & q = [o, the carrier of S] -tree p ) by A3; :: thesis: the_sort_of t = the_sort_of q
A12: q . {} = Sym (o,X) by TREES_4:def 4;
t . {} = Sym (o,( the carrier of S --> NAT)) by TREES_4:def 4;
hence the_sort_of t = the_result_sort_of o by MSATERM:17
.= the_sort_of q by A12, MSATERM:17 ;
:: thesis: verum
end;
end;
A13: for t being Term of S,X holds S1[t] from MSATERM:sch 1(A4, A6);
 t is Term of S,X by A1, Th42;
then consider tt being Term of S,( the carrier of S --> NAT), q being Term of S,X such that
A14: ( tt = F . t & q = t & the_sort_of tt = the_sort_of q ) by A13;
reconsider Ft = F . t as Element of (TermAlg S) by A14, MSATERM:13;
take Ft ; :: thesis: ex F being ManySortedSet of S -Terms X st
( Ft = F . t & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) )
take F ; :: thesis: ( Ft = F . t & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) )
thus ( Ft = F . t & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) ) by A2, A3; :: thesis: verum