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, Th44; :: 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 F9 being Functor of B,A such that
A3: F9 * F ~= id A and
A4: F * F9 ~= id B by A1, Def11;
(G * F) * F9 = G * (F * F9) by RELAT_1:36;
then A5: (G * F) * F9 ~= G by A4, Th42;
consider G9 being Functor of C,B such that
A6: G9 * G ~= id B and
A7: G * G9 ~= id C by A2, Def11;
take F9 * G9 ; :: thesis: ( (F9 * G9) * (G * F) ~= id A & (G * F) * (F9 * G9) ~= id C )
(F9 * G9) * G = F9 * (G9 * G) by RELAT_1:36;
then A8: (F9 * G9) * G ~= F9 by A6, Th42;
(F9 * G9) * (G * F) = ((F9 * G9) * G) * F by RELAT_1:36;
then (F9 * G9) * (G * F) ~= F9 * F by A8, Th41;
hence (F9 * G9) * (G * F) ~= id A by A3, NATTRA_1:29; :: thesis: (G * F) * (F9 * G9) ~= id C
(G * F) * (F9 * G9) = ((G * F) * F9) * G9 by RELAT_1:36;
then (G * F) * (F9 * G9) ~= G * G9 by A5, Th41;
hence (G * F) * (F9 * G9) ~= id C by A7, NATTRA_1:29; :: thesis: verum