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
set G = the 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:4;
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 = the free GeneratorSet of A --> 0 as Function of the free GeneratorSet of A, the carrier of B by A4;
A,B are_similar
by A5;
then consider h being Function of A,B such that
A7:
h is_homomorphism
and
h | the free GeneratorSet of A = f
by FREEALG:def 5;
A8:
len S = len the charact of B
by A5, UNIALG_1:def 4;
A9:
len S = len the charact of A
by UNIALG_1:def 4;
A10:
dom S = dom the charact of B
by A8, FINSEQ_3:29;
A11:
dom S = dom the charact of A
by A9, FINSEQ_3:29;
reconsider b1 = o1, b2 = o2 as OperSymbol of B by A8, A9, FINSEQ_3:29;
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:22;
A13:
dom oo2 = (arity oo2) -tuples_on the carrier of A
by MARGREL1:22;
len x1 =
arity oo1
by A1, A12, CARD_1:def 7
.=
j1
by A11, UNIALG_1:def 4
;
then
len h1 = j1
by FINSEQ_2:33;
then A14:
h1 is Element of j1 -tuples_on NAT
by FINSEQ_2:92;
len x2 =
arity oo2
by A2, A13, CARD_1:def 7
.=
j2
by A11, UNIALG_1:def 4
;
then
len h2 = j2
by FINSEQ_2:33;
then A15:
h2 is Element of j2 -tuples_on NAT
by FINSEQ_2:92;
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:7;
hence
o1 = o2
by A3, A15, A18, A19, A21, FUNCOP_1:7; verum