let f be non empty with_zero FinSequence of NAT ; for D being disjoint_with_NAT set holds FreeGenSetZAO f,D is free
let D be disjoint_with_NAT set ; FreeGenSetZAO f,D is free
set fgs = FreeGenSetZAO f,D;
set fua = FreeUnivAlgZAO f,D;
let U1 be Universal_Algebra; FREEALG:def 6 ( FreeUnivAlgZAO f,D,U1 are_similar implies for f being Function of (FreeGenSetZAO f,D),the carrier of U1 ex h being Function of (FreeUnivAlgZAO f,D),U1 st
( h is_homomorphism FreeUnivAlgZAO f,D,U1 & h | (FreeGenSetZAO f,D) = f ) )
assume A1:
FreeUnivAlgZAO f,D,U1 are_similar
; for f being Function of (FreeGenSetZAO f,D),the carrier of U1 ex h being Function of (FreeUnivAlgZAO f,D),U1 st
( h is_homomorphism FreeUnivAlgZAO f,D,U1 & h | (FreeGenSetZAO f,D) = f )
set A = DTConUA f,D;
set c1 = the carrier of U1;
set cf = the carrier of (FreeUnivAlgZAO f,D);
let F be Function of (FreeGenSetZAO f,D),the carrier of U1; ex h being Function of (FreeUnivAlgZAO f,D),U1 st
( h is_homomorphism FreeUnivAlgZAO f,D,U1 & h | (FreeGenSetZAO f,D) = F )
deffunc H1( Symbol of (DTConUA f,D)) -> Element of the carrier of U1 = pi F,$1;
deffunc H2( Symbol of (DTConUA f,D), FinSequence, set ) -> Element of the carrier of U1 = (oper (@ $1),U1) /. $3;
consider ff being Function of (TS (DTConUA f,D)),the carrier of U1 such that
A2:
for t being Symbol of (DTConUA f,D) st t in Terminals (DTConUA f,D) holds
ff . (root-tree t) = H1(t)
and
A3:
for nt being Symbol of (DTConUA f,D)
for ts being FinSequence of TS (DTConUA f,D) st nt ==> roots ts holds
ff . (nt -tree ts) = H2(nt, roots ts,ff * ts)
from DTCONSTR:sch 8();
reconsider ff = ff as Function of (FreeUnivAlgZAO f,D),U1 ;
take
ff
; ( ff is_homomorphism FreeUnivAlgZAO f,D,U1 & ff | (FreeGenSetZAO f,D) = F )
for n being Element of NAT st n in dom the charact of (FreeUnivAlgZAO f,D) holds
for o1 being operation of (FreeUnivAlgZAO f,D)
for o2 being operation of U1 st o1 = the charact of (FreeUnivAlgZAO f,D) . n & o2 = the charact of U1 . n holds
for x being FinSequence of (FreeUnivAlgZAO f,D) st x in dom o1 holds
ff . (o1 . x) = o2 . (ff * x)
proof
A4:
dom the
charact of
U1 = Seg (len the charact of U1)
by FINSEQ_1:def 3;
let n be
Element of
NAT ;
( n in dom the charact of (FreeUnivAlgZAO f,D) implies for o1 being operation of (FreeUnivAlgZAO f,D)
for o2 being operation of U1 st o1 = the charact of (FreeUnivAlgZAO f,D) . n & o2 = the charact of U1 . n holds
for x being FinSequence of (FreeUnivAlgZAO f,D) st x in dom o1 holds
ff . (o1 . x) = o2 . (ff * x) )
assume A5:
n in dom the
charact of
(FreeUnivAlgZAO f,D)
;
for o1 being operation of (FreeUnivAlgZAO f,D)
for o2 being operation of U1 st o1 = the charact of (FreeUnivAlgZAO f,D) . n & o2 = the charact of U1 . n holds
for x being FinSequence of (FreeUnivAlgZAO f,D) st x in dom o1 holds
ff . (o1 . x) = o2 . (ff * x)
let o1 be
operation of
(FreeUnivAlgZAO f,D);
for o2 being operation of U1 st o1 = the charact of (FreeUnivAlgZAO f,D) . n & o2 = the charact of U1 . n holds
for x being FinSequence of (FreeUnivAlgZAO f,D) st x in dom o1 holds
ff . (o1 . x) = o2 . (ff * x)let o2 be
operation of
U1;
( o1 = the charact of (FreeUnivAlgZAO f,D) . n & o2 = the charact of U1 . n implies for x being FinSequence of (FreeUnivAlgZAO f,D) st x in dom o1 holds
ff . (o1 . x) = o2 . (ff * x) )
assume that A6:
o1 = the
charact of
(FreeUnivAlgZAO f,D) . n
and A7:
o2 = the
charact of
U1 . n
;
for x being FinSequence of (FreeUnivAlgZAO f,D) st x in dom o1 holds
ff . (o1 . x) = o2 . (ff * x)
let x be
FinSequence of
(FreeUnivAlgZAO f,D);
( x in dom o1 implies ff . (o1 . x) = o2 . (ff * x) )
assume A8:
x in dom o1
;
ff . (o1 . x) = o2 . (ff * x)
reconsider xa =
x as
FinSequence of
TS (DTConUA f,D) ;
dom (roots xa) =
dom xa
by TREES_3:def 18
.=
Seg (len xa)
by FINSEQ_1:def 3
;
then A9:
len (roots xa) = len xa
by FINSEQ_1:def 3;
reconsider xa =
xa as
FinSequence of
FinTrees the
carrier of
(DTConUA f,D) ;
reconsider rxa =
roots xa as
FinSequence of
(dom f) \/ D ;
reconsider rxa =
rxa as
Element of
((dom f) \/ D) * by FINSEQ_1:def 11;
dom o1 =
(arity o1) -tuples_on the
carrier of
(FreeUnivAlgZAO f,D)
by UNIALG_2:2
.=
{ w where w is Element of the carrier of (FreeUnivAlgZAO f,D) * : len w = arity o1 }
;
then A10:
ex
w being
Element of the
carrier of
(FreeUnivAlgZAO f,D) * st
(
x = w &
len w = arity o1 )
by A8;
A11:
o1 = FreeOpZAO n,
f,
D
by A5, A6, Def18;
reconsider fx =
ff * x as
Element of the
carrier of
U1 * ;
A12:
dom o2 =
(arity o2) -tuples_on the
carrier of
U1
by UNIALG_2:2
.=
{ v where v is Element of the carrier of U1 * : len v = arity o2 }
;
A13:
(
len the
charact of
(FreeUnivAlgZAO f,D) = len the
charact of
U1 &
dom the
charact of
(FreeUnivAlgZAO f,D) = Seg (len the charact of (FreeUnivAlgZAO f,D)) )
by A1, FINSEQ_1:def 3, UNIALG_2:3;
A14:
Seg (len (FreeOpSeqZAO f,D)) = dom (FreeOpSeqZAO f,D)
by FINSEQ_1:def 3;
A15:
(
len (FreeOpSeqZAO f,D) = len f &
dom f = Seg (len f) )
by Def18, FINSEQ_1:def 3;
then reconsider nt =
n as
Symbol of
(DTConUA f,D) by A5, A14, XBOOLE_0:def 3;
reconsider nd =
n as
Element of
(dom f) \/ D by A5, A15, A14, XBOOLE_0:def 3;
A16:
f = signature (FreeUnivAlgZAO f,D)
by Th7;
then A17:
(signature (FreeUnivAlgZAO f,D)) . n = arity o1
by A5, A6, A15, A14, UNIALG_1:def 11;
then
[nd,rxa] in REL f,
D
by A5, A15, A14, A16, A10, A9, Def8;
then A18:
nt ==> roots xa
by LANG1:def 1;
then A19:
ff . (nt -tree xa) = (oper (@ nt),U1) /. (ff * x)
by A3;
@ nt = n
by A18, Def16;
then A20:
oper (@ nt),
U1 = o2
by A5, A7, A13, A4, Def4;
signature (FreeUnivAlgZAO f,D) = signature U1
by A1, UNIALG_2:def 2;
then
(
len (ff * x) = len x &
arity o2 = len x )
by A5, A7, A15, A14, A16, A10, A17, ALG_1:1, UNIALG_1:def 11;
then A21:
fx in { v where v is Element of the carrier of U1 * : len v = arity o2 }
;
reconsider xa =
xa as
Element of
(TS (DTConUA f,D)) * by FINSEQ_1:def 11;
Sym n,
f,
D = nt
by A5, A15, A14, Def10;
then
o1 . x = nt -tree xa
by A5, A8, A15, A14, A11, Def17;
hence
ff . (o1 . x) = o2 . (ff * x)
by A19, A20, A12, A21, PARTFUN1:def 8;
verum
end;
hence
ff is_homomorphism FreeUnivAlgZAO f,D,U1
by A1, ALG_1:def 1; ff | (FreeGenSetZAO f,D) = F
A22:
the carrier of (FreeUnivAlgZAO f,D) /\ (FreeGenSetZAO f,D) = FreeGenSetZAO f,D
by XBOOLE_1:28;
A23:
( dom (ff | (FreeGenSetZAO f,D)) = (dom ff) /\ (FreeGenSetZAO f,D) & dom ff = the carrier of (FreeUnivAlgZAO f,D) )
by FUNCT_2:def 1, RELAT_1:90;
A24:
now let x be
set ;
( x in dom F implies (ff | (FreeGenSetZAO f,D)) . x = F . x )assume A25:
x in dom F
;
(ff | (FreeGenSetZAO f,D)) . x = F . xthen
x in { (root-tree t) where t is Symbol of (DTConUA f,D) : t in Terminals (DTConUA f,D) }
;
then consider s being
Symbol of
(DTConUA f,D) such that A26:
(
x = root-tree s &
s in Terminals (DTConUA f,D) )
;
thus (ff | (FreeGenSetZAO f,D)) . x =
ff . x
by A23, A22, A25, FUNCT_1:70
.=
pi F,
s
by A2, A26
.=
F . x
by A26, Def21
;
verum end;
FreeGenSetZAO f,D = dom F
by FUNCT_2:def 1;
hence
ff | (FreeGenSetZAO f,D) = F
by A23, A22, A24, FUNCT_1:9; verum