theorem Th6: :: FUNCTOR0:6

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