let p9, q9 be FinSequence of X; ( rng p9 = A & ( for n, m being Nat st n in dom p9 & m in dom p9 & n < m holds
( p9 /. n <> p9 /. m & [(p9 /. n),(p9 /. m)] in R ) ) & rng q9 = A & ( for n, m being Nat st n in dom q9 & m in dom q9 & n < m holds
( q9 /. n <> q9 /. m & [(q9 /. n),(q9 /. m)] in R ) ) implies p9 = q9 )
assume that
A59:
rng p9 = A
and
A60:
for n, m being Nat st n in dom p9 & m in dom p9 & n < m holds
( p9 /. n <> p9 /. m & [(p9 /. n),(p9 /. m)] in R )
and
A61:
rng q9 = A
and
A62:
for n, m being Nat st n in dom q9 & m in dom q9 & n < m holds
( q9 /. n <> q9 /. m & [(q9 /. n),(q9 /. m)] in R )
; p9 = q9
per cases
( A is empty or not A is empty )
;
suppose A64:
not
A is
empty
;
p9 = q9then reconsider X9 =
X as non
empty set ;
reconsider A9 =
A as non
empty finite Subset of
X9 by A64;
set E =
<*> A9;
defpred S1[
FinSequence of
A9]
means ( $1 is
FinSequence of
A9 & ( for
n,
m being
Nat st
n in dom $1 &
m in dom $1 &
n < m holds
( $1
/. n <> $1
/. m &
[($1 /. n),($1 /. m)] in R ) ) implies for
q being
FinSequence of
A9 st
rng q = rng $1 & ( for
n,
m being
Nat st
n in dom q &
m in dom q &
n < m holds
(
q /. n <> q /. m &
[(q /. n),(q /. m)] in R ) ) holds
q = $1 );
reconsider p =
p9,
q =
q9 as
FinSequence of
A9 by A59, A61, FINSEQ_1:def 4;
A65:
for
p being
FinSequence of
A9 for
x being
Element of
A9 st
S1[
p] holds
S1[
p ^ <*x*>]
proof
let p be
FinSequence of
A9;
for x being Element of A9 st S1[p] holds
S1[p ^ <*x*>]let x be
Element of
A9;
( S1[p] implies S1[p ^ <*x*>] )
assume A66:
S1[
p]
;
S1[p ^ <*x*>]
assume
p ^ <*x*> is
FinSequence of
A9
;
( ex n, m being Nat st
( n in dom (p ^ <*x*>) & m in dom (p ^ <*x*>) & n < m & not ( (p ^ <*x*>) /. n <> (p ^ <*x*>) /. m & [((p ^ <*x*>) /. n),((p ^ <*x*>) /. m)] in R ) ) or for q being FinSequence of A9 st rng q = rng (p ^ <*x*>) & ( for n, m being Nat st n in dom q & m in dom q & n < m holds
( q /. n <> q /. m & [(q /. n),(q /. m)] in R ) ) holds
q = p ^ <*x*> )
assume A67:
for
n,
m being
Nat st
n in dom (p ^ <*x*>) &
m in dom (p ^ <*x*>) &
n < m holds
(
(p ^ <*x*>) /. n <> (p ^ <*x*>) /. m &
[((p ^ <*x*>) /. n),((p ^ <*x*>) /. m)] in R )
;
for q being FinSequence of A9 st rng q = rng (p ^ <*x*>) & ( for n, m being Nat st n in dom q & m in dom q & n < m holds
( q /. n <> q /. m & [(q /. n),(q /. m)] in R ) ) holds
q = p ^ <*x*>
let q be
FinSequence of
A9;
( rng q = rng (p ^ <*x*>) & ( for n, m being Nat st n in dom q & m in dom q & n < m holds
( q /. n <> q /. m & [(q /. n),(q /. m)] in R ) ) implies q = p ^ <*x*> )
assume that A68:
rng q = rng (p ^ <*x*>)
and A69:
for
n,
m being
Nat st
n in dom q &
m in dom q &
n < m holds
(
q /. n <> q /. m &
[(q /. n),(q /. m)] in R )
;
q = p ^ <*x*>
deffunc H1(
Nat)
-> set =
q . $1;
A70:
q <> 0
by A68;
then consider n being
Nat such that A71:
len q = n + 1
by NAT_1:6;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 12;
ex
q9 being
FinSequence st
(
len q9 = n & ( for
m being
Nat st
m in dom q9 holds
q9 . m = H1(
m) ) )
from FINSEQ_1:sch 2();
then consider q9 being
FinSequence such that A72:
len q9 = n
and A73:
for
m being
Nat st
m in dom q9 holds
q9 . m = q . m
;
1
in Seg 1
by FINSEQ_1:2, TARSKI:def 1;
then A74:
1
in dom <*x*>
by FINSEQ_1:def 8;
A75:
ex
m being
Element of
A9 st
(
m = x & ( for
l being
Element of
A9 st
l in rng (p ^ <*x*>) &
l <> x holds
[l,m] in R ) )
proof
reconsider m =
x as
Element of
A9 ;
take
m
;
( m = x & ( for l being Element of A9 st l in rng (p ^ <*x*>) & l <> x holds
[l,m] in R ) )
thus
m = x
;
for l being Element of A9 st l in rng (p ^ <*x*>) & l <> x holds
[l,m] in R
thus
for
l being
Element of
A9 st
l in rng (p ^ <*x*>) &
l <> x holds
[l,m] in R
verumproof
let l be
Element of
A9;
( l in rng (p ^ <*x*>) & l <> x implies [l,m] in R )
assume that A76:
l in rng (p ^ <*x*>)
and A77:
l <> x
;
[l,m] in R
consider y being
object such that A78:
y in dom (p ^ <*x*>)
and A79:
l = (p ^ <*x*>) . y
by A76, FUNCT_1:def 3;
A80:
l = (p ^ <*x*>) /. y
by A78, A79, PARTFUN1:def 6;
reconsider k =
y as
Element of
NAT by A78;
A81:
k <> (len p) + 1
A82:
y in Seg (len (p ^ <*x*>))
by A78, FINSEQ_1:def 3;
then
k <= len (p ^ <*x*>)
by FINSEQ_1:1;
then
k <= (len p) + (len <*x*>)
by FINSEQ_1:22;
then
k <= (len p) + 1
by FINSEQ_1:39;
then
k < (len p) + 1
by A81, XXREAL_0:1;
then
k < (len p) + (len <*x*>)
by FINSEQ_1:39;
then A83:
k < len (p ^ <*x*>)
by FINSEQ_1:22;
1
<= k
by A82, FINSEQ_1:1;
then
1
- (len (p ^ <*x*>)) < k - k
by A83, XREAL_1:15;
then
1
< len (p ^ <*x*>)
by XREAL_1:48;
then
len (p ^ <*x*>) in Seg (len (p ^ <*x*>))
by FINSEQ_1:1;
then A84:
len (p ^ <*x*>) in dom (p ^ <*x*>)
by FINSEQ_1:def 3;
m =
(p ^ <*x*>) . ((len p) + 1)
by FINSEQ_1:42
.=
(p ^ <*x*>) . ((len p) + (len <*x*>))
by FINSEQ_1:39
.=
(p ^ <*x*>) . (len (p ^ <*x*>))
by FINSEQ_1:22
;
then
m = (p ^ <*x*>) /. (len (p ^ <*x*>))
by A84, PARTFUN1:def 6;
hence
[l,m] in R
by A67, A78, A80, A83, A84;
verum
end;
end;
A85:
for
m being
Nat st
m in dom <*x*> holds
q . ((len q9) + m) = <*x*> . m
proof
let m be
Nat;
( m in dom <*x*> implies q . ((len q9) + m) = <*x*> . m )
assume
m in dom <*x*>
;
q . ((len q9) + m) = <*x*> . m
then A86:
m in {1}
by FINSEQ_1:2, FINSEQ_1:def 8;
A87:
q . ((len q9) + m) = x
proof
consider d1 being
Element of
A9 such that A88:
d1 = x
and A89:
for
l being
Element of
A9 st
l in rng (p ^ <*x*>) &
l <> x holds
[l,d1] in R
by A75;
reconsider d =
d1 as
Element of
A9 ;
len q in Seg (len q)
by A70, FINSEQ_1:3;
then A90:
len q in dom q
by FINSEQ_1:def 3;
then
q . (len q) in rng q
by FUNCT_1:def 3;
then reconsider k =
q . (len q) as
Element of
A9 ;
A91:
k = q /. (len q)
by A90, PARTFUN1:def 6;
A92:
field R = X
by ORDERS_1:12;
assume
q . ((len q9) + m) <> x
;
contradiction
then A93:
q . (len q) <> x
by A71, A72, A86, TARSKI:def 1;
x in {x}
by TARSKI:def 1;
then
x in rng <*x*>
by FINSEQ_1:38;
then
x in (rng p) \/ (rng <*x*>)
by XBOOLE_0:def 3;
then
x in rng q
by A68, FINSEQ_1:31;
then consider y being
object such that A94:
y in dom q
and A95:
x = q . y
by FUNCT_1:def 3;
A96:
y in Seg (len q)
by A94, FINSEQ_1:def 3;
reconsider y =
y as
Element of
NAT by A94;
y <= len q
by A96, FINSEQ_1:1;
then A97:
y < len q
by A93, A95, XXREAL_0:1;
q . (len q) in rng (p ^ <*x*>)
by A68, A90, FUNCT_1:def 3;
then A98:
[k,d] in R
by A93, A89;
A99:
d = q /. y
by A88, A94, A95, PARTFUN1:def 6;
then A100:
[d,k] in R
by A69, A94, A90, A97, A91;
k <> d
by A69, A94, A90, A97, A91, A99;
hence
contradiction
by A98, A100, A92, RELAT_2:def 4, RELAT_2:def 12;
verum
end;
m = 1
by A86, TARSKI:def 1;
hence
q . ((len q9) + m) = <*x*> . m
by A87, FINSEQ_1:40;
verum
end;
then reconsider f =
q9 as
FinSequence of
A9 by FINSEQ_1:def 4, TARSKI:def 3;
dom q =
Seg (n + 1)
by A71, FINSEQ_1:def 3
.=
Seg ((len q9) + (len <*x*>))
by A72, FINSEQ_1:39
;
then A106:
q9 ^ <*x*> = q
by A73, A85, FINSEQ_1:def 7;
A107:
not
x in rng p
proof
(len p) + 1 =
(len p) + (len <*x*>)
by FINSEQ_1:39
.=
len (p ^ <*x*>)
by FINSEQ_1:22
;
then
(len p) + 1
in Seg (len (p ^ <*x*>))
by FINSEQ_1:4;
then A108:
(len p) + 1
in dom (p ^ <*x*>)
by FINSEQ_1:def 3;
assume
x in rng p
;
contradiction
then consider y being
object such that A109:
y in dom p
and A110:
x = p . y
by FUNCT_1:def 3;
A111:
y in Seg (len p)
by A109, FINSEQ_1:def 3;
A112:
dom p c= dom (p ^ <*x*>)
by FINSEQ_1:26;
reconsider y =
y as
Element of
NAT by A109;
x = (p ^ <*x*>) . y
by A109, A110, FINSEQ_1:def 7;
then A113:
x = (p ^ <*x*>) /. y
by A109, A112, PARTFUN1:def 6;
y <= len p
by A111, FINSEQ_1:1;
then A114:
y < (len p) + 1
by NAT_1:13;
x = (p ^ <*x*>) . ((len p) + 1)
by FINSEQ_1:42;
then
(p ^ <*x*>) /. y = (p ^ <*x*>) /. ((len p) + 1)
by A108, A113, PARTFUN1:def 6;
hence
contradiction
by A67, A109, A108, A112, A114;
verum
end;
A115:
for
z being
object holds
(
z in ((rng p) \/ {x}) \ {x} iff
z in rng p )
rng (p ^ <*x*>) =
(rng p) \/ (rng <*x*>)
by FINSEQ_1:31
.=
(rng p) \/ {x}
by FINSEQ_1:39
;
then A120:
rng p = (rng (p ^ <*x*>)) \ {x}
by A115, TARSKI:2;
A121:
(
rng f = rng p & ( for
l,
m being
Nat st
l in dom f &
m in dom f &
l < m holds
(
f /. l <> f /. m &
[(f /. l),(f /. m)] in R ) ) )
proof
A122:
not
x in rng f
proof
(len f) + 1 =
(len f) + (len <*x*>)
by FINSEQ_1:39
.=
len (f ^ <*x*>)
by FINSEQ_1:22
;
then
(len f) + 1
in Seg (len (f ^ <*x*>))
by FINSEQ_1:4;
then A123:
(len f) + 1
in dom (f ^ <*x*>)
by FINSEQ_1:def 3;
assume
x in rng f
;
contradiction
then consider y being
object such that A124:
y in dom f
and A125:
x = f . y
by FUNCT_1:def 3;
A126:
y in Seg (len f)
by A124, FINSEQ_1:def 3;
A127:
dom f c= dom (f ^ <*x*>)
by FINSEQ_1:26;
reconsider y =
y as
Element of
NAT by A124;
x = q . y
by A73, A124, A125;
then A128:
x = q /. y
by A106, A124, A127, PARTFUN1:def 6;
y <= len f
by A126, FINSEQ_1:1;
then A129:
y < (len f) + 1
by NAT_1:13;
x = q . ((len f) + 1)
by A106, FINSEQ_1:42;
then
q /. y = q /. ((len f) + 1)
by A106, A123, A128, PARTFUN1:def 6;
hence
contradiction
by A69, A106, A124, A123, A127, A129;
verum
end;
A130:
for
z being
object holds
(
z in ((rng f) \/ {x}) \ {x} iff
z in rng f )
rng (f ^ <*x*>) =
(rng f) \/ (rng <*x*>)
by FINSEQ_1:31
.=
(rng f) \/ {x}
by FINSEQ_1:39
;
hence
rng f = rng p
by A68, A106, A120, A130, TARSKI:2;
for l, m being Nat st l in dom f & m in dom f & l < m holds
( f /. l <> f /. m & [(f /. l),(f /. m)] in R )
let l,
m be
Nat;
( l in dom f & m in dom f & l < m implies ( f /. l <> f /. m & [(f /. l),(f /. m)] in R ) )
assume that A135:
l in dom f
and A136:
m in dom f
and A137:
l < m
;
( f /. l <> f /. m & [(f /. l),(f /. m)] in R )
A138:
f . m = f /. m
by A136, PARTFUN1:def 6;
A139:
dom f c= dom q
by A106, FINSEQ_1:26;
then
q . m = q /. m
by A136, PARTFUN1:def 6;
then A140:
f /. m = q /. m
by A73, A136, A138;
A141:
f . l = f /. l
by A135, PARTFUN1:def 6;
q . l = q /. l
by A139, A135, PARTFUN1:def 6;
then
f /. l = q /. l
by A73, A135, A141;
hence
(
f /. l <> f /. m &
[(f /. l),(f /. m)] in R )
by A69, A139, A135, A136, A137, A140;
verum
end;
(
p is
FinSequence of
A9 & ( for
l,
m being
Nat st
l in dom p &
m in dom p &
l < m holds
(
p /. l <> p /. m &
[(p /. l),(p /. m)] in R ) ) )
proof
thus
p is
FinSequence of
A9
;
for l, m being Nat st l in dom p & m in dom p & l < m holds
( p /. l <> p /. m & [(p /. l),(p /. m)] in R )
let l,
m be
Nat;
( l in dom p & m in dom p & l < m implies ( p /. l <> p /. m & [(p /. l),(p /. m)] in R ) )
assume that A142:
l in dom p
and A143:
m in dom p
and A144:
l < m
;
( p /. l <> p /. m & [(p /. l),(p /. m)] in R )
A145:
dom p c= dom (p ^ <*x*>)
by FINSEQ_1:26;
p . m = (p ^ <*x*>) . m
by A143, FINSEQ_1:def 7;
then
p . m = (p ^ <*x*>) /. m
by A143, A145, PARTFUN1:def 6;
then A146:
p /. m = (p ^ <*x*>) /. m
by A143, PARTFUN1:def 6;
p . l = (p ^ <*x*>) . l
by A142, FINSEQ_1:def 7;
then
p . l = (p ^ <*x*>) /. l
by A142, A145, PARTFUN1:def 6;
then
p /. l = (p ^ <*x*>) /. l
by A142, PARTFUN1:def 6;
hence
(
p /. l <> p /. m &
[(p /. l),(p /. m)] in R )
by A67, A142, A143, A144, A145, A146;
verum
end;
hence
q = p ^ <*x*>
by A66, A106, A121;
verum
end; A147:
now for n, m being Nat st n in dom p & m in dom p & n < m holds
( p /. n <> p /. m & [(p /. n),(p /. m)] in R )let n,
m be
Nat;
( n in dom p & m in dom p & n < m implies ( p /. n <> p /. m & [(p /. n),(p /. m)] in R ) )assume that A148:
n in dom p
and A149:
m in dom p
and A150:
n < m
;
( p /. n <> p /. m & [(p /. n),(p /. m)] in R )A151:
p /. m =
p . m
by A149, PARTFUN1:def 6
.=
p9 /. m
by A149, PARTFUN1:def 6
;
p /. n =
p . n
by A148, PARTFUN1:def 6
.=
p9 /. n
by A148, PARTFUN1:def 6
;
hence
(
p /. n <> p /. m &
[(p /. n),(p /. m)] in R )
by A60, A148, A149, A150, A151;
verum end; A152:
now for n, m being Nat st n in dom q & m in dom q & n < m holds
( q /. n <> q /. m & [(q /. n),(q /. m)] in R )let n,
m be
Nat;
( n in dom q & m in dom q & n < m implies ( q /. n <> q /. m & [(q /. n),(q /. m)] in R ) )assume that A153:
n in dom q
and A154:
m in dom q
and A155:
n < m
;
( q /. n <> q /. m & [(q /. n),(q /. m)] in R )A156:
q /. m =
q . m
by A154, PARTFUN1:def 6
.=
q9 /. m
by A154, PARTFUN1:def 6
;
q /. n =
q . n
by A153, PARTFUN1:def 6
.=
q9 /. n
by A153, PARTFUN1:def 6
;
hence
(
q /. n <> q /. m &
[(q /. n),(q /. m)] in R )
by A62, A153, A154, A155, A156;
verum end; A157:
S1[
<*> A9]
;
for
p being
FinSequence of
A9 holds
S1[
p]
from FINSEQ_2:sch 2(A157, A65);
hence
p9 = q9
by A59, A61, A147, A152;
verum end; end;