let f1, f2, g1 be special FinSequence of (TOP-REAL 2); :: thesis: ( f1 ^' f2 is non constant standard special_circular_sequence & f1 ^' f2,g1 are_in_general_position & len g1 >= 2 & g1 is unfolded & g1 is s.n.c. implies ( card ((L~ (f1 ^' f2)) /\ (L~ g1)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & g1 . 1 in C & g1 . (len g1) in C ) ) )
assume that
A1:
( f1 ^' f2 is non constant standard special_circular_sequence & f1 ^' f2,g1 are_in_general_position )
and
A2:
len g1 >= 2
and
A3:
( g1 is unfolded & g1 is s.n.c. )
; :: thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ g1)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & g1 . 1 in C & g1 . (len g1) in C ) )
reconsider g1 = g1 as special unfolded s.n.c. FinSequence of (TOP-REAL 2) by A3;
set Lf = L~ (f1 ^' f2);
f1 ^' f2 is_in_general_position_wrt g1
by A1, Def2;
then A4:
L~ (f1 ^' f2) misses rng g1
by Def1;
defpred S1[ Nat] means ( $1 <= len g1 implies for a being FinSequence of (TOP-REAL 2) st a = g1 | (Seg $1) holds
( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) ) );
A5:
1 + 1 <= len g1
by A2;
A6:
dom g1 = Seg (len g1)
by FINSEQ_1:def 3;
A7:
1 <= len g1
by A2, XXREAL_0:2;
then A8:
1 in dom g1
by FINSEQ_3:27;
A9:
2 in dom g1
by A2, FINSEQ_3:27;
now let a be
FinSequence of
(TOP-REAL 2);
:: thesis: ( a = g1 | (Seg 2) implies ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) ) )assume A10:
a = g1 | (Seg 2)
;
:: thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) )
g1 | 1
= g1 | (Seg 1)
by FINSEQ_1:def 15;
then A11:
len (g1 | 1) = 1
by A7, FINSEQ_1:21;
A12:
L~ a =
L~ (g1 | 2)
by A10, FINSEQ_1:def 15
.=
(L~ (g1 | 1)) \/ (LSeg (g1 /. 1),(g1 /. (1 + 1)))
by A8, A9, TOPREAL3:45
.=
(L~ (g1 | 1)) \/ (LSeg g1,1)
by A2, TOPREAL1:def 5
.=
{} \/ (LSeg g1,1)
by A11, TOPREAL1:28
.=
LSeg g1,1
;
A13:
2
in Seg 2
by FINSEQ_1:4, TARSKI:def 2;
1
in Seg 2
by FINSEQ_1:4, TARSKI:def 2;
then A14:
a . 1
= g1 . 1
by A10, FUNCT_1:72;
a . (len a) =
a . 2
by A2, A10, FINSEQ_1:21
.=
g1 . (1 + 1)
by A10, A13, FUNCT_1:72
;
hence
(
card ((L~ (f1 ^' f2)) /\ (L~ a)) is
even Element of
NAT iff ex
C being
Subset of
(TOP-REAL 2) st
(
C is_a_component_of (L~ (f1 ^' f2)) ` &
a . 1
in C &
a . (len a) in C ) )
by A1, A2, A12, A14, Th34;
:: thesis: verum end;
then A15:
S1[2]
;
A16:
now let k be
Nat;
:: thesis: ( k >= 2 & S1[k] implies S1[k + 1] )assume that A17:
k >= 2
and A18:
S1[
k]
;
:: thesis: S1[k + 1]A19:
k in NAT
by ORDINAL1:def 13;
A20:
1
<= k
by A17, XXREAL_0:2;
then A21:
1
<= k + 1
by NAT_1:13;
now assume A22:
k + 1
<= len g1
;
:: thesis: for a being FinSequence of (TOP-REAL 2) st a = g1 | (Seg (k + 1)) holds
( card ((L~ (f1 ^' f2)) /\ (L~ b2)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( b3 is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b3 & C . (len C) in b3 ) )let a be
FinSequence of
(TOP-REAL 2);
:: thesis: ( a = g1 | (Seg (k + 1)) implies ( card ((L~ (f1 ^' f2)) /\ (L~ b1)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( b2 is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b2 & C . (len C) in b2 ) ) )assume A23:
a = g1 | (Seg (k + 1))
;
:: thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ b1)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( b2 is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b2 & C . (len C) in b2 ) )A24:
k < len g1
by A22, NAT_1:13;
A25:
k + 1
in Seg (len g1)
by A21, A22, FINSEQ_1:3;
A26:
(
k in dom g1 &
k + 1
in dom g1 )
by A6, A20, A21, A22, A24, FINSEQ_1:3;
A27:
k + 1
in Seg (k + 1)
by A21, FINSEQ_1:3;
1
in Seg (k + 1)
by A21, FINSEQ_1:3;
then A28:
g1 . 1
= a . 1
by A23, FUNCT_1:72;
A29:
g1 . 1
in (L~ (f1 ^' f2)) `
by A1, A5, Th9;
A30:
g1 . (k + 1) in (L~ (f1 ^' f2)) `
by A1, A19, A20, A22, Th9;
A31:
g1 . k in (L~ (f1 ^' f2)) `
by A1, A19, A20, A22, Th9;
A32:
len a = k + 1
by A22, A23, FINSEQ_1:21;
A33:
g1 . (k + 1) =
a . (k + 1)
by A23, A27, FUNCT_1:72
.=
a . (len a)
by A22, A23, FINSEQ_1:21
;
reconsider b =
g1 | (Seg k) as
FinSequence of
(TOP-REAL 2) by FINSEQ_1:23;
A34:
k in Seg k
by A20, FINSEQ_1:3;
1
in Seg k
by A20, FINSEQ_1:3;
then A35:
b . 1
= g1 . 1
by FUNCT_1:72;
A36:
b . (len b) =
b . k
by A24, FINSEQ_1:21
.=
g1 . k
by A34, FUNCT_1:72
;
set c =
LSeg g1,
k;
reconsider s1 =
(L~ (f1 ^' f2)) /\ (L~ b) as
finite set by A1, A19, Th7, Th12;
reconsider s2 =
(L~ (f1 ^' f2)) /\ (LSeg g1,k) as
finite set by A1, A19, Th13;
reconsider s =
(L~ (f1 ^' f2)) /\ (L~ a) as
finite set by A1, A23, Th7, Th12;
a = g1 | (k + 1)
by A23, FINSEQ_1:def 15;
then L~ a =
(L~ (g1 | k)) \/ (LSeg (g1 /. k),(g1 /. (k + 1)))
by A26, TOPREAL3:45
.=
(L~ b) \/ (LSeg (g1 /. k),(g1 /. (k + 1)))
by FINSEQ_1:def 15
.=
(L~ b) \/ (LSeg g1,k)
by A20, A22, TOPREAL1:def 5
;
then A37:
s = s1 \/ s2
by XBOOLE_1:23;
A38:
g1 | (k + 1) = a
by A23, FINSEQ_1:def 15;
A39:
dom a = (dom g1) /\ (Seg (k + 1))
by A23, RELAT_1:90;
A40:
k <= k + 1
by NAT_1:13;
then
k in Seg (k + 1)
by A20, FINSEQ_1:3;
then A41:
k in dom a
by A26, A39, XBOOLE_0:def 4;
A42:
Seg k c= Seg (k + 1)
by A40, FINSEQ_1:7;
A43:
a | k =
(g1 | (Seg (k + 1))) | (Seg k)
by A23, FINSEQ_1:def 15
.=
g1 | (Seg k)
by A42, FUNCT_1:82
.=
g1 | k
by FINSEQ_1:def 15
;
A44:
k + 1
in dom a
by A6, A25, A27, A39, XBOOLE_0:def 4;
k >= 1
+ 1
by A17;
then A45:
1
< k
by NAT_1:13;
A46:
a /. k =
a . k
by A41, PARTFUN1:def 8
.=
g1 . k
by A23, A41, FUNCT_1:70
.=
g1 /. k
by A26, PARTFUN1:def 8
;
A47:
a /. (k + 1) =
a . (k + 1)
by A44, PARTFUN1:def 8
.=
g1 . (k + 1)
by A23, A44, FUNCT_1:70
.=
g1 /. (k + 1)
by A6, A25, PARTFUN1:def 8
;
(L~ (a | k)) /\ (LSeg a,k) = {(a /. k)}
by A19, A32, A38, A45, GOBOARD2:9;
then
(L~ (a | k)) /\ (LSeg (a /. k),(a /. (k + 1))) = {(a /. k)}
by A20, A32, TOPREAL1:def 5;
then
(L~ b) /\ (LSeg (g1 /. k),(g1 /. (k + 1))) = {(g1 /. k)}
by A43, A46, A47, FINSEQ_1:def 15;
then
(L~ b) /\ (LSeg g1,k) = {(g1 /. k)}
by A20, A22, TOPREAL1:def 5;
then A48:
(L~ b) /\ (LSeg g1,k) = {(g1 . k)}
by A26, PARTFUN1:def 8;
A49:
s1 misses s2
per cases
( card s1 is even Element of NAT or not card s1 is even Element of NAT )
;
suppose A52:
card s1 is
even Element of
NAT
;
:: thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ b1)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( b2 is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b2 & C . (len C) in b2 ) )then reconsider c1 =
card ((L~ (f1 ^' f2)) /\ (L~ b)) as
even Integer ;
now per cases
( card s2 is even Element of NAT or not card s2 is even Element of NAT )
;
suppose A53:
card s2 is
even Element of
NAT
;
:: thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) )then reconsider c2 =
card ((L~ (f1 ^' f2)) /\ (LSeg g1,k)) as
even Integer ;
reconsider c =
card s as
Integer ;
A54:
c = c1 + c2
by A37, A49, CARD_2:53;
A55:
ex
C being
Subset of
(TOP-REAL 2) st
(
C is_a_component_of (L~ (f1 ^' f2)) ` &
g1 . k in C &
g1 . (k + 1) in C )
by A1, A19, A20, A22, A53, Th34;
ex
C being
Subset of
(TOP-REAL 2) st
(
C is_a_component_of (L~ (f1 ^' f2)) ` &
b . 1
in C &
b . (len b) in C )
by A18, A22, A52, NAT_1:13;
hence
(
card ((L~ (f1 ^' f2)) /\ (L~ a)) is
even Element of
NAT iff ex
C being
Subset of
(TOP-REAL 2) st
(
C is_a_component_of (L~ (f1 ^' f2)) ` &
a . 1
in C &
a . (len a) in C ) )
by A1, A28, A33, A35, A36, A54, A55, Th17;
:: thesis: verum end; suppose A56:
card s2 is not
even Element of
NAT
;
:: thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) )then reconsider c2 =
card ((L~ (f1 ^' f2)) /\ (LSeg g1,k)) as
odd Integer ;
reconsider c =
card s as
Integer ;
A57:
c = c1 + c2
by A37, A49, CARD_2:53;
A58:
for
C being
Subset of
(TOP-REAL 2) holds
( not
C is_a_component_of (L~ (f1 ^' f2)) ` or not
g1 . k in C or not
g1 . (k + 1) in C )
by A1, A19, A20, A22, A56, Th34;
ex
C being
Subset of
(TOP-REAL 2) st
(
C is_a_component_of (L~ (f1 ^' f2)) ` &
b . 1
in C &
b . (len b) in C )
by A18, A22, A52, NAT_1:13;
hence
(
card ((L~ (f1 ^' f2)) /\ (L~ a)) is
even Element of
NAT iff ex
C being
Subset of
(TOP-REAL 2) st
(
C is_a_component_of (L~ (f1 ^' f2)) ` &
a . 1
in C &
a . (len a) in C ) )
by A1, A28, A33, A35, A36, A57, A58, Th17;
:: thesis: verum end; hence
(
card ((L~ (f1 ^' f2)) /\ (L~ a)) is
even Element of
NAT iff ex
C being
Subset of
(TOP-REAL 2) st
(
C is_a_component_of (L~ (f1 ^' f2)) ` &
a . 1
in C &
a . (len a) in C ) )
;
:: thesis: verum end; suppose A59:
card s1 is not
even Element of
NAT
;
:: thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ b1)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( b2 is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b2 & C . (len C) in b2 ) )then reconsider c1 =
card ((L~ (f1 ^' f2)) /\ (L~ b)) as
odd Integer ;
now per cases
( card s2 is even Element of NAT or not card s2 is even Element of NAT )
;
suppose A60:
card s2 is
even Element of
NAT
;
:: thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) )then reconsider c2 =
card ((L~ (f1 ^' f2)) /\ (LSeg g1,k)) as
even Integer ;
reconsider c =
card s as
Integer ;
A61:
c = c1 + c2
by A37, A49, CARD_2:53;
A62:
ex
C being
Subset of
(TOP-REAL 2) st
(
C is_a_component_of (L~ (f1 ^' f2)) ` &
g1 . k in C &
g1 . (k + 1) in C )
by A1, A19, A20, A22, A60, Th34;
for
C being
Subset of
(TOP-REAL 2) holds
( not
C is_a_component_of (L~ (f1 ^' f2)) ` or not
b . 1
in C or not
b . (len b) in C )
by A18, A22, A59, NAT_1:13;
hence
(
card ((L~ (f1 ^' f2)) /\ (L~ a)) is
even Element of
NAT iff ex
C being
Subset of
(TOP-REAL 2) st
(
C is_a_component_of (L~ (f1 ^' f2)) ` &
a . 1
in C &
a . (len a) in C ) )
by A1, A28, A33, A35, A36, A61, A62, Th17;
:: thesis: verum end; suppose A63:
card s2 is not
even Element of
NAT
;
:: thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) )then reconsider c2 =
card ((L~ (f1 ^' f2)) /\ (LSeg g1,k)) as
odd Integer ;
reconsider c =
card s as
Integer ;
A64:
c = c1 + c2
by A37, A49, CARD_2:53;
A65:
for
C being
Subset of
(TOP-REAL 2) holds
( not
C is_a_component_of (L~ (f1 ^' f2)) ` or not
g1 . k in C or not
g1 . (k + 1) in C )
by A1, A19, A20, A22, A63, Th34;
for
C being
Subset of
(TOP-REAL 2) holds
( not
C is_a_component_of (L~ (f1 ^' f2)) ` or not
b . 1
in C or not
b . (len b) in C )
by A18, A22, A59, NAT_1:13;
hence
(
card ((L~ (f1 ^' f2)) /\ (L~ a)) is
even Element of
NAT iff ex
C being
Subset of
(TOP-REAL 2) st
(
C is_a_component_of (L~ (f1 ^' f2)) ` &
a . 1
in C &
a . (len a) in C ) )
by A1, A28, A29, A30, A31, A33, A35, A36, A64, A65, Th18;
:: thesis: verum end; hence
(
card ((L~ (f1 ^' f2)) /\ (L~ a)) is
even Element of
NAT iff ex
C being
Subset of
(TOP-REAL 2) st
(
C is_a_component_of (L~ (f1 ^' f2)) ` &
a . 1
in C &
a . (len a) in C ) )
;
:: thesis: verum end; end; hence
S1[
k + 1]
;
:: thesis: verum end;
A66:
for k being Nat st k >= 2 holds
S1[k]
from NAT_1:sch 8(A15, A16);
dom g1 = Seg (len g1)
by FINSEQ_1:def 3;
then
g1 | (Seg (len g1)) = g1
by RELAT_1:98;
hence
( card ((L~ (f1 ^' f2)) /\ (L~ g1)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & g1 . 1 in C & g1 . (len g1) in C ) )
by A2, A66; :: thesis: verum