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 )
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 & 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:9;
set G9 = G \/ {the carrier of A};
reconsider G9 = G \/ {the carrier of A} as non empty set ;
deffunc H1( set ) -> set = root-tree [0 ,$1];
consider g being Function such that
A5:
( dom g = G & ( for x being set st x in G 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
set ;
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
set such that A8:
a in dom g
and A9:
b = g . a
by FUNCT_1:def 5;
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:106;
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 G,the carrier of (FreeUnivAlgNSG S,[:{0 },G9:]) by A5, FUNCT_2:4, XBOOLE_1:1;
signature (FreeUnivAlgNSG S,[:{0 },G9:]) = S
by FREEALG:4;
then
A, FreeUnivAlgNSG S,[:{0 },G9:] are_similar
by UNIALG_2:def 2;
then consider h being Function of A,(FreeUnivAlgNSG S,[:{0 },G9:]) such that
A12:
h is_homomorphism A, FreeUnivAlgNSG S,[:{0 },G9:]
and
A13:
h | G = g
by FREEALG:def 6;
defpred S1[ Nat] means for a1, a2 being set st a1 in G |^ $1 & a2 in G |^ $1 & h . a1 = h . a2 holds
a1 = a2;
A14:
G |^ 0 = G
by Th18;
A15:
len S = len the charact of (FreeUnivAlgNSG S,[:{0 },G9:])
by A6, UNIALG_1:def 11;
A16:
len S = len the charact of A
by UNIALG_1:def 11;
A17:
dom S = dom the charact of (FreeUnivAlgNSG S,[:{0 },G9:])
by A15, FINSEQ_3:31;
A18:
now 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:31;
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:58;
then A20:
len p =
arity op
by A19, FINSEQ_1:def 18
.=
j
by A17, UNIALG_1:def 11
;
hence
(
len p = S . o &
len (h * p) = S . o )
by FINSEQ_2:37;
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
by FUNCT_7:def 1;
len hq = S . o9
by A20, FINSEQ_2:37;
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 G |^ 0 & a2 in G |^ 0 & h . a1 = h . a2 implies a1 = a2 )
assume that A24:
a1 in G |^ 0
and A25:
a2 in G |^ 0
and A26:
h . a1 = h . a2
;
a1 = a2
A27:
h . a1 = g . a1
by A13, A14, A24, FUNCT_1:72;
A28:
h . a2 = g . a2
by A13, A14, A25, FUNCT_1:72;
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 ZFMISC_1:33;
verum
end;
A30:
now let 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 G 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 G holds
not h . ((Den o,A) . p) = h . x )assume
p in dom (Den o,A)
;
for x being set st x in G 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 G implies not h . ((Den o,A) . p) = h . x )assume A32:
x in G
;
not h . ((Den o,A) . p) = h . xthen A33:
h . x =
g . x
by A13, FUNCT_1:72
.=
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= G |^ k );
let a1,
a2 be
set ;
( a1 in G |^ (k + 1) & a2 in G |^ (k + 1) & h . a1 = h . a2 implies a1 = a2 )
assume that A36:
a1 in G |^ (k + 1)
and A37:
a2 in G |^ (k + 1)
and A38:
h . a1 = h . a2
;
a1 = a2
per cases
( ( a1 in G & a2 in G ) or ( S2[a1] & S2[a2] ) or ( a1 in G & S2[a2] ) or ( S2[a1] & a2 in G ) )
by A36, A37, Th23;
suppose A39:
(
a1 in G &
a2 in G )
;
a1 = a2then A40:
h . a1 = g . a1
by A13, FUNCT_1:72;
A41:
h . a2 = g . a2
by A13, A39, FUNCT_1:72;
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 ZFMISC_1:33;
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= G |^ 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= G |^ 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 let 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:12;
A59:
q2 . j in rng q2
by A55, A56, A57, FUNCT_1:12;
A60:
h . (q1 . j) = (h * q1) . j
by A57, FUNCT_1:23;
h . (q2 . j) = (h * q2) . j
by A55, A56, A57, FUNCT_1:23;
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:17;
verum end; suppose
( (
a1 in G &
S2[
a2] ) or (
S2[
a1] &
a2 in G ) )
;
a1 = a2end;
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 let 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:12;
A69:
q2 . j in rng q2
by A65, A66, A67, FUNCT_1:12;
consider n1 being
Nat such that A70:
q1 . j in G |^ n1
by A68, Th30;
consider n2 being
Nat such that A71:
q2 . j in G |^ n2
by A69, Th30;
reconsider k =
max n1,
n2 as
Nat ;
A72:
G |^ n1 c= G |^ k
by Th21, XXREAL_0:25;
A73:
G |^ n2 c= G |^ k
by Th21, XXREAL_0:25;
A74:
h . (q1 . j) = (h * q1) . j
by A67, FUNCT_1:23;
h . (q2 . j) = (h * q2) . j
by A65, A66, A67, FUNCT_1:23;
hence
q1 . j = q2 . j
by A61, A62, A70, A71, A72, A73, A74;
verum end;
hence
p1 = p2
by A65, A66, FINSEQ_1:17; verum