let f be non empty FinSequence of NAT ; :: thesis: for D being non empty disjoint_with_NAT set holds FreeGenSetNSG f,D is free
let D be non empty disjoint_with_NAT set ; :: thesis: FreeGenSetNSG f,D is free
set fgs = FreeGenSetNSG f,D;
set fua = FreeUnivAlgNSG f,D;
let U1 be Universal_Algebra; :: according to FREEALG:def 6 :: thesis: ( 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 FreeUnivAlgNSG f,D,U1 & h | (FreeGenSetNSG f,D) = f ) )
assume A1:
FreeUnivAlgNSG f,D,U1 are_similar
; :: thesis: 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 FreeUnivAlgNSG f,D,U1 & h | (FreeGenSetNSG f,D) = f )
let F be Function of (FreeGenSetNSG f,D),the carrier of U1; :: thesis: ex h being Function of (FreeUnivAlgNSG f,D),U1 st
( h is_homomorphism FreeUnivAlgNSG f,D,U1 & h | (FreeGenSetNSG f,D) = F )
set A = DTConUA f,D;
set c1 = the carrier of U1;
set cf = the carrier of (FreeUnivAlgNSG f,D);
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
; :: thesis: ( ff is_homomorphism FreeUnivAlgNSG f,D,U1 & ff | (FreeGenSetNSG f,D) = F )
for n being Element of 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
let n be
Element of
NAT ;
:: thesis: ( 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 A4:
n in dom the
charact of
(FreeUnivAlgNSG f,D)
;
:: thesis: 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);
:: thesis: 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;
:: thesis: ( 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 A5:
(
o1 = the
charact of
(FreeUnivAlgNSG f,D) . n &
o2 = the
charact of
U1 . n )
;
:: thesis: 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);
:: thesis: ( x in dom o1 implies ff . (o1 . x) = o2 . (ff * x) )
assume A6:
x in dom o1
;
:: thesis: ff . (o1 . x) = o2 . (ff * x)
reconsider xa =
x as
FinSequence of
TS (DTConUA f,D) ;
A7:
(
len (FreeOpSeqNSG f,D) = len f &
Seg (len f) = dom f &
dom (FreeOpSeqNSG f,D) = Seg (len (FreeOpSeqNSG f,D)) & the
charact of
(FreeUnivAlgNSG f,D) = the
charact of
(FreeUnivAlgNSG f,D) )
by Def12, FINSEQ_1:def 3;
then A8:
(
n in dom f &
f = signature (FreeUnivAlgNSG f,D) )
by A4, Th4;
dom o1 =
(arity o1) -tuples_on the
carrier of
(FreeUnivAlgNSG f,D)
by UNIALG_2:2
.=
{ w where w is Element of the carrier of (FreeUnivAlgNSG f,D) * : len w = arity o1 }
;
then consider w being
Element of the
carrier of
(FreeUnivAlgNSG f,D) * such that A9:
(
x = w &
len w = arity o1 )
by A6;
A10:
(
f /. n = f . n &
f = signature (FreeUnivAlgNSG f,D) &
(signature (FreeUnivAlgNSG f,D)) . n = arity o1 )
by A5, A8, PARTFUN1:def 8, UNIALG_1:def 11;
dom (roots xa) =
dom xa
by TREES_3:def 18
.=
Seg (len xa)
by FINSEQ_1:def 3
;
then A11:
len (roots xa) = len xa
by FINSEQ_1:def 3;
reconsider nt =
n as
Symbol of
(DTConUA f,D) by A4, A7, XBOOLE_0:def 3;
reconsider nd =
n as
Element of
(dom f) \/ D by A4, A7, XBOOLE_0: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;
[nd,rxa] in REL f,
D
by A4, A7, A9, A10, A11, Def8;
then A12:
nt ==> roots xa
by LANG1:def 1;
then A13:
ff . (nt -tree xa) = (oper (@ nt),U1) /. (ff * x)
by A3;
A14:
@ nt = n
by A12, Def16;
(
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) &
Seg (len the charact of U1) = dom the
charact of
U1 )
by A1, FINSEQ_1:def 3, UNIALG_2:3;
then A15:
oper (@ nt),
U1 = o2
by A4, A5, A14, Def4;
A16:
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 }
;
A17:
len (ff * x) = len x
by ALG_1:1;
signature (FreeUnivAlgNSG f,D) = signature U1
by A1, UNIALG_2:def 2;
then A18:
arity o2 = len x
by A4, A5, A7, A9, A10, UNIALG_1:def 11;
reconsider fx =
ff * x as
Element of the
carrier of
U1 * ;
A19:
fx in { v where v is Element of the carrier of U1 * : len v = arity o2 }
by A17, A18;
A20:
Sym n,
f,
D = nt
by A4, A7, Def10;
A21:
dom (FreeOpNSG n,f,D) =
(f /. n) -tuples_on (TS (DTConUA f,D))
by A4, A7, Def11
.=
{ g where g is Element of (TS (DTConUA f,D)) * : len g = f /. n }
;
reconsider xa =
xa as
Element of
(TS (DTConUA f,D)) * by FINSEQ_1:def 11;
A22:
xa in dom (FreeOpNSG n,f,D)
by A9, A10, A21;
o1 = FreeOpNSG n,
f,
D
by A4, A5, Def12;
then
o1 . x = nt -tree xa
by A4, A7, A20, A22, Def11;
hence
ff . (o1 . x) = o2 . (ff * x)
by A13, A15, A16, A19, PARTFUN1:def 8;
:: thesis: verum
end;
hence
ff is_homomorphism FreeUnivAlgNSG f,D,U1
by A1, ALG_1:def 1; :: thesis: ff | (FreeGenSetNSG f,D) = F
A23:
( dom (ff | (FreeGenSetNSG f,D)) = (dom ff) /\ (FreeGenSetNSG f,D) & dom ff = the carrier of (FreeUnivAlgNSG f,D) & the carrier of (FreeUnivAlgNSG f,D) /\ (FreeGenSetNSG f,D) = FreeGenSetNSG f,D & FreeGenSetNSG f,D = dom F )
by FUNCT_2:def 1, RELAT_1:90, XBOOLE_1:28;
now let x be
set ;
:: thesis: ( x in dom F implies (ff | (FreeGenSetNSG f,D)) . x = F . x )assume A24:
x in dom F
;
:: thesis: (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 A25:
(
x = root-tree s &
s in Terminals (DTConUA f,D) )
;
thus (ff | (FreeGenSetNSG f,D)) . x =
ff . x
by A23, A24, FUNCT_1:70
.=
pi F,
s
by A2, A25
.=
F . x
by A25, Def15
;
:: thesis: verum end;
hence
ff | (FreeGenSetNSG f,D) = F
by A23, FUNCT_1:9; :: thesis: verum