theorem Th9: :: FUNCTOR0:9

for f, g being Function st ~ [:f,g:] is one-to-one holds
[:g,f:] is one-to-one