scheme :: FINSEQ_1:sch 6
FinSegRng{ F1() -> Nat, F2( set ) -> set , P1[ set ] } :
{ F2(i) where i is Nat : ( i <= F1() & P1[i] ) } is finite