take f = n |-> the SCBinominativeFunction of V,A; :: thesis: ( f is V,A -FPrg-yielding & f is n -element )
thus f is V,A -FPrg-yielding :: thesis: f is n -element

proof

let a be Nat; :: according to NOMIN_2:def 6 :: thesis: ( 1 <= a & a <= len f implies f . a is SCBinominativeFunction of V,A )
dom f = Seg n ;
hence ( 1 <= a & a <= len f implies f . a is SCBinominativeFunction of V,A ) by FINSEQ_2:57, FINSEQ_3:25; :: thesis: verum

end;

thus f is n -element ; :: thesis: verum