deffunc H₁( Nat) -> object = [\((frac (($1 - 1) * a)) * t)/];
consider z being FinSequence such that
A1: ( len z = t + 1 & ( for k being Nat st k in dom z holds
z . k = H₁(k) ) ) from FINSEQ_1:sch 2();
take z ; :: thesis: ( z is Element of K16(K17(omega,(Segm t))) & z is FinSequence of Segm t & len z = t + 1 & ( for i being Nat st i in dom z holds
z . i = [\((frac ((i - 1) * a)) * t)/] ) )
z is FinSequence of Segm t

proof

A2: for y being object st y in rng z holds
y in Segm t

proof

let y be object ; :: thesis: ( y in rng z implies y in Segm t )
assume y in rng z ; :: thesis: y in Segm t
then consider i being object such that
A4: i in dom z and
A5: y = z . i by FUNCT_1:def 3;
dom z = Seg (len z) by FINSEQ_1:def 3
.= Seg (t + 1) by A1 ;
then consider i0 being Nat such that
A7: i0 = i and
1 <= i0 and
i0 <= t + 1 by A4;
reconsider i = i as Nat by A7;
A8: z . i = H₁(i) by A1, A4
.= [\((frac ((i - 1) * a)) * t)/] ;
( 0 <= frac ((i - 1) * a) & frac ((i - 1) * a) < 1 ) by INT_1:43;
then consider j being Nat such that
A10: j <= t - 1 and
A11: [\((frac ((i - 1) * a)) * t)/] = j by Lm9, XXREAL_1:3;
j < (t - 1) + 1 by A10, XREAL_1:39;
hence y in Segm t by A5, NAT_1:44, A11, A8; :: thesis: verum

end;

rng z c= Segm t by A2;
hence z is FinSequence of Segm t by FINSEQ_1:def 4; :: thesis: verum

end;

hence ( z is Element of K16(K17(omega,(Segm t))) & z is FinSequence of Segm t & len z = t + 1 & ( for i being Nat st i in dom z holds
z . i = [\((frac ((i - 1) * a)) * t)/] ) ) by A1; :: thesis: verum