theorem LemmaOne: :: FUZIMPL4:2

for R being Function st R ~ is Function holds
R is one-to-one