let A, B be Category; :: thesis: ( A,B are_equivalent implies for F being Equivalence of A,B ex G being Equivalence of B,A st
( G * F ~= id A & F * G ~= id B ) )
assume A1: A,B are_equivalent ; :: thesis: for F being Equivalence of A,B ex G being Equivalence of B,A st
( G * F ~= id A & F * G ~= id B )
let F be Equivalence of A,B; :: thesis: ex G being Equivalence of B,A st
( G * F ~= id A & F * G ~= id B )
consider G being Functor of B,A such that
A2: ( G * F ~= id A & F * G ~= id B ) by A1, Def11;
G is Equivalence of B,A
proof
thus B,A are_equivalent by A1; :: according to ISOCAT_1:def 11 :: thesis: ex G being Functor of A,B st
( G * G ~= id B & G * G ~= id A )
take F ; :: thesis: ( F * G ~= id B & G * F ~= id A )
thus ( F * G ~= id B & G * F ~= id A ) by A2; :: thesis: verum
end;
hence ex G being Equivalence of B,A st
( G * F ~= id A & F * G ~= id B ) by A2; :: thesis: verum