set f = Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))));

A1: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;

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

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

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

thus Upper_Seq (C,n) is special ; :: thesis: ( Upper_Seq (C,n) is unfolded & Upper_Seq (C,n) is s.n.c. )

thus Upper_Seq (C,n) is unfolded ; :: thesis: Upper_Seq (C,n) is s.n.c.

let i, j be Nat; :: according to TOPREAL1:def 7 :: thesis: ( j <= i + 1 or LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j) )

assume A17: i + 1 < j ; :: thesis: LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j)

0 + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by NAT_1:13;

then A18: len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) in dom (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_3:25;

A1: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;

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

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

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

now :: thesis: for i1, j1 being object st i1 in dom (Upper_Seq (C,n)) & j1 in dom (Upper_Seq (C,n)) & (Upper_Seq (C,n)) . i1 = (Upper_Seq (C,n)) . j1 holds

not i1 <> j1

hence
Upper_Seq (C,n) is one-to-one
by FUNCT_1:def 4; :: thesis: ( Upper_Seq (C,n) is special & Upper_Seq (C,n) is unfolded & Upper_Seq (C,n) is s.n.c. )not i1 <> j1

let i1, j1 be object ; :: thesis: ( i1 in dom (Upper_Seq (C,n)) & j1 in dom (Upper_Seq (C,n)) & (Upper_Seq (C,n)) . i1 = (Upper_Seq (C,n)) . j1 implies not i1 <> j1 )

assume that

A4: i1 in dom (Upper_Seq (C,n)) and

A5: j1 in dom (Upper_Seq (C,n)) and

A6: (Upper_Seq (C,n)) . i1 = (Upper_Seq (C,n)) . j1 and

A7: i1 <> j1 ; :: thesis: contradiction

reconsider i2 = i1, j2 = j1 as Nat by A4, A5;

A8: i2 in Seg ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A3, A4, FINSEQ_1:def 3;

then A9: 1 <= i2 by FINSEQ_1:1;

A10: L~ (Cage (C,n)) = L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by REVROT_1:33;

A11: j2 in Seg ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A3, A5, FINSEQ_1:def 3;

then A12: 1 <= j2 by FINSEQ_1:1;

j2 <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A11, FINSEQ_1:1;

then A13: j2 < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A10, SPRECT_5:16, XXREAL_0:2;

A14: (Upper_Seq (C,n)) . j1 = (Upper_Seq (C,n)) /. j2 by A5, PARTFUN1:def 6

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. j2 by A2, A11, FINSEQ_5:43 ;

i2 <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A8, FINSEQ_1:1;

then A15: i2 < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A10, SPRECT_5:16, XXREAL_0:2;

A16: (Upper_Seq (C,n)) . i1 = (Upper_Seq (C,n)) /. i2 by A4, PARTFUN1:def 6

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

end;assume that

A4: i1 in dom (Upper_Seq (C,n)) and

A5: j1 in dom (Upper_Seq (C,n)) and

A6: (Upper_Seq (C,n)) . i1 = (Upper_Seq (C,n)) . j1 and

A7: i1 <> j1 ; :: thesis: contradiction

reconsider i2 = i1, j2 = j1 as Nat by A4, A5;

A8: i2 in Seg ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A3, A4, FINSEQ_1:def 3;

then A9: 1 <= i2 by FINSEQ_1:1;

A10: L~ (Cage (C,n)) = L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by REVROT_1:33;

A11: j2 in Seg ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A3, A5, FINSEQ_1:def 3;

then A12: 1 <= j2 by FINSEQ_1:1;

j2 <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A11, FINSEQ_1:1;

then A13: j2 < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A10, SPRECT_5:16, XXREAL_0:2;

A14: (Upper_Seq (C,n)) . j1 = (Upper_Seq (C,n)) /. j2 by A5, PARTFUN1:def 6

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. j2 by A2, A11, FINSEQ_5:43 ;

i2 <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A8, FINSEQ_1:1;

then A15: i2 < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A10, SPRECT_5:16, XXREAL_0:2;

A16: (Upper_Seq (C,n)) . i1 = (Upper_Seq (C,n)) /. i2 by A4, PARTFUN1:def 6

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

per cases
( i2 < j2 or j2 < i2 )
by A7, XXREAL_0:1;

end;

thus Upper_Seq (C,n) is special ; :: thesis: ( Upper_Seq (C,n) is unfolded & Upper_Seq (C,n) is s.n.c. )

thus Upper_Seq (C,n) is unfolded ; :: thesis: Upper_Seq (C,n) is s.n.c.

let i, j be Nat; :: according to TOPREAL1:def 7 :: thesis: ( j <= i + 1 or LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j) )

assume A17: i + 1 < j ; :: thesis: LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j)

0 + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by NAT_1:13;

then A18: len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) in dom (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_3:25;

now :: thesis: LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j)end;

hence
LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j)
; :: thesis: verumper cases
( j + 1 <= len (Upper_Seq (C,n)) or j + 1 > len (Upper_Seq (C,n)) )
;

end;

suppose A19:
j + 1 <= len (Upper_Seq (C,n))
; :: thesis: LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j)

A20:
(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 A2, FINSEQ_4:21;

A21: j + 1 <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A2, A19, FINSEQ_5:42;

then A24: LSeg ((Upper_Seq (C,n)),i) = LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i) by A17, SPPOL_2:9, XXREAL_0:2;

LSeg ((Upper_Seq (C,n)),j) = LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),j) by A19, SPPOL_2:9;

hence LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j) by A17, A24, A22, GOBOARD5:def 4; :: thesis: verum

end;A21: j + 1 <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A2, A19, FINSEQ_5:42;

A22: now :: thesis: j + 1 < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))end;

j < len (Upper_Seq (C,n))
by A19, NAT_1:13;per cases
( j + 1 < (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) or j + 1 = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) )
by A21, XXREAL_0:1;

end;

suppose
j + 1 < (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
; :: thesis: j + 1 < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))

hence
j + 1 < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
by A20, XXREAL_0:2; :: thesis: verum

end;suppose A23:
j + 1 = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
; :: thesis: not j + 1 >= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))

assume
j + 1 >= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
; :: thesis: contradiction

then (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 A20, A23, XXREAL_0:1;

then 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 A2, FINSEQ_4:19

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A18, PARTFUN1:def 6

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by FINSEQ_6:def 1

.= W-min (L~ (Cage (C,n))) by A1, FINSEQ_6:92 ;

hence contradiction by TOPREAL5:19; :: thesis: verum

end;then (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 A20, A23, XXREAL_0:1;

then 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 A2, FINSEQ_4:19

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A18, PARTFUN1:def 6

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by FINSEQ_6:def 1

.= W-min (L~ (Cage (C,n))) by A1, FINSEQ_6:92 ;

hence contradiction by TOPREAL5:19; :: thesis: verum

then A24: LSeg ((Upper_Seq (C,n)),i) = LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i) by A17, SPPOL_2:9, XXREAL_0:2;

LSeg ((Upper_Seq (C,n)),j) = LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),j) by A19, SPPOL_2:9;

hence LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j) by A17, A24, A22, GOBOARD5:def 4; :: thesis: verum

suppose
j + 1 > len (Upper_Seq (C,n))
; :: thesis: LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j)

then
LSeg ((Upper_Seq (C,n)),j) = {}
by TOPREAL1:def 3;

then (LSeg ((Upper_Seq (C,n)),i)) /\ (LSeg ((Upper_Seq (C,n)),j)) = {} ;

hence LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j) ; :: thesis: verum

end;then (LSeg ((Upper_Seq (C,n)),i)) /\ (LSeg ((Upper_Seq (C,n)),j)) = {} ;

hence LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j) ; :: thesis: verum