let C be Cartesian_category; :: thesis: for a being Object of C holds
( a,a [x] ([1] C) are_isomorphic & a,([1] C) [x] a are_isomorphic )
let a be Object of C; :: thesis: ( a,a [x] ([1] C) are_isomorphic & a,([1] C) [x] a are_isomorphic )
thus a,a [x] ([1] C) are_isomorphic :: thesis: a,([1] C) [x] a are_isomorphic

proof

thus ( Hom a,(a [x] ([1] C)) <> {} & Hom (a [x] ([1] C)),a <> {} ) by Th21, Th30; :: according to CAT_4:def 2 :: thesis: ex f being Morphism of a,a [x] ([1] C) ex f' being Morphism of a [x] ([1] C),a st
( f * f' = id (a [x] ([1] C)) & f' * f = id a )
take rho' a ; :: thesis: ex f' being Morphism of a [x] ([1] C),a st
( (rho' a) * f' = id (a [x] ([1] C)) & f' * (rho' a) = id a )
take rho a ; :: thesis: ( (rho' a) * (rho a) = id (a [x] ([1] C)) & (rho a) * (rho' a) = id a )
thus ( (rho' a) * (rho a) = id (a [x] ([1] C)) & (rho a) * (rho' a) = id a ) by Th31; :: thesis: verum

end;

thus ( Hom a,(([1] C) [x] a) <> {} & Hom (([1] C) [x] a),a <> {} ) by Th21, Th30; :: according to CAT_4:def 2 :: thesis: ex f being Morphism of a,([1] C) [x] a ex f' being Morphism of ([1] C) [x] a,a st
( f * f' = id (([1] C) [x] a) & f' * f = id a )
take lambda' a ; :: thesis: ex f' being Morphism of ([1] C) [x] a,a st
( (lambda' a) * f' = id (([1] C) [x] a) & f' * (lambda' a) = id a )
take lambda a ; :: thesis: ( (lambda' a) * (lambda a) = id (([1] C) [x] a) & (lambda a) * (lambda' a) = id a )
thus ( (lambda' a) * (lambda a) = id (([1] C) [x] a) & (lambda a) * (lambda' a) = id a ) by Th31; :: thesis: verum