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:
( 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 A2:
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 f' being Morphism of a + ([0] C),a st
( f * f' = id (a + ([0] C)) & f' * f = id a ) )
thus
Hom (a + ([0] C)),
a <> {}
by A1, Th70;
:: thesis: ex f being Morphism of a,a + ([0] C) ex f' being Morphism of a + ([0] C),a st
( f * f' = id (a + ([0] C)) & f' * f = id a )
take g =
in1 a,
([0] C);
:: thesis: ex f' being Morphism of a + ([0] C),a st
( g * f' = id (a + ([0] C)) & f' * g = id a )
take f =
[$(id a),(init a)$];
:: thesis: ( g * f = id (a + ([0] C)) & f * g = id a )
(
(in1 a,([0] C)) * (id a) = in1 a,
([0] C) &
(in1 a,([0] C)) * (init a) = in2 a,
([0] C) &
Hom ([0] C),
(a + ([0] C)) <> {} )
by A2, Th59, Th66, CAT_1:58;
then
g * f = [$(in1 a,([0] C)),(in2 a,([0] C))$]
by A1, A2, Th72;
hence
(
g * f = id (a + ([0] C)) &
f * g = id a )
by A1, Def29, Th71;
:: thesis: verum
end;
thus A3:
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 f' being Morphism of ([0] C) + a,a st
( f * f' = id (([0] C) + a) & f' * f = id a ) )
thus
Hom (([0] C) + a),a <> {}
by A1, Th70; :: thesis: ex f being Morphism of a,([0] C) + a ex f' being Morphism of ([0] C) + a,a st
( f * f' = id (([0] C) + a) & f' * f = id a )
take g = in2 ([0] C),a; :: thesis: ex f' being Morphism of ([0] C) + a,a st
( g * f' = id (([0] C) + a) & f' * 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 & (in2 ([0] C),a) * (init a) = in1 ([0] C),a & Hom ([0] C),(([0] C) + a) <> {} )
by A3, Th59, Th66, CAT_1:58;
then
g * f = [$(in1 ([0] C),a),(in2 ([0] C),a)$]
by A1, A3, Th72;
hence
( g * f = id (([0] C) + a) & f * g = id a )
by A1, Def29, Th71; :: thesis: verum