let A be free Universal_Algebra; :: thesis: for G being free GeneratorSet of A holds G = Generators A
let G be free GeneratorSet of A; :: thesis: G = Generators A
reconsider S = signature A as non empty FinSequence of NAT by MSUALG_1:9;
consider B being Universal_Algebra such that
A1:
( the carrier of B = NAT & signature B = S )
and
A2:
for i, j being Nat st i in dom S & j = S . i holds
the charact of B . i = (j -tuples_on NAT ) --> i
by Th14;
reconsider f = G --> 0 as Function of G,the carrier of B by A1;
A,B are_similar
by A1, UNIALG_2:def 2;
then consider h being Function of A,B such that
A3:
( h is_homomorphism A,B & h | G = f )
by FREEALG:def 6;
( len S = len the charact of B & len S = len the charact of A )
by A1, UNIALG_1:def 11;
then A4:
( dom S = dom the charact of B & dom S = dom the charact of A )
by FINSEQ_3:31;
thus
G c= Generators A
:: according to XBOOLE_0:def 10 :: thesis: Generators A c= Gproof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( a nin G or not a nin Generators A )
assume A5:
a in G
;
:: thesis: not a nin Generators A
then reconsider I =
a as
Element of
A ;
assume
a nin Generators A
;
:: thesis: contradiction
then
I in union { (rng o) where o is Element of Operations A : verum }
by XBOOLE_0:def 5;
then consider Y being
set such that A6:
(
I in Y &
Y in { (rng o) where o is Element of Operations A : verum } )
by TARSKI:def 4;
consider o being
Element of
Operations A such that A7:
Y = rng o
by A6;
consider i being
set such that A8:
(
i in dom the
charact of
A &
o = the
charact of
A . i )
by FUNCT_1:def 5;
reconsider i =
i as
Element of
NAT by A8;
reconsider j =
S . i as
Element of
NAT ;
reconsider o2 = the
charact of
B . i as
Element of
Operations B by A4, A8, FUNCT_1:def 5;
consider x being
set such that A9:
(
x in dom o &
I = o . x )
by A6, A7, FUNCT_1:def 5;
A10:
dom o = (arity o) -tuples_on the
carrier of
A
by UNIALG_2:2;
reconsider x =
x as
FinSequence of
A by A9, FINSEQ_1:def 11;
reconsider hx =
h * x as
FinSequence of
NAT by A1;
len (h * x) =
len x
by FINSEQ_2:37
.=
arity o
by A10, A9, FINSEQ_1:def 18
.=
j
by A4, A8, UNIALG_1:def 11
;
then A11:
hx is
Element of
j -tuples_on NAT
by FINSEQ_2:110;
0 =
f . I
by A5, FUNCOP_1:13
.=
h . (o . x)
by A3, A5, A9, FUNCT_1:72
.=
o2 . (h * x)
by A3, A8, A9, ALG_1:def 1
.=
((j -tuples_on NAT ) --> i) . (h * x)
by A2, A4, A8
.=
i
by A11, FUNCOP_1:13
;
hence
contradiction
by A8, FINSEQ_3:27;
:: thesis: verum
end;
let a be set ; :: according to TARSKI:def 3 :: thesis: ( a nin Generators A or not a nin G )
assume A12:
a in Generators A
; :: thesis: not a nin G
then A13:
( a in the carrier of A & a nin union { (rng o) where o is Element of Operations A : verum } )
by XBOOLE_0:def 5;
reconsider I = a as Element of A by A12;
assume
a nin G
; :: thesis: contradiction
then consider o0 being Element of Operations A such that
A14:
I in rng o0
by Th32;
rng o0 in { (rng o) where o is Element of Operations A : verum }
;
hence
contradiction
by A13, A14, TARSKI:def 4; :: thesis: verum