scheme :: ASYMPT_0:sch 3
FinImInit2{ F1() -> Nat, F2() -> non empty set , F3( set ) -> Element of F2() } :
{ F3(n) where n is Element of NAT : n < F1() } is non empty finite Subset of F2()
provided
A1: F1() > 0