per cases ( f <> {} or f = {} ) ;

suppose A1: f <> {} ; :: thesis: .: f is one-to-one

reconsider f0 = f as Function of (dom f),(rng f) by FUNCT_2:1;

now :: thesis: for x1, x2 being object st x1 in dom (.: f) & x2 in dom (.: f) & (.: f) . x1 = (.: f) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom (.: f) & x2 in dom (.: f) & (.: f) . x1 = (.: f) . x2 implies x1 = x2 )
assume A2: ( x1 in dom (.: f) & x2 in dom (.: f) & (.: f) . x1 = (.: f) . x2 ) ; :: thesis: x1 = x2
then reconsider X1 = x1, X2 = x2 as Subset of (dom f) by FUNCT_3:def 1;
( (.: f) . x1 = f .: X1 & (.: f) . x2 = f .: X2 ) by A2, FUNCT_3:7;
then f0 .: X1 = f0 .: X2 by A2;
hence x1 = x2 by A1, COMBGRAS:6; :: thesis: verum

end;

hence .: f is one-to-one by FUNCT_1:def 4; :: thesis: verum

end;

suppose f = {} ; :: thesis: .: f is one-to-one

hence .: f is one-to-one by Th5; :: thesis: verum

end;

end;