let i1, i2 be Nat; :: thesis: 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; :: 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
per cases ( i1 >= i2 or i1 < i2 ) ;
suppose A3: i1 >= i2 ; :: thesis: g1 = g2
then g1 = mid (f,i1,i2) by A1, Th27;
hence g1 = g2 by A2, A3, Th27; :: thesis: verum
end;
suppose A4: i1 < i2 ; :: thesis: g1 = g2
then g1 = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) by A1, Th28;
hence g1 = g2 by A2, A4, Th28; :: thesis: verum
end;
end;