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 s being SortSymbol of S
for x being Element of X . s holds # ((root-tree [x,s]),w) = root-tree [((w . s) . x),s]
let X be non-empty ManySortedSet of S; :: thesis: for w being ManySortedFunction of X, the carrier of S --> NAT
for s being SortSymbol of S
for x being Element of X . s holds # ((root-tree [x,s]),w) = root-tree [((w . s) . x),s]
let w be ManySortedFunction of X, the carrier of S --> NAT; :: thesis: for s being SortSymbol of S
for x being Element of X . s holds # ((root-tree [x,s]),w) = root-tree [((w . s) . x),s]
let s be SortSymbol of S; :: thesis: for x being Element of X . s holds # ((root-tree [x,s]),w) = root-tree [((w . s) . x),s]
let x be Element of X . s; :: thesis: # ((root-tree [x,s]),w) = root-tree [((w . s) . x),s]
reconsider t = root-tree [x,s] as Term of S,X by MSATERM:4;
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;
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
A1: # (t,w) = G . t and
A2: for s being SortSymbol of S
for x being Element of X . s holds G . (root-tree [x,s]) = H₂(x,s) and
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;
thus # ((root-tree [x,s]),w) = root-tree [((w . s) . x),s] by A1, A2; :: thesis: verum