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

now

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

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

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

end;

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

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

end;

end;

end;

hence g1 = g2 ; :: thesis: verum