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

now :: thesis: ( ( i1 <= i2 & g1 = g2 ) or ( i1 > i2 & g1 = g2 ) )

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

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

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

end;

case A4: i1 > i2 ; :: thesis: g1 = g2

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

end;

end;

end;

hence g1 = g2 ; :: thesis: verum