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: ( Hom a,([1] C) <> {} & Hom a,a <> {} ) by Th15, CAT_1:56;
A2: Hom (([1] C) [x] a),a <> {} by Th21;
then ( (id a) * (pr2 ([1] C),a) = pr2 ([1] C),a & (term a) * (pr2 ([1] C),a) = pr1 ([1] C),a & Hom (([1] C) [x] a),([1] C) <> {} ) by Th14, Th21, CAT_1:57;
then A3: <:(term a),(id a):> * (pr2 ([1] C),a) = <:(pr1 ([1] C),a),(pr2 ([1] C),a):> by A1, A2, Th27;
thus id a = (lambda a) * (lambda' a) by A1, 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)) )
thus id (([1] C) [x] a) = (lambda' a) * (lambda a) by A3, Th26; :: thesis: ( (rho a) * (rho' a) = id a & (rho' a) * (rho a) = id (a [x] ([1] C)) )
A4: Hom (a [x] ([1] C)),a <> {} by Th21;
then ( (id a) * (pr1 a,([1] C)) = pr1 a,([1] C) & (term a) * (pr1 a,([1] C)) = pr2 a,([1] C) & Hom (a [x] ([1] C)),([1] C) <> {} ) by Th14, Th21, CAT_1:57;
then A5: <:(id a),(term a):> * (pr1 a,([1] C)) = <:(pr1 a,([1] C)),(pr2 a,([1] C)):> by A1, A4, Th27;
thus id a = (rho a) * (rho' a) by A1, Def11; :: thesis: (rho' a) * (rho a) = id (a [x] ([1] C))
thus (rho' a) * (rho a) = id (a [x] ([1] C)) by A5, Th26; :: thesis: verum