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 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)))) )
let X be non-empty 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 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)))) )
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 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)))) )
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 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)))) ) )
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 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)))) )
let o be OperSymbol of S; :: thesis: 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)))) )
let p be ArgumentSeq of Sym (o,X); :: thesis: ( F * p in Args (o,(Free (S,(rngs w)))) & F * p in Args (o,(Free (S,( the carrier of S --> NAT)))) )
rng p c= dom F

proof

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

end;

then A4: dom (F * p) = dom p by RELAT_1:27;
A5: dom p = dom (the_arity_of o) by MSATERM:22;
A6: S -Terms X = Union the Sorts of (FreeMSA X) by MSATERM:13
.= Union the Sorts of (Free (S,X)) by MSAFREE3:31 ;
X is_transformable_to the carrier of S --> NAT by Th21;
then rngs w is ManySortedSubset of the carrier of S --> NAT by PBOOLE:def 18, MSSUBFAM:17;
then A7: Free (S,(rngs w)) is MSSubAlgebra of Free (S,( the carrier of S --> NAT)) by Th59;

now :: thesis: for i being Nat st i in dom p holds
ex tt being Term of S,(rngs w) st
( tt = (F * p) . i & the_sort_of tt = (the_arity_of o) . i )

let i be Nat; :: thesis: ( i in dom p implies ex tt being Term of S,(rngs w) st
( tt = (F * p) . i & the_sort_of tt = (the_arity_of o) . i ) )
assume A8: i in dom p ; :: thesis: ex tt being Term of S,(rngs w) st
( tt = (F * p) . i & the_sort_of tt = (the_arity_of o) . i )
then reconsider t = p . i as Term of S,X by MSATERM:22;
F . t = # (t,w) by A1, A2, A6, Th55;
then reconsider tt = F . t as Element of the Sorts of (Free (S,(rngs w))) . (the_sort_of t) by Th60;
A9: the Sorts of (Free (S,(rngs w))) is MSSubset of (Free (S,( the carrier of S --> NAT))) by A7, MSUALG_2:def 9;
reconsider tt = tt as Term of S,(rngs w) by Th42;
take tt = tt; :: thesis: ( tt = (F * p) . i & the_sort_of tt = (the_arity_of o) . i )
thus tt = (F * p) . i by A8, FUNCT_1:13; :: thesis: the_sort_of tt = (the_arity_of o) . i
( the Sorts of (Free (S,(rngs w))) . (the_sort_of t) c= the Sorts of (Free (S,( the carrier of S --> NAT))) . (the_sort_of t) & tt in the Sorts of (Free (S,(rngs w))) . (the_sort_of t) ) by A9, PBOOLE:def 2, PBOOLE:def 18;
then tt in the Sorts of (FreeMSA (rngs w)) . (the_sort_of t) by MSAFREE3:31;
then tt in FreeSort ((rngs w),(the_sort_of t)) by MSAFREE:def 11;
hence the_sort_of tt = the_sort_of t by MSATERM:def 5
.= (the_arity_of o) . i by A8, MSATERM:23 ;
:: thesis: verum

end;

then F * p is ArgumentSeq of Sym (o,(rngs w)) by A4, A5, MSATERM:24;
then F * p is Element of Args (o,(FreeMSA (rngs w))) by INSTALG1:1;
then F * p is Element of Args (o,(Free (S,(rngs w)))) by MSAFREE3:31;
then ( F * p in Args (o,(Free (S,(rngs w)))) & Args (o,(Free (S,(rngs w)))) c= Args (o,(Free (S,( the carrier of S --> NAT)))) ) by A7, MSAFREE3:37;
hence ( F * p in Args (o,(Free (S,(rngs w)))) & F * p in Args (o,(Free (S,( the carrier of S --> NAT)))) ) ; :: thesis: verum