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 Element of NAT holds g . n = halfline_fin ((n * (t ")),((n * (t ")) + (t ")))
let n be Element of NAT ; :: thesis: g . n = halfline_fin ((n * (t ")),((n * (t ")) + (t ")))
thus g . n = halfline_fin ((n * (t ")),((n * (t ")) + (t "))) by A1; :: thesis: verum