let f be non constant standard special_circular_sequence; 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 ; 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); ( 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)
; 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:34;
then A4:
((GoB f) * 1,j) `2 = ((GoB f) * (len (GoB f)),j) `2
by A1, A2, GOBOARD5:2;
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
;
contradiction
A7:
GoB f = GoB (Incr (X_axis f)),
(Incr (Y_axis f))
by GOBOARD2:def 3;
A8:
1
<= len (GoB f)
by GOBOARD7:34;
then A9:
[1,j] in Indices (GoB (Incr (X_axis f)),(Incr (Y_axis f)))
by A1, A2, A7, MATRIX_1:37;
A10:
[(len (GoB f)),j] in Indices (GoB (Incr (X_axis f)),(Incr (Y_axis f)))
by A1, A2, A7, A8, 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 A9, GOBOARD2:def 1
;
then A11:
((GoB f) * 1,j) `1 = (Incr (X_axis f)) . 1
by EUCLID:56;
A12:
(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 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:34;
A15:
1
<= len (Incr (X_axis f))
by A13, GOBOARD7:34;
A16:
len (GoB f) in dom (Incr (X_axis f))
by A13, A14, FINSEQ_3:27;
1
in dom (Incr (X_axis f))
by A15, FINSEQ_3:27;
then
len (GoB f) = 1
by A6, A11, A12, A16, EUCLID:56, GOBOARD2:19;
hence
contradiction
by GOBOARD7:34;
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:61;
take
gg
; TOPREAL4:def 1 ( 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:46; ( 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; ( (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:26; verum