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