let i1, i2 be Nat; :: thesis: for f being 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 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 that
A1: g1 is_a_part<_of f,i1,i2 and
A2: g2 is_a_part<_of f,i1,i2 ; :: thesis: g1 = g2

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

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

then g1 = mid (f,i1,i2) by A1, Th27;
hence g1 = g2 by A2, A3, Th27; :: thesis: verum

end;

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

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

end;

end;