deffunc H₁( Nat) -> Element of the carrier of L = 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 = 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 = eval ((~ (F /. i)),x)
hence for i being Nat st i in dom F holds
z . i = eval ((~ (F /. i)),x) by A2; :: thesis: verum