defpred S₁[ Nat, object ] means $2 = ($1 - 1) ^2 ;
A1: for k being Nat st k in Seg v holds
ex x being Element of INT st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg v implies ex x being Element of INT st S₁[k,x] )
assume k in Seg v ; :: thesis: ex x being Element of INT st S₁[k,x]
reconsider j = (k - 1) ^2 as Element of INT by INT_1:def 2;
take j ; :: thesis: S₁[k,j]
thus S₁[k,j] ; :: thesis: verum

end;

consider f being FinSequence of INT such that
A2: ( dom f = Seg v & ( for k being Nat st k in Seg v holds
S₁[k,f . k] ) ) from FINSEQ_1:sch 5(A1);
take f ; :: thesis: ( len f = v & ( for i being Nat st i in dom f holds
f . i = (i - 1) ^2 ) )
Seg (len f) = Seg v by FINSEQ_1:def 3, A2;
hence len f = v by FINSEQ_1:6; :: thesis: for i being Nat st i in dom f holds
f . i = (i - 1) ^2
thus for i being Nat st i in dom f holds
f . i = (i - 1) ^2 by A2; :: thesis: verum