let p, q be FinSequence; ( rng p = rng q & p is one-to-one & q is one-to-one implies len p = len q )
defpred S2[ FinSequence] means ( $1 is one-to-one implies for q being FinSequence st rng $1 = rng q & q is one-to-one holds
len $1 = len q );
A1:
S2[ {} ]
by RELAT_1:41;
now for p being FinSequence
for x being object st ( p is one-to-one implies for q being FinSequence st rng p = rng q & q is one-to-one holds
len p = len q ) & p ^ <*x*> is one-to-one holds
for q being FinSequence st rng (p ^ <*x*>) = rng q & q is one-to-one holds
len (p ^ <*x*>) = len qlet p be
FinSequence;
for x being object st ( p is one-to-one implies for q being FinSequence st rng p = rng q & q is one-to-one holds
len p = len q ) & p ^ <*x*> is one-to-one holds
for q being FinSequence st rng (p ^ <*x*>) = rng q & q is one-to-one holds
len (p ^ <*x*>) = len qlet x be
object ;
( ( p is one-to-one implies for q being FinSequence st rng p = rng q & q is one-to-one holds
len p = len q ) & p ^ <*x*> is one-to-one implies for q being FinSequence st rng (p ^ <*x*>) = rng q & q is one-to-one holds
len (p ^ <*x*>) = len q )assume A2:
(
p is
one-to-one implies for
q being
FinSequence st
rng p = rng q &
q is
one-to-one holds
len p = len q )
;
( p ^ <*x*> is one-to-one implies for q being FinSequence st rng (p ^ <*x*>) = rng q & q is one-to-one holds
len (p ^ <*x*>) = len q )assume A3:
p ^ <*x*> is
one-to-one
;
for q being FinSequence st rng (p ^ <*x*>) = rng q & q is one-to-one holds
len (p ^ <*x*>) = len qlet q be
FinSequence;
( rng (p ^ <*x*>) = rng q & q is one-to-one implies len (p ^ <*x*>) = len q )assume that A4:
rng (p ^ <*x*>) = rng q
and A5:
q is
one-to-one
;
len (p ^ <*x*>) = len qA6:
rng (p ^ <*x*>) =
(rng p) \/ (rng <*x*>)
by Th31
.=
(rng p) \/ {x}
by Th38
;
x in {x}
by TARSKI:def 1;
then
x in rng q
by A4, A6, XBOOLE_0:def 3;
then consider y being
object such that A7:
y in dom q
and A8:
x = q . y
by FUNCT_1:def 3;
A9:
y in Seg (len q)
by A7, Def3;
reconsider y =
y as
Element of
NAT by A7;
A10:
1
<= y
by A9, Th1;
then consider k being
Nat such that A11:
1
+ k = y
by NAT_1:10;
A12:
y <= len q
by A9, Th1;
then consider n being
Nat such that A13:
y + n = len q
by NAT_1:10;
reconsider k =
k,
n =
n as
Element of
NAT by ORDINAL1:def 12;
reconsider q1 =
q | (Seg k) as
FinSequence by Th15;
defpred S3[
Nat,
object ]
means $2
= q . (y + $1);
A14:
for
j being
Nat st
j in Seg n holds
ex
x being
object st
S3[
j,
x]
;
consider q2 being
FinSequence such that A15:
dom q2 = Seg n
and A16:
for
j being
Nat st
j in Seg n holds
S3[
j,
q2 . j]
from FINSEQ_1:sch 1(A14);
A17:
k <= y
by A11, NAT_1:12;
then A18:
k <= len q
by A12, XXREAL_0:2;
then A19:
len q1 = k
by Th17;
(len (q1 ^ <*x*>)) + (len q2) =
((len q1) + (len <*x*>)) + (len q2)
by Th22
.=
(k + 1) + (len q2)
by A19, Th39
.=
len q
by A11, A13, A15, Def3
;
then A20:
dom q = Seg ((len (q1 ^ <*x*>)) + (len q2))
by Def3;
A21:
rng (q1 ^ q2) = (rng q) \ {x}
proof
thus
rng (q1 ^ q2) c= (rng q) \ {x}
XBOOLE_0:def 10 (rng q) \ {x} c= rng (q1 ^ q2)proof
let z be
object ;
TARSKI:def 3 ( not z in rng (q1 ^ q2) or z in (rng q) \ {x} )
assume
z in rng (q1 ^ q2)
;
z in (rng q) \ {x}
then A22:
z in (rng q1) \/ (rng q2)
by Th31;
A23:
now ( z in rng q1 implies z in (rng q) \ {x} )assume A24:
z in rng q1
;
z in (rng q) \ {x}A25:
(
rng q1 = q .: (Seg k) &
q .: (Seg k) c= rng q )
by RELAT_1:111, RELAT_1:115;
consider y1 being
object such that A26:
y1 in dom q1
and A27:
q1 . y1 = z
by A24, FUNCT_1:def 3;
A28:
q1 . y1 = q . y1
by A26, FUNCT_1:47;
A29:
y1 in Seg (len q1)
by A26, Def3;
reconsider y1 =
y1 as
Element of
NAT by A26;
A30:
y1 <= k
by A19, A29, Th1;
A31:
k < y
by A11, XREAL_1:29;
Seg k c= Seg (len q)
by A17, Th5, A12, XXREAL_0:2;
then
dom q1 c= Seg (len q)
by A18, Th17;
then
dom q1 c= dom q
by Def3;
then
x <> z
by A5, A7, A8, A26, A27, A28, A30, A31;
then
not
z in {x}
by TARSKI:def 1;
hence
z in (rng q) \ {x}
by A24, A25, XBOOLE_0:def 5;
verum end;
now ( z in rng q2 implies z in (rng q) \ {x} )assume
z in rng q2
;
z in (rng q) \ {x}then consider y1 being
object such that A32:
y1 in dom q2
and A33:
q2 . y1 = z
by FUNCT_1:def 3;
reconsider y1 =
y1 as
Element of
NAT by A32;
A34:
q2 . y1 = q . (y + y1)
by A15, A16, A32;
A35:
1
<= y + y1
by A10, NAT_1:12;
y1 <= n
by A15, A32, Th1;
then
y + y1 <= len q
by A13, XREAL_1:7;
then
y + y1 in Seg (len q)
by A35;
then A36:
y + y1 in dom q
by Def3;
then A37:
z in rng q
by A33, A34, FUNCT_1:def 3;
y1 <> 0
by A15, A32, Th1;
then
y <> y + y1
;
then
x <> z
by A5, A7, A8, A33, A34, A36;
then
not
z in {x}
by TARSKI:def 1;
hence
z in (rng q) \ {x}
by A37, XBOOLE_0:def 5;
verum end;
hence
z in (rng q) \ {x}
by A22, A23, XBOOLE_0:def 3;
verum
end;
let z be
object ;
TARSKI:def 3 ( not z in (rng q) \ {x} or z in rng (q1 ^ q2) )
assume A38:
z in (rng q) \ {x}
;
z in rng (q1 ^ q2)
then consider y1 being
object such that A39:
y1 in dom q
and A40:
z = q . y1
by FUNCT_1:def 3;
A41:
y1 in Seg (len q)
by A39, Def3;
reconsider y1 =
y1 as
Element of
NAT by A39;
not
z in {x}
by A38, XBOOLE_0:def 5;
then A42:
y <> y1
by A8, A40, TARSKI:def 1;
A43:
now ( y < y1 implies z in rng q2 )assume A44:
y < y1
;
z in rng q2then consider j being
Nat such that A45:
y1 = y + j
by NAT_1:10;
A46:
1
<= j
by A44, A45, NAT_1:19;
j <= n
by A13, A41, A45, Th1, XREAL_1:6;
then A47:
j in Seg n
by A46;
then
z = q2 . j
by A16, A40, A45;
hence
z in rng q2
by A15, A47, FUNCT_1:def 3;
verum end;
then
z in (rng q1) \/ (rng q2)
by A42, A43, XBOOLE_0:def 3, XXREAL_0:1;
hence
z in rng (q1 ^ q2)
by Th31;
verum
end; A51:
p = (p ^ <*x*>) | (dom p)
by Th21;
A52:
rng p = (rng (p ^ <*x*>)) \ {x}
proof
thus
rng p c= (rng (p ^ <*x*>)) \ {x}
XBOOLE_0:def 10 (rng (p ^ <*x*>)) \ {x} c= rng pproof
let z be
object ;
TARSKI:def 3 ( not z in rng p or z in (rng (p ^ <*x*>)) \ {x} )
assume A53:
z in rng p
;
z in (rng (p ^ <*x*>)) \ {x}
A54:
rng p c= rng (p ^ <*x*>)
by A51, RELAT_1:70;
consider y1 being
object such that A55:
y1 in dom p
and A56:
p . y1 = z
by A53, FUNCT_1:def 3;
A57:
y1 in Seg (len p)
by A55, Def3;
reconsider y1 =
y1 as
Element of
NAT by A55;
A58:
(p ^ <*x*>) . ((len p) + 1) = x
by Th42;
A59:
(p ^ <*x*>) . y1 = p . y1
by A51, A55, FUNCT_1:47;
A60:
y1 <= len p
by A57, Th1;
A61:
len p < (len p) + 1
by XREAL_1:29;
A62:
1
<= y1
by A57, Th1;
y1 <= (len p) + 1
by A60, A61, XXREAL_0:2;
then A63:
y1 in Seg ((len p) + 1)
by A62;
A64:
(len p) + 1
in Seg ((len p) + 1)
by Th3;
A65:
y1 in Seg ((len p) + (len <*x*>))
by A63, Th40;
A66:
(len p) + 1
in Seg ((len p) + (len <*x*>))
by A64, Th40;
A67:
y1 in dom (p ^ <*x*>)
by A65, Def7;
(len p) + 1
in dom (p ^ <*x*>)
by A66, Def7;
then
x <> z
by A3, A56, A58, A59, A60, A61, A67;
then
not
z in {x}
by TARSKI:def 1;
hence
z in (rng (p ^ <*x*>)) \ {x}
by A53, A54, XBOOLE_0:def 5;
verum
end;
let z be
object ;
TARSKI:def 3 ( not z in (rng (p ^ <*x*>)) \ {x} or z in rng p )
assume A68:
z in (rng (p ^ <*x*>)) \ {x}
;
z in rng p
then A69:
z in rng (p ^ <*x*>)
;
A70:
not
z in {x}
by A68, XBOOLE_0:def 5;
z in (rng p) \/ (rng <*x*>)
by A69, Th31;
then
(
z in rng p or
z in rng <*x*> )
by XBOOLE_0:def 3;
hence
z in rng p
by A70, Th38;
verum
end; A71:
q1 ^ q2 is
one-to-one
proof
let y1,
y2 be
object ;
FUNCT_1:def 4 ( not y1 in dom (q1 ^ q2) or not y2 in dom (q1 ^ q2) or not (q1 ^ q2) . y1 = (q1 ^ q2) . y2 or y1 = y2 )
assume that A72:
(
y1 in dom (q1 ^ q2) &
y2 in dom (q1 ^ q2) )
and A73:
(q1 ^ q2) . y1 = (q1 ^ q2) . y2
;
y1 = y2
reconsider m1 =
y1,
m2 =
y2 as
Element of
NAT by A72;
A74:
q1 is
one-to-one
by A5, FUNCT_1:52;
A77:
now ( m1 in dom q1 & ex j being Nat st
( j in dom q2 & m2 = (len q1) + j ) implies y1 = y2 )assume A78:
m1 in dom q1
;
( ex j being Nat st
( j in dom q2 & m2 = (len q1) + j ) implies y1 = y2 )given j being
Nat such that A79:
j in dom q2
and A80:
m2 = (len q1) + j
;
y1 = y2A81:
(q1 ^ q2) . m2 = q2 . j
by A79, A80, Def7;
(
(q1 ^ q2) . m1 = q1 . m1 &
q1 . m1 = q . m1 )
by A78, Def7, FUNCT_1:47;
then A82:
q . m1 = q . (y + j)
by A15, A16, A73, A79, A81;
1
<= j
by A15, A79, Th1;
then A83:
1
<= y + j
by NAT_1:12;
j <= n
by A15, A79, Th1;
then
y + j <= len q
by A13, XREAL_1:7;
then
y + j in Seg (len q)
by A83;
then A84:
y + j in dom q
by Def3;
m1 in Seg k
by A18, A78, Th17;
then A85:
m1 <= k
by Th1;
k < y
by A11, XREAL_1:29;
then A86:
m1 < y
by A85, XXREAL_0:2;
(
dom q1 c= dom q &
y <= y + j )
by NAT_1:12, RELAT_1:60;
hence
y1 = y2
by A5, A78, A82, A84, A86;
verum end;
A87:
now ( m2 in dom q1 & ex j being Nat st
( j in dom q2 & m1 = (len q1) + j ) implies y1 = y2 )assume A88:
m2 in dom q1
;
( ex j being Nat st
( j in dom q2 & m1 = (len q1) + j ) implies y1 = y2 )given j being
Nat such that A89:
j in dom q2
and A90:
m1 = (len q1) + j
;
y1 = y2A91:
(q1 ^ q2) . m1 = q2 . j
by A89, A90, Def7;
(
(q1 ^ q2) . m2 = q1 . m2 &
q1 . m2 = q . m2 )
by A88, Def7, FUNCT_1:47;
then A92:
q . m2 = q . (y + j)
by A15, A16, A73, A89, A91;
1
<= j
by A15, A89, Th1;
then A93:
1
<= y + j
by NAT_1:12;
j <= n
by A15, A89, Th1;
then
y + j <= len q
by A13, XREAL_1:7;
then
y + j in Seg (len q)
by A93;
then A94:
y + j in dom q
by Def3;
m2 in Seg k
by A18, A88, Th17;
then A95:
m2 <= k
by Th1;
k < y
by A11, XREAL_1:29;
then A96:
m2 < y
by A95, XXREAL_0:2;
(
dom q1 c= dom q &
y <= y + j )
by NAT_1:12, RELAT_1:60;
hence
y1 = y2
by A5, A88, A92, A94, A96;
verum end;
now ( ex j1 being Nat st
( j1 in dom q2 & m1 = (len q1) + j1 ) & ex j2 being Nat st
( j2 in dom q2 & m2 = (len q1) + j2 ) implies y1 = y2 )given j1 being
Nat such that A97:
j1 in dom q2
and A98:
m1 = (len q1) + j1
;
( ex j2 being Nat st
( j2 in dom q2 & m2 = (len q1) + j2 ) implies y1 = y2 )given j2 being
Nat such that A99:
j2 in dom q2
and A100:
m2 = (len q1) + j2
;
y1 = y2A101:
(q1 ^ q2) . m1 = q2 . j1
by A97, A98, Def7;
A102:
(q1 ^ q2) . m2 = q2 . j2
by A99, A100, Def7;
A103:
(q1 ^ q2) . m1 = q . (y + j1)
by A15, A16, A97, A101;
A104:
(q1 ^ q2) . m2 = q . (y + j2)
by A15, A16, A99, A102;
A105:
1
<= j1
by A15, A97, Th1;
A106:
1
<= j2
by A15, A99, Th1;
A107:
1
<= y + j1
by A105, NAT_1:12;
A108:
1
<= y + j2
by A106, NAT_1:12;
A109:
j1 <= n
by A15, A97, Th1;
A110:
j2 <= n
by A15, A99, Th1;
A111:
y + j1 <= len q
by A13, A109, XREAL_1:7;
A112:
y + j2 <= len q
by A13, A110, XREAL_1:7;
A113:
y + j1 in Seg (len q)
by A107, A111;
A114:
y + j2 in Seg (len q)
by A108, A112;
A115:
y + j1 in dom q
by A113, Def3;
y + j2 in dom q
by A114, Def3;
then
y + j1 = y + j2
by A5, A73, A103, A104, A115;
hence
y1 = y2
by A98, A100;
verum end;
hence
y1 = y2
by A72, A75, A77, A87, Th25;
verum
end; then
(q1 ^ <*x*>) ^ q2 = q
by A20, A116, Def7;
then A122:
len q =
(len (q1 ^ <*x*>)) + (len q2)
by Th22
.=
((len <*x*>) + (len q1)) + (len q2)
by Th22
.=
(1 + (len q1)) + (len q2)
by Th40
.=
1
+ ((len q1) + (len q2))
.=
(len (q1 ^ q2)) + 1
by Th22
;
len (p ^ <*x*>) =
(len p) + (len <*x*>)
by Th22
.=
(len p) + 1
by Th40
;
hence
len (p ^ <*x*>) = len q
by A2, A3, A4, A21, A51, A52, A71, A122, FUNCT_1:52;
verum end;
then A123:
for p being FinSequence
for x being object st S2[p] holds
S2[p ^ <*x*>]
;
for p being FinSequence holds S2[p]
from FINSEQ_1:sch 3(A1, A123);
hence
( rng p = rng q & p is one-to-one & q is one-to-one implies len p = len q )
; verum