let i1, i2 be SetSequence of REAL; :: thesis: ( ( for n being Nat holds i1 . n = [.(n / t),((n / t) + (t ")).[ ) & ( for n being Nat holds i2 . n = [.(n / t),((n / t) + (t ")).[ ) implies i1 = i2 )
assume A2: for n being Nat holds i1 . n = [.(n / t),((n / t) + (t ")).[ ; :: thesis: ( ex n being Nat st not i2 . n = [.(n / t),((n / t) + (t ")).[ or i1 = i2 )
assume A3: for n being Nat holds i2 . n = [.(n / t),((n / t) + (t ")).[ ; :: thesis: i1 = i2
now :: thesis: for n being Element of NAT holds i1 . n = i2 . n
let n be Element of NAT ; :: thesis: i1 . n = i2 . n
i1 . n = [.(n / t),((n / t) + (t ")).[ by A2;
hence i1 . n = i2 . n by A3; :: thesis: verum
end;
hence i1 = i2 ; :: thesis: verum