let S be non empty non void ManySortedSign ; for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT ex h being ManySortedFunction of FreeGen X, the Sorts of (TermAlg S) st
for s being SortSymbol of S
for i being Element of X . s holds (h . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s]
let X be V5() ManySortedSet of S; for w being ManySortedFunction of X, the carrier of S --> NAT ex h being ManySortedFunction of FreeGen X, the Sorts of (TermAlg S) st
for s being SortSymbol of S
for i being Element of X . s holds (h . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s]
set Y = the carrier of S --> NAT;
let w be ManySortedFunction of X, the carrier of S --> NAT; ex h being ManySortedFunction of FreeGen X, the Sorts of (TermAlg S) st
for s being SortSymbol of S
for i being Element of X . s holds (h . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s]
deffunc H2( set , Function) -> set = root-tree [((w . $1) . (($2 . {}) `1)),$1];
consider ww being ManySortedFunction of the carrier of S such that
A1:
for x being set st x in the carrier of S holds
( dom (ww . x) = (FreeGen X) . x & ( for y being Element of (FreeGen X) . x holds (ww . x) . y = H2(x,y) ) )
from MSAFREE4:sch 1();
A2:
ww is ManySortedFunction of FreeGen X, FreeGen ( the carrier of S --> NAT)
proof
let x be
object ;
PBOOLE:def 15 ( not x in the carrier of S or ww . x is Element of bool [:((FreeGen X) . x),((FreeGen ( the carrier of S --> NAT)) . x):] )
assume
x in the
carrier of
S
;
ww . x is Element of bool [:((FreeGen X) . x),((FreeGen ( the carrier of S --> NAT)) . x):]
then reconsider s =
x as
SortSymbol of
S ;
A3:
dom (ww . s) = (FreeGen X) . s
by A1;
A4:
(
(FreeGen X) . s = FreeGen (
s,
X) &
(FreeGen ( the carrier of S --> NAT)) . s = FreeGen (
s,
( the carrier of S --> NAT)) )
by MSAFREE:def 16;
rng (ww . s) c= (FreeGen ( the carrier of S --> NAT)) . s
proof
let y be
object ;
TARSKI:def 3 ( not y in rng (ww . s) or y in (FreeGen ( the carrier of S --> NAT)) . s )
assume
y in rng (ww . s)
;
y in (FreeGen ( the carrier of S --> NAT)) . s
then consider z being
object such that A5:
(
z in dom (ww . s) &
y = (ww . s) . z )
by FUNCT_1:def 3;
reconsider z =
z as
Element of
(FreeGen X) . s by A1, A5;
consider v being
set such that A6:
(
v in X . s &
z = root-tree [v,s] )
by A4, MSAFREE:def 15;
A7:
y = H2(
s,
z)
by A1, A5;
z . {} = [v,s]
by A6, TREES_4:3;
then
(z . {}) `1 = v
;
then
(w . s) . ((z . {}) `1) in ( the carrier of S --> NAT) . s
by A6, FUNCT_2:5;
hence
y in (FreeGen ( the carrier of S --> NAT)) . s
by A4, A7, MSAFREE:def 15;
verum
end;
hence
ww . x is
Element of
bool [:((FreeGen X) . x),((FreeGen ( the carrier of S --> NAT)) . x):]
by A3, FUNCT_2:2;
verum
end;
set A = the X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;
reconsider G = FreeGen X as GeneratorSet of the X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S by Th45;
reconsider ww = ww as ManySortedFunction of FreeGen X, the Sorts of (TermAlg S) by A2, Th22;
take
ww
; for s being SortSymbol of S
for i being Element of X . s holds (ww . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s]
let s be SortSymbol of S; for i being Element of X . s holds (ww . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s]
let i be Element of X . s; (ww . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s]
( root-tree [i,s] in FreeGen (s,X) & FreeGen (s,X) = G . s )
by MSAFREE:def 15, MSAFREE:def 16;
then reconsider z = root-tree [i,s] as Element of (FreeGen X) . s ;
thus (ww . s) . (root-tree [i,s]) =
H2(s,z)
by A1
.=
root-tree [((w . s) . ([i,s] `1)),s]
by TREES_4:3
.=
root-tree [((w . s) . i),s]
; verum