:: Free Universal Algebra Construction
:: by Beata Perkowska
::
:: Received October 20, 1993
:: Copyright (c) 1993-2012 Association of Mizar Users


begin

definition
let IT be set ;
attrIT is disjoint_with_NAT  means :Def1: :: FREEALG:def 1
IT misses NAT ;
end;

:: deftheorem Def1 defines disjoint_with_NAT FREEALG:def_1_:_
 for IT being set holds
( IT is disjoint_with_NAT iff IT misses NAT );

registration
cluster non empty disjoint_with_NAT for set ;
existence
 ex b1 being set st
( not b1 is empty & b1 is disjoint_with_NAT )
proofend;
end;

Lm1:  ( not 0 in rng <*1*> &amp; 0 in rng <*0*> )
proofend;

notation
let IT be Relation;
antonym  with_zero IT for  non-empty ;
synonym  without_zero IT for  non-empty ;
end;

definition
let IT be Relation;
redefine attr IT is non-empty  means :Def2: :: FREEALG:def 2
 not 0 in rng IT;
compatibility
 ( not IT is with_zero iff not 0 in rng IT ) by RELAT_1:def_9;
end;

:: deftheorem Def2 defines with_zero FREEALG:def_2_:_
 for IT being Relation holds
( not IT is with_zero iff not 0 in rng IT );

registration
cluster non empty Relation-like with_zero NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like for FinSequence of NAT ;
existence
 ex b1 being FinSequence of NAT st
( not b1 is empty &amp; b1 is with_zero )
proofend;
cluster non empty Relation-like without_zero NAT -defined NAT -valued Function-like V30() FinSequence-like FinSubsequence-like for FinSequence of NAT ;
existence
 ex b1 being FinSequence of NAT st
( not b1 is empty &amp; b1 is without_zero )
proofend;
end;

begin

::
:: Free Universal Algebra - General Notions
::
definition
let U1 be Universal_Algebra;
let n be Element of NAT ;
assume A1: n in dom the charact of U1 ;
func oper (n,U1) ->  operation of U1 equals :Def3: :: FREEALG:def 3
 the charact of U1 . n;
coherence
 the charact of U1 . n is operation of U1 by A1, FUNCT_1:def_3;
end;

:: deftheorem Def3 defines oper FREEALG:def_3_:_
 for U1 being Universal_Algebra
for n being Element of NAT st n in dom the charact of U1 holds
oper (n,U1) = the charact of U1 . n;

definition
let U0 be Universal_Algebra;
mode GeneratorSet of U0 ->  Subset of U0 means :: FREEALG:def 4
 for A being Subset of U0 st A is opers_closed &amp; it c= A holds
A = the carrier of U0;
existence
 ex b1 being Subset of U0 st
for A being Subset of U0 st A is opers_closed &amp; b1 c= A holds
A = the carrier of U0
proofend;
end;

:: deftheorem  defines GeneratorSet FREEALG:def_4_:_
 for U0 being Universal_Algebra
for b2 being Subset of U0 holds
( b2 is GeneratorSet of U0 iff for A being Subset of U0 st A is opers_closed &amp; b2 c= A holds
A = the carrier of U0 );

Lm2:  for A being Universal_Algebra
for B being Subset of A st B is opers_closed holds
Constants A c= B
proofend;

Lm3:  for A being Universal_Algebra
for B being Subset of A st ( B <> {} or Constants A <> {} ) holds
( B is GeneratorSet of A iff the carrier of (GenUnivAlg B) = the carrier of A )
proofend;

definition
let U0 be Universal_Algebra;
let IT be GeneratorSet of U0;
attrIT is free  means :Def5: :: FREEALG:def 5
 for U1 being Universal_Algebra st U0,U1 are_similar holds
for f being Function of IT, the carrier of U1 ex h being Function of U0,U1 st
( h is_homomorphism U0,U1 &amp; h | IT = f );
end;

:: deftheorem Def5 defines free FREEALG:def_5_:_
 for U0 being Universal_Algebra
for IT being GeneratorSet of U0 holds
( IT is free iff for U1 being Universal_Algebra st U0,U1 are_similar holds
for f being Function of IT, the carrier of U1 ex h being Function of U0,U1 st
( h is_homomorphism U0,U1 &amp; h | IT = f ) );

definition
let IT be Universal_Algebra;
attrIT is free  means :Def6: :: FREEALG:def 6
 ex G being GeneratorSet of IT st G is free ;
end;

:: deftheorem Def6 defines free FREEALG:def_6_:_
 for IT being Universal_Algebra holds
( IT is free iff ex G being GeneratorSet of IT st G is free );

registration
cluster non empty strict V109() quasi_total non-empty free for UAStr ;
existence
 ex b1 being Universal_Algebra st
( b1 is free &amp; b1 is strict )
proofend;
end;

registration
let U0 be free Universal_Algebra;
cluster free for GeneratorSet of U0;
existence
 ex b1 being GeneratorSet of U0 st b1 is free by Def6;
end;

theorem :: FREEALG:1
for U0 being strict Universal_Algebra
for A being Subset of U0 st ( Constants U0 <> {} or A <> {} ) holds
( A is GeneratorSet of U0 iff GenUnivAlg A = U0 )
proofend;

begin

::
:: Construction of a Decorated Tree Structure for Free Universal Algebra
::
definition
let f be non empty FinSequence of NAT ;
let X be set ;
func REL (f,X) ->  Relation of ((dom f) \/ X),(((dom f) \/ X) *) means :Def7: :: FREEALG:def 7
 for a being Element of (dom f) \/ X
for b being Element of ((dom f) \/ X) * holds
( [a,b] in it iff ( a in dom f &amp; f . a = len b ) );
existence
 ex b1 being Relation of ((dom f) \/ X),(((dom f) \/ X) *) st
for a being Element of (dom f) \/ X
for b being Element of ((dom f) \/ X) * holds
( [a,b] in b1 iff ( a in dom f &amp; f . a = len b ) )
proofend;
uniqueness
 for b1, b2 being Relation of ((dom f) \/ X),(((dom f) \/ X) *) st ( for a being Element of (dom f) \/ X
for b being Element of ((dom f) \/ X) * holds
( [a,b] in b1 iff ( a in dom f &amp; f . a = len b ) ) ) &amp; ( for a being Element of (dom f) \/ X
for b being Element of ((dom f) \/ X) * holds
( [a,b] in b2 iff ( a in dom f &amp; f . a = len b ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines REL FREEALG:def_7_:_
 for f being non empty FinSequence of NAT
for X being set
for b3 being Relation of ((dom f) \/ X),(((dom f) \/ X) *) holds
( b3 = REL (f,X) iff for a being Element of (dom f) \/ X
for b being Element of ((dom f) \/ X) * holds
( [a,b] in b3 iff ( a in dom f &amp; f . a = len b ) ) );

definition
let f be non empty FinSequence of NAT ;
let X be set ;
func DTConUA (f,X) ->  strict DTConstrStr  equals :: FREEALG:def 8
 DTConstrStr(# ((dom f) \/ X),(REL (f,X)) #);
correctness
coherence
DTConstrStr(# ((dom f) \/ X),(REL (f,X)) #) is strict DTConstrStr ;
;
end;

:: deftheorem  defines DTConUA FREEALG:def_8_:_
 for f being non empty FinSequence of NAT
for X being set holds DTConUA (f,X) = DTConstrStr(# ((dom f) \/ X),(REL (f,X)) #);

registration
let f be non empty FinSequence of NAT ;
let X be set ;
cluster DTConUA (f,X) ->  non empty strict ;
coherence
 not DTConUA (f,X) is empty ;
end;

theorem Th2: :: FREEALG:2
for f being non empty FinSequence of NAT
for X being set holds
( Terminals (DTConUA (f,X)) c= X &amp; NonTerminals (DTConUA (f,X)) = dom f )
proofend;

theorem Th3: :: FREEALG:3
for f being non empty FinSequence of NAT
for X being disjoint_with_NAT set holds Terminals (DTConUA (f,X)) = X
proofend;

registration
let f be non empty FinSequence of NAT ;
let X be set ;
cluster DTConUA (f,X) ->  strict with_nonterminals ;
coherence
 DTConUA (f,X) is with_nonterminals
proofend;
end;

registration
let f be non empty with_zero FinSequence of NAT ;
let X be set ;
cluster DTConUA (f,X) ->  strict with_nonterminals with_useful_nonterminals ;
coherence
 ( DTConUA (f,X) is with_nonterminals &amp; DTConUA (f,X) is with_useful_nonterminals )
proofend;
end;

registration
let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
cluster DTConUA (f,D) ->  strict with_terminals with_nonterminals with_useful_nonterminals ;
coherence
 ( DTConUA (f,D) is with_terminals &amp; DTConUA (f,D) is with_nonterminals &amp; DTConUA (f,D) is with_useful_nonterminals )
proofend;
end;

definition
let f be non empty FinSequence of NAT ;
let X be set ;
let n be Nat;
assume A1: n in dom f ;
func Sym (n,f,X) ->  Symbol of (DTConUA (f,X)) equals :Def9: :: FREEALG:def 9
n;
coherence
 n is Symbol of (DTConUA (f,X)) by A1, XBOOLE_0:def_3;
end;

:: deftheorem Def9 defines Sym FREEALG:def_9_:_
 for f being non empty FinSequence of NAT
for X being set
for n being Nat st n in dom f holds
Sym (n,f,X) = n;

begin

::
:: Construction of Free Universal Algebra for Non Empty Set of Generators and
:: Given Signature
definition
let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
let n be Nat;
assume A1: n in dom f ;
func FreeOpNSG (n,f,D) ->  non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) means :Def10: :: FREEALG:def 10
( dom it = (f /. n) -tuples_on (TS (DTConUA (f,D))) &amp; ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom it holds
it . p = (Sym (n,f,D)) -tree p ) );
existence
 ex b1 being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st
( dom b1 = (f /. n) -tuples_on (TS (DTConUA (f,D))) &amp; ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b1 holds
b1 . p = (Sym (n,f,D)) -tree p ) )
proofend;
uniqueness
 for b1, b2 being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st dom b1 = (f /. n) -tuples_on (TS (DTConUA (f,D))) &amp; ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b1 holds
b1 . p = (Sym (n,f,D)) -tree p ) &amp; dom b2 = (f /. n) -tuples_on (TS (DTConUA (f,D))) &amp; ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b2 holds
b2 . p = (Sym (n,f,D)) -tree p ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines FreeOpNSG FREEALG:def_10_:_
 for f being non empty FinSequence of NAT
for D being non empty disjoint_with_NAT set
for n being Nat st n in dom f holds
for b4 being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) holds
( b4 = FreeOpNSG (n,f,D) iff ( dom b4 = (f /. n) -tuples_on (TS (DTConUA (f,D))) &amp; ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b4 holds
b4 . p = (Sym (n,f,D)) -tree p ) ) );

definition
let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
func FreeOpSeqNSG (f,D) ->  PFuncFinSequence of (TS (DTConUA (f,D))) means :Def11: :: FREEALG:def 11
( len it = len f &amp; ( for n being Element of NAT st n in dom it holds
it . n = FreeOpNSG (n,f,D) ) );
existence
 ex b1 being PFuncFinSequence of (TS (DTConUA (f,D))) st
( len b1 = len f &amp; ( for n being Element of NAT st n in dom b1 holds
b1 . n = FreeOpNSG (n,f,D) ) )
proofend;
uniqueness
 for b1, b2 being PFuncFinSequence of (TS (DTConUA (f,D))) st len b1 = len f &amp; ( for n being Element of NAT st n in dom b1 holds
b1 . n = FreeOpNSG (n,f,D) ) &amp; len b2 = len f &amp; ( for n being Element of NAT st n in dom b2 holds
b2 . n = FreeOpNSG (n,f,D) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines FreeOpSeqNSG FREEALG:def_11_:_
 for f being non empty FinSequence of NAT
for D being non empty disjoint_with_NAT set
for b3 being PFuncFinSequence of (TS (DTConUA (f,D))) holds
( b3 = FreeOpSeqNSG (f,D) iff ( len b3 = len f &amp; ( for n being Element of NAT st n in dom b3 holds
b3 . n = FreeOpNSG (n,f,D) ) ) );

definition
let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
func FreeUnivAlgNSG (f,D) ->  strict Universal_Algebra equals :: FREEALG:def 12
 UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #);
coherence
 UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) is strict Universal_Algebra
proofend;
end;

:: deftheorem  defines FreeUnivAlgNSG FREEALG:def_12_:_
 for f being non empty FinSequence of NAT
for D being non empty disjoint_with_NAT set holds FreeUnivAlgNSG (f,D) = UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #);

theorem Th4: :: FREEALG:4
for f being non empty FinSequence of NAT
for D being non empty disjoint_with_NAT set holds signature (FreeUnivAlgNSG (f,D)) = f
proofend;

definition
let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
func FreeGenSetNSG (f,D) ->  Subset of (FreeUnivAlgNSG (f,D)) equals :: FREEALG:def 13
 {  (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D))  }  ;
coherence
  {  (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D))  }  is Subset of (FreeUnivAlgNSG (f,D))
proofend;
end;

:: deftheorem  defines FreeGenSetNSG FREEALG:def_13_:_
 for f being non empty FinSequence of NAT
for D being non empty disjoint_with_NAT set holds FreeGenSetNSG (f,D) =  {  (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D))  }  ;

theorem Th5: :: FREEALG:5
for f being non empty FinSequence of NAT
for D being non empty disjoint_with_NAT set holds not FreeGenSetNSG (f,D) is empty
proofend;

definition
let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
:: original:FreeGenSetNSG
redefine func FreeGenSetNSG (f,D) ->  GeneratorSet of FreeUnivAlgNSG (f,D);
coherence
 FreeGenSetNSG (f,D) is GeneratorSet of FreeUnivAlgNSG (f,D)
proofend;
end;

definition
let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
let C be non empty set ;
let s be Symbol of (DTConUA (f,D));
let F be Function of (FreeGenSetNSG (f,D)),C;
assume A1: s in Terminals (DTConUA (f,D)) ;
func pi (F,s) ->  Element of C equals :Def14: :: FREEALG:def 14
F . (root-tree s);
coherence
 F . (root-tree s) is Element of C
proofend;
end;

:: deftheorem Def14 defines pi FREEALG:def_14_:_
 for f being non empty FinSequence of NAT
for D being non empty disjoint_with_NAT set
for C being non empty set
for s being Symbol of (DTConUA (f,D))
for F being Function of (FreeGenSetNSG (f,D)),C st s in Terminals (DTConUA (f,D)) holds
pi (F,s) = F . (root-tree s);

definition
let f be non empty FinSequence of NAT ;
let D be set ;
let s be Symbol of (DTConUA (f,D));
given p being FinSequence such that A1: s ==> p ;
func @ s ->  Element of NAT  equals :Def15: :: FREEALG:def 15
s;
coherence
 s is Element of NAT
proofend;
end;

:: deftheorem Def15 defines @ FREEALG:def_15_:_
 for f being non empty FinSequence of NAT
for D being set
for s being Symbol of (DTConUA (f,D)) st ex p being FinSequence st s ==> p holds
@ s = s;

theorem Th6: :: FREEALG:6
for f being non empty FinSequence of NAT
for D being non empty disjoint_with_NAT set holds FreeGenSetNSG (f,D) is free
proofend;

registration
let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
cluster FreeUnivAlgNSG (f,D) ->  strict free ;
coherence
 FreeUnivAlgNSG (f,D) is free
proofend;
end;

definition
let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
:: original:FreeGenSetNSG
redefine func FreeGenSetNSG (f,D) ->  free GeneratorSet of FreeUnivAlgNSG (f,D);
coherence
 FreeGenSetNSG (f,D) is free GeneratorSet of FreeUnivAlgNSG (f,D) by Th6;
end;

begin

::
:: Construction of Free Universal Algebra for Given Signature
:: (with at Last One Zero Argument Operation) and Set of Generators
::
definition
let f be non empty with_zero FinSequence of NAT ;
let D be disjoint_with_NAT set ;
let n be Nat;
assume A1: n in dom f ;
func FreeOpZAO (n,f,D) ->  non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) means :Def16: :: FREEALG:def 16
( dom it = (f /. n) -tuples_on (TS (DTConUA (f,D))) &amp; ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom it holds
it . p = (Sym (n,f,D)) -tree p ) );
existence
 ex b1 being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st
( dom b1 = (f /. n) -tuples_on (TS (DTConUA (f,D))) &amp; ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b1 holds
b1 . p = (Sym (n,f,D)) -tree p ) )
proofend;
uniqueness
 for b1, b2 being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st dom b1 = (f /. n) -tuples_on (TS (DTConUA (f,D))) &amp; ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b1 holds
b1 . p = (Sym (n,f,D)) -tree p ) &amp; dom b2 = (f /. n) -tuples_on (TS (DTConUA (f,D))) &amp; ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b2 holds
b2 . p = (Sym (n,f,D)) -tree p ) holds
b1 = b2
proofend;
end;

:: deftheorem Def16 defines FreeOpZAO FREEALG:def_16_:_
 for f being non empty with_zero FinSequence of NAT
for D being disjoint_with_NAT set
for n being Nat st n in dom f holds
for b4 being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) holds
( b4 = FreeOpZAO (n,f,D) iff ( dom b4 = (f /. n) -tuples_on (TS (DTConUA (f,D))) &amp; ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b4 holds
b4 . p = (Sym (n,f,D)) -tree p ) ) );

definition
let f be non empty with_zero FinSequence of NAT ;
let D be disjoint_with_NAT set ;
func FreeOpSeqZAO (f,D) ->  PFuncFinSequence of (TS (DTConUA (f,D))) means :Def17: :: FREEALG:def 17
( len it = len f &amp; ( for n being Element of NAT st n in dom it holds
it . n = FreeOpZAO (n,f,D) ) );
existence
 ex b1 being PFuncFinSequence of (TS (DTConUA (f,D))) st
( len b1 = len f &amp; ( for n being Element of NAT st n in dom b1 holds
b1 . n = FreeOpZAO (n,f,D) ) )
proofend;
uniqueness
 for b1, b2 being PFuncFinSequence of (TS (DTConUA (f,D))) st len b1 = len f &amp; ( for n being Element of NAT st n in dom b1 holds
b1 . n = FreeOpZAO (n,f,D) ) &amp; len b2 = len f &amp; ( for n being Element of NAT st n in dom b2 holds
b2 . n = FreeOpZAO (n,f,D) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines FreeOpSeqZAO FREEALG:def_17_:_
 for f being non empty with_zero FinSequence of NAT
for D being disjoint_with_NAT set
for b3 being PFuncFinSequence of (TS (DTConUA (f,D))) holds
( b3 = FreeOpSeqZAO (f,D) iff ( len b3 = len f &amp; ( for n being Element of NAT st n in dom b3 holds
b3 . n = FreeOpZAO (n,f,D) ) ) );

definition
let f be non empty with_zero FinSequence of NAT ;
let D be disjoint_with_NAT set ;
func FreeUnivAlgZAO (f,D) ->  strict Universal_Algebra equals :: FREEALG:def 18
 UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #);
coherence
 UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) is strict Universal_Algebra
proofend;
end;

:: deftheorem  defines FreeUnivAlgZAO FREEALG:def_18_:_
 for f being non empty with_zero FinSequence of NAT
for D being disjoint_with_NAT set holds FreeUnivAlgZAO (f,D) = UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #);

theorem Th7: :: FREEALG:7
for f being non empty with_zero FinSequence of NAT
for D being disjoint_with_NAT set holds signature (FreeUnivAlgZAO (f,D)) = f
proofend;

theorem Th8: :: FREEALG:8
for f being non empty with_zero FinSequence of NAT
for D being disjoint_with_NAT set holds FreeUnivAlgZAO (f,D) is with_const_op
proofend;

theorem Th9: :: FREEALG:9
for f being non empty with_zero FinSequence of NAT
for D being disjoint_with_NAT set holds Constants (FreeUnivAlgZAO (f,D)) <> {}
proofend;

definition
let f be non empty with_zero FinSequence of NAT ;
let D be disjoint_with_NAT set ;
func FreeGenSetZAO (f,D) ->  Subset of (FreeUnivAlgZAO (f,D)) equals :: FREEALG:def 19
 {  (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D))  }  ;
coherence
  {  (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D))  }  is Subset of (FreeUnivAlgZAO (f,D))
proofend;
end;

:: deftheorem  defines FreeGenSetZAO FREEALG:def_19_:_
 for f being non empty with_zero FinSequence of NAT
for D being disjoint_with_NAT set holds FreeGenSetZAO (f,D) =  {  (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D))  }  ;

definition
let f be non empty with_zero FinSequence of NAT ;
let D be disjoint_with_NAT set ;
:: original:FreeGenSetZAO
redefine func FreeGenSetZAO (f,D) ->  GeneratorSet of FreeUnivAlgZAO (f,D);
coherence
 FreeGenSetZAO (f,D) is GeneratorSet of FreeUnivAlgZAO (f,D)
proofend;
end;

definition
let f be non empty with_zero FinSequence of NAT ;
let D be disjoint_with_NAT set ;
let C be non empty set ;
let s be Symbol of (DTConUA (f,D));
let F be Function of (FreeGenSetZAO (f,D)),C;
assume A1: s in Terminals (DTConUA (f,D)) ;
func pi (F,s) ->  Element of C equals :Def20: :: FREEALG:def 20
F . (root-tree s);
coherence
 F . (root-tree s) is Element of C
proofend;
end;

:: deftheorem Def20 defines pi FREEALG:def_20_:_
 for f being non empty with_zero FinSequence of NAT
for D being disjoint_with_NAT set
for C being non empty set
for s being Symbol of (DTConUA (f,D))
for F being Function of (FreeGenSetZAO (f,D)),C st s in Terminals (DTConUA (f,D)) holds
pi (F,s) = F . (root-tree s);

theorem Th10: :: FREEALG:10
for f being non empty with_zero FinSequence of NAT
for D being disjoint_with_NAT set holds FreeGenSetZAO (f,D) is free
proofend;

registration
let f be non empty with_zero FinSequence of NAT ;
let D be disjoint_with_NAT set ;
cluster FreeUnivAlgZAO (f,D) ->  strict free ;
coherence
 FreeUnivAlgZAO (f,D) is free
proofend;
end;

definition
let f be non empty with_zero FinSequence of NAT ;
let D be disjoint_with_NAT set ;
:: original:FreeGenSetZAO
redefine func FreeGenSetZAO (f,D) ->  free GeneratorSet of FreeUnivAlgZAO (f,D);
coherence
 FreeGenSetZAO (f,D) is free GeneratorSet of FreeUnivAlgZAO (f,D) by Th10;
end;

registration
cluster non empty strict V109() quasi_total non-empty with_const_op free for UAStr ;
existence
 ex b1 being Universal_Algebra st
( b1 is strict &amp; b1 is free &amp; b1 is with_const_op )
proofend;
end;