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

then A3: p .. f <= len f by FINSEQ_4:21;
A4: len (f :- p) = ((len f) - (p .. f)) + 1 by A2, FINSEQ_5:50;
let i be Nat; :: according to JORDAN23:def 2 :: thesis: ( 1 <= i & i < len (Rotate (f,p)) implies (Rotate (f,p)) . i <> (Rotate (f,p)) . (i + 1) )
1 <= p .. f by A2, FINSEQ_4:21;
then A5: (i -' 1) + (p .. f) >= 0 + 1 by XREAL_1:7;
then A6: ((i -' 1) + (p .. f)) + 1 > 1 by NAT_1:13;
assume that
A7: 1 <= i and
A8: i < len (Rotate (f,p)) ; :: thesis: (Rotate (f,p)) . i <> (Rotate (f,p)) . (i + 1)
A9: i + 1 > 1 by A7, NAT_1:13;
(i - 1) + 1 >= 1 by A7;
then A10: i - 1 >= 1 - 1 by XREAL_1:20;
A11: ((i + 1) -' 1) + (p .. f) = ((i + 1) - 1) + (p .. f) by A7, XREAL_0:def 2
.= ((i - 1) + (p .. f)) + 1
.= ((i -' 1) + (p .. f)) + 1 by A10, XREAL_0:def 2 ;
A12: i + 1 <= len (Rotate (f,p)) by A8, NAT_1:13;
A13: len (Rotate (f,p)) = len f by FINSEQ_6:179;
then A14: len f > 1 by A7, A8, XXREAL_0:2;
then A15: len f >= 1 + 1 by NAT_1:13;

now :: thesis: (Rotate (f,p)) . i <> (Rotate (f,p)) . (i + 1)

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

suppose A16: 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:19;
then (i - 1) + (p .. f) < len f by XREAL_1:20;
then A17: (i -' 1) + (p .. f) < len f by A10, XREAL_0:def 2;
then A18: ((i -' 1) + (p .. f)) + 1 <= len f by NAT_1:13;
(Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f)) by A2, A7, A16, FINSEQ_6:174
.= f . ((i -' 1) + (p .. f)) by A5, A17, FINSEQ_4:15 ;
then A19: (Rotate (f,p)) . i = f . ((i -' 1) + (p .. f)) by A7, A8, FINSEQ_4:15;
i + 1 <= len (f :- p) by A16, NAT_1:13;
then (Rotate (f,p)) /. (i + 1) = f /. (((i + 1) -' 1) + (p .. f)) by A2, A9, FINSEQ_6:174
.= f . (((i + 1) -' 1) + (p .. f)) by A6, A11, A18, FINSEQ_4:15 ;
then (Rotate (f,p)) . (i + 1) = f . (((i + 1) -' 1) + (p .. f)) by A9, A12, FINSEQ_4:15;
hence (Rotate (f,p)) . i <> (Rotate (f,p)) . (i + 1) by A1, A5, A11, A17, A19; :: thesis: verum

end;

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

then (Rotate (f,p)) /. i = f /. (len f) by A2, FINSEQ_6:176
.= f /. 1 by A1, FINSEQ_6:def 1
.= f . 1 by A14, FINSEQ_4:15 ;
then A21: (Rotate (f,p)) . i = f . 1 by A7, A8, FINSEQ_4:15;
A22: ((i + 1) + (p .. f)) -' (len f) = ((len f) + (1 + 1)) - (len f) by A4, A20, XREAL_0:def 2
.= 2 ;
i + 1 > len (f :- p) by A20, NAT_1:13;
then (Rotate (f,p)) /. (i + 1) = f /. (((i + 1) + (p .. f)) -' (len f)) by A2, A13, A12, FINSEQ_6:177
.= f . (((i + 1) + (p .. f)) -' (len f)) by A15, A22, FINSEQ_4:15 ;
then (Rotate (f,p)) . (i + 1) = f . (1 + 1) by A9, A12, A22, FINSEQ_4:15;
hence (Rotate (f,p)) . i <> (Rotate (f,p)) . (i + 1) by A1, A14, A21; :: thesis: verum

end;

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

then A24: i - ((len f) - (p .. f)) > 1 by A4, XREAL_1:20;
then (i + (p .. f)) - (len f) > 1 - 1 by XXREAL_0:2;
then A25: ((i + (p .. f)) - (len f)) + 1 > 1 by XREAL_1:19;
then A26: ((i + 1) + (p .. f)) -' (len f) = ((i + 1) + (p .. f)) - (len f) by XREAL_0:def 2
.= ((i + (p .. f)) - (len f)) + 1
.= ((i + (p .. f)) -' (len f)) + 1 by A24, XREAL_0:def 2 ;
(i + 1) + (p .. f) <= (len f) + (len f) by A3, A13, A12, XREAL_1:7;
then ((i + 1) + (p .. f)) - (len f) <= len f by XREAL_1:20;
then A27: ((i + 1) + (p .. f)) -' (len f) <= len f by A25, XREAL_0:def 2;
((i + 1) + (p .. f)) - (len f) > 1 by A25;
then A28: ((i + 1) + (p .. f)) -' (len f) > 1 by XREAL_0:def 2;
i + 1 > len (f :- p) by A23, NAT_1:13;
then (Rotate (f,p)) /. (i + 1) = f /. (((i + 1) + (p .. f)) -' (len f)) by A2, A13, A12, FINSEQ_6:177
.= f . (((i + 1) + (p .. f)) -' (len f)) by A28, A27, FINSEQ_4:15 ;
then A29: (Rotate (f,p)) . (i + 1) = f . (((i + 1) + (p .. f)) -' (len f)) by A9, A12, FINSEQ_4:15;
(i + (p .. f)) - (len f) > 1 by A24;
then A30: (i + (p .. f)) -' (len f) > 1 by XREAL_0:def 2;
i + (p .. f) < (len f) + (len f) by A3, A13, A8, XREAL_1:8;
then (i + (p .. f)) - (len f) < len f by XREAL_1:19;
then A31: (i + (p .. f)) -' (len f) < len f by A24, XREAL_0:def 2;
(Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) by A2, A13, A8, A23, FINSEQ_6:177
.= f . ((i + (p .. f)) -' (len f)) by A30, A31, FINSEQ_4:15 ;
then (Rotate (f,p)) . i = f . ((i + (p .. f)) -' (len f)) by A7, A8, FINSEQ_4:15;
hence (Rotate (f,p)) . i <> (Rotate (f,p)) . (i + 1) by A1, A30, A31, A29, A26; :: 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;