let i1, i2 be SetSequence of REAL; :: thesis: ( ( for n being Element of NAT holds i1 . n = halfline_fin ((n * (t ")),((n * (t ")) + (t "))) ) & ( for n being Element of NAT holds i2 . n = halfline_fin ((n * (t ")),((n * (t ")) + (t "))) ) implies i1 = i2 )
assume A2: for n being Element of NAT holds i1 . n = halfline_fin ((n * (t ")),((n * (t ")) + (t "))) ; :: thesis: ( ex n being Element of NAT st not i2 . n = halfline_fin ((n * (t ")),((n * (t ")) + (t "))) or i1 = i2 )
assume A3: for n being Element of NAT holds i2 . n = halfline_fin ((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 = halfline_fin ((n * (t ")),((n * (t ")) + (t "))) by A2;
hence i1 . n = i2 . n by A3; :: thesis: verum

end;

hence i1 = i2 ; :: thesis: verum