let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT holds Rotate (Cage C,n),(W-min (L~ (Cage C,n))) = (Upper_Seq C,n) ^' (Lower_Seq C,n)
let n be Element of NAT ; :: thesis: Rotate (Cage C,n),(W-min (L~ (Cage C,n))) = (Upper_Seq C,n) ^' (Lower_Seq C,n)
A1: (len ((Upper_Seq C,n) ^' (Lower_Seq C,n))) + 1 = (len (Upper_Seq C,n)) + (len (Lower_Seq C,n)) by GRAPH_2:13
.= (len (Cage C,n)) + 1 by Th14
.= (len (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) + 1 by REVROT_1:14 ;
X: 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;

now

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₁ = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) . b₁ )
assume A2: i in dom (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) ; :: thesis: ((Upper_Seq C,n) ^' (Lower_Seq C,n)) . b₁ = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) . b₁
then A3: ( 1 <= i & i <= len (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) ) by X, FINSEQ_1:3;
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A4: E-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by FINSEQ_6:96, SPRECT_2:47;
A5: i in dom (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A2;

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

suppose A6: i <= len (Upper_Seq C,n) ; :: thesis: ((Upper_Seq C,n) ^' (Lower_Seq C,n)) . b₁ = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) . b₁

then i <= (E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by Th12;
then A7: i in Seg ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) by A3, FINSEQ_1:3;
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 A4, FINSEQ_5:45;
then A8: i in dom ((Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) -: (E-max (L~ (Cage C,n)))) by A7, FINSEQ_1:def 3;
i in NAT by ORDINAL1:def 13;
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)))) . i by A3, A6, GRAPH_2:14
.= ((Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) -: (E-max (L~ (Cage C,n)))) /. i by A8, PARTFUN1:def 8
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. i by A4, A7, FINSEQ_5:46
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) . i by A5, PARTFUN1:def 8 ;
:: thesis: verum

end;

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

then i >= (len (Upper_Seq C,n)) + 1 by NAT_1:13;
then consider j being Nat such that
A9: i = ((len (Upper_Seq C,n)) + 1) + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
A10: i = (len (Upper_Seq C,n)) + (j + 1) by A9;
i < (len ((Upper_Seq C,n) ^' (Lower_Seq C,n))) + 1 by A1, A3, NAT_1:13;
then i < (len (Lower_Seq C,n)) + (len (Upper_Seq C,n)) by GRAPH_2:13;
then A11: i - (len (Upper_Seq C,n)) < len (Lower_Seq C,n) by XREAL_1:21;
A12: i = ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) + (j + 1) by A10, Th12;
A13: (j + 1) + 1 >= 1 by NAT_1:11;
A14: 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 A4, FINSEQ_5:53;
(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 A3, A10, Th12;
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:21;
then (j + 1) + 1 <= len ((Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) :- (E-max (L~ (Cage C,n)))) by A14, XREAL_1:9;
then A15: (j + 1) + 1 in dom ((Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) :- (E-max (L~ (Cage C,n)))) by A13, FINSEQ_3:27;
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)))) . ((j + 1) + 1) by A10, A11, GRAPH_2:15, NAT_1:11
.= ((Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) :- (E-max (L~ (Cage C,n)))) /. ((j + 1) + 1) by A15, PARTFUN1:def 8
.= (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 A4, A15, FINSEQ_5:55
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) . i by A5, A12, PARTFUN1:def 8 ; :: thesis: verum

end;

end;

end;

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