let i1, i2 be Element of NAT ; :: thesis: for f being non constant standard special_circular_sequence
for g1, g2 being FinSequence of (TOP-REAL 2) st g1 is_a_part<_of f,i1,i2 & g2 is_a_part<_of f,i1,i2 holds
g1 = g2
let f be non constant standard special_circular_sequence; :: thesis: for g1, g2 being FinSequence of (TOP-REAL 2) st g1 is_a_part<_of f,i1,i2 & g2 is_a_part<_of f,i1,i2 holds
g1 = g2
let g1, g2 be FinSequence of (TOP-REAL 2); :: thesis: ( g1 is_a_part<_of f,i1,i2 & g2 is_a_part<_of f,i1,i2 implies g1 = g2 )
assume A1: ( g1 is_a_part<_of f,i1,i2 & g2 is_a_part<_of f,i1,i2 ) ; :: thesis: g1 = g2

per cases ( i1 >= i2 or i1 < i2 ) ;

suppose A2: i1 >= i2 ; :: thesis: g1 = g2

then g1 = mid f,i1,i2 by A1, Th39;
hence g1 = g2 by A1, A2, Th39; :: thesis: verum

end;

suppose A3: i1 < i2 ; :: thesis: g1 = g2

then g1 = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) by A1, Th40;
hence g1 = g2 by A1, A3, Th40; :: thesis: verum

end;

end;