let C be Cocartesian_category; :: thesis: for a being Object of C holds
( a,a + (EmptyMS C) are_isomorphic & a,(EmptyMS C) + a are_isomorphic )
let a be Object of C; :: thesis: ( a,a + (EmptyMS C) are_isomorphic & a,(EmptyMS C) + a are_isomorphic )
A1: (in2 ((EmptyMS C),a)) * (init a) = in1 ((EmptyMS C),a) by Th54;
A2: ( Hom ((EmptyMS C),a) <> {} & Hom (a,a) <> {} ) by Th55;
thus a,a + (EmptyMS C) are_isomorphic :: thesis: a,(EmptyMS C) + a are_isomorphic
proof
thus A3: Hom (a,(a + (EmptyMS C))) <> {} by Th61; :: according to CAT_4:def 1 :: thesis: ( Hom ((a + (EmptyMS C)),a) <> {} & ex f being Morphism of a,a + (EmptyMS C) ex f9 being Morphism of a + (EmptyMS C),a st
( f * f9 = id (a + (EmptyMS C)) & f9 * f = id a ) )
thus Hom ((a + (EmptyMS C)),a) <> {} by A2, Th65; :: thesis: ex f being Morphism of a,a + (EmptyMS C) ex f9 being Morphism of a + (EmptyMS C),a st
( f * f9 = id (a + (EmptyMS C)) & f9 * f = id a )
take g = in1 (a,(EmptyMS C)); :: thesis: ex f9 being Morphism of a + (EmptyMS C),a st
( g * f9 = id (a + (EmptyMS C)) & f9 * g = id a )
take f = [$(id a),(init a)$]; :: thesis: ( g * f = id (a + (EmptyMS C)) & f * g = id a )
A4: (in1 (a,(EmptyMS C))) * (init a) = in2 (a,(EmptyMS C)) by Th54;
(in1 (a,(EmptyMS C))) * (id a) = in1 (a,(EmptyMS C)) by A3, CAT_1:29;
then g * f = [$(in1 (a,(EmptyMS C))),(in2 (a,(EmptyMS C)))$] by A2, A3, A4, Th67;
hence ( g * f = id (a + (EmptyMS C)) & f * g = id a ) by A2, Def28, Th66; :: thesis: verum
end;
thus A5: Hom (a,((EmptyMS C) + a)) <> {} by Th61; :: according to CAT_4:def 1 :: thesis: ( Hom (((EmptyMS C) + a),a) <> {} & ex f being Morphism of a,(EmptyMS C) + a ex f9 being Morphism of (EmptyMS C) + a,a st
( f * f9 = id ((EmptyMS C) + a) & f9 * f = id a ) )
thus Hom (((EmptyMS C) + a),a) <> {} by A2, Th65; :: thesis: ex f being Morphism of a,(EmptyMS C) + a ex f9 being Morphism of (EmptyMS C) + a,a st
( f * f9 = id ((EmptyMS C) + a) & f9 * f = id a )
take g = in2 ((EmptyMS C),a); :: thesis: ex f9 being Morphism of (EmptyMS C) + a,a st
( g * f9 = id ((EmptyMS C) + a) & f9 * g = id a )
take f = [$(init a),(id a)$]; :: thesis: ( g * f = id ((EmptyMS C) + a) & f * g = id a )
(in2 ((EmptyMS C),a)) * (id a) = in2 ((EmptyMS C),a) by A5, CAT_1:29;
then g * f = [$(in1 ((EmptyMS C),a)),(in2 ((EmptyMS C),a))$] by A2, A5, A1, Th67;
hence ( g * f = id ((EmptyMS C) + a) & f * g = id a ) by A2, Def28, Th66; :: thesis: verum