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 Th33; :: according to CAT_4:def 2 :: thesis: ex f being Morphism of a [x] b,b [x] a ex f' being Morphism of b [x] a,a [x] b st
( f * f' = id (b [x] a) & f' * f = id (a [x] b) )
take Switch a,b ; :: thesis: ex f' being Morphism of b [x] a,a [x] b st
( (Switch a,b) * f' = id (b [x] a) & f' * (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 Th34; :: thesis: verum