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 & p1 = p2 )
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 & p1 = p2 )
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 & p1 = p2 ) )
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 & p1 = p2 )
thus A4:
o1 = o2
by A1, A2, A3, Lm2; p1 = p2
reconsider S = signature A as non empty FinSequence of NAT by MSUALG_1:4;
set G9 = the free GeneratorSet of A \/ { the carrier of A};
reconsider G9 = the free GeneratorSet of A \/ { the carrier of A} as non empty set ;
deffunc H1( object ) -> set = root-tree [0,$1];
consider g being Function such that
A5:
( dom g = the free GeneratorSet of A & ( for x being object st x in the free GeneratorSet of A holds
g . x = H1(x) ) )
from FUNCT_1:sch 3();
set X = [:{0},G9:];
set B = FreeUnivAlgNSG (S,[:{0},G9:]);
A6:
signature (FreeUnivAlgNSG (S,[:{0},G9:])) = S
by FREEALG:4;
A7:
Terminals (DTConUA (S,[:{0},G9:])) = [:{0},G9:]
by FREEALG:3;
rng g c= FreeGenSetNSG (S,[:{0},G9:])
proof
let b be
object ;
TARSKI:def 3 ( b nin rng g or not b nin FreeGenSetNSG (S,[:{0},G9:]) )
assume
b in rng g
;
not b nin FreeGenSetNSG (S,[:{0},G9:])
then consider a being
object such that A8:
a in dom g
and A9:
b = g . a
by FUNCT_1:def 3;
reconsider a =
a as
Element of
A by A5, A8;
A10:
a in G9
by A5, A8, XBOOLE_0:def 3;
0 in {0}
by TARSKI:def 1;
then A11:
[0,a] in [:{0},G9:]
by A10, ZFMISC_1:87;
then reconsider s =
[0,a] as
Symbol of
(DTConUA (S,[:{0},G9:])) by A7;
root-tree s in FreeGenSetNSG (
S,
[:{0},G9:])
by A7, A11;
hence
not
b nin FreeGenSetNSG (
S,
[:{0},G9:])
by A5, A8, A9;
verum
end;
then reconsider g = g as Function of the free GeneratorSet of A, the carrier of (FreeUnivAlgNSG (S,[:{0},G9:])) by A5, FUNCT_2:2, XBOOLE_1:1;
signature (FreeUnivAlgNSG (S,[:{0},G9:])) = S
by FREEALG:4;
then
A, FreeUnivAlgNSG (S,[:{0},G9:]) are_similar
;
then consider h being Function of A,(FreeUnivAlgNSG (S,[:{0},G9:])) such that
A12:
h is_homomorphism
and
A13:
h | the free GeneratorSet of A = g
by FREEALG:def 5;
defpred S1[ Nat] means for a1, a2 being set st a1 in the free GeneratorSet of A |^ $1 & a2 in the free GeneratorSet of A |^ $1 & h . a1 = h . a2 holds
a1 = a2;
A14:
the free GeneratorSet of A |^ 0 = the free GeneratorSet of A
by Th18;
A15:
len S = len the charact of (FreeUnivAlgNSG (S,[:{0},G9:]))
by A6, UNIALG_1:def 4;
A16:
len S = len the charact of A
by UNIALG_1:def 4;
A17:
dom S = dom the charact of (FreeUnivAlgNSG (S,[:{0},G9:]))
by A15, FINSEQ_3:29;
A18:
now for o being Element of dom the charact of A
for p being FinSequence of A st p in dom (Den (o,A)) holds
( len p = S . o & len (h * p) = S . o & h . ((Den (o,A)) . p) = o -tree (h * p) )let o be
Element of
dom the
charact of
A;
for p being FinSequence of A st p in dom (Den (o,A)) holds
( len p = S . o & len (h * p) = S . o & h . ((Den (o,A)) . p) = o -tree (h * p) )let p be
FinSequence of
A;
( p in dom (Den (o,A)) implies ( len p = S . o & len (h * p) = S . o & h . ((Den (o,A)) . p) = o -tree (h * p) ) )assume A19:
p in dom (Den (o,A))
;
( len p = S . o & len (h * p) = S . o & h . ((Den (o,A)) . p) = o -tree (h * p) )reconsider q =
p as
FinSequence of
A ;
reconsider hq =
h * q as
FinSequence of
(FreeUnivAlgNSG (S,[:{0},G9:])) ;
reconsider op =
Den (
o,
A) as
Element of
Operations A ;
reconsider on =
o as
Element of
NAT ;
reconsider o9 =
on as
OperSymbol of
(FreeUnivAlgNSG (S,[:{0},G9:])) by A15, A16, FINSEQ_3:29;
reconsider op9 =
Den (
o9,
(FreeUnivAlgNSG (S,[:{0},G9:]))) as
Element of
Operations (FreeUnivAlgNSG (S,[:{0},G9:])) ;
reconsider j =
S . o9 as
Element of
NAT ;
dom op = (arity op) -tuples_on the
carrier of
A
by MARGREL1:22;
then A20:
len p =
arity op
by A19, CARD_1:def 7
.=
j
by A17, UNIALG_1:def 4
;
hence
(
len p = S . o &
len (h * p) = S . o )
by FINSEQ_2:33;
h . ((Den (o,A)) . p) = o -tree (h * p)A21:
h . (op . q) = op9 . hq
by A12, A19, ALG_1:def 1;
A22:
In (
o9,
(dom the charact of (FreeUnivAlgNSG (S,[:{0},G9:]))))
= o9
;
len hq = S . o9
by A20, FINSEQ_2:33;
hence
h . ((Den (o,A)) . p) = o -tree (h * p)
by A17, A21, A22, Th17;
verum end;
A23:
S1[ 0 ]
proof
let a1,
a2 be
set ;
( a1 in the free GeneratorSet of A |^ 0 & a2 in the free GeneratorSet of A |^ 0 & h . a1 = h . a2 implies a1 = a2 )
assume that A24:
a1 in the
free GeneratorSet of
A |^ 0
and A25:
a2 in the
free GeneratorSet of
A |^ 0
and A26:
h . a1 = h . a2
;
a1 = a2
A27:
h . a1 = g . a1
by A13, A14, A24, FUNCT_1:49;
A28:
h . a2 = g . a2
by A13, A14, A25, FUNCT_1:49;
A29:
h . a1 = H1(
a1)
by A5, A14, A24, A27;
h . a2 = H1(
a2)
by A5, A14, A25, A28;
then
[0,a1] = [0,a2]
by A26, A29, TREES_4:4;
hence
a1 = a2
by XTUPLE_0:1;
verum
end;
A30:
now for o being Element of dom the charact of A
for p being Element of the carrier of A * st p in dom (Den (o,A)) holds
for x being set st x in the free GeneratorSet of A holds
not h . ((Den (o,A)) . p) = h . xlet o be
Element of
dom the
charact of
A;
for p being Element of the carrier of A * st p in dom (Den (o,A)) holds
for x being set st x in the free GeneratorSet of A holds
not h . ((Den (o,A)) . p) = h . xlet p be
Element of the
carrier of
A * ;
( p in dom (Den (o,A)) implies for x being set st x in the free GeneratorSet of A holds
not h . ((Den (o,A)) . p) = h . x )assume
p in dom (Den (o,A))
;
for x being set st x in the free GeneratorSet of A holds
not h . ((Den (o,A)) . p) = h . xthen A31:
h . ((Den (o,A)) . p) = o -tree (h * p)
by A18;
let x be
set ;
( x in the free GeneratorSet of A implies not h . ((Den (o,A)) . p) = h . x )assume A32:
x in the
free GeneratorSet of
A
;
not h . ((Den (o,A)) . p) = h . xthen A33:
h . x =
g . x
by A13, FUNCT_1:49
.=
H1(
x)
by A5, A32
;
assume
h . ((Den (o,A)) . p) = h . x
;
contradictionhence
contradiction
by A31, A33, TREES_4:17;
verum end;
A34:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A35:
S1[
k]
;
S1[k + 1]
defpred S2[
set ]
means ex
o being
Element of
dom the
charact of
A ex
p being
Element of the
carrier of
A * st
( $1
= (Den (o,A)) . p &
p in dom (Den (o,A)) &
rng p c= the
free GeneratorSet of
A |^ k );
let a1,
a2 be
set ;
( a1 in the free GeneratorSet of A |^ (k + 1) & a2 in the free GeneratorSet of A |^ (k + 1) & h . a1 = h . a2 implies a1 = a2 )
assume that A36:
a1 in the
free GeneratorSet of
A |^ (k + 1)
and A37:
a2 in the
free GeneratorSet of
A |^ (k + 1)
and A38:
h . a1 = h . a2
;
a1 = a2
per cases
( ( a1 in the free GeneratorSet of A & a2 in the free GeneratorSet of A ) or ( S2[a1] & S2[a2] ) or ( a1 in the free GeneratorSet of A & S2[a2] ) or ( S2[a1] & a2 in the free GeneratorSet of A ) )
by A36, A37, Th23;
suppose A39:
(
a1 in the
free GeneratorSet of
A &
a2 in the
free GeneratorSet of
A )
;
a1 = a2then A40:
h . a1 = g . a1
by A13, FUNCT_1:49;
A41:
h . a2 = g . a2
by A13, A39, FUNCT_1:49;
A42:
h . a1 = H1(
a1)
by A5, A39, A40;
h . a2 = H1(
a2)
by A5, A39, A41;
then
[0,a1] = [0,a2]
by A38, A42, TREES_4:4;
hence
a1 = a2
by XTUPLE_0:1;
verum end; suppose A43:
(
S2[
a1] &
S2[
a2] )
;
a1 = a2then consider b1 being
Element of
dom the
charact of
A,
q1 being
Element of the
carrier of
A * such that A44:
a1 = (Den (b1,A)) . q1
and A45:
q1 in dom (Den (b1,A))
and A46:
rng q1 c= the
free GeneratorSet of
A |^ k
;
consider b2 being
Element of
dom the
charact of
A,
q2 being
Element of the
carrier of
A * such that A47:
a2 = (Den (b2,A)) . q2
and A48:
q2 in dom (Den (b2,A))
and A49:
rng q2 c= the
free GeneratorSet of
A |^ k
by A43;
A50:
b1 -tree (h * q1) =
h . a1
by A18, A44, A45
.=
b2 -tree (h * q2)
by A18, A38, A47, A48
;
then A51:
b1 = b2
by TREES_4:15;
A52:
h * q1 = h * q2
by A50, TREES_4:15;
A53:
len q1 = S . b1
by A18, A45;
A54:
len q2 = S . b2
by A18, A48;
A55:
dom q1 = Seg (len q1)
by FINSEQ_1:def 3;
A56:
dom q2 = Seg (len q1)
by A51, A53, A54, FINSEQ_1:def 3;
now for j being Nat st j in dom q1 holds
q1 . j = q2 . jlet j be
Nat;
( j in dom q1 implies q1 . j = q2 . j )assume A57:
j in dom q1
;
q1 . j = q2 . jthen A58:
q1 . j in rng q1
by FUNCT_1:3;
A59:
q2 . j in rng q2
by A55, A56, A57, FUNCT_1:3;
A60:
h . (q1 . j) = (h * q1) . j
by A57, FUNCT_1:13;
h . (q2 . j) = (h * q2) . j
by A55, A56, A57, FUNCT_1:13;
hence
q1 . j = q2 . j
by A35, A46, A49, A52, A58, A59, A60;
verum end; hence
a1 = a2
by A44, A47, A51, A55, A56, FINSEQ_1:13;
verum end;
end;
A61:
for k being Nat holds S1[k]
from NAT_1:sch 2(A23, A34);
reconsider q1 = p1, q2 = p2 as FinSequence of A by A1, A2, FINSEQ_1:def 11;
o1 -tree (h * q1) =
h . ((Den (o1,A)) . p1)
by A1, A18
.=
o2 -tree (h * q2)
by A2, A3, A18
;
then A62:
h * p1 = h * p2
by TREES_4:15;
A63:
len q1 = S . o1
by A1, A18;
A64:
len q2 = S . o2
by A2, A18;
A65:
dom q1 = Seg (len q1)
by FINSEQ_1:def 3;
A66:
dom q2 = Seg (len q1)
by A4, A63, A64, FINSEQ_1:def 3;
now for j being Nat st j in dom q1 holds
q1 . j = q2 . jlet j be
Nat;
( j in dom q1 implies q1 . j = q2 . j )assume A67:
j in dom q1
;
q1 . j = q2 . jthen A68:
q1 . j in rng q1
by FUNCT_1:3;
A69:
q2 . j in rng q2
by A65, A66, A67, FUNCT_1:3;
consider n1 being
Nat such that A70:
q1 . j in the
free GeneratorSet of
A |^ n1
by A68, Th30;
consider n2 being
Nat such that A71:
q2 . j in the
free GeneratorSet of
A |^ n2
by A69, Th30;
reconsider k =
max (
n1,
n2) as
Nat by TARSKI:1;
A72:
the
free GeneratorSet of
A |^ n1 c= the
free GeneratorSet of
A |^ k
by Th21, XXREAL_0:25;
A73:
the
free GeneratorSet of
A |^ n2 c= the
free GeneratorSet of
A |^ k
by Th21, XXREAL_0:25;
A74:
h . (q1 . j) = (h * q1) . j
by A67, FUNCT_1:13;
h . (q2 . j) = (h * q2) . j
by A65, A66, A67, FUNCT_1:13;
hence
q1 . j = q2 . j
by A61, A62, A70, A71, A72, A73, A74;
verum end;
hence
p1 = p2
by A65, A66; verum