thus ( f is one-to-one implies for x, y being Element of L1 st f . x = f . y holds
x = y ) by FUNCT_2:19; :: thesis: ( ( for x, y being Element of L1 st f . x = f . y holds
x = y ) implies f is one-to-one )
assume for x, y being Element of L1 st f . x = f . y holds
x = y ; :: thesis: f is one-to-one
then for x, y being object st x in the carrier of L1 & y in the carrier of L1 & f . x = f . y holds
x = y ;
hence f is one-to-one by FUNCT_2:19; :: thesis: verum