defpred S₁[ set , set ] means ex p being Polynomial of L st
( p = F . $1 & $2 = p . i );
A1: for k being Nat st k in Seg (len F) holds
ex x being Element of the carrier of L st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len F) implies ex x being Element of the carrier of L st S₁[k,x] )
assume A2: k in Seg (len F) ; :: thesis: ex x being Element of the carrier of L st S₁[k,x]
reconsider t = F /. k as Polynomial of L by POLYNOM3:def 10;
take t . i ; :: thesis: S₁[k,t . i]
take t ; :: thesis: ( t = F . k & t . i = t . i )
k in dom F by A2, FINSEQ_1:def 3;
hence t = F . k by PARTFUN1:def 6; :: thesis: t . i = t . i
thus t . i = t . i ; :: thesis: verum

end;

consider G being FinSequence of L such that
A3: ( dom G = Seg (len F) & ( for k being Nat st k in Seg (len F) holds
S₁[k,G . k] ) ) from FINSEQ_1:sch 5(A1);
take G ; :: thesis: ( len G = len F & ( for j being Element of NAT st j in dom G holds
ex p being Polynomial of L st
( p = F . j & G . j = p . i ) ) )
thus len G = len F by A3, FINSEQ_1:def 3; :: thesis: for j being Element of NAT st j in dom G holds
ex p being Polynomial of L st
( p = F . j & G . j = p . i )
thus for j being Element of NAT st j in dom G holds
ex p being Polynomial of L st
( p = F . j & G . j = p . i ) by A3; :: thesis: verum