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 ;
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
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))) . b1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . b1 )
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))) . b1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . b1
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)) ) ;
suppose A7: i <= len (Upper_Seq (C,n)) ; :: thesis: ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . b1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . b1
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;
suppose i > len (Upper_Seq (C,n)) ; :: thesis: ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . b1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . b1
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;
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:9; :: thesis: verum