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;
then A5: L~ (f1 ^' f2) misses rng g1 ;
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 ) ) );
A6: dom g1 = Seg (len g1) by FINSEQ_1:def 3;
A7: 1 + 1 <= len g1 by A3;
A8: now :: thesis: for k being Nat st k >= 2 & S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( k >= 2 & S1[k] implies S1[k + 1] )
assume that
A9: k >= 2 and
A10: S1[k] ; :: thesis: S1[k + 1]
A11: 1 <= k by A9, XXREAL_0:2;
then A12: 1 <= k + 1 by NAT_1:13;
now :: thesis: ( k + 1 <= len g1 implies for a being FinSequence of (TOP-REAL 2) st a = g1 | (Seg (k + 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 ) ) )
reconsider b = g1 | (Seg k) as FinSequence of (TOP-REAL 2) by FINSEQ_1:18;
1 in Seg k by A11, FINSEQ_1:1;
then A13: b . 1 = g1 . 1 by FUNCT_1:49;
reconsider s1 = (L~ (f1 ^' f2)) /\ (L~ b) as finite set by A2, Th6, Th11;
set c = LSeg (g1,k);
A14: k in Seg k by A11, FINSEQ_1:1;
reconsider s2 = (L~ (f1 ^' f2)) /\ (LSeg (g1,k)) as finite set by A2, Th12;
A15: k <= k + 1 by NAT_1:13;
then A16: Seg k c= Seg (k + 1) by FINSEQ_1:5;
k >= 1 + 1 by A9;
then A17: 1 < k by NAT_1:13;
A18: g1 . 1 in (L~ (f1 ^' f2)) ` by A2, A7, Th8;
assume A19: 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 ) )
then A20: ( g1 . (k + 1) in (L~ (f1 ^' f2)) ` & g1 . k in (L~ (f1 ^' f2)) ` ) by A2, A11, Th8;
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 A21: 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 ) )
A22: dom a = (dom g1) /\ (Seg (k + 1)) by A21, RELAT_1:61;
A23: k + 1 in Seg (k + 1) by A12, FINSEQ_1:1;
then A24: g1 . (k + 1) = a . (k + 1) by A21, FUNCT_1:49
.= a . (len a) by A19, A21, FINSEQ_1:17 ;
A25: k + 1 in Seg (len g1) by A12, A19, FINSEQ_1:1;
then A26: k + 1 in dom a by A6, A23, A22, XBOOLE_0:def 4;
then A27: a /. (k + 1) = a . (k + 1) by PARTFUN1:def 6
.= g1 . (k + 1) by A21, A26, FUNCT_1:47
.= g1 /. (k + 1) by A6, A25, PARTFUN1:def 6 ;
A28: len a = k + 1 by A19, A21, FINSEQ_1:17;
g1 | (k + 1) = a by A21, FINSEQ_1:def 15;
then (L~ (a | k)) /\ (LSeg (a,k)) = {(a /. k)} by A28, A17, GOBOARD2:4;
then A29: (L~ (a | k)) /\ (LSeg ((a /. k),(a /. (k + 1)))) = {(a /. k)} by A11, A28, TOPREAL1:def 3;
1 in Seg (k + 1) by A12, FINSEQ_1:1;
then A30: g1 . 1 = a . 1 by A21, FUNCT_1:49;
reconsider s = (L~ (f1 ^' f2)) /\ (L~ a) as finite set by A2, A21, Th6, Th11;
A31: a = g1 | (k + 1) by A21, FINSEQ_1:def 15;
A32: k < len g1 by A19, NAT_1:13;
then A33: k in dom g1 by A6, A11, FINSEQ_1:1;
A34: a | k = (g1 | (Seg (k + 1))) | (Seg k) by A21, FINSEQ_1:def 15
.= g1 | (Seg k) by A16, FUNCT_1:51
.= g1 | k by FINSEQ_1:def 15 ;
A35: b . (len b) = b . k by A32, FINSEQ_1:17
.= g1 . k by A14, FUNCT_1:49 ;
k in Seg (k + 1) by A11, A15, FINSEQ_1:1;
then A36: k in dom a by A33, A22, XBOOLE_0:def 4;
then a /. k = a . k by PARTFUN1:def 6
.= g1 . k by A21, A36, FUNCT_1:47
.= g1 /. k by A33, PARTFUN1:def 6 ;
then (L~ b) /\ (LSeg ((g1 /. k),(g1 /. (k + 1)))) = {(g1 /. k)} by A34, A27, A29, FINSEQ_1:def 15;
then (L~ b) /\ (LSeg (g1,k)) = {(g1 /. k)} by A11, A19, TOPREAL1:def 3;
then A37: (L~ b) /\ (LSeg (g1,k)) = {(g1 . k)} by A33, PARTFUN1:def 6;
A38: s1 misses s2
proof
assume s1 meets s2 ; :: thesis: contradiction
then consider x being object such that
A39: x in s1 and
A40: x in s2 by XBOOLE_0:3;
( x in L~ b & x in LSeg (g1,k) ) by A39, A40, XBOOLE_0:def 4;
then x in (L~ b) /\ (LSeg (g1,k)) by XBOOLE_0:def 4;
then x = g1 . k by A37, TARSKI:def 1;
then A41: x in rng g1 by A33, FUNCT_1:3;
x in L~ (f1 ^' f2) by A39, XBOOLE_0:def 4;
hence contradiction by A5, A41, XBOOLE_0:3; :: thesis: verum
end;
k + 1 in dom g1 by A6, A12, A19, FINSEQ_1:1;
then L~ a = (L~ (g1 | k)) \/ (LSeg ((g1 /. k),(g1 /. (k + 1)))) by A33, A31, TOPREAL3:38
.= (L~ b) \/ (LSeg ((g1 /. k),(g1 /. (k + 1)))) by FINSEQ_1:def 15
.= (L~ b) \/ (LSeg (g1,k)) by A11, A19, TOPREAL1:def 3 ;
then A42: 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 A43: 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 :: 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 ) )
per cases ( card s2 is even Element of NAT or not card s2 is even Element of NAT ) ;
suppose A44: 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 ;
A45: ( 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, A19, A42, A38, A43, 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, A19, A44, Th33;
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, A30, A24, A13, A35, A45, Th16; :: thesis: verum
end;
suppose A46: 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 ;
A47: ( 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, A19, A42, A38, A43, 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, A19, A46, Th33;
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, A30, A24, A13, A35, A47, Th16; :: 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 A48: 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 :: 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 ) )
per cases ( card s2 is even Element of NAT or not card s2 is even Element of NAT ) ;
suppose A49: 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 ;
A50: ( 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, A19, A42, A38, A48, 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, A19, A49, Th33;
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, A30, A24, A13, A35, A50, Th16; :: thesis: verum
end;
suppose A51: 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 ;
A52: ( 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, A19, A42, A38, A48, 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, A19, A51, Th33;
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, A30, A18, A20, A24, A13, A35, A52, 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;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
dom g1 = Seg (len g1) by FINSEQ_1:def 3;
then A53: g1 | (Seg (len g1)) = g1 ;
A54: 2 in dom g1 by A3, FINSEQ_3:25;
A55: 1 <= len g1 by A3, XXREAL_0:2;
then A56: 1 in dom g1 by FINSEQ_3:25;
now :: thesis: for a being FinSequence of (TOP-REAL 2) st a = g1 | (Seg 2) 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 ) )
g1 | 1 = g1 | (Seg 1) by FINSEQ_1:def 15;
then A57: len (g1 | 1) = 1 by A55, FINSEQ_1:17;
A58: 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 A59: 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 ) )
A60: a . (len a) = a . 2 by A3, A59, FINSEQ_1:17
.= g1 . (1 + 1) by A59, A58, FUNCT_1:49 ;
1 in Seg 2 by FINSEQ_1:2, TARSKI:def 2;
then A61: a . 1 = g1 . 1 by A59, FUNCT_1:49;
L~ a = L~ (g1 | 2) by A59, FINSEQ_1:def 15
.= (L~ (g1 | 1)) \/ (LSeg ((g1 /. 1),(g1 /. (1 + 1)))) by A56, A54, TOPREAL3:38
.= (L~ (g1 | 1)) \/ (LSeg (g1,1)) by A3, TOPREAL1:def 3
.= {} \/ (LSeg (g1,1)) by A57, 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, A61, A60, Th33; :: thesis: verum
end;
then A62: S1[2] ;
 for k being Nat st k >= 2 holds
S1[k] from NAT_1:sch 8(A62, 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, A53; :: thesis: verum