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

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 )
;

end;

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

end;

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) )

hence
Rotate (p,v) is_in_the_area_of q
by SPRECT_2:def 1; :: thesis: verum( 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}) `1 & ((Rotate (p,v)) /. b_{1}) `1 <= E-bound (L~ q) & S-bound (L~ q) <= ((Rotate (p,v)) /. b_{1}) `2 & ((Rotate (p,v)) /. b_{1}) `2 <= N-bound (L~ q) ) )

assume n in dom (Rotate (p,v)) ; :: thesis: ( W-bound (L~ q) <= ((Rotate (p,v)) /. b_{1}) `1 & ((Rotate (p,v)) /. b_{1}) `1 <= E-bound (L~ q) & S-bound (L~ q) <= ((Rotate (p,v)) /. b_{1}) `2 & ((Rotate (p,v)) /. b_{1}) `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;

end;assume n in dom (Rotate (p,v)) ; :: thesis: ( W-bound (L~ q) <= ((Rotate (p,v)) /. b

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) )
;

end;

suppose A7:
n <= len (p :- v)
; :: thesis: ( W-bound (L~ q) <= ((Rotate (p,v)) /. b_{1}) `1 & ((Rotate (p,v)) /. b_{1}) `1 <= E-bound (L~ q) & S-bound (L~ q) <= ((Rotate (p,v)) /. b_{1}) `2 & ((Rotate (p,v)) /. b_{1}) `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;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

suppose A11:
n > len (p :- v)
; :: thesis: ( W-bound (L~ q) <= ((Rotate (p,v)) /. b_{1}) `1 & ((Rotate (p,v)) /. b_{1}) `1 <= E-bound (L~ q) & S-bound (L~ q) <= ((Rotate (p,v)) /. b_{1}) `2 & ((Rotate (p,v)) /. b_{1}) `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;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