let C be Cocartesian_category; :: thesis: for a, b being Object of C holds a + b,b + a are_isomorphic
let a, b be Object of C; :: thesis: a + b,b + a are_isomorphic
A1: ( Hom (a,(b + a)) <> {} & Hom (b,(b + a)) <> {} ) by Th66;
hence A2: Hom ((a + b),(b + a)) <> {} by Th70; :: according to CAT_4:def 1 :: thesis: ( Hom ((b + a),(a + b)) <> {} & ex f being Morphism of a + b,b + a ex f9 being Morphism of b + a,a + b st
( f * f9 = id (b + a) & f9 * f = id (a + b) ) )
A3: ( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} ) by Th66;
hence A4: Hom ((b + a),(a + b)) <> {} by Th70; :: thesis: ex f being Morphism of a + b,b + a ex f9 being Morphism of b + a,a + b st
( f * f9 = id (b + a) & f9 * f = id (a + b) )
take f9 = [$(in2 (b,a)),(in1 (b,a))$]; :: thesis: ex f9 being Morphism of b + a,a + b st
( f9 * f9 = id (b + a) & f9 * f9 = id (a + b) )
take f = [$(in2 (a,b)),(in1 (a,b))$]; :: thesis: ( f9 * f = id (b + a) & f * f9 = id (a + b) )
thus f9 * f = [$(f9 * (in2 (a,b))),(f9 * (in1 (a,b)))$] by A2, A3, Th72
.= [$(in1 (b,a)),(f9 * (in1 (a,b)))$] by A1, Def29
.= [$(in1 (b,a)),(in2 (b,a))$] by A1, Def29
.= id (b + a) by Th71 ; :: thesis: f * f9 = id (a + b)
thus f * f9 = [$(f * (in2 (b,a))),(f * (in1 (b,a)))$] by A1, A4, Th72
.= [$(in1 (a,b)),(f * (in1 (b,a)))$] by A3, Def29
.= [$(in1 (a,b)),(in2 (a,b))$] by A3, Def29
.= id (a + b) by Th71 ; :: thesis: verum