deffunc H₁( Element of NAT ) -> Element of K16(REAL) = halfline_fin (($1 / t),(($1 / t) + (t ")));
consider g being SetSequence of REAL such that
A1: for x being Element of NAT holds g . x = H₁(x) from FUNCT_2:sch 4();
take g ; :: thesis: for n being Nat holds g . n = [.(n / t),((n / t) + (t ")).[
let n be Nat; :: thesis: g . n = [.(n / t),((n / t) + (t ")).[
n in NAT by ORDINAL1:def 12;
hence g . n = [.(n / t),((n / t) + (t ")).[ by A1; :: thesis: verum