let n be Nat; :: according to NOMIN_2:def 6 :: thesis: ( 1 <= n & n <= len <*f*> implies <*f*> . n is SCBinominativeFunction of V,A )
assume A1: ( 1 <= n & n <= len <*f*> ) ; :: thesis: <*f*> . n is SCBinominativeFunction of V,A
len <*f*> = 1 by FINSEQ_1:40;
then n = 1 by A1, XXREAL_0:1;
hence <*f*> . n is SCBinominativeFunction of V,A ; :: thesis: verum