for A, B being Category
for F being Functor of A,B
for G being Functor of B,A st G * F ~= id A holds
F is faithful