:: deftheorem Def6 defines double-one-to-one FLEXARY1:def 6 :
for F being Function-yielding Function holds
( F is double-one-to-one iff for x1, x2, y1, y2 being object st x1 in dom F & y1 in dom (F . x1) & x2 in dom F & y2 in dom (F . x2) & F _ (x1,y1) = F _ (x2,y2) holds
( x1 = x2 & y1 = y2 ) );