let f be V8() standard special_circular_sequence; :: thesis: for j being 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 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:33;
then A4: ((GoB f) * (j,1)) `1 = ((GoB f) * (j,(width (GoB f)))) `1 by A1, A2, GOBOARD5:2;
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 2;
A8: 1 <= width (GoB f) by GOBOARD7:33;
then A9: [j,1] in Indices (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) by A1, A2, A7, MATRIX_0:30;
A10: [j,(width (GoB f))] in Indices (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) by A1, A2, A7, A8, MATRIX_0:30;
(GoB f) * (j,1) = (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) * (j,1) by GOBOARD2:def 2
.= |[((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:52;
A12: (GoB f) * (j,(width (GoB f))) = (GoB ((Incr (X_axis f)),(Incr (Y_axis f)))) * (j,(width (GoB f))) by GOBOARD2:def 2
.= |[((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:33;
A15: 1 <= len (Incr (Y_axis f)) by A13, GOBOARD7:33;
A16: width (GoB f) in dom (Incr (Y_axis f)) by A13, A14, FINSEQ_3:25;
1 in dom (Incr (Y_axis f)) by A15, FINSEQ_3:25;
then width (GoB f) = 1 by A6, A11, A12, A16, EUCLID:52, SEQ_4:138;
hence contradiction by GOBOARD7:33; :: 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:44;
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:43; :: 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:17; :: thesis: verum