let p be Point of (TOP-REAL 2); :: thesis: for f being circular FinSequence of (TOP-REAL 2) holds L~ (Rotate f,p) = L~ f
let f be circular FinSequence of (TOP-REAL 2); :: thesis: L~ (Rotate f,p) = L~ f

per cases ( not p in rng f or p in rng f ) ;

suppose not p in rng f ; :: thesis: L~ (Rotate f,p) = L~ f

hence L~ (Rotate f,p) = L~ f by FINSEQ_6:def 2; :: thesis: verum

end;

suppose A1: p in rng f ; :: thesis: L~ (Rotate f,p) = L~ f

A2: len (Rotate f,p) = len f by Th14;
set A = { (LSeg (Rotate f,p),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
set B = { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
{ (LSeg (Rotate f,p),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } = { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) }

proof

A3: p .. f <= len f by A1, FINSEQ_4:31;
thus { (LSeg (Rotate f,p),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } c= { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } :: according to XBOOLE_0:def 10 :: thesis: { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } c= { (LSeg (Rotate f,p),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (LSeg (Rotate f,p),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } or x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } )
assume x in { (LSeg (Rotate f,p),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; :: thesis: x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) }
then consider i being Element of NAT such that
A4: x = LSeg (Rotate f,p),i and
A5: 1 <= i and
A6: i + 1 <= len f ;
A7: i < len f by A6, NAT_1:13;
A8: 1 <= p .. f by A1, FINSEQ_4:31;

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

suppose A9: i < len (f :- p) ; :: thesis: x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) }

then A10: LSeg (Rotate f,p),i = LSeg f,((i -' 1) + (p .. f)) by A1, A5, Th24;
1 + 1 <= i + (p .. f) by A5, A8, XREAL_1:9;
then 1 <= (i + (p .. f)) -' 1 by NAT_D:55;
then A11: 1 <= (i -' 1) + (p .. f) by A5, NAT_D:38;
i < ((len f) - (p .. f)) + 1 by A1, A9, FINSEQ_5:53;
then i < ((len f) -' (p .. f)) + 1 by A3, XREAL_1:235;
then i -' 1 < (len f) -' (p .. f) by A5, NAT_D:54;
then (i -' 1) + (p .. f) < len f by NAT_D:53;
then ((i -' 1) + (p .. f)) + 1 <= len f by NAT_1:13;
hence x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A4, A10, A11; :: thesis: verum

end;

suppose A12: i >= len (f :- p) ; :: thesis: x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) }

then A13: LSeg (Rotate f,p),i = LSeg f,((i + (p .. f)) -' (len f)) by A1, A7, Th31;
((len f) - (p .. f)) + 1 <= i by A1, A12, FINSEQ_5:53;
then ((len f) -' (p .. f)) + 1 <= i by A3, XREAL_1:235;
then (1 + (len f)) -' (p .. f) <= i by A3, NAT_D:38;
then A14: 1 + (len f) <= i + (p .. f) by NAT_D:52;
then A15: 1 <= (i + (p .. f)) -' (len f) by NAT_D:55;
A16: len f <= (len f) + 1 by NAT_1:11;
(i + 1) + (p .. f) <= (len f) + (len f) by A3, A6, XREAL_1:9;
then ((i + (p .. f)) + 1) -' (len f) <= len f by NAT_D:53;
then ((i + (p .. f)) -' (len f)) + 1 <= len f by A14, A16, NAT_D:38, XXREAL_0:2;
hence x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A4, A13, A15; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } or x in { (LSeg (Rotate f,p),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } )
assume x in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; :: thesis: x in { (LSeg (Rotate f,p),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) }
then consider i being Element of NAT such that
A17: x = LSeg f,i and
A18: 1 <= i and
A19: i + 1 <= len f ;
A20: i < len f by A19, NAT_1:13;

per cases ( p .. f <= i or i < p .. f ) ;

suppose A21: p .. f <= i ; :: thesis: x in { (LSeg (Rotate f,p),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) }

then A22: LSeg f,i = LSeg (Rotate f,p),((i -' (p .. f)) + 1) by A1, A20, Th25;
1 + (p .. f) <= i + 1 by A21, XREAL_1:8;
then 1 <= (i + 1) -' (p .. f) by NAT_D:55;
then A23: 1 <= (i -' (p .. f)) + 1 by A21, NAT_D:38;
i <= i + 1 by NAT_1:11;
then A24: p .. f <= i + 1 by A21, XXREAL_0:2;
1 <= p .. f by A1, FINSEQ_4:31;
then i + 1 < (len f) + (p .. f) by A20, XREAL_1:10;
then (i + 1) -' (p .. f) < len f by A24, NAT_D:54;
then (i -' (p .. f)) + 1 < len f by A21, NAT_D:38;
then ((i -' (p .. f)) + 1) + 1 <= len f by NAT_1:13;
hence x in { (LSeg (Rotate f,p),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A17, A22, A23; :: thesis: verum

end;

suppose A25: i < p .. f ; :: thesis: x in { (LSeg (Rotate f,p),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) }

then A26: LSeg f,i = LSeg (Rotate f,p),((i + (len f)) -' (p .. f)) by A1, A18, Th32;
1 + (p .. f) <= i + (len f) by A3, A18, XREAL_1:9;
then A27: 1 <= (i + (len f)) -' (p .. f) by NAT_D:55;
A28: p .. f <= len f by A1, FINSEQ_4:31;
A29: len f <= i + (len f) by NAT_1:11;
i + 1 <= p .. f by A25, NAT_1:13;
then (i + 1) + (len f) <= (len f) + (p .. f) by XREAL_1:8;
then ((i + (len f)) + 1) -' (p .. f) <= len f by NAT_D:53;
then ((i + (len f)) -' (p .. f)) + 1 <= len f by A28, A29, NAT_D:38, XXREAL_0:2;
hence x in { (LSeg (Rotate f,p),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A17, A26, A27; :: thesis: verum

end;

end;

end;

hence L~ (Rotate f,p) = L~ f by A2; :: thesis: verum

end;

end;