let A, B be non empty set ; :: thesis: for f being Function of A,B holds
( f is one-to-one iff for a, b being Element of A st f . a = f . b holds
a = b )
let f be Function of A,B; :: thesis: ( f is one-to-one iff for a, b being Element of A st f . a = f . b holds
a = b )
thus ( f is one-to-one implies for a, b being Element of A st f . a = f . b holds
a = b ) by FUNCT_2:19; :: thesis: ( ( for a, b being Element of A st f . a = f . b holds
a = b ) implies f is one-to-one )
assume for a, b being Element of A st f . a = f . b holds
a = b ; :: thesis: f is one-to-one
then for a, b being object st a in A & b in A & f . a = f . b holds
a = b ;
hence f is one-to-one by FUNCT_2:19; :: thesis: verum