scheme :: TEX_2:sch 1
ExChoiceFCol{ F1() -> non empty TopStruct , F2() -> Subset-Family of F1(), P1[ object , object ] } :
ex f being Function of F2(), the carrier of F1() st
for S being Subset of F1() st S in F2() holds
P1[S,f . S]
provided
A1: for S being Subset of F1() st S in F2() holds
ex x being Point of F1() st P1[S,x]