theorem
for
S being non
empty non
void ManySortedSign for
X being
non-empty 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
o being
OperSymbol of
S for
p being
ArgumentSeq of
Sym (
o,
X) holds
(
F * p in Args (
o,
(Free (S,(rngs w)))) &
F * p in Args (
o,
(Free (S,( the carrier of S --> NAT)))) )