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