:: deftheorem defines is_a_part<_of JORDAN4:def 3 :
for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat holds
( g is_a_part<_of f,i1,i2 iff ( 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & g . (len g) = f . i2 & 1 <= len g & len g < len f & ( for i being Nat st 1 <= i & i <= len g holds
g . i = f . (S_Drop ((((len f) + i1) -' i),f)) ) ) );