let C be Cocartesian_category; :: thesis: for a, b being Object of holds a + b,b + a are_isomorphic
let a, b be Object of ; :: 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 2 :: thesis: ( Hom (b + a),(a + b) <> {} & ex f being Morphism of a + b,b + a ex f' being Morphism of b + a,a + b st
( f * f' = id (b + a) & f' * 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 f' being Morphism of b + a,a + b st
( f * f' = id (b + a) & f' * f = id (a + b) )
take f' = [$(in2 b,a),(in1 b,a)$]; :: thesis: ex f' being Morphism of b + a,a + b st
( f' * f' = id (b + a) & f' * f' = id (a + b) )
take f = [$(in2 a,b),(in1 a,b)$]; :: thesis: ( f' * f = id (b + a) & f * f' = id (a + b) )
thus f' * f = [$(f' * (in2 a,b)),(f' * (in1 a,b))$] by A2, A3, Th72
.= [$(in1 b,a),(f' * (in1 a,b))$] by A1, Def29
.= [$(in1 b,a),(in2 b,a)$] by A1, Def29
.= id (b + a) by Th71 ; :: thesis: f * f' = id (a + b)
thus f * f' = [$(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