let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for F being ManySortedSet of S -Terms X st ( 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) ) holds
for t being Element of (Free (S,X)) holds F . t = # (t,w)
let X be V5() ManySortedSet of S; :: thesis: for w being ManySortedFunction of X, the carrier of S --> NAT
for F being ManySortedSet of S -Terms X st ( 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) ) holds
for t being Element of (Free (S,X)) holds F . t = # (t,w)
let w be ManySortedFunction of X, the carrier of S --> NAT; :: thesis: for F being ManySortedSet of S -Terms X st ( 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) ) holds
for t being Element of (Free (S,X)) holds F . t = # (t,w)
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;
let F be ManySortedSet of S -Terms X; :: thesis: ( ( 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) ) implies for t being Element of (Free (S,X)) holds F . t = # (t,w) )
assume that
A1: for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = H₂(x,s) and
A2: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = H₃(o,F * p) ; :: thesis: for t being Element of (Free (S,X)) holds F . t = # (t,w)
let t be Element of (Free (S,X)); :: thesis: F . t = # (t,w)
consider G being ManySortedSet of S -Terms X such that
A3: # (t,w) = G . t and
A4: for s being SortSymbol of S
for x being Element of X . s holds G . (root-tree [x,s]) = H₂(x,s) and
A5: 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;
F = G from MSAFREE4:sch 4(A1, A2, A4, A5);
hence F . t = # (t,w) by A3; :: thesis: verum