let i1, i2 be Nat; for f being V26() 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 V26() 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 g1, g2 be FinSequence of (TOP-REAL 2); ( 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
; g1 = g2
now ( ( i1 <= i2 & g1 = g2 ) or ( i1 > i2 & g1 = g2 ) )end;
hence
g1 = g2
; verum