theorem Th4: :: HILBERT4:1

for f, g being one-to-one Function st f " = g " holds
f = g