let f be non empty with_zero FinSequence of NAT ; :: thesis:
let D be disjoint_with_NAT set ; :: thesis:
set fgs = FreeGenSetZAO (f,D);
set fua = FreeUnivAlgZAO (f,D);
let U1 be Universal_Algebra; :: according to FREEALG:def 5 :: thesis:
assume A1: FreeUnivAlgZAO (f,D),U1 are_similar ; :: thesis:
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; :: thesis:
deffunc H₁( Symbol of (DTConUA (f,D))) -> Element of the carrier of U1 = pi (F,$1);
deffunc H₂( 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) = H₁(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) = H₂(nt, roots ts,ff * ts) from DTCONSTR:sch 8();
reconsider ff = ff as Function of (FreeUnivAlgZAO (f,D)),U1 ;
take ff ; :: thesis:
for n being 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 Nat; :: thesis:
assume A5: n in dom the charact of (FreeUnivAlgZAO (f,D)) ; :: thesis:
let o1 be operation of (FreeUnivAlgZAO (f,D)); :: thesis:
let o2 be operation of U1; :: thesis:
assume that
A6: o1 = the charact of (FreeUnivAlgZAO (f,D)) . n and
A7: o2 = the charact of U1 . n ; :: thesis:
let x be FinSequence of (FreeUnivAlgZAO (f,D)); :: thesis:
assume A8: x in dom o1 ; :: thesis:
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 MARGREL1:22
.= { 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, Def17;
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 (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:1;
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 Def17, 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 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 (FreeUnivAlgZAO (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, Def16;
hence ff . (o1 . x) = o2 . (ff * x) by A19, A20, A12, A21, PARTFUN1:def 6; :: thesis:

end;

hence ff is_homomorphism by A1, ALG_1:def 1; :: thesis:
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:61;

A24: now :: thesis:

let x be object ; :: thesis:
assume A25: x in dom F ; :: thesis:
then 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:47
.= pi (F,s) by A2, A26
.= F . x by A26, Def20 ; :: thesis:

end;

FreeGenSetZAO (f,D) = dom F by FUNCT_2:def 1;
hence ff | (FreeGenSetZAO (f,D)) = F by A23, A22, A24, FUNCT_1:2; :: thesis: