:: deftheorem defines one-to-one YELLOW18:def 1 :
for A, B, C being non empty set
for f being Function of [:A,B:],C holds
( f is one-to-one iff for a1, a2 being Element of A
for b1, b2 being Element of B st f . (a1,b1) = f . (a2,b2) holds
( a1 = a2 & b1 = b2 ) );