let C be Cartesian_category; :: thesis: for a, b being Object of C holds (Switch (a,b)) * (Switch (b,a)) = id (b [x] a)
let a, b be Object of C; :: thesis: (Switch (a,b)) * (Switch (b,a)) = id (b [x] a)
A1: ( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) by Th19;
A2: ( Hom ((b [x] a),b) <> {} & Hom ((b [x] a),a) <> {} ) by Th19;
then Hom ((b [x] a),(a [x] b)) <> {} by Th23;
hence (Switch (a,b)) * (Switch (b,a)) = <:((pr2 (a,b)) * <:(pr2 (b,a)),(pr1 (b,a)):>),((pr1 (a,b)) * <:(pr2 (b,a)),(pr1 (b,a)):>):> by A1, Th25
.= <:(pr1 (b,a)),((pr1 (a,b)) * <:(pr2 (b,a)),(pr1 (b,a)):>):> by A2, Def10
.= <:(pr1 (b,a)),(pr2 (b,a)):> by A2, Def10
.= id (b [x] a) by Th24 ;
:: thesis: verum