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