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 Th19, Th28; :: according to CAT_4:def 1 :: thesis: ex f being Morphism of a,a [x] ([1] C) ex f9 being Morphism of a [x] ([1] C),a st
( f * f9 = id (a [x] ([1] C)) & f9 * f = id a )
take rho' a ; :: thesis: ex f9 being Morphism of a [x] ([1] C),a st
( (rho' a) * f9 = id (a [x] ([1] C)) & f9 * (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 Th29; :: thesis: verum
end;
thus ( Hom (a,(([1] C) [x] a)) <> {} & Hom ((([1] C) [x] a),a) <> {} ) by Th19, Th28; :: according to CAT_4:def 1 :: thesis: ex f being Morphism of a,([1] C) [x] a ex f9 being Morphism of ([1] C) [x] a,a st
( f * f9 = id (([1] C) [x] a) & f9 * f = id a )
take lambda' a ; :: thesis: ex f9 being Morphism of ([1] C) [x] a,a st
( (lambda' a) * f9 = id (([1] C) [x] a) & f9 * (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 Th29; :: thesis: verum