theorem Th43: :: JORDAN4:43

for f being constant standard special_circular_sequence
for i1, i2 being Nat
for g1, g2 being FinSequence of (TOP-REAL 2) st 1 <= i1 & i1 < i2 & i2 < len f & g1 = mid (f,i1,i2) & g2 = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) holds
( (L~ g1) /\ (L~ g2) = {(f . i1),(f . i2)} & (L~ g1) \/ (L~ g2) = L~ f )