for i1, i2 being Nat
for f being V26() standard special_circular_sequence
for g1, g2 being FinSequence of (TOP-REAL 2) st i1 <> i2 & g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & g1 . 2 = g2 . 2 holds
g1 = g2