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 that
A1: 1 <= j and
A2: j <= len (GoB f) and
A3: 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 <= width (GoB f) by GOBOARD7:35;
then A4: ((GoB f) * j,1) `1 = ((GoB f) * j,(width (GoB f))) `1 by A1, A2, GOBOARD5:3;
A5: ((GoB f) * j,1) `2 <> ((GoB f) * j,(width (GoB f))) `2

proof

assume A6: ((GoB f) * j,1) `2 = ((GoB f) * j,(width (GoB f))) `2 ; :: thesis: contradiction
A7: GoB f = GoB (Incr (X_axis f)),(Incr (Y_axis f)) by GOBOARD2:def 3;
A8: 1 <= width (GoB f) by GOBOARD7:35;
then A9: [j,1] in Indices (GoB (Incr (X_axis f)),(Incr (Y_axis f))) by A1, A2, A7, MATRIX_1:37;
A10: [j,(width (GoB f))] in Indices (GoB (Incr (X_axis f)),(Incr (Y_axis f))) by A1, A2, A7, A8, 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 A9, GOBOARD2:def 1 ;
then A11: ((GoB f) * j,1) `2 = (Incr (Y_axis f)) . 1 by EUCLID:56;
A12: (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 A10, GOBOARD2:def 1 ;
A13: len (Incr (Y_axis f)) = width (GoB f) by A7, GOBOARD2:def 1;
A14: 1 <= width (GoB f) by GOBOARD7:35;
A15: 1 <= len (Incr (Y_axis f)) by A13, GOBOARD7:35;
A16: width (GoB f) in dom (Incr (Y_axis f)) by A13, A14, FINSEQ_3:27;
1 in dom (Incr (Y_axis f)) by A15, FINSEQ_3:27;
then width (GoB f) = 1 by A6, A11, A12, A16, EUCLID:56, SEQ_4:155;
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) ;
A17: 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 A4, A5, 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 A3, 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 A17, FINSEQ_4:26; :: thesis: verum