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 Th66;
A2: Hom b,(b + c) <> {} by Th66;
then A3: Hom b,(a + (b + c)) <> {} by A1, CAT_1:52;
A4: Hom a,(a + (b + c)) <> {} by Th66;
then A5: Hom (a + b),(a + (b + c)) <> {} by A3, Th70;
A6: Hom c,(b + c) <> {} by Th66;
then A7: Hom c,(a + (b + c)) <> {} by A1, CAT_1:52;
hence A8: Hom ((a + b) + c),(a + (b + c)) <> {} by A5, Th70; :: according to CAT_4:def 2 :: 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 Th66;
A10: Hom b,(a + b) <> {} by Th66;
then A11: Hom b,((a + b) + c) <> {} by A9, CAT_1:52;
A12: Hom c,((a + b) + c) <> {} by Th66;
then A13: Hom (b + c),((a + b) + c) <> {} by A11, Th70;
A14: Hom a,(a + b) <> {} by Th66;
then A15: Hom a,((a + b) + c) <> {} by A9, CAT_1:52;
hence A16: Hom (a + (b + c)),((a + b) + c) <> {} by A13, Th70; :: 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:54
.= [$(in1 a,(b + c)),((in2 a,(b + c)) * (in1 b,c))$] * (in2 a,b) by A7, A5, Def29
.= (in2 a,(b + c)) * (in1 b,c) by A3, A4, Def29 ;
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, Th72
.= [$((in2 a,(b + c)) * (in1 b,c)),((in2 a,(b + c)) * (in2 b,c))$] by A7, A5, Def29
.= (in2 a,(b + c)) * [$(in1 b,c),(in2 b,c)$] by A2, A1, A6, Th72
.= (in2 a,(b + c)) * (id (b + c)) by Th71
.= in2 a,(b + c) by A1, CAT_1:58 ;
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:54
.= [$((in1 (a + b),c) * (in2 a,b)),(in2 (a + b),c)$] * (in1 b,c) by A15, A13, Def29
.= (in1 (a + b),c) * (in2 a,b) by A11, A12, Def29 ;
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, Th72
.= [$((in1 (a + b),c) * (in1 a,b)),((in1 (a + b),c) * (in2 a,b))$] by A15, A13, Def29
.= (in1 (a + b),c) * [$(in1 a,b),(in2 a,b)$] by A14, A9, A10, Th72
.= (in1 (a + b),c) * (id (a + b)) by Th71
.= in1 (a + b),c by A9, CAT_1:58 ;
g * ((in1 (a + b),c) * (in1 a,b)) = (g * (in1 (a + b),c)) * (in1 a,b) by A8, A14, A9, CAT_1:54
.= [$(in1 a,(b + c)),((in2 a,(b + c)) * (in1 b,c))$] * (in1 a,b) by A7, A5, Def29
.= in1 a,(b + c) by A3, A4, Def29 ;
hence g * f = [$(in1 a,(b + c)),(in2 a,(b + c))$] by A8, A15, A13, A17, Th72
.= id (a + (b + c)) by Th71 ;
:: 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:54
.= [$((in1 (a + b),c) * (in2 a,b)),(in2 (a + b),c)$] * (in2 b,c) by A15, A13, Def29
.= in2 (a + b),c by A11, A12, Def29 ;
hence f * g = [$(in1 (a + b),c),(in2 (a + b),c)$] by A7, A5, A16, A18, Th72
.= id ((a + b) + c) by Th71 ;
:: thesis: verum