let f1, f2, g1 be special FinSequence of (); :: 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 () 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 () 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 () 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 () st a = g1 | (Seg \$1) holds
( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of () 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 ;
then A12: 1 <= k + 1 by NAT_1:13;
now :: thesis: ( k + 1 <= len g1 implies for a being FinSequence of () st a = g1 | (Seg (k + 1)) holds
( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of () 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 () by FINSEQ_1:18;
1 in Seg k by ;
then A13: b . 1 = g1 . 1 by FUNCT_1:49;
reconsider s1 = (L~ (f1 ^' f2)) /\ (L~ b) as finite set by ;
set c = LSeg (g1,k);
A14: k in Seg k by ;
reconsider s2 = (L~ (f1 ^' f2)) /\ (LSeg (g1,k)) as finite set by ;
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 () st a = g1 | (Seg (k + 1)) holds
( card ((L~ (f1 ^' f2)) /\ (L~ b2)) is even Element of NAT iff ex C being Subset of () 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 (); :: thesis: ( a = g1 | (Seg (k + 1)) implies ( card ((L~ (f1 ^' f2)) /\ (L~ b1)) is even Element of NAT iff ex C being Subset of () 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 () 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 ;
A23: k + 1 in Seg (k + 1) by ;
then A24: g1 . (k + 1) = a . (k + 1) by
.= a . (len a) by ;
A25: k + 1 in Seg (len g1) by ;
then A26: k + 1 in dom a by ;
then A27: a /. (k + 1) = a . (k + 1) by PARTFUN1:def 6
.= g1 . (k + 1) by
.= g1 /. (k + 1) by ;
A28: len a = k + 1 by ;
g1 | (k + 1) = a by ;
then (L~ (a | k)) /\ (LSeg (a,k)) = {(a /. k)} by ;
then A29: (L~ (a | k)) /\ (LSeg ((a /. k),(a /. (k + 1)))) = {(a /. k)} by ;
1 in Seg (k + 1) by ;
then A30: g1 . 1 = a . 1 by ;
reconsider s = (L~ (f1 ^' f2)) /\ (L~ a) as finite set by A2, A21, Th6, Th11;
A31: a = g1 | (k + 1) by ;
A32: k < len g1 by ;
then A33: k in dom g1 by ;
A34: a | k = (g1 | (Seg (k + 1))) | (Seg k) by
.= g1 | (Seg k) by
.= g1 | k by FINSEQ_1:def 15 ;
A35: b . (len b) = b . k by
.= g1 . k by ;
k in Seg (k + 1) by ;
then A36: k in dom a by ;
then a /. k = a . k by PARTFUN1:def 6
.= g1 . k by
.= g1 /. k by ;
then (L~ b) /\ (LSeg ((g1 /. k),(g1 /. (k + 1)))) = {(g1 /. k)} by ;
then (L~ b) /\ (LSeg (g1,k)) = {(g1 /. k)} by ;
then A37: (L~ b) /\ (LSeg (g1,k)) = {(g1 . k)} by ;
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 ;
then x in (L~ b) /\ (LSeg (g1,k)) by XBOOLE_0:def 4;
then x = g1 . k by ;
then A41: x in rng g1 by ;
x in L~ (f1 ^' f2) by ;
hence contradiction by A5, A41, XBOOLE_0:3; :: thesis: verum
end;
k + 1 in dom g1 by ;
then L~ a = (L~ (g1 | k)) \/ (LSeg ((g1 /. k),(g1 /. (k + 1)))) by
.= (L~ b) \/ (LSeg ((g1 /. k),(g1 /. (k + 1)))) by FINSEQ_1:def 15
.= (L~ b) \/ (LSeg (g1,k)) by ;
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 () 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 () 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 () 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 () st
( C is_a_component_of (L~ (f1 ^' f2)) ` & b . 1 in C & b . (len b) in C ) ) by ;
ex C being Subset of () 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 () 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 () 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 () st
( C is_a_component_of (L~ (f1 ^' f2)) ` & b . 1 in C & b . (len b) in C ) ) by ;
for C being Subset of () 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 () 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 () 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 () 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 () 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 () 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 () holds
( not C is_a_component_of (L~ (f1 ^' f2)) ` or not b . 1 in C or not b . (len b) in C ) ) ) by ;
ex C being Subset of () 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 () 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 () 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 () holds
( not C is_a_component_of (L~ (f1 ^' f2)) ` or not b . 1 in C or not b . (len b) in C ) ) ) by ;
for C being Subset of () 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 () 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 () 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 ;
A55: 1 <= len g1 by ;
then A56: 1 in dom g1 by FINSEQ_3:25;
now :: thesis: for a being FinSequence of () st a = g1 | (Seg 2) holds
( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of () 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 ;
A58: 2 in Seg 2 by ;
let a be FinSequence of (); :: thesis: ( a = g1 | (Seg 2) implies ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of () 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 () 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
.= g1 . (1 + 1) by ;
1 in Seg 2 by ;
then A61: a . 1 = g1 . 1 by ;
L~ a = L~ (g1 | 2) by
.= (L~ (g1 | 1)) \/ (LSeg ((g1 /. 1),(g1 /. (1 + 1)))) by
.= (L~ (g1 | 1)) \/ (LSeg (g1,1)) by
.= {} \/ (LSeg (g1,1)) by
.= LSeg (g1,1) ;
hence ( card ((L~ (f1 ^' f2)) /\ (L~ a)) is even Element of NAT iff ex C being Subset of () 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 ;
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 () st
( C is_a_component_of (L~ (f1 ^' f2)) ` & g1 . 1 in C & g1 . (len g1) in C ) ) by ; :: thesis: verum