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;
now 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 <> j1let i1,
j1 be
object ;
( 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
;
contradictionreconsider 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;
hence
Upper_Seq (C,n) is one-to-one
by FUNCT_1:def 4; ( Upper_Seq (C,n) is special & Upper_Seq (C,n) is unfolded & Upper_Seq (C,n) is s.n.c. )
thus
Upper_Seq (C,n) is special
; ( Upper_Seq (C,n) is unfolded & Upper_Seq (C,n) is s.n.c. )
thus
Upper_Seq (C,n) is unfolded
; Upper_Seq (C,n) is s.n.c.
let i, j be Nat; TOPREAL1:def 7 ( j <= i + 1 or LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j) )
assume A17:
i + 1 < j
; 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 LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j)per cases
( j + 1 <= len (Upper_Seq (C,n)) or j + 1 > len (Upper_Seq (C,n)) )
;
suppose A19:
j + 1
<= len (Upper_Seq (C,n))
;
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;
A22:
now j + 1 < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))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;
suppose A23:
j + 1
= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
;
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))))))
;
contradictionthen
(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;
verum end; end; end;
j < len (Upper_Seq (C,n))
by A19, NAT_1:13;
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;
verum end; suppose
j + 1
> len (Upper_Seq (C,n))
;
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)
;
verum end; end; end;
hence
LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j)
; verum