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

proof

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 (len z) by FINSEQ_1:def 3;
then consider i0 being Nat such that
A5: i0 = i and
1 <= i0 and
i0 <= len z by A3;
reconsider i = i as Nat by A5;
z . i = ((Der1 INT.Ring) |^ (i -' 1)) . f by A1, A3;
hence y in the carrier of (Polynom-Ring INT.Ring) by A4; :: thesis: verum

end;

hence z is FinSequence of the carrier of (Polynom-Ring INT.Ring) by FINSEQ_1:def 4; :: thesis: verum

end;

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 = len f & ( for i being Nat st i in dom z holds
z . i = ((Der1 INT.Ring) |^ (i -' 1)) . f ) ) by A1; :: thesis: verum