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

proof

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

end;

reconsider gg = <*((GoB f) * j,1),((GoB f) * j,(width (GoB f)))*> 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) * j,1 = gg /. 1 & (GoB f) * j,(width (GoB f)) = gg /. (len gg) )
thus gg is being_S-Seq by A2, A3, SPPOL_2:46; :: thesis: ( P = L~ gg & (GoB f) * j,1 = gg /. 1 & (GoB f) * j,(width (GoB f)) = gg /. (len gg) )
thus P = L~ gg by A1, SPPOL_2:21; :: thesis: ( (GoB f) * j,1 = gg /. 1 & (GoB f) * j,(width (GoB f)) = gg /. (len gg) )
thus ( (GoB f) * j,1 = gg /. 1 & (GoB f) * j,(width (GoB f)) = gg /. (len gg) ) by A9, FINSEQ_4:26; :: thesis: verum