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 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
let f be non constant standard special_circular_sequence; :: thesis: 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
let g1, g2 be FinSequence of (TOP-REAL 2); :: thesis: ( i1 <> i2 & g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & g1 . 2 = g2 . 2 implies g1 = g2 )
assume A1: ( i1 <> i2 & g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2 & g1 . 2 = g2 . 2 ) ; :: thesis: g1 = g2
per cases ( g1 is_a_part>_of f,i1,i2 or g1 is_a_part<_of f,i1,i2 ) by A1, Def4;
suppose A2: g1 is_a_part>_of f,i1,i2 ; :: thesis: g1 = g2
now
per cases ( g2 is_a_part>_of f,i1,i2 or g2 is_a_part<_of f,i1,i2 ) by A1, Def4;
case g2 is_a_part>_of f,i1,i2 ; :: thesis: g1 = g2
hence g1 = g2 by A2, Th64; :: thesis: verum
end;
end;
end;
hence g1 = g2 ; :: thesis: verum
end;
suppose A3: g1 is_a_part<_of f,i1,i2 ; :: thesis: g1 = g2
now
per cases ( g2 is_a_part>_of f,i1,i2 or g2 is_a_part<_of f,i1,i2 ) by A1, Def4;
case g2 is_a_part<_of f,i1,i2 ; :: thesis: g1 = g2
hence g1 = g2 by A3, Th65; :: thesis: verum
end;
end;
end;
hence g1 = g2 ; :: thesis: verum
end;
end;