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 and
A2: f1 ^' f2,g1 are_in_general_position and
A3: len g1 >= 2 and
A4: ( 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 A4;
set Lf = L~ (f1 ^' f2);
f1 ^' f2 is_in_general_position_wrt g1 by A2, Def2;
then A5: L~ (f1 ^' f2) misses rng g1 by Def1;
defpred S₁[ 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 ) ) );
A6: dom g1 = Seg (len g1) by FINSEQ_1:def 3;
A7: 1 + 1 <= len g1 by A3;

A8: now

let k be Nat; :: thesis: ( k >= 2 & S₁[k] implies S₁[k + 1] )
assume that
A9: k >= 2 and
A10: S₁[k] ; :: thesis: S₁[k + 1]
A11: k in NAT by ORDINAL1:def 12;
A12: 1 <= k by A9, XXREAL_0:2;
then A13: 1 <= k + 1 by NAT_1:13;

now

reconsider b = g1 | (Seg k) as FinSequence of (TOP-REAL 2) by FINSEQ_1:18;
1 in Seg k by A12, FINSEQ_1:1;
then A14: b . 1 = g1 . 1 by FUNCT_1:49;
reconsider s1 = (L~ (f1 ^' f2)) /\ (L~ b) as finite set by A2, A11, Th7, Th12;
set c = LSeg (g1,k);
A15: k in Seg k by A12, FINSEQ_1:1;
reconsider s2 = (L~ (f1 ^' f2)) /\ (LSeg (g1,k)) as finite set by A2, A11, Th13;
A16: k <= k + 1 by NAT_1:13;
then A17: Seg k c= Seg (k + 1) by FINSEQ_1:5;
k >= 1 + 1 by A9;
then A18: 1 < k by NAT_1:13;
A19: g1 . 1 in (L~ (f1 ^' f2)) ` by A2, A7, Th9;
assume A20: 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~ b<sub>2</sub>)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( b<sub>3</sub> is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b₃ & C . (len C) in b₃ ) )
then A21: ( g1 . (k + 1) in (L~ (f1 ^' f2)) ` & g1 . k in (L~ (f1 ^' f2)) ` ) by A2, A11, A12, Th9;
let a be FinSequence of (TOP-REAL 2); :: thesis: ( a = g1 | (Seg (k + 1)) implies ( card ((L~ (f1 ^' f2)) /\ (L~ b₁)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( b₂ is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b<sub>2</sub> & C . (len C) in b<sub>2</sub> ) ) )
assume A22: a = g1 | (Seg (k + 1)) ; :: thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ b<sub>1</sub>)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( b<sub>2</sub> is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b₂ & C . (len C) in b₂ ) )
A23: dom a = (dom g1) /\ (Seg (k + 1)) by A22, RELAT_1:61;
A24: k + 1 in Seg (k + 1) by A13, FINSEQ_1:1;
then A25: g1 . (k + 1) = a . (k + 1) by A22, FUNCT_1:49
.= a . (len a) by A20, A22, FINSEQ_1:17 ;
A26: k + 1 in Seg (len g1) by A13, A20, FINSEQ_1:1;
then A27: k + 1 in dom a by A6, A24, A23, XBOOLE_0:def 4;
then A28: a /. (k + 1) = a . (k + 1) by PARTFUN1:def 6
.= g1 . (k + 1) by A22, A27, FUNCT_1:47
.= g1 /. (k + 1) by A6, A26, PARTFUN1:def 6 ;
A29: len a = k + 1 by A20, A22, FINSEQ_1:17;
g1 | (k + 1) = a by A22, FINSEQ_1:def 15;
then (L~ (a | k)) /\ (LSeg (a,k)) = {(a /. k)} by A11, A29, A18, GOBOARD2:4;
then A30: (L~ (a | k)) /\ (LSeg ((a /. k),(a /. (k + 1)))) = {(a /. k)} by A12, A29, TOPREAL1:def 3;
1 in Seg (k + 1) by A13, FINSEQ_1:1;
then A31: g1 . 1 = a . 1 by A22, FUNCT_1:49;
reconsider s = (L~ (f1 ^' f2)) /\ (L~ a) as finite set by A2, A22, Th7, Th12;
A32: a = g1 | (k + 1) by A22, FINSEQ_1:def 15;
A33: k < len g1 by A20, NAT_1:13;
then A34: k in dom g1 by A6, A12, FINSEQ_1:1;
A35: a | k = (g1 | (Seg (k + 1))) | (Seg k) by A22, FINSEQ_1:def 15
.= g1 | (Seg k) by A17, FUNCT_1:51
.= g1 | k by FINSEQ_1:def 15 ;
A36: b . (len b) = b . k by A33, FINSEQ_1:17
.= g1 . k by A15, FUNCT_1:49 ;
k in Seg (k + 1) by A12, A16, FINSEQ_1:1;
then A37: k in dom a by A34, A23, XBOOLE_0:def 4;
then a /. k = a . k by PARTFUN1:def 6
.= g1 . k by A22, A37, FUNCT_1:47
.= g1 /. k by A34, PARTFUN1:def 6 ;
then (L~ b) /\ (LSeg ((g1 /. k),(g1 /. (k + 1)))) = {(g1 /. k)} by A35, A28, A30, FINSEQ_1:def 15;
then (L~ b) /\ (LSeg (g1,k)) = {(g1 /. k)} by A12, A20, TOPREAL1:def 3;
then A38: (L~ b) /\ (LSeg (g1,k)) = {(g1 . k)} by A34, PARTFUN1:def 6;
A39: s1 misses s2

proof

assume s1 meets s2 ; :: thesis: contradiction
then consider x being set such that
A40: x in s1 and
A41: x in s2 by XBOOLE_0:3;
( x in L~ b & x in LSeg (g1,k) ) by A40, A41, XBOOLE_0:def 4;
then x in (L~ b) /\ (LSeg (g1,k)) by XBOOLE_0:def 4;
then x = g1 . k by A38, TARSKI:def 1;
then A42: x in rng g1 by A34, FUNCT_1:3;
x in L~ (f1 ^' f2) by A40, XBOOLE_0:def 4;
hence contradiction by A5, A42, XBOOLE_0:3; :: thesis: verum

end;

k + 1 in dom g1 by A6, A13, A20, FINSEQ_1:1;
then L~ a = (L~ (g1 | k)) \/ (LSeg ((g1 /. k),(g1 /. (k + 1)))) by A34, A32, TOPREAL3:38
.= (L~ b) \/ (LSeg ((g1 /. k),(g1 /. (k + 1)))) by FINSEQ_1:def 15
.= (L~ b) \/ (LSeg (g1,k)) by A12, A20, TOPREAL1:def 3 ;
then A43: s = s1 \/ s2 by XBOOLE_1:23;

per cases ( card s1 is even Element of NAT or not card s1 is even Element of NAT ) ;

suppose A44: card s1 is even Element of NAT ; :: thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ b₁)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( b₂ is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b₂ & C . (len C) in b₂ ) )

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 A45: 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 ;
A46: ( c = c1 + c2 & 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 A10, A20, A43, A39, A44, CARD_2:40, NAT_1:13;
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, A2, A11, A12, A20, A45, Th34;
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, A31, A25, A14, A36, A46, Th17; :: thesis: verum

end;

suppose A47: 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 ;
A48: ( c = c1 + c2 & 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 A10, A20, A43, A39, A44, CARD_2:40, NAT_1:13;
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, A2, A11, A12, A20, A47, Th34;
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, A31, A25, A14, A36, A48, Th17; :: thesis: verum

end;

end;

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 A49: card s1 is not even Element of NAT ; :: thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ b₁)) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st
( b₂ is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b₂ & C . (len C) in b₂ ) )

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 A50: 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 ;
A51: ( c = c1 + c2 & ( 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 A10, A20, A43, A39, A49, CARD_2:40, NAT_1:13;
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, A2, A11, A12, A20, A50, Th34;
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, A31, A25, A14, A36, A51, Th17; :: thesis: verum

end;

suppose A52: 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 ;
A53: ( c = c1 + c2 & ( 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 A10, A20, A43, A39, A49, CARD_2:40, NAT_1:13;
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, A2, A11, A12, A20, A52, Th34;
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, A31, A19, A21, A25, A14, A36, A53, Th18; :: thesis: verum

end;

end;

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;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

dom g1 = Seg (len g1) by FINSEQ_1:def 3;
then A54: g1 | (Seg (len g1)) = g1 by RELAT_1:69;
A55: 2 in dom g1 by A3, FINSEQ_3:25;
A56: 1 <= len g1 by A3, XXREAL_0:2;
then A57: 1 in dom g1 by FINSEQ_3:25;

now

g1 | 1 = g1 | (Seg 1) by FINSEQ_1:def 15;
then A58: len (g1 | 1) = 1 by A56, FINSEQ_1:17;
A59: 2 in Seg 2 by FINSEQ_1:2, TARSKI:def 2;
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 A60: 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 ) )
A61: a . (len a) = a . 2 by A3, A60, FINSEQ_1:17
.= g1 . (1 + 1) by A60, A59, FUNCT_1:49 ;
1 in Seg 2 by FINSEQ_1:2, TARSKI:def 2;
then A62: a . 1 = g1 . 1 by A60, FUNCT_1:49;
L~ a = L~ (g1 | 2) by A60, FINSEQ_1:def 15
.= (L~ (g1 | 1)) \/ (LSeg ((g1 /. 1),(g1 /. (1 + 1)))) by A57, A55, TOPREAL3:38
.= (L~ (g1 | 1)) \/ (LSeg (g1,1)) by A3, TOPREAL1:def 3
.= {} \/ (LSeg (g1,1)) by A58, TOPREAL1:22
.= LSeg (g1,1) ;
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, A3, A62, A61, Th34; :: thesis: verum

end;

then A63: S₁[2] ;
for k being Nat st k >= 2 holds
S₁[k] from NAT_1:sch 8(A63, A8);
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 A3, A54; :: thesis: verum