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 object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in K49(f) or not x2 in K49(f) or not f . x1 = f . x2 or x1 = x2 )
assume that
A1: x1 in dom f and
A2: x2 in dom f and
A3: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as set by TARSKI:1;
A4: not {} in P ;
then A5: f . x1 in x1 by A1, ORDERS_1:89;
f . x1 in x2 by A2, A3, A4, ORDERS_1:89;
then x1 meets x2 by A5, XBOOLE_0:3;
hence x1 = x2 by A1, A2, TAXONOM2:def 5; :: thesis: verum