let A be free Universal_Algebra; for o1, o2 being OperSymbol of A
for p1, p2 being FinSequence st p1 in dom (Den o1,A) & p2 in dom (Den o2,A) & (Den o1,A) . p1 = (Den o2,A) . p2 holds
o1 = o2
consider G being free GeneratorSet of A;
let o1, o2 be OperSymbol of A; for p1, p2 being FinSequence st p1 in dom (Den o1,A) & p2 in dom (Den o2,A) & (Den o1,A) . p1 = (Den o2,A) . p2 holds
o1 = o2
let p1, p2 be FinSequence; ( p1 in dom (Den o1,A) & p2 in dom (Den o2,A) & (Den o1,A) . p1 = (Den o2,A) . p2 implies o1 = o2 )
assume that
A1:
p1 in dom (Den o1,A)
and
A2:
p2 in dom (Den o2,A)
and
A3:
(Den o1,A) . p1 = (Den o2,A) . p2
; o1 = o2
reconsider S = signature A as non empty FinSequence of NAT by MSUALG_1:9;
consider B being Universal_Algebra such that
A4:
the carrier of B = NAT
and
A5:
signature B = S
and
A6:
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 A4;
A,B are_similar
by A5, UNIALG_2:def 2;
then consider h being Function of A,B such that
A7:
h is_homomorphism A,B
and
h | G = f
by FREEALG:def 6;
A8:
len S = len the charact of B
by A5, UNIALG_1:def 11;
A9:
len S = len the charact of A
by UNIALG_1:def 11;
A10:
dom S = dom the charact of B
by A8, FINSEQ_3:31;
A11:
dom S = dom the charact of A
by A9, FINSEQ_3:31;
reconsider b1 = o1, b2 = o2 as OperSymbol of B by A8, A9, FINSEQ_3:31;
reconsider n1 = o1, n2 = o2 as Element of NAT ;
reconsider j1 = S . n1, j2 = S . n2 as Element of NAT ;
reconsider x1 = p1, x2 = p2 as FinSequence of A by A1, A2, FINSEQ_1:def 11;
reconsider h1 = h * x1, h2 = h * x2 as FinSequence of NAT by A4;
reconsider oo1 = Den o1,A, oo2 = Den o2,A as Element of Operations A ;
A12:
dom oo1 = (arity oo1) -tuples_on the carrier of A
by MARGREL1:58;
A13:
dom oo2 = (arity oo2) -tuples_on the carrier of A
by MARGREL1:58;
len x1 =
arity oo1
by A1, A12, FINSEQ_1:def 18
.=
j1
by A11, UNIALG_1:def 11
;
then
len h1 = j1
by FINSEQ_2:37;
then A14:
h1 is Element of j1 -tuples_on NAT
by FINSEQ_2:110;
len x2 =
arity oo2
by A2, A13, FINSEQ_1:def 18
.=
j2
by A11, UNIALG_1:def 11
;
then
len h2 = j2
by FINSEQ_2:37;
then A15:
h2 is Element of j2 -tuples_on NAT
by FINSEQ_2:110;
A16:
Den o1,A is Element of Operations A
;
A17:
Den b1,B is Element of Operations B
;
then A18:
h . ((Den o1,A) . x1) = (Den b1,B) . h1
by A1, A7, A16, ALG_1:def 1;
A19:
h . ((Den o2,A) . x2) = (Den b2,B) . h2
by A2, A7, A16, A17, ALG_1:def 1;
A20:
Den b1,B = (j1 -tuples_on NAT ) --> n1
by A6, A10;
A21:
Den b2,B = (j2 -tuples_on NAT ) --> n2
by A6, A10;
(Den b1,B) . h1 = n1
by A14, A20, FUNCOP_1:13;
hence
o1 = o2
by A3, A15, A18, A19, A21, FUNCOP_1:13; verum