let C be Cocartesian_category; :: thesis: for a being Object of C holds
( a,a + ([[0]] C) are_isomorphic & a,([[0]] C) + a are_isomorphic )
let a be Object of C; :: thesis: ( a,a + ([[0]] C) are_isomorphic & a,([[0]] C) + a are_isomorphic )
A1: (in2 ([[0]] C),a) * (init a) = in1 ([[0]] C),a by Th59;
A2: ( Hom ([[0]] C),a <> {} & Hom a,a <> {} ) by Th60, CAT_1:56;
thus a,a + ([[0]] C) are_isomorphic :: thesis: a,([[0]] C) + a are_isomorphic

proof

thus A3: Hom a,(a + ([[0]] C)) <> {} by Th66; :: according to CAT_4:def 2 :: thesis: ( Hom (a + ([[0]] C)),a <> {} & ex f being Morphism of a,a + ([[0]] C) ex f9 being Morphism of a + ([[0]] C),a st
( f * f9 = id (a + ([[0]] C)) & f9 * f = id a ) )
thus Hom (a + ([[0]] C)),a <> {} by A2, Th70; :: thesis: ex f being Morphism of a,a + ([[0]] C) ex f9 being Morphism of a + ([[0]] C),a st
( f * f9 = id (a + ([[0]] C)) & f9 * f = id a )
take g = in1 a,([[0]] C); :: thesis: ex f9 being Morphism of a + ([[0]] C),a st
( g * f9 = id (a + ([[0]] C)) & f9 * g = id a )
take f = [$(id a),(init a)$]; :: thesis: ( g * f = id (a + ([[0]] C)) & f * g = id a )
A4: (in1 a,([[0]] C)) * (init a) = in2 a,([[0]] C) by Th59;
(in1 a,([[0]] C)) * (id a) = in1 a,([[0]] C) by A3, CAT_1:58;
then g * f = [$(in1 a,([[0]] C)),(in2 a,([[0]] C))$] by A2, A3, A4, Th72;
hence ( g * f = id (a + ([[0]] C)) & f * g = id a ) by A2, Def29, Th71; :: thesis: verum

end;

thus A5: Hom a,(([[0]] C) + a) <> {} by Th66; :: according to CAT_4:def 2 :: thesis: ( Hom (([[0]] C) + a),a <> {} & ex f being Morphism of a,([[0]] C) + a ex f9 being Morphism of ([[0]] C) + a,a st
( f * f9 = id (([[0]] C) + a) & f9 * f = id a ) )
thus Hom (([[0]] C) + a),a <> {} by A2, Th70; :: thesis: ex f being Morphism of a,([[0]] C) + a ex f9 being Morphism of ([[0]] C) + a,a st
( f * f9 = id (([[0]] C) + a) & f9 * f = id a )
take g = in2 ([[0]] C),a; :: thesis: ex f9 being Morphism of ([[0]] C) + a,a st
( g * f9 = id (([[0]] C) + a) & f9 * g = id a )
take f = [$(init a),(id a)$]; :: thesis: ( g * f = id (([[0]] C) + a) & f * g = id a )
(in2 ([[0]] C),a) * (id a) = in2 ([[0]] C),a by A5, CAT_1:58;
then g * f = [$(in1 ([[0]] C),a),(in2 ([[0]] C),a)$] by A2, A5, A1, Th72;
hence ( g * f = id (([[0]] C) + a) & f * g = id a ) by A2, Def29, Th71; :: thesis: verum