let f be constant standard special_circular_sequence; :: thesis: for j being 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 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 that
A1: 1 <= j and
A2: j <= width (GoB f) and
A3: 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 <= len (GoB f) by GOBOARD7:32;
then A4: ((GoB f) * (1,j)) `2 = ((GoB f) * ((len (GoB f)),j)) `2 by A1, A2, GOBOARD5:1;
A5: ((GoB f) * (1,j)) `1 <> ((GoB f) * ((len (GoB f)),j)) `1

proof

assume A6: ((GoB f) * (1,j)) `1 = ((GoB f) * ((len (GoB f)),j)) `1 ; :: thesis: contradiction
A7: GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by GOBOARD2:def 2;
A8: 1 <= len (GoB f) by GOBOARD7:32;
then A9: [1,j] in Indices (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) by A1, A2, A7, MATRIX_0:30;
A10: [(len (GoB f)),j] in Indices (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) by A1, A2, A7, A8, MATRIX_0:30;
(GoB f) * (1,j) = (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) * (1,j) by GOBOARD2:def 2
.= |[((Incr (X_axis f)) . 1),((Incr (Y_axis f)) . j)]| by A9, GOBOARD2:def 1 ;
then A11: ((GoB f) * (1,j)) `1 = (Incr (X_axis f)) . 1 by EUCLID:52;
A12: (GoB f) * ((len (GoB f)),j) = (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) * ((len (GoB f)),j) by GOBOARD2:def 2
.= |[((Incr (X_axis f)) . (len (GoB f))),((Incr (Y_axis f)) . j)]| by A10, GOBOARD2:def 1 ;
A13: len (Incr (X_axis f)) = len (GoB f) by A7, GOBOARD2:def 1;
A14: 1 <= len (GoB f) by GOBOARD7:32;
A15: 1 <= len (Incr (X_axis f)) by A13, GOBOARD7:32;
A16: len (GoB f) in dom (Incr (X_axis f)) by A13, A14, FINSEQ_3:25;
1 in dom (Incr (X_axis f)) by A15, FINSEQ_3:25;
then len (GoB f) = 1 by A6, A11, A12, A16, EUCLID:52, SEQ_4:138;
hence contradiction by GOBOARD7:32; :: thesis: verum

end;

reconsider gg = <*((GoB f) * (1,j)),((GoB f) * ((len (GoB f)),j))*> as FinSequence of the carrier of (TOP-REAL 2) ;
A17: len gg = 2 by FINSEQ_1:44;
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 A4, A5, SPPOL_2:43; :: thesis: ( P = L~ gg & (GoB f) * (1,j) = gg /. 1 & (GoB f) * ((len (GoB f)),j) = gg /. (len gg) )
thus P = L~ gg by A3, 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 A17, FINSEQ_4:17; :: thesis: verum