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 S_{1}[ 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;

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;

_{1}[2]
;

for k being Nat st k >= 2 holds

S_{1}[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

( 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 S

( 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 & S_{1}[k] holds

S_{1}[k + 1]

dom g1 = Seg (len g1)
by FINSEQ_1:def 3;S

let k be Nat; :: thesis: ( k >= 2 & S_{1}[k] implies S_{1}[k + 1] )

assume that

A9: k >= 2 and

A10: S_{1}[k]
; :: thesis: S_{1}[k + 1]

A11: 1 <= k by A9, XXREAL_0:2;

then A12: 1 <= k + 1 by NAT_1:13;

_{1}[k + 1]
; :: thesis: verum

end;assume that

A9: k >= 2 and

A10: S

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 ) ) )

hence
S( 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~ b_{2})) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st

( b_{3} is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b_{3} & C . (len C) in b_{3} ) )

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~ b_{1})) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st

( b_{2} is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b_{2} & C . (len C) in b_{2} ) ) )

assume A21: a = g1 | (Seg (k + 1)) ; :: thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ b_{1})) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st

( b_{2} is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b_{2} & C . (len C) in b_{2} ) )

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

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;

end;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~ b

( b

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~ b

( b

assume A21: a = g1 | (Seg (k + 1)) ; :: thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ b

( b

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

k + 1 in dom g1
by A6, A12, A19, FINSEQ_1:1;
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;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

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 )
;

end;

suppose A43:
card s1 is even Element of NAT
; :: thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ b_{1})) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st

( b_{2} is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b_{2} & C . (len C) in b_{2} ) )

( b

then reconsider c1 = card ((L~ (f1 ^' f2)) /\ (L~ b)) as even Integer ;

( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) ) ; :: thesis: verum

end;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 ) )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 ) )

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

end;

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 ) )

( 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;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

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 ) )

( 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;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

( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) ) ; :: thesis: verum

suppose A48:
card s1 is not even Element of NAT
; :: thesis: ( card ((L~ (f1 ^' f2)) /\ (L~ b_{1})) is even Element of NAT iff ex C being Subset of (TOP-REAL 2) st

( b_{2} is_a_component_of (L~ (f1 ^' f2)) ` & C . 1 in b_{2} & C . (len C) in b_{2} ) )

( b

then reconsider c1 = card ((L~ (f1 ^' f2)) /\ (L~ b)) as odd Integer ;

( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) ) ; :: thesis: verum

end;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 ) )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 ) )

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

end;

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 ) )

( 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;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

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 ) )

( 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;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

( C is_a_component_of (L~ (f1 ^' f2)) ` & a . 1 in C & a . (len a) in C ) ) ; :: thesis: verum

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 ) )

then A62:
S( 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 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

for k being Nat st k >= 2 holds

S

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