let i1, i2 be Nat; :: thesis:
let f be constant standard special_circular_sequence; :: thesis:
let g1, g2 be FinSequence of (TOP-REAL 2); :: thesis:
assume that
A1: i1 <> i2 and
A2: g1 is_a_part_of f,i1,i2 and
A3: g2 is_a_part_of f,i1,i2 and
A4: g1 . 2 = g2 . 2 ; :: thesis:

per cases by A2;

suppose A5: g1 is_a_part>_of f,i1,i2 ; :: thesis:

now :: thesis:

per cases by A3;

case g2 is_a_part>_of f,i1,i2 ; :: thesis:

hence g1 = g2 by A5, Th52; :: thesis:

end;

case g2 is_a_part<_of f,i1,i2 ; :: thesis:

hence contradiction by A1, A4, A5, Th54; :: thesis:

end;

end;

end;

hence g1 = g2 ; :: thesis:

end;

suppose A6: g1 is_a_part<_of f,i1,i2 ; :: thesis:

now :: thesis:

per cases by A3;

case g2 is_a_part>_of f,i1,i2 ; :: thesis:

hence contradiction by A1, A4, A6, Th54; :: thesis:

end;

case g2 is_a_part<_of f,i1,i2 ; :: thesis:

hence g1 = g2 by A6, Th53; :: thesis:

end;

end;

end;

hence g1 = g2 ; :: thesis:

end;

end;