theorem Th10: :: FUNCTOR0:10

for f, g being Function st f is one-to-one & g is one-to-one holds
(~ [:f,g:]) " = ~ ([:g,f:] ")