let f be non constant standard special_circular_sequence; :: thesis: for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part_of f,i1,i2 holds
( 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 Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop ((i1 + i) -' 1),f) or for i being Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop (((len f) + i1) -' i),f) ) )
let g be FinSequence of (TOP-REAL 2); :: thesis: for i1, i2 being Element of NAT st g is_a_part_of f,i1,i2 holds
( 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 Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop ((i1 + i) -' 1),f) or for i being Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop (((len f) + i1) -' i),f) ) )
let i1, i2 be Element of NAT ; :: thesis: ( g is_a_part_of f,i1,i2 implies ( 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 Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop ((i1 + i) -' 1),f) or for i being Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop (((len f) + i1) -' i),f) ) ) )
assume A1: g is_a_part_of f,i1,i2 ; :: thesis: ( 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 Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop ((i1 + i) -' 1),f) or for i being Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop (((len f) + i1) -' i),f) ) )

now

per cases ( g is_a_part>_of f,i1,i2 or g is_a_part<_of f,i1,i2 ) by A1, Def4;

case g is_a_part>_of f,i1,i2 ; :: thesis: ( 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 Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop ((i1 + i) -' 1),f) or for i being Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop (((len f) + i1) -' i),f) ) )

hence ( 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 Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop ((i1 + i) -' 1),f) or for i being Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop (((len f) + i1) -' i),f) ) ) by Def2; :: thesis: verum

end;

case g is_a_part<_of f,i1,i2 ; :: thesis: ( 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 Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop ((i1 + i) -' 1),f) or for i being Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop (((len f) + i1) -' i),f) ) )

hence ( 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 Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop ((i1 + i) -' 1),f) or for i being Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop (((len f) + i1) -' i),f) ) ) by Def3; :: thesis: verum

end;

end;

end;

hence ( 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 Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop ((i1 + i) -' 1),f) or for i being Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop (((len f) + i1) -' i),f) ) ) ; :: thesis: verum