let C be Cartesian_category; :: thesis: for a, b, c being Object of C holds (a [x] b) [x] c,a [x] (b [x] c) are_isomorphic
let a, b, c be Object of C; :: 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 Th36; :: according to CAT_4:def 1 :: thesis: ex f being Morphism of (a [x] b) [x] c,a [x] (b [x] c) ex f9 being Morphism of a [x] (b [x] c),(a [x] b) [x] c st
( f * f9 = id (a [x] (b [x] c)) & f9 * f = id ((a [x] b) [x] c) )
take Alpha (a,b,c) ; :: thesis: ex f9 being Morphism of a [x] (b [x] c),(a [x] b) [x] c st
( (Alpha (a,b,c)) * f9 = id (a [x] (b [x] c)) & f9 * (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 Th37; :: thesis: verum