let f be non empty FinSequence of NAT ; for D being non empty disjoint_with_NAT set holds FreeGenSetNSG (f,D) is free
let D be non empty disjoint_with_NAT set ; FreeGenSetNSG (f,D) is free
set fgs = FreeGenSetNSG (f,D);
set fua = FreeUnivAlgNSG (f,D);
let U1 be Universal_Algebra; FREEALG:def 5 ( FreeUnivAlgNSG (f,D),U1 are_similar implies for f being Function of (FreeGenSetNSG (f,D)), the carrier of U1 ex h being Function of (FreeUnivAlgNSG (f,D)),U1 st
( h is_homomorphism & h | (FreeGenSetNSG (f,D)) = f ) )
assume A1:
FreeUnivAlgNSG (f,D),U1 are_similar
; for f being Function of (FreeGenSetNSG (f,D)), the carrier of U1 ex h being Function of (FreeUnivAlgNSG (f,D)),U1 st
( h is_homomorphism & h | (FreeGenSetNSG (f,D)) = f )
set A = DTConUA (f,D);
set c1 = the carrier of U1;
set cf = the carrier of (FreeUnivAlgNSG (f,D));
let F be Function of (FreeGenSetNSG (f,D)), the carrier of U1; ex h being Function of (FreeUnivAlgNSG (f,D)),U1 st
( h is_homomorphism & h | (FreeGenSetNSG (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 (FreeUnivAlgNSG (f,D)),U1 ;
take
ff
; ( ff is_homomorphism & ff | (FreeGenSetNSG (f,D)) = F )
for n being Nat st n in dom the charact of (FreeUnivAlgNSG (f,D)) holds
for o1 being operation of (FreeUnivAlgNSG (f,D))
for o2 being operation of U1 st o1 = the charact of (FreeUnivAlgNSG (f,D)) . n & o2 = the charact of U1 . n holds
for x being FinSequence of (FreeUnivAlgNSG (f,D)) st x in dom o1 holds
ff . (o1 . x) = o2 . (ff * x)
proof
A4:
Seg (len the charact of U1) = dom the
charact of
U1
by FINSEQ_1:def 3;
let n be
Nat;
( n in dom the charact of (FreeUnivAlgNSG (f,D)) implies for o1 being operation of (FreeUnivAlgNSG (f,D))
for o2 being operation of U1 st o1 = the charact of (FreeUnivAlgNSG (f,D)) . n & o2 = the charact of U1 . n holds
for x being FinSequence of (FreeUnivAlgNSG (f,D)) st x in dom o1 holds
ff . (o1 . x) = o2 . (ff * x) )
assume A5:
n in dom the
charact of
(FreeUnivAlgNSG (f,D))
;
for o1 being operation of (FreeUnivAlgNSG (f,D))
for o2 being operation of U1 st o1 = the charact of (FreeUnivAlgNSG (f,D)) . n & o2 = the charact of U1 . n holds
for x being FinSequence of (FreeUnivAlgNSG (f,D)) st x in dom o1 holds
ff . (o1 . x) = o2 . (ff * x)
let o1 be
operation of
(FreeUnivAlgNSG (f,D));
for o2 being operation of U1 st o1 = the charact of (FreeUnivAlgNSG (f,D)) . n & o2 = the charact of U1 . n holds
for x being FinSequence of (FreeUnivAlgNSG (f,D)) st x in dom o1 holds
ff . (o1 . x) = o2 . (ff * x)let o2 be
operation of
U1;
( o1 = the charact of (FreeUnivAlgNSG (f,D)) . n & o2 = the charact of U1 . n implies for x being FinSequence of (FreeUnivAlgNSG (f,D)) st x in dom o1 holds
ff . (o1 . x) = o2 . (ff * x) )
assume that A6:
o1 = the
charact of
(FreeUnivAlgNSG (f,D)) . n
and A7:
o2 = the
charact of
U1 . n
;
for x being FinSequence of (FreeUnivAlgNSG (f,D)) st x in dom o1 holds
ff . (o1 . x) = o2 . (ff * x)
let x be
FinSequence of
(FreeUnivAlgNSG (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
(FreeUnivAlgNSG (f,D))
by MARGREL1:22
.=
{ w where w is Element of the carrier of (FreeUnivAlgNSG (f,D)) * : len w = arity o1 }
;
then A10:
ex
w being
Element of the
carrier of
(FreeUnivAlgNSG (f,D)) * st
(
x = w &
len w = arity o1 )
by A8;
A11:
o1 = FreeOpNSG (
n,
f,
D)
by A5, A6, Def11;
reconsider fx =
ff * x as
Element of the
carrier of
U1 * ;
A12:
dom o2 =
(arity o2) -tuples_on the
carrier of
U1
by MARGREL1:22
.=
{ v where v is Element of the carrier of U1 * : len v = arity o2 }
;
A13:
(
len the
charact of
(FreeUnivAlgNSG (f,D)) = len the
charact of
U1 &
Seg (len the charact of (FreeUnivAlgNSG (f,D))) = dom the
charact of
(FreeUnivAlgNSG (f,D)) )
by A1, FINSEQ_1:def 3, UNIALG_2:1;
A14:
dom (FreeOpSeqNSG (f,D)) = Seg (len (FreeOpSeqNSG (f,D)))
by FINSEQ_1:def 3;
A15:
(
len (FreeOpSeqNSG (f,D)) = len f &
Seg (len f) = dom f )
by Def11, 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 (FreeUnivAlgNSG (f,D))
by Th4;
then A17:
(signature (FreeUnivAlgNSG (f,D))) . n = arity o1
by A5, A6, A15, A14, UNIALG_1:def 4;
then
[nd,rxa] in REL (
f,
D)
by A5, A15, A14, A16, A10, A9, Def7;
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, Def15;
then A20:
oper (
(@ nt),
U1)
= o2
by A5, A7, A13, A4, Def3;
signature (FreeUnivAlgNSG (f,D)) = signature U1
by A1;
then
(
len (ff * x) = len x &
arity o2 = len x )
by A5, A7, A15, A14, A16, A10, A17, FINSEQ_3:120, UNIALG_1:def 4;
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, Def9;
then
o1 . x = nt -tree xa
by A5, A8, A15, A14, A11, Def10;
hence
ff . (o1 . x) = o2 . (ff * x)
by A19, A20, A12, A21, PARTFUN1:def 6;
verum
end;
hence
ff is_homomorphism
by A1, ALG_1:def 1; ff | (FreeGenSetNSG (f,D)) = F
A22:
the carrier of (FreeUnivAlgNSG (f,D)) /\ (FreeGenSetNSG (f,D)) = FreeGenSetNSG (f,D)
by XBOOLE_1:28;
A23:
( dom (ff | (FreeGenSetNSG (f,D))) = (dom ff) /\ (FreeGenSetNSG (f,D)) & dom ff = the carrier of (FreeUnivAlgNSG (f,D)) )
by FUNCT_2:def 1, RELAT_1:61;
A24:
now for x being object st x in dom F holds
(ff | (FreeGenSetNSG (f,D))) . x = F . xlet x be
object ;
( x in dom F implies (ff | (FreeGenSetNSG (f,D))) . x = F . x )assume A25:
x in dom F
;
(ff | (FreeGenSetNSG (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 | (FreeGenSetNSG (f,D))) . x =
ff . x
by A23, A22, A25, FUNCT_1:47
.=
pi (
F,
s)
by A2, A26
.=
F . x
by A26, Def14
;
verum end;
FreeGenSetNSG (f,D) = dom F
by FUNCT_2:def 1;
hence
ff | (FreeGenSetNSG (f,D)) = F
by A23, A22, A24, FUNCT_1:2; verum