let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Nat holds Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) = (Upper_Seq (C,n)) ^' (Lower_Seq (C,n))

let n be Nat; :: thesis: Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) = (Upper_Seq (C,n)) ^' (Lower_Seq (C,n))

A1: dom (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = Seg (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by FINSEQ_1:def 3;

A2: (len ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n)))) + 1 = (len (Upper_Seq (C,n))) + (len (Lower_Seq (C,n))) by FINSEQ_6:139

.= (len (Cage (C,n))) + 1 by Th10

.= (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + 1 by FINSEQ_6:179 ;

let n be Nat; :: thesis: Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) = (Upper_Seq (C,n)) ^' (Lower_Seq (C,n))

A1: dom (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = Seg (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by FINSEQ_1:def 3;

A2: (len ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n)))) + 1 = (len (Upper_Seq (C,n))) + (len (Lower_Seq (C,n))) by FINSEQ_6:139

.= (len (Cage (C,n))) + 1 by Th10

.= (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + 1 by FINSEQ_6:179 ;

now :: thesis: for i being Nat st i in dom (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) holds

((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . i = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . i

hence
Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) = (Upper_Seq (C,n)) ^' (Lower_Seq (C,n))
by A2, FINSEQ_2:9; :: thesis: verum((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . i = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . i

let i be Nat; :: thesis: ( i in dom (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) implies ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . b_{1} = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . b_{1} )

E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;

then A3: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;

assume A4: i in dom (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ; :: thesis: ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . b_{1} = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . b_{1}

then A5: 1 <= i by A1, FINSEQ_1:1;

A6: i <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A1, A4, FINSEQ_1:1;

end;E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;

then A3: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;

assume A4: i in dom (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ; :: thesis: ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . b

then A5: 1 <= i by A1, FINSEQ_1:1;

A6: i <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A1, A4, FINSEQ_1:1;

per cases
( i <= len (Upper_Seq (C,n)) or i > len (Upper_Seq (C,n)) )
;

end;

suppose A7:
i <= len (Upper_Seq (C,n))
; :: thesis: ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . b_{1} = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . b_{1}

then
i <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
by Th8;

then A8: i in Seg ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A5, FINSEQ_1:1;

len ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A3, FINSEQ_5:42;

then A9: i in dom ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))) by A8, FINSEQ_1:def 3;

thus ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . i = ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))) . i by A5, A7, FINSEQ_6:140

.= ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))) /. i by A9, PARTFUN1:def 6

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. i by A3, A8, FINSEQ_5:43

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . i by A4, PARTFUN1:def 6 ; :: thesis: verum

end;then A8: i in Seg ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A5, FINSEQ_1:1;

len ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A3, FINSEQ_5:42;

then A9: i in dom ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))) by A8, FINSEQ_1:def 3;

thus ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . i = ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))) . i by A5, A7, FINSEQ_6:140

.= ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))) /. i by A9, PARTFUN1:def 6

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. i by A3, A8, FINSEQ_5:43

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . i by A4, PARTFUN1:def 6 ; :: thesis: verum

suppose
i > len (Upper_Seq (C,n))
; :: thesis: ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . b_{1} = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . b_{1}

then
i >= (len (Upper_Seq (C,n))) + 1
by NAT_1:13;

then consider j being Nat such that

A10: i = ((len (Upper_Seq (C,n))) + 1) + j by NAT_1:10;

reconsider j = j as Nat ;

A11: i = (len (Upper_Seq (C,n))) + (j + 1) by A10;

then A12: i = ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + (j + 1) by Th8;

A13: len ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))))) = ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by A3, FINSEQ_5:50;

(j + 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A6, A11, Th8;

then j + 1 <= (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:19;

then ( (j + 1) + 1 >= 1 & (j + 1) + 1 <= len ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))))) ) by A13, NAT_1:11, XREAL_1:7;

then A14: (j + 1) + 1 in dom ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))))) by FINSEQ_3:25;

i < (len ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n)))) + 1 by A2, A6, NAT_1:13;

then i < (len (Lower_Seq (C,n))) + (len (Upper_Seq (C,n))) by FINSEQ_6:139;

then i - (len (Upper_Seq (C,n))) < len (Lower_Seq (C,n)) by XREAL_1:19;

hence ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . i = ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))))) . ((j + 1) + 1) by A11, FINSEQ_6:141, NAT_1:11

.= ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))))) /. ((j + 1) + 1) by A14, PARTFUN1:def 6

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((j + 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by A3, A14, FINSEQ_5:52

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . i by A4, A12, PARTFUN1:def 6 ;

:: thesis: verum

end;then consider j being Nat such that

A10: i = ((len (Upper_Seq (C,n))) + 1) + j by NAT_1:10;

reconsider j = j as Nat ;

A11: i = (len (Upper_Seq (C,n))) + (j + 1) by A10;

then A12: i = ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + (j + 1) by Th8;

A13: len ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))))) = ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by A3, FINSEQ_5:50;

(j + 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A6, A11, Th8;

then j + 1 <= (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:19;

then ( (j + 1) + 1 >= 1 & (j + 1) + 1 <= len ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))))) ) by A13, NAT_1:11, XREAL_1:7;

then A14: (j + 1) + 1 in dom ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))))) by FINSEQ_3:25;

i < (len ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n)))) + 1 by A2, A6, NAT_1:13;

then i < (len (Lower_Seq (C,n))) + (len (Upper_Seq (C,n))) by FINSEQ_6:139;

then i - (len (Upper_Seq (C,n))) < len (Lower_Seq (C,n)) by XREAL_1:19;

hence ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . i = ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))))) . ((j + 1) + 1) by A11, FINSEQ_6:141, NAT_1:11

.= ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))))) /. ((j + 1) + 1) by A14, PARTFUN1:def 6

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((j + 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by A3, A14, FINSEQ_5:52

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . i by A4, A12, PARTFUN1:def 6 ;

:: thesis: verum