begin
Lm1:
( not 0 in rng <*1*> & 0 in rng <*0*> )
begin
Lm2:
for A being Universal_Algebra
for B being Subset of A st B is opers_closed holds
Constants A c= B
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 )
begin
begin
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
;
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))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b1 holds
b1 . p = (Sym (n,f,D)) -tree p ) )
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))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b1 holds
b1 . p = (Sym (n,f,D)) -tree p ) & dom b2 = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( 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
end;
begin
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
;
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))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b1 holds
b1 . p = (Sym (n,f,D)) -tree p ) )
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))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b1 holds
b1 . p = (Sym (n,f,D)) -tree p ) & dom b2 = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( 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
end;
:: Free Universal Algebra - General Notions
::