let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X)
for q being FinSequence st dom q = dom p & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom p & t = p . i holds
q . i = # (t,w) ) holds
# (((Sym (o,X)) -tree p),w) = (Sym (o,( the carrier of S --> NAT))) -tree q
let X be non-empty ManySortedSet of S; :: thesis: for w being ManySortedFunction of X, the carrier of S --> NAT
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X)
for q being FinSequence st dom q = dom p & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom p & t = p . i holds
q . i = # (t,w) ) holds
# (((Sym (o,X)) -tree p),w) = (Sym (o,( the carrier of S --> NAT))) -tree q
let w be ManySortedFunction of X, the carrier of S --> NAT; :: thesis: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X)
for q being FinSequence st dom q = dom p & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom p & t = p . i holds
q . i = # (t,w) ) holds
# (((Sym (o,X)) -tree p),w) = (Sym (o,( the carrier of S --> NAT))) -tree q
let o be OperSymbol of S; :: thesis: for p being ArgumentSeq of Sym (o,X)
for q being FinSequence st dom q = dom p & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom p & t = p . i holds
q . i = # (t,w) ) holds
# (((Sym (o,X)) -tree p),w) = (Sym (o,( the carrier of S --> NAT))) -tree q
let p be ArgumentSeq of Sym (o,X); :: thesis: for q being FinSequence st dom q = dom p & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom p & t = p . i holds
q . i = # (t,w) ) holds
# (((Sym (o,X)) -tree p),w) = (Sym (o,( the carrier of S --> NAT))) -tree q
let q be FinSequence; :: thesis: ( dom q = dom p & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom p & t = p . i holds
q . i = # (t,w) ) implies # (((Sym (o,X)) -tree p),w) = (Sym (o,( the carrier of S --> NAT))) -tree q )
assume that
A1: dom q = dom p and
A2: for i being Nat
for t being Element of (Free (S,X)) st i in dom p & t = p . i holds
q . i = # (t,w) ; :: thesis: # (((Sym (o,X)) -tree p),w) = (Sym (o,( the carrier of S --> NAT))) -tree q
reconsider t = (Sym (o,X)) -tree p as Term of S,X ;
deffunc H₂( set , set ) -> set = root-tree [((w . $2) . $1),$2];
deffunc H₃( OperSymbol of S, FinSequence) -> set = (Sym ($1,( the carrier of S --> NAT))) -tree $2;
A3: S -Terms X = Union the Sorts of (FreeMSA X) by MSATERM:13;
then t is Element of (Free (S,X)) by MSAFREE3:31;
then consider G being ManySortedSet of S -Terms X such that
A4: # (t,w) = G . t and
A5: for s being SortSymbol of S
for x being Element of X . s holds G . (root-tree [x,s]) = H₂(x,s) and
A6: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds G . ((Sym (o,X)) -tree p) = H₃(o,G * p) by Def15;
rng p c= dom G

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in dom G )
assume y in rng p ; :: thesis: y in dom G
then consider x being object such that
A7: ( x in dom p & y = p . x ) by FUNCT_1:def 3;
reconsider x = x as Nat by A7;
y is Term of S,X by A7, MSATERM:22;
then y in S -Terms X ;
hence y in dom G by PARTFUN1:def 2; :: thesis: verum

end;

then A8: dom (G * p) = dom p by RELAT_1:27;

now :: thesis: for x being object st x in dom p holds
q . x = (G * p) . x

let x be object ; :: thesis: ( x in dom p implies q . x = (G * p) . x )
assume A9: x in dom p ; :: thesis: q . x = (G * p) . x
then reconsider i = x as Nat ;
reconsider t = p . i as Term of S,X by A9, MSATERM:22;
reconsider t = t as Element of (Free (S,X)) by A3, MSAFREE3:31;
thus q . x = # (t,w) by A2, A9
.= G . t by A5, A6, Th55
.= (G * p) . x by A9, FUNCT_1:13 ; :: thesis: verum

end;

then q = G * p by A1, A8;
hence # (((Sym (o,X)) -tree p),w) = (Sym (o,( the carrier of S --> NAT))) -tree q by A4, A6; :: thesis: verum