let C be Cartesian_category; :: thesis: for a being Object of C holds
( (lambda a) * (lambda' a) = id a & (lambda' a) * (lambda a) = id (([1] C) [x] a) & (rho a) * (rho' a) = id a & (rho' a) * (rho a) = id (a [x] ([1] C)) )
let a be Object of C; :: thesis: ( (lambda a) * (lambda' a) = id a & (lambda' a) * (lambda a) = id (([1] C) [x] a) & (rho a) * (rho' a) = id a & (rho' a) * (rho a) = id (a [x] ([1] C)) )
A1: (term a) * (pr2 (([1] C),a)) = pr1 (([1] C),a) by Th14;
A2: ( Hom (a,([1] C)) <> {} & Hom (a,a) <> {} ) by Th15, CAT_1:27;
hence id a = (lambda a) * (lambda' a) by Def11; :: thesis: ( (lambda' a) * (lambda a) = id (([1] C) [x] a) & (rho a) * (rho' a) = id a & (rho' a) * (rho a) = id (a [x] ([1] C)) )
A3: Hom ((([1] C) [x] a),a) <> {} by Th21;
then (id a) * (pr2 (([1] C),a)) = pr2 (([1] C),a) by CAT_1:28;
then <:(term a),(id a):> * (pr2 (([1] C),a)) = <:(pr1 (([1] C),a)),(pr2 (([1] C),a)):> by A2, A3, A1, Th27;
hence id (([1] C) [x] a) = (lambda' a) * (lambda a) by Th26; :: thesis: ( (rho a) * (rho' a) = id a & (rho' a) * (rho a) = id (a [x] ([1] C)) )
thus id a = (rho a) * (rho' a) by A2, Def11; :: thesis: (rho' a) * (rho a) = id (a [x] ([1] C))
A4: (term a) * (pr1 (a,([1] C))) = pr2 (a,([1] C)) by Th14;
A5: Hom ((a [x] ([1] C)),a) <> {} by Th21;
then (id a) * (pr1 (a,([1] C))) = pr1 (a,([1] C)) by CAT_1:28;
then <:(id a),(term a):> * (pr1 (a,([1] C))) = <:(pr1 (a,([1] C))),(pr2 (a,([1] C))):> by A2, A5, A4, Th27;
hence (rho' a) * (rho a) = id (a [x] ([1] C)) by Th26; :: thesis: verum