scheme :: ASYMPT_0:sch 2
FinImInit1{ F₁() -> Nat, F₂() -> non empty set , F₃( set ) -> Element of F₂() } :

{ F₃(n) where n is Element of NAT : n <= F₁() } is non empty finite Subset of F₂()