let C be Cartesian_category; :: thesis: for a, b being Object of C holds a [x] b,b [x] a are_isomorphic
let a, b be Object of C; :: thesis: a [x] b,b [x] a are_isomorphic
thus ( Hom ((a [x] b),(b [x] a)) <> {} & Hom ((b [x] a),(a [x] b)) <> {} ) by Th31; :: according to CAT_4:def 1 :: thesis: ex f being Morphism of a [x] b,b [x] a ex f9 being Morphism of b [x] a,a [x] b st
( f * f9 = id (b [x] a) & f9 * f = id (a [x] b) )
take Switch (a,b) ; :: thesis: ex f9 being Morphism of b [x] a,a [x] b st
( (Switch (a,b)) * f9 = id (b [x] a) & f9 * (Switch (a,b)) = id (a [x] b) )
take Switch (b,a) ; :: thesis: ( (Switch (a,b)) * (Switch (b,a)) = id (b [x] a) & (Switch (b,a)) * (Switch (a,b)) = id (a [x] b) )
thus ( (Switch (a,b)) * (Switch (b,a)) = id (b [x] a) & (Switch (b,a)) * (Switch (a,b)) = id (a [x] b) ) by Th32; :: thesis: verum