E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A23: 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;
set f = Rotate (Cage C,n),(W-min (L~ (Cage C,n)));
A24: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A25: 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;
A26: len (Lower_Seq 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 Th13;
A27: L~ (Cage C,n) = L~ (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by REVROT_1:33;
then A28: (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 1 = W-min (L~ (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) by A24, FINSEQ_6:98;
then (W-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) <= (N-min (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A27, SPRECT_5:24;
then (N-min (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) > 1 by A27, A28, SPRECT_5:23, XXREAL_0:2;
then (N-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) > 1 by A27, A28, SPRECT_5:25, XXREAL_0:2;
then A29: (E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) > 1 by A27, A28, SPRECT_5:26, XXREAL_0:2;
now
let i1, j1 be set ; :: thesis: ( i1 in dom (Lower_Seq C,n) & j1 in dom (Lower_Seq C,n) & (Lower_Seq C,n) . i1 = (Lower_Seq C,n) . j1 implies not i1 <> j1 )
assume that
A30: i1 in dom (Lower_Seq C,n) and
A31: j1 in dom (Lower_Seq C,n) and
A32: (Lower_Seq C,n) . i1 = (Lower_Seq C,n) . j1 and
A33: i1 <> j1 ; :: thesis: contradiction
reconsider i2 = i1, j2 = j1 as Element of NAT by A30, A31;
A34: ( i2 in Seg (len (Lower_Seq C,n)) & j2 in Seg (len (Lower_Seq C,n)) ) by A30, A31, FINSEQ_1:def 3;
then ( i2 >= 1 & j2 >= 1 ) by FINSEQ_1:3;
then A35: ( i2 = (i2 -' 1) + 1 & j2 = (j2 -' 1) + 1 ) by XREAL_1:237;
A36: (Lower_Seq C,n) . i1 = (Lower_Seq C,n) /. i2 by A30, PARTFUN1:def 8
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. ((i2 -' 1) + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) by A25, A30, A35, FINSEQ_5:55 ;
A37: (Lower_Seq C,n) . j1 = (Lower_Seq C,n) /. j2 by A31, PARTFUN1:def 8
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. ((j2 -' 1) + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) by A25, A31, A35, FINSEQ_5:55 ;
( 0 + 1 <= i2 & 0 + 1 <= j2 ) by A34, FINSEQ_1:3;
then A38: ( i2 - 1 >= 0 & j2 - 1 >= 0 ) by XREAL_1:21;
( j2 <= ((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 & i2 <= ((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 A26, A34, FINSEQ_1:3;
then ( j2 - 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))))) & i2 - 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:22;
then ( (j2 - 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)))) & (i2 - 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 XREAL_1:21;
then A39: ( (j2 -' 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)))) & (i2 -' 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 A38, XREAL_0:def 2;
( (i2 -' 1) + ((E-max (L~ (Cage C,n))) .. (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)))) & (j2 -' 1) + ((E-max (L~ (Cage C,n))) .. (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 NAT_1:11;
then A40: ( 1 < (i2 -' 1) + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) & 1 < (j2 -' 1) + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) ) by A29, XXREAL_0:2;
per cases ( i2 < j2 or j2 < i2 ) by A33, XXREAL_0:1;
suppose i2 < j2 ; :: thesis: contradiction
then i2 - 1 < j2 - 1 by XREAL_1:11;
then i2 - 1 < j2 -' 1 by XREAL_0:def 2;
then i2 -' 1 < j2 -' 1 by A38, XREAL_0:def 2;
then (i2 -' 1) + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) < (j2 -' 1) + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) by XREAL_1:8;
hence contradiction by A32, A36, A37, A39, A40, GOBOARD7:39; :: thesis: verum
end;
suppose j2 < i2 ; :: thesis: contradiction
then j2 - 1 < i2 - 1 by XREAL_1:11;
then j2 - 1 < i2 -' 1 by XREAL_0:def 2;
then j2 -' 1 < i2 -' 1 by A38, XREAL_0:def 2;
then (j2 -' 1) + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) < (i2 -' 1) + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) by XREAL_1:8;
hence contradiction by A32, A36, A37, A39, A40, GOBOARD7:39; :: thesis: verum
end;
end;
end;
hence Lower_Seq C,n is one-to-one by FUNCT_1:def 8; :: thesis: ( Lower_Seq C,n is special & Lower_Seq C,n is unfolded & Lower_Seq C,n is s.n.c. )
thus Lower_Seq C,n is special by A23, SPPOL_2:41; :: thesis: ( Lower_Seq C,n is unfolded & Lower_Seq C,n is s.n.c. )
thus Lower_Seq C,n is unfolded by A23, SPPOL_2:28; :: thesis: Lower_Seq C,n is s.n.c.
let i, j be Nat; :: according to TOPREAL1:def 9 :: thesis: ( j <= i + 1 or LSeg (Lower_Seq C,n),i misses LSeg (Lower_Seq C,n),j )
assume A41: i + 1 < j ; :: thesis: LSeg (Lower_Seq C,n),i misses LSeg (Lower_Seq C,n),j
A42: i + 1 >= 1 by NAT_1:11;
j = (j -' 1) + 1 by A41, A42, XREAL_1:237, XXREAL_0:2;
then A44: LSeg (Lower_Seq C,n),j = LSeg (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 A23, SPPOL_2:10;
now
per cases ( i > 0 or i = 0 ) by NAT_1:2;
suppose i > 0 ; :: thesis: (LSeg (Lower_Seq C,n),i) /\ (LSeg (Lower_Seq C,n),j) = {}
then A45: i >= 0 + 1 by NAT_1:13;
then i = (i -' 1) + 1 by XREAL_1:237;
then A46: LSeg (Lower_Seq C,n),i = LSeg (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))),((i -' 1) + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) by A25, SPPOL_2:10;
A48: i - 1 >= 0 by A45, XREAL_1:21;
(i + 1) - 1 < j - 1 by A41, XREAL_1:11;
then (i - 1) + 1 < j -' 1 by XREAL_0:def 2;
then (i -' 1) + 1 < j -' 1 by A48, XREAL_0:def 2;
then ((i -' 1) + 1) + ((E-max (L~ (Cage C,n))) .. (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 XREAL_1:8;
then A49: ((i -' 1) + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) + 1 < (j -' 1) + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) ;
A50: (i -' 1) + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) > 0 + 1 by A29, XREAL_1:10;
now
per cases ( ((j -' 1) + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) + 1 <= len (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)))))) + 1 > len (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) ) ;
suppose ((j -' 1) + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) + 1 <= len (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) ; :: thesis: (LSeg (Lower_Seq C,n),i) /\ (LSeg (Lower_Seq C,n),j) = {}
then (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 NAT_1:13;
then LSeg (Lower_Seq C,n),i misses LSeg (Lower_Seq C,n),j by A44, A46, A49, A50, GOBOARD5:def 4;
hence (LSeg (Lower_Seq C,n),i) /\ (LSeg (Lower_Seq C,n),j) = {} by XBOOLE_0:def 7; :: thesis: verum
end;
suppose ((j -' 1) + ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) + 1 > len (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) ; :: thesis: (LSeg (Lower_Seq C,n),i) /\ (LSeg (Lower_Seq C,n),j) = {}
then LSeg (Lower_Seq C,n),j = {} by A44, TOPREAL1:def 5;
hence (LSeg (Lower_Seq C,n),i) /\ (LSeg (Lower_Seq C,n),j) = {} ; :: thesis: verum
end;
end;
end;
hence (LSeg (Lower_Seq C,n),i) /\ (LSeg (Lower_Seq C,n),j) = {} ; :: thesis: verum
end;
end;
end;
hence LSeg (Lower_Seq C,n),i misses LSeg (Lower_Seq C,n),j by XBOOLE_0:def 7; :: thesis: verum