let f1, f2, g1, g2 be special FinSequence of (TOP-REAL 2); :: thesis: ( f1 ^' f2 is non constant standard special_circular_sequence & g1 ^' g2 is non constant standard special_circular_sequence & L~ f1 misses L~ g2 & L~ f2 misses L~ g1 & f1 ^' f2,g1 ^' g2 are_in_general_position implies for p1, p2, q1, q2 being Point of (TOP-REAL 2) st f1 . 1 = p1 & f1 . (len f1) = p2 & g1 . 1 = q1 & g1 . (len g1) = q2 & f1 /. (len f1) = f2 /. 1 & g1 /. (len g1) = g2 /. 1 & p1 in (L~ f1) /\ (L~ f2) & q1 in (L~ g1) /\ (L~ g2) & ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & q1 in C & q2 in C ) holds
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (g1 ^' g2)) ` & p1 in C & p2 in C ) )
assume that
A1: f1 ^' f2 is non constant standard special_circular_sequence and
A2: g1 ^' g2 is non constant standard special_circular_sequence and
A3: L~ f1 misses L~ g2 and
A4: L~ f2 misses L~ g1 and
A5: f1 ^' f2,g1 ^' g2 are_in_general_position ; :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st f1 . 1 = p1 & f1 . (len f1) = p2 & g1 . 1 = q1 & g1 . (len g1) = q2 & f1 /. (len f1) = f2 /. 1 & g1 /. (len g1) = g2 /. 1 & p1 in (L~ f1) /\ (L~ f2) & q1 in (L~ g1) /\ (L~ g2) & ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & q1 in C & q2 in C ) holds
ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (g1 ^' g2)) ` & p1 in C & p2 in C )
let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( f1 . 1 = p1 & f1 . (len f1) = p2 & g1 . 1 = q1 & g1 . (len g1) = q2 & f1 /. (len f1) = f2 /. 1 & g1 /. (len g1) = g2 /. 1 & p1 in (L~ f1) /\ (L~ f2) & q1 in (L~ g1) /\ (L~ g2) & ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & q1 in C & q2 in C ) implies ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (g1 ^' g2)) ` & p1 in C & p2 in C ) )
assume that
A6: ( f1 . 1 = p1 & f1 . (len f1) = p2 ) and
A7: ( g1 . 1 = q1 & g1 . (len g1) = q2 ) and
A8: f1 /. (len f1) = f2 /. 1 and
A9: g1 /. (len g1) = g2 /. 1 and
A10: p1 in (L~ f1) /\ (L~ f2) and
A11: q1 in (L~ g1) /\ (L~ g2) and
A12: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (f1 ^' f2)) ` & q1 in C & q2 in C ) ; :: thesis: ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (g1 ^' g2)) ` & p1 in C & p2 in C )
A13: f1 ^' f2,g1 are_in_general_position by A5, Th7;

A14: now :: thesis: ( not len f1 = 0 & not len f1 = 1 & not len f2 = 0 & not len f2 = 1 )

assume A15: ( len f1 = 0 or len f1 = 1 or len f2 = 0 or len f2 = 1 ) ; :: thesis: contradiction

per cases ( len f1 = 0 or len f1 = 1 or len f2 = 0 or len f2 = 1 ) by A15;

suppose ( len f1 = 0 or len f1 = 1 ) ; :: thesis: contradiction

then L~ f1 = {} by TOPREAL1:22;
hence contradiction by A10; :: thesis: verum

end;

suppose ( len f2 = 0 or len f2 = 1 ) ; :: thesis: contradiction

then L~ f2 = {} by TOPREAL1:22;
hence contradiction by A10; :: thesis: verum

end;

end;

end;

then A16: not len f2 is trivial by NAT_2:def 1;
then A17: not f2 is trivial by Lm2;

A18: now :: thesis: ( not len g1 = 0 & not len g1 = 1 & not len g2 = 0 & not len g2 = 1 )

assume A19: ( len g1 = 0 or len g1 = 1 or len g2 = 0 or len g2 = 1 ) ; :: thesis: contradiction

per cases ( len g1 = 0 or len g1 = 1 or len g2 = 0 or len g2 = 1 ) by A19;

suppose ( len g1 = 0 or len g1 = 1 ) ; :: thesis: contradiction

then L~ g1 = {} by TOPREAL1:22;
hence contradiction by A11; :: thesis: verum

end;

suppose ( len g2 = 0 or len g2 = 1 ) ; :: thesis: contradiction

then L~ g2 = {} by TOPREAL1:22;
hence contradiction by A11; :: thesis: verum

end;

end;

end;

then A20: not len g2 is trivial by NAT_2:def 1;
then A21: not g2 is trivial by Lm2;
A22: not len g1 is trivial by A18, NAT_2:def 1;
then A23: not g1 is empty by Lm2;
len g2 >= 1 + 1 by A20, NAT_2:29;
then A24: ( g1 is unfolded & g1 is s.n.c. ) by A2, Th4;
len g1 >= 2 by A22, NAT_2:29;
then A25: card ((L~ (f1 ^' f2)) /\ (L~ g1)) is even Element of NAT by A1, A7, A12, A13, A24, Th34;
len f2 >= 1 + 1 by A16, NAT_2:29;
then A26: ( f1 is unfolded & f1 is s.n.c. ) by A1, Th4;
A27: g1 ^' g2,f1 are_in_general_position by A5, Th7;
A28: not len f1 is trivial by A14, NAT_2:def 1;
then not f1 is empty by Lm2;
then A29: (L~ (f1 ^' f2)) /\ (L~ g1) = ((L~ f1) \/ (L~ f2)) /\ (L~ g1) by A8, A17, TOPREAL8:35
.= ((L~ f1) /\ (L~ g1)) \/ ((L~ f2) /\ (L~ g1)) by XBOOLE_1:23
.= ((L~ f1) /\ (L~ g1)) \/ {} by A4
.= ((L~ f1) /\ (L~ g1)) \/ ((L~ f1) /\ (L~ g2)) by A3
.= ((L~ g1) \/ (L~ g2)) /\ (L~ f1) by XBOOLE_1:23
.= (L~ f1) /\ (L~ (g1 ^' g2)) by A9, A23, A21, TOPREAL8:35 ;
len f1 >= 2 by A28, NAT_2:29;
hence ex C being Subset of (TOP-REAL 2) st
( C is_a_component_of (L~ (g1 ^' g2)) ` & p1 in C & p2 in C ) by A2, A6, A29, A27, A26, A25, Th34; :: thesis: verum