scheme :: FUNCT_2:sch 10
MChoice{ F₁() -> non empty set , F₂() -> non empty set , F₃( object ) -> set } :

ex t being Function of F₁(),F₂() st
for a being Element of F₁() holds t . a in F₃(a)

provided

A1: for a being Element of F₁() holds F₂() meets F₃(a)