theorem Th32: :: CAT_4:32

for C being Cartesian_category
for a, b being Object of C holds (Switch (a,b)) * (Switch (b,a)) = id (b [x] a)