environ
vocabularies HIDDEN, NUMBERS, PRE_TOPC, EUCLID, REAL_1, FUNCT_1, GOBOARD5, FINSEQ_1, XBOOLE_0, SUBSET_1, XXREAL_0, PARTFUN1, RLTOPSP1, ARYTM_1, ARYTM_3, INT_1, RELAT_1, JORDAN4, GOBOARD2, TREES_1, MCART_1, GOBOARD1, MATRIX_1, NAT_1, ZFMISC_1, PSCOMP_1, TOPREAL1, STRUCT_0, TARSKI, SEQ_4, FINSET_1, SPPOL_1, XXREAL_2, CARD_1, JORDAN5D;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, MCART_1, XCMPLX_0, REAL_1, NAT_1, NAT_D, RELAT_1, FINSEQ_1, FUNCT_1, PARTFUN1, FINSET_1, MATRIX_0, XXREAL_2, STRUCT_0, TOPREAL1, SPPOL_1, GOBOARD1, GOBOARD2, GOBOARD5, PRE_TOPC, RLTOPSP1, EUCLID, JORDAN4, PSCOMP_1, XXREAL_0, SEQ_4;
definitions TARSKI, XBOOLE_0, XXREAL_2;
theorems EUCLID, FINSEQ_3, FINSEQ_6, FUNCT_1, FUNCT_2, GOBOARD1, GOBOARD2, GOBOARD5, GOBOARD7, NAT_1, PRE_TOPC, SEQ_4, SPPOL_1, SPPOL_2, TOPREAL1, MATRIX_0, FINSEQ_1, ZFMISC_1, JORDAN4, PSCOMP_1, SPRECT_2, FINSEQ_2, XBOOLE_0, XBOOLE_1, ORDINAL1, XREAL_1, XXREAL_0, PARTFUN1, XXREAL_2, NAT_D, XREAL_0, TARSKI;
schemes DOMAIN_1;
registrations ORDINAL1, RELSET_1, FINSET_1, XREAL_0, MEMBERED, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD2, GOBOARD5, SPRECT_1, VALUED_0, XXREAL_2, FUNCT_1, SEQ_4;
constructors HIDDEN, REAL_1, NAT_D, BINARITH, COMPTS_1, GOBOARD2, SPPOL_1, PSCOMP_1, JORDAN4, GOBOARD1, SEQ_4, RELSET_1, RVSUM_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0, PSCOMP_1, STRUCT_0;
expansions XXREAL_2;
Lm1:
for i1 being Nat
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `1 = W-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [1,j] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = min Y holds
((GoB h) * (1,i1)) `2 <= p `2
Lm2:
for i1 being Nat
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `1 = W-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [1,j] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * (1,j) ) ) } & i1 = max Y holds
((GoB h) * (1,i1)) `2 >= p `2
Lm3:
for i1 being Nat
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `1 = E-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [(len (GoB h)),j] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * ((len (GoB h)),j) ) ) } & i1 = min Y holds
((GoB h) * ((len (GoB h)),i1)) `2 <= p `2
Lm4:
for i1 being Nat
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `1 = E-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [(len (GoB h)),j] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * ((len (GoB h)),j) ) ) } & i1 = max Y holds
((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
Lm5:
for i1 being Nat
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `2 = S-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,1] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = min Y holds
((GoB h) * (i1,1)) `1 <= p `1
Lm6:
for i1 being Nat
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `2 = N-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = min Y holds
((GoB h) * (i1,(width (GoB h)))) `1 <= p `1
Lm7:
for h being non constant standard special_circular_sequence
for i1 being Nat
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT st p `2 = S-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,1] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * (j,1) ) ) } & i1 = max Y holds
((GoB h) * (i1,1)) `1 >= p `1
Lm8:
for h being non constant standard special_circular_sequence
for i1 being Nat
for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT st p `2 = N-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = max Y holds
((GoB h) * (i1,(width (GoB h)))) `1 >= p `1
Lm9:
for h being non constant standard special_circular_sequence holds len h >= 2
by GOBOARD7:34, XXREAL_0:2;
definition
let g be non
constant standard special_circular_sequence;
existence
ex b1 being Nat st
( [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-min (L~ g) )
uniqueness
for b1, b2 being Nat st [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-min (L~ g) & [1,b2] in Indices (GoB g) & (GoB g) * (1,b2) = W-min (L~ g) holds
b1 = b2
by GOBOARD1:5;
existence
ex b1 being Nat st
( [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-max (L~ g) )
uniqueness
for b1, b2 being Nat st [1,b1] in Indices (GoB g) & (GoB g) * (1,b1) = W-max (L~ g) & [1,b2] in Indices (GoB g) & (GoB g) * (1,b2) = W-max (L~ g) holds
b1 = b2
by GOBOARD1:5;
existence
ex b1 being Nat st
( [(len (GoB g)),b1] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b1) = E-min (L~ g) )
uniqueness
for b1, b2 being Nat st [(len (GoB g)),b1] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b1) = E-min (L~ g) & [(len (GoB g)),b2] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b2) = E-min (L~ g) holds
b1 = b2
by GOBOARD1:5;
existence
ex b1 being Nat st
( [(len (GoB g)),b1] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b1) = E-max (L~ g) )
uniqueness
for b1, b2 being Nat st [(len (GoB g)),b1] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b1) = E-max (L~ g) & [(len (GoB g)),b2] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b2) = E-max (L~ g) holds
b1 = b2
by GOBOARD1:5;
existence
ex b1 being Nat st
( [b1,1] in Indices (GoB g) & (GoB g) * (b1,1) = S-min (L~ g) )
uniqueness
for b1, b2 being Nat st [b1,1] in Indices (GoB g) & (GoB g) * (b1,1) = S-min (L~ g) & [b2,1] in Indices (GoB g) & (GoB g) * (b2,1) = S-min (L~ g) holds
b1 = b2
by GOBOARD1:5;
existence
ex b1 being Nat st
( [b1,1] in Indices (GoB g) & (GoB g) * (b1,1) = S-max (L~ g) )
uniqueness
for b1, b2 being Nat st [b1,1] in Indices (GoB g) & (GoB g) * (b1,1) = S-max (L~ g) & [b2,1] in Indices (GoB g) & (GoB g) * (b2,1) = S-max (L~ g) holds
b1 = b2
by GOBOARD1:5;
existence
ex b1 being Nat st
( [b1,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b1,(width (GoB g))) = N-min (L~ g) )
uniqueness
for b1, b2 being Nat st [b1,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b1,(width (GoB g))) = N-min (L~ g) & [b2,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b2,(width (GoB g))) = N-min (L~ g) holds
b1 = b2
by GOBOARD1:5;
existence
ex b1 being Nat st
( [b1,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b1,(width (GoB g))) = N-max (L~ g) )
uniqueness
for b1, b2 being Nat st [b1,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b1,(width (GoB g))) = N-max (L~ g) & [b2,(width (GoB g))] in Indices (GoB g) & (GoB g) * (b2,(width (GoB g))) = N-max (L~ g) holds
b1 = b2
by GOBOARD1:5;
end;
Lm10:
for h being non constant standard special_circular_sequence
for i1, i2 being Nat st 1 <= i1 & i1 + 1 <= len h & 1 <= i2 & i2 + 1 <= len h & h . i1 = h . i2 holds
i1 = i2