defpred S₁[ Nat, set ] means $2 = (F . $1) . x;
A1: for n being Nat st n in Seg (len F) holds
ex z being Element of ExtREAL st S₁[n,z] ;
consider p being FinSequence of ExtREAL such that
A2: dom p = Seg (len F) and
A3: for n being Nat st n in Seg (len F) holds
S₁[n,p . n] from FINSEQ_1:sch 5(A1);
take p ; :: thesis: ( dom p = dom F & ( for n being Element of NAT st n in dom p holds
p . n = (F . n) . x ) )
thus dom p = dom F by A2, FINSEQ_1:def 3; :: thesis: for n being Element of NAT st n in dom p holds
p . n = (F . n) . x
thus for n being Element of NAT st n in dom p holds
p . n = (F . n) . x by A2, A3; :: thesis: verum