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 A1: ( A,B are_equivalent & 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
consider F' being Functor of B,A such that
A2: ( F' * F ~= id A & F * F' ~= id B ) by A1, Def11;
consider G' being Functor of C,B such that
A3: ( G' * G ~= id B & G * G' ~= id C ) by A1, Def11;
thus A,C are_equivalent by A1, 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 )
take F' * G' ; :: thesis: ( (F' * G') * (G * F) ~= id A & (G * F) * (F' * G') ~= id C )
( (F' * G') * G = F' * (G' * G) & F' * (id B) = F' ) by FUNCT_2:23, RELAT_1:55;
then A4: (F' * G') * G ~= F' by A3, Th49;
(F' * G') * (G * F) = ((F' * G') * G) * F by RELAT_1:55;
then (F' * G') * (G * F) ~= F' * F by A4, Th48;
hence (F' * G') * (G * F) ~= id A by A2, NATTRA_1:32; :: thesis: (G * F) * (F' * G') ~= id C
( (G * F) * F' = G * (F * F') & G * (id B) = G ) by FUNCT_2:23, RELAT_1:55;
then A5: (G * F) * F' ~= G by A2, Th49;
(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 A3, NATTRA_1:32; :: thesis: verum