let A, B be Category; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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; :: thesis: verum