let f be non constant standard special_circular_sequence; :: thesis: for j being Element of NAT
for P being Subset of (TOP-REAL 2) st 1 <= j & j <= width (GoB f) & P = LSeg ((GoB f) * 1,j),((GoB f) * (len (GoB f)),j) holds
P is_S-P_arc_joining (GoB f) * 1,j,(GoB f) * (len (GoB f)),j
let j be Element of NAT ; :: thesis: for P being Subset of (TOP-REAL 2) st 1 <= j & j <= width (GoB f) & P = LSeg ((GoB f) * 1,j),((GoB f) * (len (GoB f)),j) holds
P is_S-P_arc_joining (GoB f) * 1,j,(GoB f) * (len (GoB f)),j
let P be Subset of (TOP-REAL 2); :: thesis: ( 1 <= j & j <= width (GoB f) & P = LSeg ((GoB f) * 1,j),((GoB f) * (len (GoB f)),j) implies P is_S-P_arc_joining (GoB f) * 1,j,(GoB f) * (len (GoB f)),j )
assume A1: ( 1 <= j & j <= width (GoB f) & P = LSeg ((GoB f) * 1,j),((GoB f) * (len (GoB f)),j) ) ; :: thesis: P is_S-P_arc_joining (GoB f) * 1,j,(GoB f) * (len (GoB f)),j
set p = (GoB f) * 1,j;
set q = (GoB f) * (len (GoB f)),j;
( 1 <= j & j <= width (GoB f) & 1 <= len (GoB f) & len (GoB f) <= len (GoB f) ) by A1, GOBOARD7:34;
then A2: ((GoB f) * 1,j) `2 = ((GoB f) * (len (GoB f)),j) `2 by GOBOARD5:2;
A3: ((GoB f) * 1,j) `1 <> ((GoB f) * (len (GoB f)),j) `1

proof

assume A4: ((GoB f) * 1,j) `1 = ((GoB f) * (len (GoB f)),j) `1 ; :: thesis: contradiction
A5: GoB f = GoB (Incr (X_axis f)),(Incr (Y_axis f)) by GOBOARD2:def 3;
( 1 <= len (GoB f) & len (GoB f) <= len (GoB (Incr (X_axis f)),(Incr (Y_axis f))) ) by GOBOARD2:def 3, GOBOARD7:34;
then A6: ( [1,j] in Indices (GoB (Incr (X_axis f)),(Incr (Y_axis f))) & [(len (GoB f)),j] in Indices (GoB (Incr (X_axis f)),(Incr (Y_axis f))) ) by A1, A5, MATRIX_1:37;
(GoB f) * 1,j = (GoB (Incr (X_axis f)),(Incr (Y_axis f))) * 1,j by GOBOARD2:def 3
.= |[((Incr (X_axis f)) . 1),((Incr (Y_axis f)) . j)]| by A6, GOBOARD2:def 1 ;
then A7: ((GoB f) * 1,j) `1 = (Incr (X_axis f)) . 1 by EUCLID:56;
(GoB f) * (len (GoB f)),j = (GoB (Incr (X_axis f)),(Incr (Y_axis f))) * (len (GoB f)),j by GOBOARD2:def 3
.= |[((Incr (X_axis f)) . (len (GoB f))),((Incr (Y_axis f)) . j)]| by A6, GOBOARD2:def 1 ;
then A8: (Incr (X_axis f)) . (len (GoB f)) = (Incr (X_axis f)) . 1 by A4, A7, EUCLID:56;
len (Incr (X_axis f)) = len (GoB f) by A5, GOBOARD2:def 1;
then ( 1 <= len (GoB f) & 1 <= len (Incr (X_axis f)) & len (GoB f) <= len (Incr (X_axis f)) ) by GOBOARD7:34;
then ( len (GoB f) in dom (Incr (X_axis f)) & 1 in dom (Incr (X_axis f)) ) by FINSEQ_3:27;
then len (GoB f) = 1 by A8, GOBOARD2:19;
hence contradiction by GOBOARD7:34; :: thesis: verum

end;

reconsider gg = <*((GoB f) * 1,j),((GoB f) * (len (GoB f)),j)*> as FinSequence of the carrier of (TOP-REAL 2) ;
A9: len gg = 2 by FINSEQ_1:61;
take gg ; :: according to TOPREAL4:def 1 :: thesis: ( gg is being_S-Seq & P = L~ gg & (GoB f) * 1,j = gg /. 1 & (GoB f) * (len (GoB f)),j = gg /. (len gg) )
thus gg is being_S-Seq by A2, A3, SPPOL_2:46; :: thesis: ( P = L~ gg & (GoB f) * 1,j = gg /. 1 & (GoB f) * (len (GoB f)),j = gg /. (len gg) )
thus P = L~ gg by A1, SPPOL_2:21; :: thesis: ( (GoB f) * 1,j = gg /. 1 & (GoB f) * (len (GoB f)),j = gg /. (len gg) )
thus ( (GoB f) * 1,j = gg /. 1 & (GoB f) * (len (GoB f)),j = gg /. (len gg) ) by A9, FINSEQ_4:26; :: thesis: verum