let P be non empty mutually-disjoint with_non-empty_elements set ; :: thesis: for f being Choice_Function of P holds f is one-to-one
let f be Choice_Function of P; :: thesis: f is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume 00: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
not {} in P ;
then ( f . x1 in x1 & f . x1 in x2 ) by 00, ORDERS_1:def 1;
then x1 meets x2 by XBOOLE_0:3;
hence x1 = x2 by 00, TAXONOM2:def 5; :: thesis: verum