theorem Th92: :: FINSEQ_3:94

for x, y being object holds
( x <> y iff <*x,y*> is one-to-one )