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:56;
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:57;
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:57;
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