let A, B, C be Category; :: thesis: ( A,B are_equivalent & B,C are_equivalent implies for F being Equivalence of A,B
for G being Equivalence of B,C holds G * F is Equivalence of A,C )
assume that
A1: A,B are_equivalent and
A2: B,C are_equivalent ; :: thesis: for F being Equivalence of A,B
for G being Equivalence of B,C holds G * F is Equivalence of A,C
let F be Equivalence of A,B; :: thesis: for G being Equivalence of B,C holds G * F is Equivalence of A,C
let G be Equivalence of B,C; :: thesis: G * F is Equivalence of A,C
thus A,C are_equivalent by A1, A2, Th53; :: according to ISOCAT_1:def 11 :: thesis: ex G being Functor of C,A st
( G * (G * F) ~= id A & (G * F) * G ~= id C )
consider F' being Functor of B,A such that
A3: F' * F ~= id A and
A4: F * F' ~= id B by A1, Def11;
(G * F) * F' = G * (F * F') by RELAT_1:55;
then A5: (G * F) * F' ~= G by A4, Th49;
consider G' being Functor of C,B such that
A6: G' * G ~= id B and
A7: G * G' ~= id C by A2, Def11;
take F' * G' ; :: thesis: ( (F' * G') * (G * F) ~= id A & (G * F) * (F' * G') ~= id C )
(F' * G') * G = F' * (G' * G) by RELAT_1:55;
then A8: (F' * G') * G ~= F' by A6, Th49;
(F' * G') * (G * F) = ((F' * G') * G) * F by RELAT_1:55;
then (F' * G') * (G * F) ~= F' * F by A8, Th48;
hence (F' * G') * (G * F) ~= id A by A3, NATTRA_1:32; :: thesis: (G * F) * (F' * G') ~= id C
(G * F) * (F' * G') = ((G * F) * F') * G' by RELAT_1:55;
then (G * F) * (F' * G') ~= G * G' by A5, Th48;
hence (G * F) * (F' * G') ~= id C by A7, NATTRA_1:32; :: thesis: verum