let D be non empty set ; :: thesis: for f being FinSequence of D st f is weakly-one-to-one & f is circular holds
for p being Element of D holds Rotate f,p is weakly-one-to-one
let f be FinSequence of D; :: thesis: ( f is weakly-one-to-one & f is circular implies for p being Element of D holds Rotate f,p is weakly-one-to-one )
assume A1: ( f is weakly-one-to-one & f is circular ) ; :: thesis: for p being Element of D holds Rotate f,p is weakly-one-to-one
let p be Element of D; :: thesis: Rotate f,p is weakly-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 weakly-one-to-one

let i be Element of NAT ; :: according to JORDAN23:def 2 :: thesis: ( 1 <= i & i < len (Rotate f,p) implies (Rotate f,p) . i <> (Rotate f,p) . (i + 1) )
A3: ( 1 <= p .. f & p .. f <= len f ) by A2, FINSEQ_4:31;
A4: len (f :- p) = ((len f) - (p .. f)) + 1 by A2, FINSEQ_5:53;
A5: len (Rotate f,p) = len f by REVROT_1:14;
assume A6: ( 1 <= i & i < len (Rotate f,p) ) ; :: thesis: (Rotate f,p) . i <> (Rotate f,p) . (i + 1)
then A7: ( i + 1 > 1 & i + 1 <= len (Rotate f,p) ) by NAT_1:13;
A8: len f > 1 by A5, A6, XXREAL_0:2;
then A9: len f >= 1 + 1 by NAT_1:13;
(i - 1) + 1 >= 1 by A6;
then A10: i - 1 >= 1 - 1 by XREAL_1:22;
A11: (i -' 1) + (p .. f) >= 0 + 1 by A3, XREAL_1:9;
then A12: ((i -' 1) + (p .. f)) + 1 > 1 by NAT_1:13;
A13: ((i + 1) -' 1) + (p .. f) = ((i + 1) - 1) + (p .. f) by A6, XREAL_0:def 2
.= ((i - 1) + (p .. f)) + 1
.= ((i -' 1) + (p .. f)) + 1 by A10, XREAL_0:def 2 ;

now

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

suppose A14: i < len (f :- p) ; :: thesis: (Rotate f,p) . i <> (Rotate f,p) . (i + 1)

then i - 1 < (len f) - (p .. f) by A4, XREAL_1:21;
then (i - 1) + (p .. f) < len f by XREAL_1:22;
then A15: (i -' 1) + (p .. f) < len f by A10, XREAL_0:def 2;
then A16: ((i -' 1) + (p .. f)) + 1 <= len f by NAT_1:13;
i + 1 <= len (f :- p) by A14, NAT_1:13;
then (Rotate f,p) /. (i + 1) = f /. (((i + 1) -' 1) + (p .. f)) by A2, A7, REVROT_1:9
.= f . (((i + 1) -' 1) + (p .. f)) by A12, A13, A16, FINSEQ_4:24 ;
then A17: (Rotate f,p) . (i + 1) = f . (((i + 1) -' 1) + (p .. f)) by A7, FINSEQ_4:24;
(Rotate f,p) /. i = f /. ((i -' 1) + (p .. f)) by A2, A6, A14, REVROT_1:9
.= f . ((i -' 1) + (p .. f)) by A11, A15, FINSEQ_4:24 ;
then (Rotate f,p) . i = f . ((i -' 1) + (p .. f)) by A6, FINSEQ_4:24;
hence (Rotate f,p) . i <> (Rotate f,p) . (i + 1) by A1, A11, A13, A15, A17, Def2; :: thesis: verum

end;

suppose A18: i = len (f :- p) ; :: thesis: (Rotate f,p) . i <> (Rotate f,p) . (i + 1)

then (Rotate f,p) /. i = f /. (len f) by A2, REVROT_1:11
.= f /. 1 by A1, FINSEQ_6:def 1
.= f . 1 by A8, FINSEQ_4:24 ;
then A19: (Rotate f,p) . i = f . 1 by A6, FINSEQ_4:24;
A20: ((i + 1) + (p .. f)) -' (len f) = ((len f) + (1 + 1)) - (len f) by A4, A18, XREAL_0:def 2
.= 2 ;
i + 1 > len (f :- p) by A18, NAT_1:13;
then (Rotate f,p) /. (i + 1) = f /. (((i + 1) + (p .. f)) -' (len f)) by A2, A5, A7, REVROT_1:12
.= f . (((i + 1) + (p .. f)) -' (len f)) by A9, A20, FINSEQ_4:24 ;
then (Rotate f,p) . (i + 1) = f . (1 + 1) by A7, A20, FINSEQ_4:24;
hence (Rotate f,p) . i <> (Rotate f,p) . (i + 1) by A1, A8, A19, Def2; :: thesis: verum

end;

suppose A21: i > len (f :- p) ; :: thesis: (Rotate f,p) . i <> (Rotate f,p) . (i + 1)

then A22: i - ((len f) - (p .. f)) > 1 by A4, XREAL_1:22;
then A23: (i + (p .. f)) - (len f) > 1 ;
A24: (i + (p .. f)) - (len f) > 1 - 1 by A22, XXREAL_0:2;
A25: (i + (p .. f)) -' (len f) > 1 by A23, XREAL_0:def 2;
A26: ((i + (p .. f)) - (len f)) + 1 > 1 by A24, XREAL_1:21;
then ((i + 1) + (p .. f)) - (len f) > 1 ;
then A27: ((i + 1) + (p .. f)) -' (len f) > 1 by XREAL_0:def 2;
i + (p .. f) < (len f) + (len f) by A3, A5, A6, XREAL_1:10;
then (i + (p .. f)) - (len f) < len f by XREAL_1:21;
then A28: (i + (p .. f)) -' (len f) < len f by A22, XREAL_0:def 2;
(i + 1) + (p .. f) <= (len f) + (len f) by A3, A5, A7, XREAL_1:9;
then ((i + 1) + (p .. f)) - (len f) <= len f by XREAL_1:22;
then A29: ((i + 1) + (p .. f)) -' (len f) <= len f by A26, XREAL_0:def 2;
i + 1 > len (f :- p) by A21, NAT_1:13;
then (Rotate f,p) /. (i + 1) = f /. (((i + 1) + (p .. f)) -' (len f)) by A2, A5, A7, REVROT_1:12
.= f . (((i + 1) + (p .. f)) -' (len f)) by A27, A29, FINSEQ_4:24 ;
then A30: (Rotate f,p) . (i + 1) = f . (((i + 1) + (p .. f)) -' (len f)) by A7, FINSEQ_4:24;
(Rotate f,p) /. i = f /. ((i + (p .. f)) -' (len f)) by A2, A5, A6, A21, REVROT_1:12
.= f . ((i + (p .. f)) -' (len f)) by A25, A28, FINSEQ_4:24 ;
then A31: (Rotate f,p) . i = f . ((i + (p .. f)) -' (len f)) by A6, FINSEQ_4:24;
((i + 1) + (p .. f)) -' (len f) = ((i + 1) + (p .. f)) - (len f) by A26, XREAL_0:def 2
.= ((i + (p .. f)) - (len f)) + 1
.= ((i + (p .. f)) -' (len f)) + 1 by A22, XREAL_0:def 2 ;
hence (Rotate f,p) . i <> (Rotate f,p) . (i + 1) by A1, A25, A28, A30, A31, Def2; :: thesis: verum

end;

end;

end;

hence (Rotate f,p) . i <> (Rotate f,p) . (i + 1) ; :: thesis: verum

end;

suppose not p in rng f ; :: thesis: Rotate f,p is weakly-one-to-one

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

end;

end;