let n be Nat; NOMIN_2:def 6 ( 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*> )
; <*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; verum