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

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₁ )
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A3: 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;
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₁ = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) . b₁
then A5: 1 <= i by A1, FINSEQ_1:3;
A6: i <= len (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A1, A4, FINSEQ_1:3;

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

suppose A7: 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 A8: i in Seg ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) by A5, 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 A3, FINSEQ_5:45;
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;
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 A5, A7, GRAPH_2:14
.= ((Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) -: (E-max (L~ (Cage C,n)))) /. i by A9, PARTFUN1:def 8
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. i by A3, A8, FINSEQ_5:46
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) . i by A4, 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
A10: i = ((len (Upper_Seq C,n)) + 1) + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
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 Th12;
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: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 A6, A11, 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 >= 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:9;
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:27;
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 GRAPH_2:13;
then i - (len (Upper_Seq C,n)) < len (Lower_Seq C,n) by XREAL_1:21;
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, 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 A14, 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 A3, A14, FINSEQ_5:55
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) . i by A4, 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 A2, FINSEQ_2:10; :: thesis: verum