let C be Cocartesian_category; 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; ( 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
a,([0] C) + a are_isomorphic proof
thus A3:
Hom a,
(a + ([0] C)) <> {}
by Th66;
CAT_4:def 2 ( 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;
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);
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)$];
( 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;
verum
end;
thus A5:
Hom a,(([0] C) + a) <> {}
by Th66; CAT_4:def 2 ( 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; 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; 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)$]; ( 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; verum