let p, q be FinSequence of (TOP-REAL 2); :: thesis: for v being Point of (TOP-REAL 2) st p is_in_the_area_of q holds
Rotate (p,v) is_in_the_area_of q
let v be Point of (TOP-REAL 2); :: thesis: ( p is_in_the_area_of q implies Rotate (p,v) is_in_the_area_of q )
assume A1: p is_in_the_area_of q ; :: thesis: Rotate (p,v) is_in_the_area_of q

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

suppose A2: v in rng p ; :: thesis: Rotate (p,v) is_in_the_area_of q

now :: thesis: for n being Nat st n in dom (Rotate (p,v)) holds
( W-bound (L~ q) <= ((Rotate (p,v)) /. n) `1 & ((Rotate (p,v)) /. n) `1 <= E-bound (L~ q) & S-bound (L~ q) <= ((Rotate (p,v)) /. n) `2 & ((Rotate (p,v)) /. n) `2 <= N-bound (L~ q) )

let n be Nat; :: thesis: ( n in dom (Rotate (p,v)) implies ( W-bound (L~ q) <= ((Rotate (p,v)) /. b₁) `1 & ((Rotate (p,v)) /. b<sub>1</sub>) `1 <= E-bound (L~ q) & S-bound (L~ q) <= ((Rotate (p,v)) /. b₁) `2 & ((Rotate (p,v)) /. b<sub>1</sub>) `2 <= N-bound (L~ q) ) )
assume n in dom (Rotate (p,v)) ; :: thesis: ( W-bound (L~ q) <= ((Rotate (p,v)) /. b₁) `1 & ((Rotate (p,v)) /. b<sub>1</sub>) `1 <= E-bound (L~ q) & S-bound (L~ q) <= ((Rotate (p,v)) /. b₁) `2 & ((Rotate (p,v)) /. b<sub>1</sub>) `2 <= N-bound (L~ q) )
then n in dom p by FINSEQ_6:180;
then A3: n in Seg (len p) by FINSEQ_1:def 3;
then A4: n <= len p by FINSEQ_1:1;
A5: 0 + 1 <= n by A3, FINSEQ_1:1;
then A6: n - 1 >= 0 by XREAL_1:19;

per cases ( n <= len (p :- v) or n > len (p :- v) ) ;

suppose A7: n <= len (p :- v) ; :: thesis: ( W-bound (L~ q) <= ((Rotate (p,v)) /. b₁) `1 & ((Rotate (p,v)) /. b<sub>1</sub>) `1 <= E-bound (L~ q) & S-bound (L~ q) <= ((Rotate (p,v)) /. b₁) `2 & ((Rotate (p,v)) /. b<sub>1</sub>) `2 <= N-bound (L~ q) )

then n <= ((len p) - (v .. p)) + 1 by A2, FINSEQ_5:50;
then n - 1 <= (len p) - (v .. p) by XREAL_1:20;
then (n - 1) + (v .. p) <= len p by XREAL_1:19;
then A8: (n -' 1) + (v .. p) <= len p by A6, XREAL_0:def 2;
1 <= v .. p by A2, FINSEQ_4:21;
then 0 + 1 <= (n -' 1) + (v .. p) by XREAL_1:7;
then (n -' 1) + (v .. p) in Seg (len p) by A8, FINSEQ_1:1;
then A9: (n -' 1) + (v .. p) in dom p by FINSEQ_1:def 3;
A10: (Rotate (p,v)) /. n = p /. ((n -' 1) + (v .. p)) by A2, A5, A7, FINSEQ_6:174;
hence W-bound (L~ q) <= ((Rotate (p,v)) /. n) `1 by A1, A9, SPRECT_2:def 1; :: thesis: ( ((Rotate (p,v)) /. n) `1 <= E-bound (L~ q) & S-bound (L~ q) <= ((Rotate (p,v)) /. n) `2 & ((Rotate (p,v)) /. n) `2 <= N-bound (L~ q) )
thus ((Rotate (p,v)) /. n) `1 <= E-bound (L~ q) by A1, A10, A9, SPRECT_2:def 1; :: thesis: ( S-bound (L~ q) <= ((Rotate (p,v)) /. n) `2 & ((Rotate (p,v)) /. n) `2 <= N-bound (L~ q) )
thus S-bound (L~ q) <= ((Rotate (p,v)) /. n) `2 by A1, A10, A9, SPRECT_2:def 1; :: thesis: ((Rotate (p,v)) /. n) `2 <= N-bound (L~ q)
thus ((Rotate (p,v)) /. n) `2 <= N-bound (L~ q) by A1, A10, A9, SPRECT_2:def 1; :: thesis: verum

end;

suppose A11: n > len (p :- v) ; :: thesis: ( W-bound (L~ q) <= ((Rotate (p,v)) /. b₁) `1 & ((Rotate (p,v)) /. b<sub>1</sub>) `1 <= E-bound (L~ q) & S-bound (L~ q) <= ((Rotate (p,v)) /. b₁) `2 & ((Rotate (p,v)) /. b<sub>1</sub>) `2 <= N-bound (L~ q) )

then n > ((len p) - (v .. p)) + 1 by A2, FINSEQ_5:50;
then n > (1 + (len p)) - (v .. p) ;
then n + (v .. p) > 1 + (len p) by XREAL_1:19;
then (n + (v .. p)) - (len p) > 1 by XREAL_1:20;
then A12: 1 <= (n + (v .. p)) -' (len p) by XREAL_0:def 2;
v .. p <= len p by A2, FINSEQ_4:21;
then n + (v .. p) <= (len p) + (len p) by A4, XREAL_1:7;
then (n + (v .. p)) - (len p) <= len p by XREAL_1:20;
then (n + (v .. p)) -' (len p) <= len p by XREAL_0:def 2;
then (n + (v .. p)) -' (len p) in Seg (len p) by A12, FINSEQ_1:1;
then A13: (n + (v .. p)) -' (len p) in dom p by FINSEQ_1:def 3;
A14: (Rotate (p,v)) /. n = p /. ((n + (v .. p)) -' (len p)) by A2, A4, A11, FINSEQ_6:177;
hence W-bound (L~ q) <= ((Rotate (p,v)) /. n) `1 by A1, A13, SPRECT_2:def 1; :: thesis: ( ((Rotate (p,v)) /. n) `1 <= E-bound (L~ q) & S-bound (L~ q) <= ((Rotate (p,v)) /. n) `2 & ((Rotate (p,v)) /. n) `2 <= N-bound (L~ q) )
thus ((Rotate (p,v)) /. n) `1 <= E-bound (L~ q) by A1, A14, A13, SPRECT_2:def 1; :: thesis: ( S-bound (L~ q) <= ((Rotate (p,v)) /. n) `2 & ((Rotate (p,v)) /. n) `2 <= N-bound (L~ q) )
thus S-bound (L~ q) <= ((Rotate (p,v)) /. n) `2 by A1, A14, A13, SPRECT_2:def 1; :: thesis: ((Rotate (p,v)) /. n) `2 <= N-bound (L~ q)
thus ((Rotate (p,v)) /. n) `2 <= N-bound (L~ q) by A1, A14, A13, SPRECT_2:def 1; :: thesis: verum

end;

end;

end;

hence Rotate (p,v) is_in_the_area_of q by SPRECT_2:def 1; :: thesis: verum

end;

suppose not v in rng p ; :: thesis: Rotate (p,v) is_in_the_area_of q

hence Rotate (p,v) is_in_the_area_of q by A1, FINSEQ_6:def 2; :: thesis: verum

end;

end;