let f be Function; :: thesis: ( f is empty implies f is one-to-one )
assume A1: f is empty ; :: thesis: f is one-to-one
let x1 be set ; :: according to FUNCT_1:def 8 :: thesis: for x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
let x2 be set ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
thus ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 ) by A1; :: thesis: verum