let i1, i2 be SetSequence of REAL; ( ( 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 ")).[
; ( 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 ")).[
; i1 = i2
hence
i1 = i2
; verum