deffunc H₁( Nat) -> Element of L = E_eval ((F /. $1),x);
ex z being FinSequence of the carrier of L 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 L 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 = E_eval ((F /. i),x) ) )
thus dom z = dom F by A1, FINSEQ_3:29; :: thesis: for i being Nat st i in dom F holds
z . i = E_eval ((F /. i),x)
hence for i being Nat st i in dom F holds
z . i = E_eval ((F /. i),x) by A2; :: thesis: verum