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

let n be Element of 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 REVROT_1:15;
then n in Seg (len p) by FINSEQ_1:def 3;
then A3: ( 0 + 1 <= n & n <= len p ) by FINSEQ_1:3;
then A4: n - 1 >= 0 by XREAL_1:21;

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

suppose A5: 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 A6: (Rotate p,v) /. n = p /. ((n -' 1) + (v .. p)) by A2, A3, REVROT_1:9;
n <= ((len p) - (v .. p)) + 1 by A2, A5, FINSEQ_5:53;
then n - 1 <= (len p) - (v .. p) by XREAL_1:22;
then (n - 1) + (v .. p) <= len p by XREAL_1:21;
then A7: (n -' 1) + (v .. p) <= len p by A4, XREAL_0:def 2;
1 <= v .. p by A2, FINSEQ_4:31;
then 0 + 1 <= (n -' 1) + (v .. p) by XREAL_1:9;
then (n -' 1) + (v .. p) in Seg (len p) by A7, FINSEQ_1:3;
then A8: (n -' 1) + (v .. p) in dom p by FINSEQ_1:def 3;
hence W-bound (L~ q) <= ((Rotate p,v) /. n) `1 by A1, A6, 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, A6, A8, 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, A6, A8, 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, A6, A8, SPRECT_2:def 1; :: thesis: verum

end;

suppose A9: 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 A10: (Rotate p,v) /. n = p /. ((n + (v .. p)) -' (len p)) by A2, A3, REVROT_1:12;
n > ((len p) - (v .. p)) + 1 by A2, A9, FINSEQ_5:53;
then n > (1 + (len p)) - (v .. p) ;
then n + (v .. p) > 1 + (len p) by XREAL_1:21;
then A11: (n + (v .. p)) - (len p) > 1 by XREAL_1:22;
v .. p <= len p by A2, FINSEQ_4:31;
then n + (v .. p) <= (len p) + (len p) by A3, XREAL_1:9;
then (n + (v .. p)) - (len p) <= len p by XREAL_1:22;
then A12: (n + (v .. p)) -' (len p) <= len p by XREAL_0:def 2;
1 <= (n + (v .. p)) -' (len p) by A11, XREAL_0:def 2;
then (n + (v .. p)) -' (len p) in Seg (len p) by A12, FINSEQ_1:3;
then A13: (n + (v .. p)) -' (len p) in dom p by FINSEQ_1:def 3;
hence W-bound (L~ q) <= ((Rotate p,v) /. n) `1 by A1, A10, 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, 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, A10, 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, A10, 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;