let S be non empty non void ManySortedSign ; for X being V16() ManySortedSet of the carrier of S holds FreeGen X is free
let X be V16() 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 of 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( set ) -> 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 set 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 4, RELAT_1:def 18;
for s being set 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, Def22;
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, Def14;
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 5, 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:106;
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 4;
then A16:
dom ( the Sorts of (FreeMSA X) * (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt)))
by A13, RELAT_1:46;
A17:
the_arity_of (@ (X,nt)) = the
Arity of
S . (@ (X,nt))
by MSUALG_1:def 6;
dom the
Sorts of
U1 = the
carrier of
S
by PARTFUN1:def 4;
then A18:
dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt)))
by A13, RELAT_1:46;
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:129;
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
set 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
set ;
( 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 by A18;
A24:
ts . n in rng ts
by A18, A14, A15, A19, A23, FUNCT_1:def 5;
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:129;
(the_arity_of (@ (X,nt))) . x in rng (the_arity_of (@ (X,nt)))
by A18, A23, FUNCT_1:def 5;
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 4;
then A27:
the
Sorts of
(FreeMSA X) . s in rng the
Sorts of
(FreeMSA X)
by FUNCT_1:def 5;
dom G =
TS (DTConMSA X)
by FUNCT_2:def 1
.=
union (rng the Sorts of (FreeMSA X))
by Th12
;
then A28:
dom (h . s) = the
Sorts of
(FreeMSA X) . s
by A26, A27, RELAT_1:91, ZFMISC_1:92;
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:18;
then A29:
ts . x in (FreeSort X) . ((the_arity_of (@ (X,nt))) . x)
by A18, A16, A23, FUNCT_1:22;
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:70;
hence
(G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x
by A23, A25, FUNCT_1:22;
verum
end;
dom the
Sorts of
U1 = the
carrier of
S
by PARTFUN1:def 4;
then A30:
dom ( the Sorts of U1 * the ResultSort of S) = dom the
ResultSort of
S
by A12, RELAT_1:46;
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 4;
then
dom ( the Sorts of (FreeMSA X) * the ResultSort of S) = dom the
ResultSort of
S
by A12, RELAT_1:46;
then
nt -tree ts in the
Sorts of
(FreeMSA X) . ( the ResultSort of S . (@ (X,nt)))
by A32, A11, FUNCT_1:22;
then A33:
nt -tree ts in the
Sorts of
(FreeMSA X) . (the_result_sort_of (@ (X,nt)))
by MSUALG_1:def 7;
Args (
(@ (X,nt)),
U1) =
(( the Sorts of U1 #) * the Arity of S) . (@ (X,nt))
by MSUALG_1:def 9
.=
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:18;
then
pi (
(@ (X,nt)),
U1,
(G * ts))
= (Den ((@ (X,nt)),U1)) . (G * ts)
by Def23;
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 5, 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
G . (nt -tree ts) = pi (
(@ (X,nt)),
U1,
(G * ts))
by A2, A5;
then A39:
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:72;
Result (
(@ (X,nt)),
U1) =
( the Sorts of U1 * the ResultSort of S) . (@ (X,nt))
by MSUALG_1:def 10
.=
the
Sorts of
U1 . ( the ResultSort of S . (@ (X,nt)))
by A30, A32, FUNCT_1:22
.=
the
Sorts of
U1 . (the_result_sort_of (@ (X,nt)))
by MSUALG_1:def 7
;
hence
(h . s) . (nt -tree ts) in the
Sorts of
U1 . s
by A3, A35, A39, A37;
verum
end;
A40:
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 A41:
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 A42:
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;
A43:
t `2 = s
by A42, MCART_1:7;
then A44:
root-tree t in { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) }
by A41;
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) ;
A45:
dom f = (FreeGen X) . s
by FUNCT_2:def 1;
A46:
{ (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } = FreeGen (
s,
X)
by Th14;
then
(FreeGen X) . s = { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) }
by Def18;
then A47:
(
rng f c= the
Sorts of
U1 . s &
f . (root-tree t) in rng f )
by A44, A45, FUNCT_1:def 5, RELAT_1:def 19;
assume A48:
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 A44, A46, FUNCT_1:72
.=
pi (
F, the
Sorts of
U1,
t)
by A1, A41
.=
f . (root-tree t)
by A41, A43, Def21
;
hence
(h . s1) . (root-tree t) in the
Sorts of
U1 . s1
by A47, A49;
verum
end;
A51:
for t being DecoratedTree of the carrier of (DTConMSA X) st t in TS (DTConMSA X) holds
S1[t]
from DTCONSTR:sch 7(A40, A4);
for s being set 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
set ;
( 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 ;
A52:
dom G =
TS (DTConMSA X)
by FUNCT_2:def 1
.=
union (rng the Sorts of (FreeMSA X))
by Th12
;
dom the
Sorts of
(FreeMSA X) = the
carrier of
S
by PARTFUN1:def 4;
then A53:
the
Sorts of
(FreeMSA X) . s in rng the
Sorts of
(FreeMSA X)
by FUNCT_1:def 5;
A54:
h . s = G | ( the Sorts of (FreeMSA X) . s)
by A3;
then A55:
dom (h . s) = the
Sorts of
(FreeMSA X) . s
by A52, A53, RELAT_1:91, ZFMISC_1:92;
A56:
the
Sorts of
(FreeMSA X) . s c= dom G
by A52, A53, ZFMISC_1:92;
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 A55, FUNCT_2:def 1, RELSET_1:11;
verum
end;
then reconsider h = h as ManySortedFunction of (FreeMSA X),U1 by PBOOLE:def 18;
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 4, RELAT_1:def 19;
then A59:
(
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:46;
let o be
OperSymbol of
S;
MSUALG_3:def 9 ( 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;
A60:
the_arity_of o = the
Arity of
S . o
by MSUALG_1:def 6;
A61:
Args (
o,
(FreeMSA X))
= (((FreeSort X) #) * the Arity of S) . o
by MSUALG_1:def 9;
then reconsider p =
x as
FinSequence of
TS (DTConMSA X) by Th8;
A62:
Sym (
o,
X)
==> roots p
by A61, Th10;
then A63:
@ (
X,
(Sym (o,X)))
= o
by Def22;
A64:
dom (G * p) = dom p
by FINSEQ_3:129;
A65:
x in (((FreeSort X) #) * the Arity of S) . o
by A61;
A66:
for
a being
set 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 4;
then A67:
dom ( the Sorts of (FreeMSA X) * (the_arity_of o)) = dom (the_arity_of o)
by RELAT_1:46;
set rt =
roots p;
let a be
set ;
( a in dom p implies (G * p) . a = (h # x) . a )
assume A68:
a in dom p
;
(G * p) . a = (h # x) . a
then reconsider n =
a as
Nat ;
A69:
[[o, the carrier of S],(roots p)] in the
Rules of
(DTConMSA X)
by A62, 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:106;
A70:
len rt = len (the_arity_of o)
by A69, Th5;
A71:
(
(G * p) . n = G . (x . n) &
(h # x) . n = (h . ((the_arity_of o) /. n)) . (x . n) )
by A64, A68, FINSEQ_3:129, MSUALG_3:def 8;
A72:
h . ((the_arity_of o) /. n) = G | ( the Sorts of (FreeMSA X) . ((the_arity_of o) /. n))
by A3;
A73:
Seg (len rt) = dom rt
by FINSEQ_1:def 3;
A74:
(
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 A65, A60, Th1;
then A75:
p . n in ((FreeSort X) * (the_arity_of o)) . n
by A68, A67, A70, A73, A74, CARD_3:18;
((FreeSort X) * (the_arity_of o)) . n =
the
Sorts of
(FreeMSA X) . ((the_arity_of o) . n)
by A68, A67, A70, A73, A74, FUNCT_1:22
.=
the
Sorts of
(FreeMSA X) . ((the_arity_of o) /. n)
by A68, A70, A73, A74, PARTFUN1:def 8
;
hence
(G * p) . a = (h # x) . a
by A71, A72, A75, FUNCT_1:72;
verum
end;
dom (h # x) = dom (the_arity_of o)
by MSUALG_3:6;
then A76:
G * p = h # x
by A64, A66, FUNCT_1:9, MSUALG_3:6;
A77:
h . (the_result_sort_of o) = G | ( the Sorts of (FreeMSA X) . (the_result_sort_of o))
by A3;
A78:
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 A62, Def14;
then
(
rng (DenOp (o,X)) c= ((FreeSort X) * the ResultSort of S) . o &
(Sym (o,X)) -tree p in rng (DenOp (o,X)) )
by A61, A78, FUNCT_1:def 5, 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 A59, FUNCT_1:22;
then A79:
(Sym (o,X)) -tree p in the
Sorts of
(FreeMSA X) . (the_result_sort_of o)
by MSUALG_1:def 7;
dom the
Sorts of
(FreeMSA X) = the
carrier of
S
by PARTFUN1:def 4;
then A80:
the
Sorts of
(FreeMSA X) . (the_result_sort_of o) in rng the
Sorts of
(FreeMSA X)
by FUNCT_1:def 5;
dom G =
TS (DTConMSA X)
by FUNCT_2:def 1
.=
union (rng the Sorts of (FreeMSA X))
by Th12
;
then A81:
dom (h . (the_result_sort_of o)) = the
Sorts of
(FreeMSA X) . (the_result_sort_of o)
by A77, A80, RELAT_1:91, ZFMISC_1:92;
Den (
o,
(FreeMSA X)) =
(FreeOper X) . o
by MSUALG_1:def 11
.=
DenOp (
o,
X)
by Def15
;
then
(Den (o,(FreeMSA X))) . x = (Sym (o,X)) -tree p
by A62, Def14;
hence (h . (the_result_sort_of o)) . ((Den (o,(FreeMSA X))) . x) =
G . ((Sym (o,X)) -tree p)
by A79, A77, A81, FUNCT_1:70
.=
pi (
(@ (X,(Sym (o,X)))),
U1,
(G * p))
by A2, A62
.=
(Den (o,U1)) . (h # x)
by A63, A76, Def23
;
verum
end;
for x being set st x in the carrier of S holds
(h || (FreeGen X)) . x = F . x
proof
set hf =
h || (FreeGen X);
let x be
set ;
( 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 ;
A82:
dom (h . s) = the
Sorts of
(FreeMSA X) . s
by FUNCT_2:def 1;
A83:
dom ((h || (FreeGen X)) . s) = (FreeGen X) . s
by FUNCT_2:def 1;
A84:
(FreeGen X) . s = FreeGen (
s,
X)
by Def18;
A85:
(h || (FreeGen X)) . s = (h . s) | ((FreeGen X) . s)
by Def1;
A86:
for
a being
set st
a in (FreeGen X) . s holds
((h || (FreeGen X)) . s) . a = (F . s) . a
proof
let a be
set ;
( a in (FreeGen X) . s implies ((h || (FreeGen X)) . s) . a = (F . s) . a )
A87:
h . s = G | ( the Sorts of (FreeMSA X) . s)
by A3;
assume A88:
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 A84, Th14;
then consider t being
Symbol of
(DTConMSA X) such that A89:
(
a = root-tree t &
t in Terminals (DTConMSA X) )
and A90:
t `2 = s
;
thus ((h || (FreeGen X)) . s) . a =
(h . s) . a
by A85, A83, A88, FUNCT_1:70
.=
G . a
by A82, A84, A88, A87, FUNCT_1:70
.=
pi (
F, the
Sorts of
U1,
t)
by A1, A89
.=
(F . s) . a
by A89, A90, Def21
;
verum
end;
dom (F . s) = (FreeGen X) . s
by FUNCT_2:def 1;
hence
(h || (FreeGen X)) . x = F . x
by A83, A86, FUNCT_1:9;
verum
end;
hence
h || (FreeGen X) = F
by PBOOLE:3; verum