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