let S be non empty non void ManySortedSign ; for X being V5() ManySortedSet of the carrier of S holds FreeGen X is free
let X be V5() ManySortedSet of the carrier of S; FreeGen X is free
set D = DTConMSA X;
set FA = FreeMSA X;
set FG = FreeGen X;
let U1 be non-empty MSAlgebra over S; MSAFREE:def 5 for f being ManySortedFunction of FreeGen X, the Sorts of U1 ex h being ManySortedFunction of (FreeMSA X),U1 st
( h is_homomorphism FreeMSA X,U1 & h || (FreeGen X) = f )
let F be ManySortedFunction of FreeGen X, the Sorts of U1; ex h being ManySortedFunction of (FreeMSA X),U1 st
( h is_homomorphism FreeMSA X,U1 & h || (FreeGen X) = F )
set SA = the Sorts of (FreeMSA X);
set AR = the Arity of S;
set S1 = the Sorts of U1;
set O = the carrier' of S;
set RS = the ResultSort of S;
set DU = Union the Sorts of U1;
deffunc H1( Symbol of (DTConMSA X)) -> Element of Union the Sorts of U1 = pi (F, the Sorts of U1,$1);
deffunc H2( Symbol of (DTConMSA X), FinSequence, FinSequence) -> Element of Union the Sorts of U1 = pi ((@ (X,$1)),U1,$3);
consider G being Function of (TS (DTConMSA X)),(Union the Sorts of U1) such that
A1:
for t being Symbol of (DTConMSA X) st t in Terminals (DTConMSA X) holds
G . (root-tree t) = H1(t)
and
A2:
for nt being Symbol of (DTConMSA X)
for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts holds
G . (nt -tree ts) = H2(nt, roots ts,G * ts)
from DTCONSTR:sch 8();
deffunc H3( object ) -> Element of bool [:(TS (DTConMSA X)),(Union the Sorts of U1):] = G | ( the Sorts of (FreeMSA X) . $1);
consider h being Function such that
A3:
( dom h = the carrier of S & ( for s being object st s in the carrier of S holds
h . s = H3(s) ) )
from FUNCT_1:sch 3();
reconsider h = h as ManySortedSet of the carrier of S by A3, PARTFUN1:def 2, RELAT_1:def 18;
for s being object st s in dom h holds
h . s is Function
then reconsider h = h as ManySortedFunction of the carrier of S by FUNCOP_1:def 6;
defpred S1[ set ] means for s being SortSymbol of S st $1 in the Sorts of (FreeMSA X) . s holds
(h . s) . $1 in the Sorts of U1 . s;
A4:
for nt being Symbol of (DTConMSA X)
for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]
proof
let nt be
Symbol of
(DTConMSA X);
for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]let ts be
FinSequence of
TS (DTConMSA X);
( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds
S1[t] ) implies S1[nt -tree ts] )
assume that A5:
nt ==> roots ts
and A6:
for
t being
DecoratedTree of the
carrier of
(DTConMSA X) st
t in rng ts holds
S1[
t]
;
S1[nt -tree ts]
set p =
G * ts;
set o =
@ (
X,
nt);
set ar =
the_arity_of (@ (X,nt));
set rs =
the_result_sort_of (@ (X,nt));
set OU =
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
set rt =
roots ts;
A7:
[(@ (X,nt)), the carrier of S] = nt
by A5, Def20;
then A8:
[[(@ (X,nt)), the carrier of S],(roots ts)] in the
Rules of
(DTConMSA X)
by A5, LANG1:def 1;
A9:
[(@ (X,nt)), the carrier of S] = Sym (
(@ (X,nt)),
X)
;
then A10:
(DenOp ((@ (X,nt)),X)) . ts = nt -tree ts
by A5, A7, Def12;
dom (DenOp ((@ (X,nt)),X)) = (((FreeSort X) #) * the Arity of S) . (@ (X,nt))
by FUNCT_2:def 1;
then
ts in dom (DenOp ((@ (X,nt)),X))
by A5, A7, A9, Th10;
then
(
rng (DenOp ((@ (X,nt)),X)) c= ((FreeSort X) * the ResultSort of S) . (@ (X,nt)) &
nt -tree ts in rng (DenOp ((@ (X,nt)),X)) )
by A10, FUNCT_1:def 3, RELAT_1:def 19;
then A11:
nt -tree ts in ( the Sorts of (FreeMSA X) * the ResultSort of S) . (@ (X,nt))
;
set ppi =
pi (
(@ (X,nt)),
U1,
(G * ts));
A12:
rng the
ResultSort of
S c= the
carrier of
S
by RELAT_1:def 19;
A13:
rng (the_arity_of (@ (X,nt))) c= the
carrier of
S
by FINSEQ_1:def 4;
reconsider rt =
roots ts as
Element of
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by A8, ZFMISC_1:87;
A14:
len rt = len (the_arity_of (@ (X,nt)))
by A8, Th5;
A15:
dom rt = Seg (len rt)
by FINSEQ_1:def 3;
dom the
Sorts of
(FreeMSA X) = the
carrier of
S
by PARTFUN1:def 2;
then A16:
dom ( the Sorts of (FreeMSA X) * (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt)))
by A13, RELAT_1:27;
A17:
the_arity_of (@ (X,nt)) = the
Arity of
S . (@ (X,nt))
by MSUALG_1:def 1;
dom the
Sorts of
U1 = the
carrier of
S
by PARTFUN1:def 2;
then A18:
dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt)))
by A13, RELAT_1:27;
A19:
(
dom rt = dom ts &
Seg (len (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt))) )
by FINSEQ_1:def 3, TREES_3:def 18;
A20:
dom (G * ts) = dom ts
by FINSEQ_3:120;
then A21:
dom (G * ts) = dom ( the Sorts of U1 * (the_arity_of (@ (X,nt))))
by A18, A8, A15, A19, Th5;
A22:
for
x being
object st
x in dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) holds
(G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x
proof
let x be
object ;
( x in dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) implies (G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x )
assume A23:
x in dom ( the Sorts of U1 * (the_arity_of (@ (X,nt))))
;
(G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x
then reconsider n =
x as
Nat ;
A24:
ts . n in rng ts
by A18, A14, A15, A19, A23, FUNCT_1:def 3;
rng ts c= TS (DTConMSA X)
by FINSEQ_1:def 4;
then reconsider t =
ts . n as
Element of
TS (DTConMSA X) by A24;
A25:
(G * ts) . n = G . (ts . n)
by A21, A23, FINSEQ_3:120;
(the_arity_of (@ (X,nt))) . x in rng (the_arity_of (@ (X,nt)))
by A18, A23, FUNCT_1:def 3;
then reconsider s =
(the_arity_of (@ (X,nt))) . x as
SortSymbol of
S by A13;
A26:
h . s = G | ( the Sorts of (FreeMSA X) . s)
by A3;
dom the
Sorts of
(FreeMSA X) = the
carrier of
S
by PARTFUN1:def 2;
then A27:
the
Sorts of
(FreeMSA X) . s in rng the
Sorts of
(FreeMSA X)
by FUNCT_1:def 3;
dom G =
TS (DTConMSA X)
by FUNCT_2:def 1
.=
union (rng the Sorts of (FreeMSA X))
by Th11
;
then A28:
dom (h . s) = the
Sorts of
(FreeMSA X) . s
by A26, A27, RELAT_1:62, ZFMISC_1:74;
ts in (((FreeSort X) #) * the Arity of S) . (@ (X,nt))
by A5, A7, A9, Th10;
then
ts in product ((FreeSort X) * (the_arity_of (@ (X,nt))))
by A17, Th1;
then
ts . x in ((FreeSort X) * (the_arity_of (@ (X,nt)))) . x
by A18, A16, A23, CARD_3:9;
then A29:
ts . x in (FreeSort X) . ((the_arity_of (@ (X,nt))) . x)
by A18, A16, A23, FUNCT_1:12;
then
(h . s) . t in the
Sorts of
U1 . s
by A6, A24;
then
G . t in the
Sorts of
U1 . s
by A29, A26, A28, FUNCT_1:47;
hence
(G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x
by A23, A25, FUNCT_1:12;
verum
end;
dom the
Sorts of
U1 = the
carrier of
S
by PARTFUN1:def 2;
then A30:
dom ( the Sorts of U1 * the ResultSort of S) = dom the
ResultSort of
S
by A12, RELAT_1:27;
let s be
SortSymbol of
S;
( nt -tree ts in the Sorts of (FreeMSA X) . s implies (h . s) . (nt -tree ts) in the Sorts of U1 . s )
A31:
dom (Den ((@ (X,nt)),U1)) = Args (
(@ (X,nt)),
U1)
by FUNCT_2:def 1;
A32:
dom the
ResultSort of
S = the
carrier' of
S
by FUNCT_2:def 1;
dom the
Sorts of
(FreeMSA X) = the
carrier of
S
by PARTFUN1:def 2;
then
dom ( the Sorts of (FreeMSA X) * the ResultSort of S) = dom the
ResultSort of
S
by A12, RELAT_1:27;
then
nt -tree ts in the
Sorts of
(FreeMSA X) . ( the ResultSort of S . (@ (X,nt)))
by A32, A11, FUNCT_1:12;
then A33:
nt -tree ts in the
Sorts of
(FreeMSA X) . (the_result_sort_of (@ (X,nt)))
by MSUALG_1:def 2;
Args (
(@ (X,nt)),
U1) =
(( the Sorts of U1 #) * the Arity of S) . (@ (X,nt))
by MSUALG_1:def 4
.=
product ( the Sorts of U1 * (the_arity_of (@ (X,nt))))
by A17, Th1
;
then A34:
G * ts in Args (
(@ (X,nt)),
U1)
by A20, A18, A14, A15, A19, A22, CARD_3:9;
then
pi (
(@ (X,nt)),
U1,
(G * ts))
= (Den ((@ (X,nt)),U1)) . (G * ts)
by Def21;
then
(
rng (Den ((@ (X,nt)),U1)) c= Result (
(@ (X,nt)),
U1) &
pi (
(@ (X,nt)),
U1,
(G * ts))
in rng (Den ((@ (X,nt)),U1)) )
by A34, A31, FUNCT_1:def 3, RELAT_1:def 19;
then A35:
pi (
(@ (X,nt)),
U1,
(G * ts))
in Result (
(@ (X,nt)),
U1)
;
assume A36:
nt -tree ts in the
Sorts of
(FreeMSA X) . s
;
(h . s) . (nt -tree ts) in the Sorts of U1 . s
A37:
the_result_sort_of (@ (X,nt)) = s
by A33, A36, XBOOLE_0:3, Th12;
G . (nt -tree ts) = pi (
(@ (X,nt)),
U1,
(G * ts))
by A2, A5;
then A38:
pi (
(@ (X,nt)),
U1,
(G * ts))
= (G | ( the Sorts of (FreeMSA X) . (the_result_sort_of (@ (X,nt))))) . (nt -tree ts)
by A33, FUNCT_1:49;
Result (
(@ (X,nt)),
U1) =
( the Sorts of U1 * the ResultSort of S) . (@ (X,nt))
by MSUALG_1:def 5
.=
the
Sorts of
U1 . ( the ResultSort of S . (@ (X,nt)))
by A30, A32, FUNCT_1:12
.=
the
Sorts of
U1 . (the_result_sort_of (@ (X,nt)))
by MSUALG_1:def 2
;
hence
(h . s) . (nt -tree ts) in the
Sorts of
U1 . s
by A3, A35, A38, A37;
verum
end;
A39:
for t being Symbol of (DTConMSA X) st t in Terminals (DTConMSA X) holds
S1[ root-tree t]
proof
let t be
Symbol of
(DTConMSA X);
( t in Terminals (DTConMSA X) implies S1[ root-tree t] )
assume A40:
t in Terminals (DTConMSA X)
;
S1[ root-tree t]
then consider s being
SortSymbol of
S,
x being
set such that
x in X . s
and A41:
t = [x,s]
by Th7;
set E =
{ (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } ;
set a =
root-tree t;
A42:
t `2 = s
by A41;
then A43:
root-tree t in { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) }
by A40;
let s1 be
SortSymbol of
S;
( root-tree t in the Sorts of (FreeMSA X) . s1 implies (h . s1) . (root-tree t) in the Sorts of U1 . s1 )
reconsider f =
F . s as
Function of
((FreeGen X) . s),
( the Sorts of U1 . s) ;
A44:
dom f = (FreeGen X) . s
by FUNCT_2:def 1;
A45:
{ (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } = FreeGen (
s,
X)
by Th13;
then
(FreeGen X) . s = { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) }
by Def16;
then A46:
(
rng f c= the
Sorts of
U1 . s &
f . (root-tree t) in rng f )
by A43, A44, FUNCT_1:def 3, RELAT_1:def 19;
assume A47:
root-tree t in the
Sorts of
(FreeMSA X) . s1
;
(h . s1) . (root-tree t) in the Sorts of U1 . s1
h . s = G | ( the Sorts of (FreeMSA X) . s)
by A3;
then (h . s) . (root-tree t) =
G . (root-tree t)
by A43, A45, FUNCT_1:49
.=
pi (
F, the
Sorts of
U1,
t)
by A1, A40
.=
f . (root-tree t)
by A40, A42, Def19
;
hence
(h . s1) . (root-tree t) in the
Sorts of
U1 . s1
by A46, A48;
verum
end;
A50:
for t being DecoratedTree of the carrier of (DTConMSA X) st t in TS (DTConMSA X) holds
S1[t]
from DTCONSTR:sch 7(A39, A4);
for s being object st s in the carrier of S holds
h . s is Function of ( the Sorts of (FreeMSA X) . s),( the Sorts of U1 . s)
proof
let x be
object ;
( x in the carrier of S implies h . x is Function of ( the Sorts of (FreeMSA X) . x),( the Sorts of U1 . x) )
assume
x in the
carrier of
S
;
h . x is Function of ( the Sorts of (FreeMSA X) . x),( the Sorts of U1 . x)
then reconsider s =
x as
SortSymbol of
S ;
A51:
dom G =
TS (DTConMSA X)
by FUNCT_2:def 1
.=
union (rng the Sorts of (FreeMSA X))
by Th11
;
dom the
Sorts of
(FreeMSA X) = the
carrier of
S
by PARTFUN1:def 2;
then A52:
the
Sorts of
(FreeMSA X) . s in rng the
Sorts of
(FreeMSA X)
by FUNCT_1:def 3;
A53:
h . s = G | ( the Sorts of (FreeMSA X) . s)
by A3;
then A54:
dom (h . s) = the
Sorts of
(FreeMSA X) . s
by A51, A52, RELAT_1:62, ZFMISC_1:74;
A55:
the
Sorts of
(FreeMSA X) . s c= dom G
by A51, A52, ZFMISC_1:74;
rng (h . s) c= the
Sorts of
U1 . s
hence
h . x is
Function of
( the Sorts of (FreeMSA X) . x),
( the Sorts of U1 . x)
by A54, FUNCT_2:def 1, RELSET_1:4;
verum
end;
then reconsider h = h as ManySortedFunction of (FreeMSA X),U1 by PBOOLE:def 15;
take
h
; ( h is_homomorphism FreeMSA X,U1 & h || (FreeGen X) = F )
thus
h is_homomorphism FreeMSA X,U1
h || (FreeGen X) = Fproof
(
rng the
ResultSort of
S c= the
carrier of
S &
dom the
Sorts of
(FreeMSA X) = the
carrier of
S )
by PARTFUN1:def 2, RELAT_1:def 19;
then A58:
(
dom the
ResultSort of
S = the
carrier' of
S &
dom ( the Sorts of (FreeMSA X) * the ResultSort of S) = dom the
ResultSort of
S )
by FUNCT_2:def 1, RELAT_1:27;
let o be
OperSymbol of
S;
MSUALG_3:def 7 ( Args (o,(FreeMSA X)) = {} or for b1 being Element of Args (o,(FreeMSA X)) holds (h . (the_result_sort_of o)) . ((Den (o,(FreeMSA X))) . b1) = (Den (o,U1)) . (h # b1) )
assume
Args (
o,
(FreeMSA X))
<> {}
;
for b1 being Element of Args (o,(FreeMSA X)) holds (h . (the_result_sort_of o)) . ((Den (o,(FreeMSA X))) . b1) = (Den (o,U1)) . (h # b1)
let x be
Element of
Args (
o,
(FreeMSA X));
(h . (the_result_sort_of o)) . ((Den (o,(FreeMSA X))) . x) = (Den (o,U1)) . (h # x)
set rs =
the_result_sort_of o;
set DA =
Den (
o,
(FreeMSA X));
set D1 =
Den (
o,
U1);
set OU =
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
set ar =
the_arity_of o;
A59:
the_arity_of o = the
Arity of
S . o
by MSUALG_1:def 1;
A60:
Args (
o,
(FreeMSA X))
= (((FreeSort X) #) * the Arity of S) . o
by MSUALG_1:def 4;
then reconsider p =
x as
FinSequence of
TS (DTConMSA X) by Th8;
A61:
Sym (
o,
X)
==> roots p
by A60, Th10;
then A62:
@ (
X,
(Sym (o,X)))
= o
by Def20;
A63:
dom (G * p) = dom p
by FINSEQ_3:120;
A64:
x in (((FreeSort X) #) * the Arity of S) . o
by A60;
A65:
for
a being
object st
a in dom p holds
(G * p) . a = (h # x) . a
proof
(
rng (the_arity_of o) c= the
carrier of
S &
dom the
Sorts of
(FreeMSA X) = the
carrier of
S )
by FINSEQ_1:def 4, PARTFUN1:def 2;
then A66:
dom ( the Sorts of (FreeMSA X) * (the_arity_of o)) = dom (the_arity_of o)
by RELAT_1:27;
set rt =
roots p;
let a be
object ;
( a in dom p implies (G * p) . a = (h # x) . a )
assume A67:
a in dom p
;
(G * p) . a = (h # x) . a
then reconsider n =
a as
Nat ;
A68:
[[o, the carrier of S],(roots p)] in the
Rules of
(DTConMSA X)
by A61, LANG1:def 1;
then reconsider rt =
roots p as
Element of
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:87;
A69:
len rt = len (the_arity_of o)
by A68, Th5;
A70:
(
(G * p) . n = G . (x . n) &
(h # x) . n = (h . ((the_arity_of o) /. n)) . (x . n) )
by A63, A67, FINSEQ_3:120, MSUALG_3:def 6;
A71:
h . ((the_arity_of o) /. n) = G | ( the Sorts of (FreeMSA X) . ((the_arity_of o) /. n))
by A3;
A72:
Seg (len rt) = dom rt
by FINSEQ_1:def 3;
A73:
(
dom rt = dom p &
Seg (len (the_arity_of o)) = dom (the_arity_of o) )
by FINSEQ_1:def 3, TREES_3:def 18;
p in product ((FreeSort X) * (the_arity_of o))
by A64, A59, Th1;
then A74:
p . n in ((FreeSort X) * (the_arity_of o)) . n
by A67, A66, A69, A72, A73, CARD_3:9;
((FreeSort X) * (the_arity_of o)) . n =
the
Sorts of
(FreeMSA X) . ((the_arity_of o) . n)
by A67, A66, A69, A72, A73, FUNCT_1:12
.=
the
Sorts of
(FreeMSA X) . ((the_arity_of o) /. n)
by A67, A69, A72, A73, PARTFUN1:def 6
;
hence
(G * p) . a = (h # x) . a
by A70, A71, A74, FUNCT_1:49;
verum
end;
dom (h # x) = dom (the_arity_of o)
by MSUALG_3:6;
then A75:
G * p = h # x
by A63, A65, FUNCT_1:2, MSUALG_3:6;
A76:
h . (the_result_sort_of o) = G | ( the Sorts of (FreeMSA X) . (the_result_sort_of o))
by A3;
A77:
dom (DenOp (o,X)) = (((FreeSort X) #) * the Arity of S) . o
by FUNCT_2:def 1;
(DenOp (o,X)) . p = (Sym (o,X)) -tree p
by A61, Def12;
then
(
rng (DenOp (o,X)) c= ((FreeSort X) * the ResultSort of S) . o &
(Sym (o,X)) -tree p in rng (DenOp (o,X)) )
by A60, A77, FUNCT_1:def 3, RELAT_1:def 19;
then
(Sym (o,X)) -tree p in ( the Sorts of (FreeMSA X) * the ResultSort of S) . o
;
then
(Sym (o,X)) -tree p in the
Sorts of
(FreeMSA X) . ( the ResultSort of S . o)
by A58, FUNCT_1:12;
then A78:
(Sym (o,X)) -tree p in the
Sorts of
(FreeMSA X) . (the_result_sort_of o)
by MSUALG_1:def 2;
dom the
Sorts of
(FreeMSA X) = the
carrier of
S
by PARTFUN1:def 2;
then A79:
the
Sorts of
(FreeMSA X) . (the_result_sort_of o) in rng the
Sorts of
(FreeMSA X)
by FUNCT_1:def 3;
dom G =
TS (DTConMSA X)
by FUNCT_2:def 1
.=
union (rng the Sorts of (FreeMSA X))
by Th11
;
then A80:
dom (h . (the_result_sort_of o)) = the
Sorts of
(FreeMSA X) . (the_result_sort_of o)
by A76, A79, RELAT_1:62, ZFMISC_1:74;
Den (
o,
(FreeMSA X)) =
(FreeOper X) . o
by MSUALG_1:def 6
.=
DenOp (
o,
X)
by Def13
;
then
(Den (o,(FreeMSA X))) . x = (Sym (o,X)) -tree p
by A61, Def12;
hence (h . (the_result_sort_of o)) . ((Den (o,(FreeMSA X))) . x) =
G . ((Sym (o,X)) -tree p)
by A78, A76, A80, FUNCT_1:47
.=
pi (
(@ (X,(Sym (o,X)))),
U1,
(G * p))
by A2, A61
.=
(Den (o,U1)) . (h # x)
by A62, A75, Def21
;
verum
end;
for x being object st x in the carrier of S holds
(h || (FreeGen X)) . x = F . x
proof
set hf =
h || (FreeGen X);
let x be
object ;
( x in the carrier of S implies (h || (FreeGen X)) . x = F . x )
assume
x in the
carrier of
S
;
(h || (FreeGen X)) . x = F . x
then reconsider s =
x as
SortSymbol of
S ;
A81:
dom (h . s) = the
Sorts of
(FreeMSA X) . s
by FUNCT_2:def 1;
A82:
dom ((h || (FreeGen X)) . s) = (FreeGen X) . s
by FUNCT_2:def 1;
A83:
(FreeGen X) . s = FreeGen (
s,
X)
by Def16;
A84:
(h || (FreeGen X)) . s = (h . s) | ((FreeGen X) . s)
by Def1;
A85:
for
a being
object st
a in (FreeGen X) . s holds
((h || (FreeGen X)) . s) . a = (F . s) . a
proof
let a be
object ;
( a in (FreeGen X) . s implies ((h || (FreeGen X)) . s) . a = (F . s) . a )
A86:
h . s = G | ( the Sorts of (FreeMSA X) . s)
by A3;
assume A87:
a in (FreeGen X) . s
;
((h || (FreeGen X)) . s) . a = (F . s) . a
then
a in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }
by A83, Th13;
then consider t being
Symbol of
(DTConMSA X) such that A88:
(
a = root-tree t &
t in Terminals (DTConMSA X) )
and A89:
t `2 = s
;
thus ((h || (FreeGen X)) . s) . a =
(h . s) . a
by A84, A82, A87, FUNCT_1:47
.=
G . a
by A81, A83, A87, A86, FUNCT_1:47
.=
pi (
F, the
Sorts of
U1,
t)
by A1, A88
.=
(F . s) . a
by A88, A89, Def19
;
verum
end;
dom (F . s) = (FreeGen X) . s
by FUNCT_2:def 1;
hence
(h || (FreeGen X)) . x = F . x
by A82, A85, FUNCT_1:2;
verum
end;
hence
h || (FreeGen X) = F
; verum