deffunc H₁( Nat) -> Element of the carrier of (Polynom-Ring INT.Ring) = (tau $1) |^ p;
consider z being FinSequence such that
A1: ( len z = m & ( 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 (Polynom-Ring INT.Ring))) & z is FinSequence of the carrier of (Polynom-Ring INT.Ring) & len z = m & ( for i being Nat st i in dom z holds
z . i = (tau i) |^ p ) )
rng z c= the carrier of (Polynom-Ring INT.Ring)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng z or y in the carrier of (Polynom-Ring INT.Ring) )
assume y in rng z ; :: thesis: y in the carrier of (Polynom-Ring INT.Ring)
then consider i being object such that
A3: i in dom z and
A4: y = z . i by FUNCT_1:def 3;
dom z = Seg m by A1, FINSEQ_1:def 3;
then consider i0 being Nat such that
A5: i0 = i and
1 <= i0 and
i0 <= m by A3;
z . i0 = (tau i0) |^ p by A1, A3, A5;
hence y in the carrier of (Polynom-Ring INT.Ring) by A4, A5; :: thesis: verum

end;

then z is FinSequence of the carrier of (Polynom-Ring INT.Ring) by FINSEQ_1:def 4;
hence ( z is Element of K10(K11(NAT, the carrier of (Polynom-Ring INT.Ring))) & z is FinSequence of the carrier of (Polynom-Ring INT.Ring) & len z = m & ( for i being Nat st i in dom z holds
z . i = (tau i) |^ p ) ) by A1; :: thesis: verum