theorem Th2: :: NAGATA_2:2

PairFunc is bijective