let A be free Universal_Algebra; for G being free GeneratorSet of A holds G = Generators A
let G be free GeneratorSet of A; G = Generators A
reconsider S = signature A as non empty FinSequence of NAT by MSUALG_1:4;
consider B being Universal_Algebra such that
A1:
the carrier of B = NAT
and
A2:
signature B = S
and
A3:
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 A2;
then consider h being Function of A,B such that
A4:
h is_homomorphism
and
A5:
h | G = f
by FREEALG:def 5;
A6:
len S = len the charact of B
by A2, UNIALG_1:def 4;
A7:
len S = len the charact of A
by UNIALG_1:def 4;
A8:
dom S = dom the charact of B
by A6, FINSEQ_3:29;
A9:
dom S = dom the charact of A
by A7, FINSEQ_3:29;
thus
G c= Generators A
XBOOLE_0:def 10 Generators A c= Gproof
let a be
object ;
TARSKI:def 3 ( a nin G or not a nin Generators A )
assume A10:
a in G
;
not a nin Generators A
then reconsider I =
a as
Element of
A ;
assume
a nin Generators A
;
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 A11:
I in Y
and A12:
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 A13:
Y = rng o
by A12;
consider i being
object such that A14:
i in dom the
charact of
A
and A15:
o = the
charact of
A . i
by FUNCT_1:def 3;
reconsider i =
i as
Element of
NAT by A14;
reconsider j =
S . i as
Element of
NAT ;
reconsider o2 = the
charact of
B . i as
Element of
Operations B by A8, A9, A14, FUNCT_1:def 3;
consider x being
object such that A16:
x in dom o
and A17:
I = o . x
by A11, A13, FUNCT_1:def 3;
A18:
dom o = (arity o) -tuples_on the
carrier of
A
by MARGREL1:22;
reconsider x =
x as
FinSequence of
A by A16, FINSEQ_1:def 11;
reconsider hx =
h * x as
FinSequence of
NAT by A1;
len (h * x) =
len x
by FINSEQ_2:33
.=
arity o
by A16, A18, CARD_1:def 7
.=
j
by A9, A14, A15, UNIALG_1:def 4
;
then A19:
hx is
Element of
j -tuples_on NAT
by FINSEQ_2:92;
0 =
f . I
by A10, FUNCOP_1:7
.=
h . (o . x)
by A5, A10, A17, FUNCT_1:49
.=
o2 . (h * x)
by A4, A14, A15, A16, ALG_1:def 1
.=
((j -tuples_on NAT) --> i) . (h * x)
by A3, A9, A14
.=
i
by A19, FUNCOP_1:7
;
hence
contradiction
by A14, FINSEQ_3:25;
verum
end;
let a be object ; TARSKI:def 3 ( a nin Generators A or not a nin G )
assume A20:
a in Generators A
; not a nin G
then A21:
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 A20;
assume
a nin G
; contradiction
then consider o0 being Element of Operations A such that
A22:
I in rng o0
by Th32;
rng o0 in { (rng o) where o is Element of Operations A : verum }
;
hence
contradiction
by A21, A22, TARSKI:def 4; verum