deffunc H₁( Nat) -> Element of the carrier of R = Product (Replace (s,$1,(D . (s /. $1))));
consider z being FinSequence such that
A1: ( len z = len s & ( 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 K10(K11(NAT, the carrier of R)) & z is FinSequence of the carrier of R & len z = len s & ( for i being Nat st i in dom z holds
z . i = Product (Replace (s,i,(D . (s /. i)))) ) )
z is FinSequence of the carrier of R

proof

A2: for p being object st p in rng z holds
p in the carrier of R

proof

let p be object ; :: thesis: ( p in rng z implies p in the carrier of R )
assume p in rng z ; :: thesis: p in the carrier of R
then consider i being object such that
A3: i in dom z and
A4: p = z . i by FUNCT_1:def 3;
reconsider i = i as Nat by A3;
z . i = Product (Replace (s,i,(D . (s /. i)))) by A1, A3;
hence p in the carrier of R by A4; :: thesis: verum

end;

rng z c= the carrier of R by A2;
hence z is FinSequence of the carrier of R by FINSEQ_1:def 4; :: thesis: verum

end;

hence ( z is Element of K10(K11(NAT, the carrier of R)) & z is FinSequence of the carrier of R & len z = len s & ( for i being Nat st i in dom z holds
z . i = Product (Replace (s,i,(D . (s /. i)))) ) ) by A1; :: thesis: verum