let D be non empty set ; for f being FinSequence of D st f is almost-one-to-one holds
for p being Element of D holds Rotate (f,p) is almost-one-to-one
let f be FinSequence of D; ( f is almost-one-to-one implies for p being Element of D holds Rotate (f,p) is almost-one-to-one )
assume A1:
f is almost-one-to-one
; for p being Element of D holds Rotate (f,p) is almost-one-to-one
let p be Element of D; Rotate (f,p) is almost-one-to-one
per cases
( p in rng f or not p in rng f )
;
suppose A2:
p in rng f
;
Rotate (f,p) is almost-one-to-one then
0 + 1
<= p .. f
by FINSEQ_4:21;
then A3:
(p .. f) - 1
>= 0
by XREAL_1:19;
A4:
len (f :- p) = ((len f) - (p .. f)) + 1
by A2, FINSEQ_5:50;
let i,
j be
Nat;
JORDAN23:def 1 ( i in dom (Rotate (f,p)) & j in dom (Rotate (f,p)) & ( i <> 1 or j <> len (Rotate (f,p)) ) & ( i <> len (Rotate (f,p)) or j <> 1 ) & (Rotate (f,p)) . i = (Rotate (f,p)) . j implies i = j )assume that A5:
i in dom (Rotate (f,p))
and A6:
j in dom (Rotate (f,p))
and A7:
(
i <> 1 or
j <> len (Rotate (f,p)) )
and A8:
(
i <> len (Rotate (f,p)) or
j <> 1 )
and A9:
(Rotate (f,p)) . i = (Rotate (f,p)) . j
;
i = jA10:
0 + 1
<= i
by A5, FINSEQ_3:25;
A11:
dom (Rotate (f,p)) = dom f
by FINSEQ_6:180;
then A12:
i <= len f
by A5, FINSEQ_3:25;
then A13:
i - (len f) <= (len f) - (len f)
by XREAL_1:9;
A14:
j <= len f
by A6, A11, FINSEQ_3:25;
then A15:
j - (len f) <= (len f) - (len f)
by XREAL_1:9;
A16:
len (Rotate (f,p)) = len f
by FINSEQ_6:179;
A17:
0 + 1
<= j
by A6, FINSEQ_3:25;
then A18:
j - 1
>= 0
by XREAL_1:19;
A23:
p .. f <= len f
by A2, FINSEQ_4:21;
A24:
i - 1
>= 0
by A10, XREAL_1:19;
now i = jper cases
( i <= len (f :- p) or i > len (f :- p) )
;
suppose A29:
i <= len (f :- p)
;
i = jthen
i in dom (f :- p)
by A10, FINSEQ_3:25;
then
(i -' 1) + 1
in dom (f :- p)
by A10, XREAL_1:235;
then A30:
(i -' 1) + (p .. f) in dom f
by A2, FINSEQ_5:51;
(Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f))
by A2, A10, A29, FINSEQ_6:174;
then A31:
(Rotate (f,p)) . i = f /. ((i -' 1) + (p .. f))
by A5, PARTFUN1:def 6;
now i = jper cases
( j <= len (f :- p) or j > len (f :- p) )
;
suppose A32:
j <= len (f :- p)
;
i = jthen
j in dom (f :- p)
by A17, FINSEQ_3:25;
then
(j -' 1) + 1
in dom (f :- p)
by A17, XREAL_1:235;
then A33:
(j -' 1) + (p .. f) in dom f
by A2, FINSEQ_5:51;
(Rotate (f,p)) /. j = f /. ((j -' 1) + (p .. f))
by A2, A17, A32, FINSEQ_6:174;
then A34:
f /. ((i -' 1) + (p .. f)) = f /. ((j -' 1) + (p .. f))
by A6, A9, A31, PARTFUN1:def 6;
f . ((i -' 1) + (p .. f)) =
f /. ((i -' 1) + (p .. f))
by A30, PARTFUN1:def 6
.=
f . ((j -' 1) + (p .. f))
by A34, A33, PARTFUN1:def 6
;
then
(i -' 1) + (p .. f) = (j -' 1) + (p .. f)
by A1, A25, A19, A30, A33;
hence
i = j
by A10, A17, XREAL_1:234;
verum end; suppose A35:
j > len (f :- p)
;
i = jthen
(Rotate (f,p)) /. j = f /. ((j + (p .. f)) -' (len f))
by A2, A14, FINSEQ_6:177;
then A36:
f /. ((i -' 1) + (p .. f)) = f /. ((j + (p .. f)) -' (len f))
by A6, A9, A31, PARTFUN1:def 6;
A37:
j - ((len f) - (p .. f)) > 1
by A4, A35, XREAL_1:20;
then A38:
(j + (p .. f)) - (len f) > 1
;
then A39:
(j + (p .. f)) -' (len f) >= 1
by XREAL_0:def 2;
j + (p .. f) <= (len f) + (len f)
by A23, A14, XREAL_1:7;
then
(j + (p .. f)) - (len f) <= len f
by XREAL_1:20;
then
(j + (p .. f)) -' (len f) <= len f
by A37, XREAL_0:def 2;
then A40:
(j + (p .. f)) -' (len f) in dom f
by A39, FINSEQ_3:25;
A45:
(
(i -' 1) + (p .. f) <> len f or
(j + (p .. f)) -' (len f) <> 1 )
by A38, XREAL_0:def 2;
f . ((i -' 1) + (p .. f)) =
f /. ((i -' 1) + (p .. f))
by A30, PARTFUN1:def 6
.=
f . ((j + (p .. f)) -' (len f))
by A36, A40, PARTFUN1:def 6
;
then
(i -' 1) + (p .. f) = (j + (p .. f)) -' (len f)
by A1, A30, A41, A45, A40;
then A46:
(i -' 1) + (p .. f) = (j + (p .. f)) - (len f)
by A37, XREAL_0:def 2;
then A47:
j - (len f) = 0
by A15;
i - 1
= 0
by A24, A15, A46, XREAL_0:def 2;
hence
i = j
by A7, A47, FINSEQ_6:179;
verum end; end; end; hence
i = j
;
verum end; suppose A48:
i > len (f :- p)
;
i = jthen A49:
i - ((len f) - (p .. f)) > 1
by A4, XREAL_1:20;
i + (p .. f) <= (len f) + (len f)
by A23, A12, XREAL_1:7;
then
(i + (p .. f)) - (len f) <= len f
by XREAL_1:20;
then A50:
(i + (p .. f)) -' (len f) <= len f
by A49, XREAL_0:def 2;
A51:
(i + (p .. f)) - (len f) > 1
by A49;
then
(i + (p .. f)) -' (len f) >= 1
by XREAL_0:def 2;
then A52:
(i + (p .. f)) -' (len f) in dom f
by A50, FINSEQ_3:25;
A53:
(Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f))
by A2, A12, A48, FINSEQ_6:177;
now i = jper cases
( j <= len (f :- p) or j > len (f :- p) )
;
suppose A54:
j <= len (f :- p)
;
i = j
(Rotate (f,p)) /. j = f /. ((j -' 1) + (p .. f))
by A2, A17, A54, FINSEQ_6:174;
then
(Rotate (f,p)) . j = f /. ((j -' 1) + (p .. f))
by A6, PARTFUN1:def 6;
then A59:
f /. ((j -' 1) + (p .. f)) = f /. ((i + (p .. f)) -' (len f))
by A5, A9, A53, PARTFUN1:def 6;
A60:
(
(j -' 1) + (p .. f) <> len f or
(i + (p .. f)) -' (len f) <> 1 )
by A51, XREAL_0:def 2;
j in dom (f :- p)
by A17, A54, FINSEQ_3:25;
then
(j -' 1) + 1
in dom (f :- p)
by A17, XREAL_1:235;
then A61:
(j -' 1) + (p .. f) in dom f
by A2, FINSEQ_5:51;
then f . ((j -' 1) + (p .. f)) =
f /. ((j -' 1) + (p .. f))
by PARTFUN1:def 6
.=
f . ((i + (p .. f)) -' (len f))
by A52, A59, PARTFUN1:def 6
;
then
(j -' 1) + (p .. f) = (i + (p .. f)) -' (len f)
by A1, A52, A61, A55, A60;
then A62:
(j -' 1) + (p .. f) = (i + (p .. f)) - (len f)
by A49, XREAL_0:def 2;
then A63:
i - (len f) = 0
by A13;
j - 1
= 0
by A18, A13, A62, XREAL_0:def 2;
hence
i = j
by A8, A63, FINSEQ_6:179;
verum end; suppose A64:
j > len (f :- p)
;
i = jthen
(Rotate (f,p)) /. j = f /. ((j + (p .. f)) -' (len f))
by A2, A14, FINSEQ_6:177;
then
(Rotate (f,p)) . j = f /. ((j + (p .. f)) -' (len f))
by A6, PARTFUN1:def 6;
then A65:
f /. ((j + (p .. f)) -' (len f)) = f /. ((i + (p .. f)) -' (len f))
by A5, A9, A53, PARTFUN1:def 6;
A66:
(
(i + (p .. f)) -' (len f) <> 1 or
(j + (p .. f)) -' (len f) <> len f )
by A51, XREAL_0:def 2;
A67:
j - ((len f) - (p .. f)) > 1
by A4, A64, XREAL_1:20;
then A68:
(j + (p .. f)) - (len f) > 1
;
then A69:
(j + (p .. f)) -' (len f) >= 1
by XREAL_0:def 2;
j + (p .. f) <= (len f) + (len f)
by A23, A14, XREAL_1:7;
then
(j + (p .. f)) - (len f) <= len f
by XREAL_1:20;
then
(j + (p .. f)) -' (len f) <= len f
by A67, XREAL_0:def 2;
then A70:
(j + (p .. f)) -' (len f) in dom f
by A69, FINSEQ_3:25;
A71:
(
(i + (p .. f)) -' (len f) <> len f or
(j + (p .. f)) -' (len f) <> 1 )
by A68, XREAL_0:def 2;
f . ((i + (p .. f)) -' (len f)) =
f /. ((i + (p .. f)) -' (len f))
by A52, PARTFUN1:def 6
.=
f . ((j + (p .. f)) -' (len f))
by A65, A70, PARTFUN1:def 6
;
then
(i + (p .. f)) -' (len f) = (j + (p .. f)) -' (len f)
by A1, A52, A70, A66, A71;
then
(i + (p .. f)) - (len f) = (j + (p .. f)) -' (len f)
by A49, XREAL_0:def 2;
then
(i + (p .. f)) - (len f) = (j + (p .. f)) - (len f)
by A67, XREAL_0:def 2;
hence
i = j
;
verum end; end; end; hence
i = j
;
verum end; end; end; hence
i = j
;
verum end; end;