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 A3: ( 0 + 1 <= p .. f & p .. f <= len f ) by FINSEQ_4:31;
A4: len (f :- p) = ((len f) - (p .. f)) + 1 by A2, FINSEQ_5:53;
let i, j be Element of 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: dom (Rotate f,p) = dom f by REVROT_1:15;
A11: len (Rotate f,p) = len f by REVROT_1:14;
A12: ( 0 + 1 <= i & i <= len f ) by A5, A10, FINSEQ_3:27;
A13: ( 0 + 1 <= j & j <= len f ) by A6, A10, FINSEQ_3:27;
then A14: ( i - 1 >= 0 & j - 1 >= 0 ) by A12, XREAL_1:21;
A16: ( j - (len f) <= (len f) - (len f) & i - (len f) <= (len f) - (len f) ) by A12, A13, XREAL_1:11;
A17: (p .. f) - 1 >= 0 by A3, XREAL_1:21;

A18: now

assume A19: ( (i -' 1) + (p .. f) = 1 & (j -' 1) + (p .. f) = len f ) ; :: thesis: contradiction
then (i -' 1) + ((p .. f) - 1) = 0 ;
then A20: ( i -' 1 = 0 & (p .. f) - 1 = 0 ) by A17;
then i - 1 = 0 by A14, XREAL_0:def 2;
hence contradiction by A7, A11, A13, A19, A20, XREAL_1:237; :: thesis: verum

end;

A21: now

assume A22: ( (i -' 1) + (p .. f) = len f & (j -' 1) + (p .. f) = 1 ) ; :: thesis: contradiction
then (j -' 1) + ((p .. f) - 1) = 0 ;
then A23: ( j -' 1 = 0 & (p .. f) - 1 = 0 ) by A17;
then j - 1 = 0 by A14, XREAL_0:def 2;
hence contradiction by A8, A11, A12, A22, A23, XREAL_1:237; :: thesis: verum

end;

now

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

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

then (Rotate f,p) /. i = f /. ((i -' 1) + (p .. f)) by A2, A12, REVROT_1:9;
then A25: (Rotate f,p) . i = f /. ((i -' 1) + (p .. f)) by A5, PARTFUN1:def 8;
i in dom (f :- p) by A12, A24, FINSEQ_3:27;
then (i -' 1) + 1 in dom (f :- p) by A12, XREAL_1:237;
then A26: (i -' 1) + (p .. f) in dom f by A2, FINSEQ_5:54;

now

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

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

then (Rotate f,p) /. j = f /. ((j -' 1) + (p .. f)) by A2, A13, REVROT_1:9;
then A28: f /. ((i -' 1) + (p .. f)) = f /. ((j -' 1) + (p .. f)) by A6, A9, A25, PARTFUN1:def 8;
j in dom (f :- p) by A13, A27, FINSEQ_3:27;
then (j -' 1) + 1 in dom (f :- p) by A13, XREAL_1:237;
then A29: (j -' 1) + (p .. f) in dom f by A2, FINSEQ_5:54;
f . ((i -' 1) + (p .. f)) = f /. ((i -' 1) + (p .. f)) by A26, PARTFUN1:def 8
.= f . ((j -' 1) + (p .. f)) by A28, A29, PARTFUN1:def 8 ;
then (i -' 1) + (p .. f) = (j -' 1) + (p .. f) by A1, A18, A21, A26, A29, Def1;
hence i = j by A12, A13, XREAL_1:236; :: thesis: verum

end;

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

then (Rotate f,p) /. j = f /. ((j + (p .. f)) -' (len f)) by A2, A13, REVROT_1:12;
then A31: f /. ((i -' 1) + (p .. f)) = f /. ((j + (p .. f)) -' (len f)) by A6, A9, A25, PARTFUN1:def 8;
A32: j - ((len f) - (p .. f)) > 1 by A4, A30, XREAL_1:22;
then A33: (j + (p .. f)) - (len f) > 1 ;
then A34: (j + (p .. f)) -' (len f) >= 1 by XREAL_0:def 2;

A35: now

assume A36: ( (i -' 1) + (p .. f) = 1 & (j + (p .. f)) -' (len f) = len f ) ; :: thesis: contradiction
then (i -' 1) + ((p .. f) - 1) = 0 ;
then ( i -' 1 = 0 & (p .. f) - 1 = 0 ) by A17;
then A37: i - 1 = 0 by A14, XREAL_0:def 2;
(j + (p .. f)) - (len f) = len f by A32, A36, XREAL_0:def 2;
then j + (p .. f) = (len f) + (len f) ;
then j >= len f by A3, XREAL_1:10;
hence contradiction by A7, A11, A13, A37, XXREAL_0:1; :: thesis: verum

end;

A38: ( (i -' 1) + (p .. f) <> len f or (j + (p .. f)) -' (len f) <> 1 ) by A33, XREAL_0:def 2;
j + (p .. f) <= (len f) + (len f) by A3, A13, XREAL_1:9;
then (j + (p .. f)) - (len f) <= len f by XREAL_1:22;
then (j + (p .. f)) -' (len f) <= len f by A32, XREAL_0:def 2;
then A39: (j + (p .. f)) -' (len f) in dom f by A34, FINSEQ_3:27;
f . ((i -' 1) + (p .. f)) = f /. ((i -' 1) + (p .. f)) by A26, PARTFUN1:def 8
.= f . ((j + (p .. f)) -' (len f)) by A31, A39, PARTFUN1:def 8 ;
then (i -' 1) + (p .. f) = (j + (p .. f)) -' (len f) by A1, A26, A35, A38, A39, Def1;
then (i -' 1) + (p .. f) = (j + (p .. f)) - (len f) by A32, XREAL_0:def 2;
then ( i - 1 = 0 & j - (len f) = 0 ) by A14, A16, XREAL_0:def 2;
hence i = j by A7, REVROT_1:14; :: thesis: verum

end;

end;

end;

hence i = j ; :: thesis: verum

end;

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

then A41: (Rotate f,p) /. i = f /. ((i + (p .. f)) -' (len f)) by A2, A12, REVROT_1:12;
A42: i - ((len f) - (p .. f)) > 1 by A4, A40, XREAL_1:22;
then A43: (i + (p .. f)) - (len f) > 1 ;
then A44: (i + (p .. f)) -' (len f) >= 1 by XREAL_0:def 2;
i + (p .. f) <= (len f) + (len f) by A3, A12, XREAL_1:9;
then (i + (p .. f)) - (len f) <= len f by XREAL_1:22;
then (i + (p .. f)) -' (len f) <= len f by A42, XREAL_0:def 2;
then A45: (i + (p .. f)) -' (len f) in dom f by A44, FINSEQ_3:27;

now

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

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

then (Rotate f,p) /. j = f /. ((j -' 1) + (p .. f)) by A2, A13, REVROT_1:9;
then (Rotate f,p) . j = f /. ((j -' 1) + (p .. f)) by A6, PARTFUN1:def 8;
then A47: f /. ((j -' 1) + (p .. f)) = f /. ((i + (p .. f)) -' (len f)) by A5, A9, A41, PARTFUN1:def 8;
j in dom (f :- p) by A13, A46, FINSEQ_3:27;
then (j -' 1) + 1 in dom (f :- p) by A13, XREAL_1:237;
then A48: (j -' 1) + (p .. f) in dom f by A2, FINSEQ_5:54;

A49: now

assume A50: ( (j -' 1) + (p .. f) = 1 & (i + (p .. f)) -' (len f) = len f ) ; :: thesis: contradiction
then (j -' 1) + ((p .. f) - 1) = 0 ;
then ( j -' 1 = 0 & (p .. f) - 1 = 0 ) by A17;
then A51: j - 1 = 0 by A14, XREAL_0:def 2;
(i + (p .. f)) - (len f) = len f by A42, A50, XREAL_0:def 2;
then i + (p .. f) = (len f) + (len f) ;
then i >= len f by A3, XREAL_1:10;
hence contradiction by A8, A11, A12, A51, XXREAL_0:1; :: thesis: verum

end;

A52: ( (j -' 1) + (p .. f) <> len f or (i + (p .. f)) -' (len f) <> 1 ) by A43, XREAL_0:def 2;
f . ((j -' 1) + (p .. f)) = f /. ((j -' 1) + (p .. f)) by A48, PARTFUN1:def 8
.= f . ((i + (p .. f)) -' (len f)) by A45, A47, PARTFUN1:def 8 ;
then (j -' 1) + (p .. f) = (i + (p .. f)) -' (len f) by A1, A45, A48, A49, A52, Def1;
then (j -' 1) + (p .. f) = (i + (p .. f)) - (len f) by A42, XREAL_0:def 2;
then ( j - 1 = 0 & i - (len f) = 0 ) by A14, A16, XREAL_0:def 2;
hence i = j by A8, REVROT_1:14; :: thesis: verum

end;

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

then (Rotate f,p) /. j = f /. ((j + (p .. f)) -' (len f)) by A2, A13, REVROT_1:12;
then (Rotate f,p) . j = f /. ((j + (p .. f)) -' (len f)) by A6, PARTFUN1:def 8;
then A54: f /. ((j + (p .. f)) -' (len f)) = f /. ((i + (p .. f)) -' (len f)) by A5, A9, A41, PARTFUN1:def 8;
A55: j - ((len f) - (p .. f)) > 1 by A4, A53, XREAL_1:22;
then A56: (j + (p .. f)) - (len f) > 1 ;
then A57: (j + (p .. f)) -' (len f) >= 1 by XREAL_0:def 2;
j + (p .. f) <= (len f) + (len f) by A3, A13, XREAL_1:9;
then (j + (p .. f)) - (len f) <= len f by XREAL_1:22;
then (j + (p .. f)) -' (len f) <= len f by A55, XREAL_0:def 2;
then A58: (j + (p .. f)) -' (len f) in dom f by A57, FINSEQ_3:27;
A59: ( (i + (p .. f)) -' (len f) <> 1 or (j + (p .. f)) -' (len f) <> len f ) by A43, XREAL_0:def 2;
A60: ( (i + (p .. f)) -' (len f) <> len f or (j + (p .. f)) -' (len f) <> 1 ) by A56, XREAL_0:def 2;
f . ((i + (p .. f)) -' (len f)) = f /. ((i + (p .. f)) -' (len f)) by A45, PARTFUN1:def 8
.= f . ((j + (p .. f)) -' (len f)) by A54, A58, PARTFUN1:def 8 ;
then (i + (p .. f)) -' (len f) = (j + (p .. f)) -' (len f) by A1, A45, A58, A59, A60, Def1;
then (i + (p .. f)) - (len f) = (j + (p .. f)) -' (len f) by A42, XREAL_0:def 2;
then (i + (p .. f)) - (len f) = (j + (p .. f)) - (len f) by A55, 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;