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

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