let C be Cocartesian_category; :: thesis: for a, b, c being Object of C holds (a + b) + c,a + (b + c) are_isomorphic
let a, b, c be Object of C; :: thesis: (a + b) + c,a + (b + c) are_isomorphic
set k = [$((in1 ((a + b),c)) * (in2 (a,b))),(in2 ((a + b),c))$];
set l = [$(in1 (a,(b + c))),((in2 (a,(b + c))) * (in1 (b,c)))$];
A1: Hom ((b + c),(a + (b + c))) <> {} by Th61;
A2: Hom (b,(b + c)) <> {} by Th61;
then A3: Hom (b,(a + (b + c))) <> {} by A1, CAT_1:24;
A4: Hom (a,(a + (b + c))) <> {} by Th61;
then A5: Hom ((a + b),(a + (b + c))) <> {} by A3, Th65;
A6: Hom (c,(b + c)) <> {} by Th61;
then A7: Hom (c,(a + (b + c))) <> {} by A1, CAT_1:24;
hence A8: Hom (((a + b) + c),(a + (b + c))) <> {} by A5, Th65; :: according to CAT_4:def 1 :: thesis: ( Hom ((a + (b + c)),((a + b) + c)) <> {} & ex f being Morphism of (a + b) + c,a + (b + c) ex f9 being Morphism of a + (b + c),(a + b) + c st
( f * f9 = id (a + (b + c)) & f9 * f = id ((a + b) + c) ) )
A9: Hom ((a + b),((a + b) + c)) <> {} by Th61;
A10: Hom (b,(a + b)) <> {} by Th61;
then A11: Hom (b,((a + b) + c)) <> {} by A9, CAT_1:24;
A12: Hom (c,((a + b) + c)) <> {} by Th61;
then A13: Hom ((b + c),((a + b) + c)) <> {} by A11, Th65;
A14: Hom (a,(a + b)) <> {} by Th61;
then A15: Hom (a,((a + b) + c)) <> {} by A9, CAT_1:24;
hence A16: Hom ((a + (b + c)),((a + b) + c)) <> {} by A13, Th65; :: thesis: ex f being Morphism of (a + b) + c,a + (b + c) ex f9 being Morphism of a + (b + c),(a + b) + c st
( f * f9 = id (a + (b + c)) & f9 * f = id ((a + b) + c) )
take g = [$[$(in1 (a,(b + c))),((in2 (a,(b + c))) * (in1 (b,c)))$],((in2 (a,(b + c))) * (in2 (b,c)))$]; :: thesis: ex f9 being Morphism of a + (b + c),(a + b) + c st
( g * f9 = id (a + (b + c)) & f9 * g = id ((a + b) + c) )
g * ((in1 ((a + b),c)) * (in2 (a,b))) = (g * (in1 ((a + b),c))) * (in2 (a,b)) by A8, A9, A10, CAT_1:25
.= [$(in1 (a,(b + c))),((in2 (a,(b + c))) * (in1 (b,c)))$] * (in2 (a,b)) by A7, A5, Def28
.= (in2 (a,(b + c))) * (in1 (b,c)) by A3, A4, Def28 ;
then A17: g * [$((in1 ((a + b),c)) * (in2 (a,b))),(in2 ((a + b),c))$] = [$((in2 (a,(b + c))) * (in1 (b,c))),(g * (in2 ((a + b),c)))$] by A8, A11, A12, Th67
.= [$((in2 (a,(b + c))) * (in1 (b,c))),((in2 (a,(b + c))) * (in2 (b,c)))$] by A7, A5, Def28
.= (in2 (a,(b + c))) * [$(in1 (b,c)),(in2 (b,c))$] by A2, A1, A6, Th67
.= (in2 (a,(b + c))) * (id (b + c)) by Th66
.= in2 (a,(b + c)) by A1, CAT_1:29 ;
take f = [$((in1 ((a + b),c)) * (in1 (a,b))),[$((in1 ((a + b),c)) * (in2 (a,b))),(in2 ((a + b),c))$]$]; :: thesis: ( g * f = id (a + (b + c)) & f * g = id ((a + b) + c) )
f * ((in2 (a,(b + c))) * (in1 (b,c))) = (f * (in2 (a,(b + c)))) * (in1 (b,c)) by A2, A1, A16, CAT_1:25
.= [$((in1 ((a + b),c)) * (in2 (a,b))),(in2 ((a + b),c))$] * (in1 (b,c)) by A15, A13, Def28
.= (in1 ((a + b),c)) * (in2 (a,b)) by A11, A12, Def28 ;
then A18: f * [$(in1 (a,(b + c))),((in2 (a,(b + c))) * (in1 (b,c)))$] = [$(f * (in1 (a,(b + c)))),((in1 ((a + b),c)) * (in2 (a,b)))$] by A3, A4, A16, Th67
.= [$((in1 ((a + b),c)) * (in1 (a,b))),((in1 ((a + b),c)) * (in2 (a,b)))$] by A15, A13, Def28
.= (in1 ((a + b),c)) * [$(in1 (a,b)),(in2 (a,b))$] by A14, A9, A10, Th67
.= (in1 ((a + b),c)) * (id (a + b)) by Th66
.= in1 ((a + b),c) by A9, CAT_1:29 ;
g * ((in1 ((a + b),c)) * (in1 (a,b))) = (g * (in1 ((a + b),c))) * (in1 (a,b)) by A8, A14, A9, CAT_1:25
.= [$(in1 (a,(b + c))),((in2 (a,(b + c))) * (in1 (b,c)))$] * (in1 (a,b)) by A7, A5, Def28
.= in1 (a,(b + c)) by A3, A4, Def28 ;
hence g * f = [$(in1 (a,(b + c))),(in2 (a,(b + c)))$] by A8, A15, A13, A17, Th67
.= id (a + (b + c)) by Th66 ;
:: thesis: f * g = id ((a + b) + c)
f * ((in2 (a,(b + c))) * (in2 (b,c))) = (f * (in2 (a,(b + c)))) * (in2 (b,c)) by A1, A6, A16, CAT_1:25
.= [$((in1 ((a + b),c)) * (in2 (a,b))),(in2 ((a + b),c))$] * (in2 (b,c)) by A15, A13, Def28
.= in2 ((a + b),c) by A11, A12, Def28 ;
hence f * g = [$(in1 ((a + b),c)),(in2 ((a + b),c))$] by A7, A5, A16, A18, Th67
.= id ((a + b) + c) by Th66 ;
:: thesis: verum