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:27;
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 1 :: 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:29;
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 1 :: 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:29;
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