let D be non empty set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: for p being Element of D holds Rotate (f,p) is almost-one-to-one
let p be Element of D; :: thesis: 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 ; :: thesis: 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; :: according to JORDAN23:def 1 :: thesis: ( 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 ; :: thesis: i = j
A10: 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;

A19: now :: thesis: ( (i -' 1) + (p .. f) = len f implies not (j -' 1) + (p .. f) = 1 )

assume that
A20: (i -' 1) + (p .. f) = len f and
A21: (j -' 1) + (p .. f) = 1 ; :: thesis: contradiction
(j -' 1) + ((p .. f) - 1) = 0 by A21;
then A22: j -' 1 = 0 by A3;
then j - 1 = 0 by A18, XREAL_0:def 2;
hence contradiction by A8, A16, A10, A20, A21, A22, XREAL_1:235; :: thesis: verum

end;

A23: p .. f <= len f by A2, FINSEQ_4:21;
A24: i - 1 >= 0 by A10, XREAL_1:19;

A25: now :: thesis: ( (i -' 1) + (p .. f) = 1 implies not (j -' 1) + (p .. f) = len f )

assume that
A26: (i -' 1) + (p .. f) = 1 and
A27: (j -' 1) + (p .. f) = len f ; :: thesis: contradiction
(i -' 1) + ((p .. f) - 1) = 0 by A26;
then A28: i -' 1 = 0 by A3;
then i - 1 = 0 by A24, XREAL_0:def 2;
hence contradiction by A7, A16, A17, A26, A27, A28, XREAL_1:235; :: thesis: verum

end;

now :: thesis: i = j

per cases ( i <= len (f :- p) or i > len (f :- p) ) ;

suppose A29: i <= len (f :- p) ; :: thesis: i = j

then 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 :: thesis: i = j

per cases ( j <= len (f :- p) or j > len (f :- p) ) ;

suppose A32: j <= len (f :- p) ; :: thesis: i = j

then 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; :: thesis: verum

end;

suppose A35: j > len (f :- p) ; :: thesis: i = j

then (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;

A41: now :: thesis: ( (i -' 1) + (p .. f) = 1 implies not (j + (p .. f)) -' (len f) = len f )

assume that
A42: (i -' 1) + (p .. f) = 1 and
A43: (j + (p .. f)) -' (len f) = len f ; :: thesis: contradiction
(j + (p .. f)) - (len f) = len f by A37, A43, XREAL_0:def 2;
then j + (p .. f) = (len f) + (len f) ;
then A44: j >= len f by A23, XREAL_1:8;
(i -' 1) + ((p .. f) - 1) = 0 by A42;
then i -' 1 = 0 by A3;
then i - 1 = 0 by A24, XREAL_0:def 2;
hence contradiction by A7, A16, A14, A44, XXREAL_0:1; :: thesis: verum

end;

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; :: thesis: verum

end;

end;

end;

hence i = j ; :: thesis: verum

end;

suppose A48: i > len (f :- p) ; :: thesis: i = j

then 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 :: thesis: i = j

per cases ( j <= len (f :- p) or j > len (f :- p) ) ;

suppose A54: j <= len (f :- p) ; :: thesis: i = j

A55: now :: thesis: ( (j -' 1) + (p .. f) = 1 implies not (i + (p .. f)) -' (len f) = len f )

assume that
A56: (j -' 1) + (p .. f) = 1 and
A57: (i + (p .. f)) -' (len f) = len f ; :: thesis: contradiction
(i + (p .. f)) - (len f) = len f by A49, A57, XREAL_0:def 2;
then i + (p .. f) = (len f) + (len f) ;
then A58: i >= len f by A23, XREAL_1:8;
(j -' 1) + ((p .. f) - 1) = 0 by A56;
then j -' 1 = 0 by A3;
then j - 1 = 0 by A18, XREAL_0:def 2;
hence contradiction by A8, A16, A12, A58, XXREAL_0:1; :: thesis: verum

end;

(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; :: thesis: verum

end;

suppose A64: j > len (f :- p) ; :: thesis: i = j

then (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 ; :: thesis: verum

end;

end;

end;

hence i = j ; :: thesis: verum

end;

end;

end;

hence i = j ; :: thesis: verum

end;

suppose not p in rng f ; :: thesis: Rotate (f,p) is almost-one-to-one

hence Rotate (f,p) is almost-one-to-one by A1, FINSEQ_6:def 2; :: thesis: verum

end;

end;