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:64;
now let p be
FinSequence;
for x being set 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
set ;
( ( 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 Th44
.=
(rng p) \/ {x}
by Th55
;
x in {x}
by TARSKI:def 1;
then
x in rng q
by A4, A6, XBOOLE_0:def 3;
then consider y being
set such that A7:
y in dom q
and A8:
x = q . y
by FUNCT_1:def 5;
A9:
y in Seg (len q)
by A7, Def3;
reconsider y =
y as
Element of
NAT by A7;
A10:
1
<= y
by A9, Th3;
then consider k being
Nat such that A11:
1
+ k = y
by NAT_1:10;
A12:
y <= len q
by A9, Th3;
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 13;
reconsider q1 =
q | (Seg k) as
FinSequence by Th19;
defpred S3[
Nat,
set ]
means $2
= q . (y + $1);
A14:
for
j being
Nat st
j in Seg n holds
ex
x being
set 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);
k <= y
by A11, NAT_1:12;
then A17:
k <= len q
by A12, XXREAL_0:2;
then A18:
len q1 = k
by Th21;
(len (q1 ^ <*x*>)) + (len q2) =
((len q1) + (len <*x*>)) + (len q2)
by Th35
.=
(k + 1) + (len q2)
by A18, Th56
.=
len q
by A11, A13, A15, Def3
;
then A19:
dom q = Seg ((len (q1 ^ <*x*>)) + (len q2))
by Def3;
A20:
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
set ;
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 A21:
z in (rng q1) \/ (rng q2)
by Th44;
A22:
now assume A23:
z in rng q1
;
z in (rng q) \ {x}A24:
(
rng q1 = q .: (Seg k) &
q .: (Seg k) c= rng q )
by RELAT_1:144, RELAT_1:148;
consider y1 being
set such that A25:
y1 in dom q1
and A26:
q1 . y1 = z
by A23, FUNCT_1:def 5;
A27:
q1 . y1 = q . y1
by A25, FUNCT_1:70;
A28:
y1 in Seg (len q1)
by A25, Def3;
reconsider y1 =
y1 as
Element of
NAT by A25;
A29:
y1 <= k
by A18, A28, Th3;
A30:
k < y
by A11, XREAL_1:31;
Seg k c= Seg (len q)
by A17, Th7;
then
dom q1 c= Seg (len q)
by A17, Th21;
then
dom q1 c= dom q
by Def3;
then
x <> z
by A5, A7, A8, A25, A26, A27, A29, A30, FUNCT_1:def 8;
then
not
z in {x}
by TARSKI:def 1;
hence
z in (rng q) \ {x}
by A23, A24, XBOOLE_0:def 5;
verum end;
now assume
z in rng q2
;
z in (rng q) \ {x}then consider y1 being
set such that A31:
y1 in dom q2
and A32:
q2 . y1 = z
by FUNCT_1:def 5;
reconsider y1 =
y1 as
Element of
NAT by A31;
A33:
q2 . y1 = q . (y + y1)
by A15, A16, A31;
A34:
1
<= y + y1
by A10, NAT_1:12;
y1 <= n
by A15, A31, Th3;
then
y + y1 <= len q
by A13, XREAL_1:9;
then
y + y1 in Seg (len q)
by A34;
then A35:
y + y1 in dom q
by Def3;
then A36:
z in rng q
by A32, A33, FUNCT_1:def 5;
y1 <> 0
by A15, A31, Th3;
then
y <> y + y1
;
then
x <> z
by A5, A7, A8, A32, A33, A35, FUNCT_1:def 8;
then
not
z in {x}
by TARSKI:def 1;
hence
z in (rng q) \ {x}
by A36, XBOOLE_0:def 5;
verum end;
hence
z in (rng q) \ {x}
by A21, A22, XBOOLE_0:def 3;
verum
end;
let z be
set ;
TARSKI:def 3 ( not z in (rng q) \ {x} or z in rng (q1 ^ q2) )
assume A37:
z in (rng q) \ {x}
;
z in rng (q1 ^ q2)
then consider y1 being
set such that A38:
y1 in dom q
and A39:
z = q . y1
by FUNCT_1:def 5;
A40:
y1 in Seg (len q)
by A38, Def3;
reconsider y1 =
y1 as
Element of
NAT by A38;
not
z in {x}
by A37, XBOOLE_0:def 5;
then A41:
y <> y1
by A8, A39, TARSKI:def 1;
then
z in (rng q1) \/ (rng q2)
by A41, A42, XBOOLE_0:def 3, XXREAL_0:1;
hence
z in rng (q1 ^ q2)
by Th44;
verum
end; A50:
p = (p ^ <*x*>) | (dom p)
by Th33;
A51:
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
set ;
TARSKI:def 3 ( not z in rng p or z in (rng (p ^ <*x*>)) \ {x} )
assume A52:
z in rng p
;
z in (rng (p ^ <*x*>)) \ {x}
A53:
rng p c= rng (p ^ <*x*>)
by A50, RELAT_1:99;
consider y1 being
set such that A54:
y1 in dom p
and A55:
p . y1 = z
by A52, FUNCT_1:def 5;
A56:
y1 in Seg (len p)
by A54, Def3;
reconsider y1 =
y1 as
Element of
NAT by A54;
A57:
(p ^ <*x*>) . ((len p) + 1) = x
by Th59;
A58:
(p ^ <*x*>) . y1 = p . y1
by A50, A54, FUNCT_1:70;
A59:
y1 <= len p
by A56, Th3;
A60:
len p < (len p) + 1
by XREAL_1:31;
A61:
1
<= y1
by A56, Th3;
y1 <= (len p) + 1
by A59, A60, XXREAL_0:2;
then A62:
y1 in Seg ((len p) + 1)
by A61;
A63:
(len p) + 1
in Seg ((len p) + 1)
by Th5;
A64:
y1 in Seg ((len p) + (len <*x*>))
by A62, Th57;
A65:
(len p) + 1
in Seg ((len p) + (len <*x*>))
by A63, Th57;
A66:
y1 in dom (p ^ <*x*>)
by A64, Def7;
(len p) + 1
in dom (p ^ <*x*>)
by A65, Def7;
then
x <> z
by A3, A55, A57, A58, A59, A60, A66, FUNCT_1:def 8;
then
not
z in {x}
by TARSKI:def 1;
hence
z in (rng (p ^ <*x*>)) \ {x}
by A52, A53, XBOOLE_0:def 5;
verum
end;
let z be
set ;
TARSKI:def 3 ( not z in (rng (p ^ <*x*>)) \ {x} or z in rng p )
assume A67:
z in (rng (p ^ <*x*>)) \ {x}
;
z in rng p
then A68:
z in rng (p ^ <*x*>)
;
A69:
not
z in {x}
by A67, XBOOLE_0:def 5;
z in (rng p) \/ (rng <*x*>)
by A68, Th44;
then
(
z in rng p or
z in rng <*x*> )
by XBOOLE_0:def 3;
hence
z in rng p
by A69, Th55;
verum
end; A70:
q1 ^ q2 is
one-to-one
proof
let y1 be
set ;
FUNCT_1:def 8 for b1 being set holds
( not y1 in proj1 (q1 ^ q2) or not b1 in proj1 (q1 ^ q2) or not (q1 ^ q2) . y1 = (q1 ^ q2) . b1 or y1 = b1 )let y2 be
set ;
( not y1 in proj1 (q1 ^ q2) or not y2 in proj1 (q1 ^ q2) or not (q1 ^ q2) . y1 = (q1 ^ q2) . y2 or y1 = y2 )
assume that A71:
(
y1 in dom (q1 ^ q2) &
y2 in dom (q1 ^ q2) )
and A72:
(q1 ^ q2) . y1 = (q1 ^ q2) . y2
;
y1 = y2
reconsider m1 =
y1,
m2 =
y2 as
Element of
NAT by A71;
A73:
q1 is
one-to-one
by A5, FUNCT_1:84;
A76:
now assume A77:
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 A78:
j in dom q2
and A79:
m2 = (len q1) + j
;
y1 = y2reconsider j =
j as
Element of
NAT by ORDINAL1:def 13;
A80:
(q1 ^ q2) . m2 = q2 . j
by A78, A79, Def7;
(
(q1 ^ q2) . m1 = q1 . m1 &
q1 . m1 = q . m1 )
by A77, Def7, FUNCT_1:70;
then A81:
q . m1 = q . (y + j)
by A15, A16, A72, A78, A80;
1
<= j
by A15, A78, Th3;
then A82:
1
<= y + j
by NAT_1:12;
j <= n
by A15, A78, Th3;
then
y + j <= len q
by A13, XREAL_1:9;
then
y + j in Seg (len q)
by A82;
then A83:
y + j in dom q
by Def3;
m1 in Seg k
by A17, A77, Th21;
then A84:
m1 <= k
by Th3;
k < y
by A11, XREAL_1:31;
then A85:
m1 < y
by A84, XXREAL_0:2;
(
dom q1 c= dom q &
y <= y + j )
by NAT_1:12, RELAT_1:89;
hence
y1 = y2
by A5, A77, A81, A83, A85, FUNCT_1:def 8;
verum end;
A86:
now assume A87:
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 A88:
j in dom q2
and A89:
m1 = (len q1) + j
;
y1 = y2reconsider j =
j as
Element of
NAT by ORDINAL1:def 13;
A90:
(q1 ^ q2) . m1 = q2 . j
by A88, A89, Def7;
(
(q1 ^ q2) . m2 = q1 . m2 &
q1 . m2 = q . m2 )
by A87, Def7, FUNCT_1:70;
then A91:
q . m2 = q . (y + j)
by A15, A16, A72, A88, A90;
1
<= j
by A15, A88, Th3;
then A92:
1
<= y + j
by NAT_1:12;
j <= n
by A15, A88, Th3;
then
y + j <= len q
by A13, XREAL_1:9;
then
y + j in Seg (len q)
by A92;
then A93:
y + j in dom q
by Def3;
m2 in Seg k
by A17, A87, Th21;
then A94:
m2 <= k
by Th3;
k < y
by A11, XREAL_1:31;
then A95:
m2 < y
by A94, XXREAL_0:2;
(
dom q1 c= dom q &
y <= y + j )
by NAT_1:12, RELAT_1:89;
hence
y1 = y2
by A5, A87, A91, A93, A95, FUNCT_1:def 8;
verum end;
now given j1 being
Nat such that A96:
j1 in dom q2
and A97:
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 A98:
j2 in dom q2
and A99:
m2 = (len q1) + j2
;
y1 = y2reconsider j1 =
j1,
j2 =
j2 as
Element of
NAT by ORDINAL1:def 13;
A100:
(q1 ^ q2) . m1 = q2 . j1
by A96, A97, Def7;
A101:
(q1 ^ q2) . m2 = q2 . j2
by A98, A99, Def7;
A102:
(q1 ^ q2) . m1 = q . (y + j1)
by A15, A16, A96, A100;
A103:
(q1 ^ q2) . m2 = q . (y + j2)
by A15, A16, A98, A101;
A104:
1
<= j1
by A15, A96, Th3;
A105:
1
<= j2
by A15, A98, Th3;
A106:
1
<= y + j1
by A104, NAT_1:12;
A107:
1
<= y + j2
by A105, NAT_1:12;
A108:
j1 <= n
by A15, A96, Th3;
A109:
j2 <= n
by A15, A98, Th3;
A110:
y + j1 <= len q
by A13, A108, XREAL_1:9;
A111:
y + j2 <= len q
by A13, A109, XREAL_1:9;
A112:
y + j1 in Seg (len q)
by A106, A110;
A113:
y + j2 in Seg (len q)
by A107, A111;
A114:
y + j1 in dom q
by A112, Def3;
y + j2 in dom q
by A113, Def3;
then
y + j1 = y + j2
by A5, A72, A102, A103, A114, FUNCT_1:def 8;
hence
y1 = y2
by A97, A99;
verum end;
hence
y1 = y2
by A71, A74, A76, A86, Th38;
verum
end; then
(q1 ^ <*x*>) ^ q2 = q
by A19, A115, Def7;
then A121:
len q =
(len (q1 ^ <*x*>)) + (len q2)
by Th35
.=
((len <*x*>) + (len q1)) + (len q2)
by Th35
.=
(1 + (len q1)) + (len q2)
by Th57
.=
1
+ ((len q1) + (len q2))
.=
(len (q1 ^ q2)) + 1
by Th35
;
len (p ^ <*x*>) =
(len p) + (len <*x*>)
by Th35
.=
(len p) + 1
by Th57
;
hence
len (p ^ <*x*>) = len q
by A2, A3, A4, A20, A50, A51, A70, A121, FUNCT_1:84;
verum end;
then A122:
for p being FinSequence
for x being set st S2[p] holds
S2[p ^ <*x*>]
;
for p being FinSequence holds S2[p]
from FINSEQ_1:sch 3(A1, A122);
hence
( rng p = rng q & p is one-to-one & q is one-to-one implies len p = len q )
; verum