deffunc H₁( Nat) -> Element of the carrier of (Polynom-Ring F_Real) = ^ (F /. $1);
ex z being FinSequence of the carrier of (Polynom-Ring F_Real) st
( len z = len F & ( for j being Nat st j in dom z holds
z . j = H₁(j) ) ) from FINSEQ_2:sch 1();
then consider z being FinSequence of the carrier of (Polynom-Ring F_Real) such that
A1: len z = len F and
A2: for j being Nat st j in dom z holds
z . j = H₁(j) ;
take z ; :: thesis: ( dom z = dom F & ( for i being Nat st i in dom F holds
z . i = ^ (F /. i) ) )
thus dom z = dom F by A1, FINSEQ_3:29; :: thesis: for i being Nat st i in dom F holds
z . i = ^ (F /. i)
hence for i being Nat st i in dom F holds
z . i = ^ (F /. i) by A2; :: thesis: verum