let A, B be Category; for F being Functor of A,B
for G being Functor of B,A
for I being Functor of A,A st I ~= id A holds
( F * I ~= F & I * G ~= G )
let F be Functor of A,B; for G being Functor of B,A
for I being Functor of A,A st I ~= id A holds
( F * I ~= F & I * G ~= G )
let G be Functor of B,A; for I being Functor of A,A st I ~= id A holds
( F * I ~= F & I * G ~= G )
let I be Functor of A,A; ( I ~= id A implies ( F * I ~= F & I * G ~= G ) )
( F * (id A) = F & (id A) * G = G )
by FUNCT_2:17;
hence
( I ~= id A implies ( F * I ~= F & I * G ~= G ) )
by Th41; verum