let C be Cartesian_category; :: thesis: for a, b, c being Object of holds (a [x] b) [x] c,a [x] (b [x] c) are_isomorphic
let a, b, c be Object of ; :: thesis: (a [x] b) [x] c,a [x] (b [x] c) are_isomorphic
thus ( Hom ((a [x] b) [x] c),(a [x] (b [x] c)) <> {} & Hom (a [x] (b [x] c)),((a [x] b) [x] c) <> {} ) by Th38; :: according to CAT_4:def 2 :: thesis: ex f being Morphism of (a [x] b) [x] c,a [x] (b [x] c) ex f' being Morphism of a [x] (b [x] c),(a [x] b) [x] c st
( f * f' = id (a [x] (b [x] c)) & f' * f = id ((a [x] b) [x] c) )
take Alpha a,b,c ; :: thesis: ex f' being Morphism of a [x] (b [x] c),(a [x] b) [x] c st
( (Alpha a,b,c) * f' = id (a [x] (b [x] c)) & f' * (Alpha a,b,c) = id ((a [x] b) [x] c) )
take Alpha' a,b,c ; :: thesis: ( (Alpha a,b,c) * (Alpha' a,b,c) = id (a [x] (b [x] c)) & (Alpha' a,b,c) * (Alpha a,b,c) = id ((a [x] b) [x] c) )
thus ( (Alpha a,b,c) * (Alpha' a,b,c) = id (a [x] (b [x] c)) & (Alpha' a,b,c) * (Alpha a,b,c) = id ((a [x] b) [x] c) ) by Th39; :: thesis: verum