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 Th21;
A2: ( Hom (b [x] a),b <> {} & Hom (b [x] a),a <> {} ) by Th21;
then Hom (b [x] a),(a [x] b) <> {} by Th25;
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, Th27
.= <:(pr1 b,a),((pr1 a,b) * <:(pr2 b,a),(pr1 b,a):>):> by A2, Def11
.= <:(pr1 b,a),(pr2 b,a):> by A2, Def11
.= id (b [x] a) by Th26 ;
:: thesis: verum