:: CAT_4 semantic presentation begin definition let C be Category; let a, b be Object of C; redefine pred a,b are_isomorphic means :: CAT_4:def 1 ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st ( f * f9 = id b & f9 * f = id a ) ); compatibility ( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st ( f * f9 = id b & f9 * f = id a ) ) ) by CAT_1:48; end; :: deftheorem defines are_isomorphic CAT_4:def_1_:_ for C being Category for a, b being Object of C holds ( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st ( f * f9 = id b & f9 * f = id a ) ) ); begin definition let C be Category; attrC is with_finite_product means :: CAT_4:def 2 for I being finite set for F being Function of I, the carrier of C ex a being Object of C ex F9 being Projections_family of a,I st ( cods F9 = F & a is_a_product_wrt F9 ); end; :: deftheorem defines with_finite_product CAT_4:def_2_:_ for C being Category holds ( C is with_finite_product iff for I being finite set for F being Function of I, the carrier of C ex a being Object of C ex F9 being Projections_family of a,I st ( cods F9 = F & a is_a_product_wrt F9 ) ); theorem Th1: :: CAT_4:1 for C being Category holds ( C is with_finite_product iff ( ex a being Object of C st a is terminal & ( for a, b being Object of C ex c being Object of C ex p1, p2 being Morphism of C st ( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 ) ) ) ) proof let C be Category; ::_thesis: ( C is with_finite_product iff ( ex a being Object of C st a is terminal & ( for a, b being Object of C ex c being Object of C ex p1, p2 being Morphism of C st ( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 ) ) ) ) thus ( C is with_finite_product implies ( ex a being Object of C st a is terminal & ( for a, b being Object of C ex c being Object of C ex p1, p2 being Morphism of C st ( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 ) ) ) ) ::_thesis: ( ex a being Object of C st a is terminal & ( for a, b being Object of C ex c being Object of C ex p1, p2 being Morphism of C st ( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 ) ) implies C is with_finite_product ) proof reconsider F = {} as Function of {}, the carrier of C by RELSET_1:12; assume A1: for I being finite set for F being Function of I, the carrier of C ex a being Object of C ex F9 being Projections_family of a,I st ( cods F9 = F & a is_a_product_wrt F9 ) ; :: according to CAT_4:def_2 ::_thesis: ( ex a being Object of C st a is terminal & ( for a, b being Object of C ex c being Object of C ex p1, p2 being Morphism of C st ( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 ) ) ) then consider a being Object of C, F9 being Projections_family of a, {} such that cods F9 = F and A2: a is_a_product_wrt F9 ; thus ex a being Object of C st a is terminal by A2, CAT_3:50; ::_thesis: for a, b being Object of C ex c being Object of C ex p1, p2 being Morphism of C st ( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 ) let a, b be Object of C; ::_thesis: ex c being Object of C ex p1, p2 being Morphism of C st ( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 ) set F = (0,1) --> (a,b); consider c being Object of C, F9 being Projections_family of c,{0,1} such that A3: cods F9 = (0,1) --> (a,b) and A4: c is_a_product_wrt F9 by A1; take c ; ::_thesis: ex p1, p2 being Morphism of C st ( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 ) take p1 = F9 /. 0; ::_thesis: ex p2 being Morphism of C st ( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 ) take p2 = F9 /. 1; ::_thesis: ( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 ) A5: 1 in {0,1} by TARSKI:def_2; then A6: p2 = F9 . 1 by FUNCT_2:def_13; A7: 0 in {0,1} by TARSKI:def_2; hence ( dom p1 = c & dom p2 = c ) by A5, CAT_3:41; ::_thesis: ( cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 ) ( ((0,1) --> (a,b)) /. 0 = a & ((0,1) --> (a,b)) /. 1 = b ) by CAT_3:3; hence ( cod p1 = a & cod p2 = b ) by A3, A7, A5, CAT_3:def_2; ::_thesis: c is_a_product_wrt p1,p2 ( dom F9 = {0,1} & p1 = F9 . 0 ) by A7, FUNCT_2:def_1, FUNCT_2:def_13; then F9 = (0,1) --> (p1,p2) by A6, FUNCT_4:66; hence c is_a_product_wrt p1,p2 by A4, CAT_3:54; ::_thesis: verum end; given a being Object of C such that A8: a is terminal ; ::_thesis: ( ex a, b being Object of C st for c being Object of C for p1, p2 being Morphism of C holds ( not dom p1 = c or not dom p2 = c or not cod p1 = a or not cod p2 = b or not c is_a_product_wrt p1,p2 ) or C is with_finite_product ) defpred S1[ Nat] means for I being finite set for F being Function of I, the carrier of C st card I = \$1 holds ex a being Object of C ex F9 being Projections_family of a,I st ( cods F9 = F & a is_a_product_wrt F9 ); assume A9: for a, b being Object of C ex c being Object of C ex p1, p2 being Morphism of C st ( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 ) ; ::_thesis: C is with_finite_product A10: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A11: S1[n] ; ::_thesis: S1[n + 1] let I be finite set ; ::_thesis: for F being Function of I, the carrier of C st card I = n + 1 holds ex a being Object of C ex F9 being Projections_family of a,I st ( cods F9 = F & a is_a_product_wrt F9 ) let F be Function of I, the carrier of C; ::_thesis: ( card I = n + 1 implies ex a being Object of C ex F9 being Projections_family of a,I st ( cods F9 = F & a is_a_product_wrt F9 ) ) assume A12: card I = n + 1 ; ::_thesis: ex a being Object of C ex F9 being Projections_family of a,I st ( cods F9 = F & a is_a_product_wrt F9 ) set x = the Element of I; reconsider Ix = I \ { the Element of I} as finite set ; reconsider sx = { the Element of I} as finite set ; reconsider G = F | (I \ { the Element of I}) as Function of (I \ { the Element of I}), the carrier of C by FUNCT_2:32; card Ix = (card I) - (card sx) by CARD_2:44, A12, CARD_1:27, ZFMISC_1:31 .= (card I) - 1 by CARD_1:30 .= n by A12, XCMPLX_1:26 ; then consider a being Object of C, G9 being Projections_family of a,I \ { the Element of I} such that A13: cods G9 = G and A14: a is_a_product_wrt G9 by A11; consider c being Object of C, p1, p2 being Morphism of C such that A15: dom p1 = c and A16: dom p2 = c and A17: cod p1 = a and A18: cod p2 = F /. the Element of I and A19: c is_a_product_wrt p1,p2 by A9; set F9 = (G9 * p1) +* ( the Element of I .--> p2); A20: dom ({ the Element of I} --> p2) = { the Element of I} by FUNCT_2:def_1; rng ((G9 * p1) +* ( the Element of I .--> p2)) c= (rng (G9 * p1)) \/ (rng ( the Element of I .--> p2)) by FUNCT_4:17; then A21: rng ((G9 * p1) +* ( the Element of I .--> p2)) c= the carrier' of C by XBOOLE_1:1; dom (G9 * p1) = I \ { the Element of I} by FUNCT_2:def_1; then A22: (dom (G9 * p1)) \/ (dom ( the Element of I .--> p2)) = I \/ { the Element of I} by A20, XBOOLE_1:39 .= I by A12, CARD_1:27, ZFMISC_1:40 ; then dom ((G9 * p1) +* ( the Element of I .--> p2)) = I by FUNCT_4:def_1; then reconsider F9 = (G9 * p1) +* ( the Element of I .--> p2) as Function of I, the carrier' of C by A21, FUNCT_2:def_1, RELSET_1:4; A23: doms G9 = (I \ { the Element of I}) --> a by CAT_3:def_13; now__::_thesis:_for_y_being_set_st_y_in_I_holds_ (doms_F9)_._y_=_(I_-->_c)_._y let y be set ; ::_thesis: ( y in I implies (doms F9) . y = (I --> c) . y ) assume A24: y in I ; ::_thesis: (doms F9) . y = (I --> c) . y now__::_thesis:_(I_-->_c)_._y_=_(doms_F9)_/._y percases ( y = the Element of I or y <> the Element of I ) ; suppose y = the Element of I ; ::_thesis: (I --> c) . y = (doms F9) /. y then A25: y in { the Element of I} by TARSKI:def_1; F9 /. y = F9 . y by A24, FUNCT_2:def_13 .= ( the Element of I .--> p2) . y by A20, A25, FUNCT_4:13 .= p2 by A25, FUNCOP_1:7 ; hence (I --> c) . y = dom (F9 /. y) by A16, A24, FUNCOP_1:7 .= (doms F9) /. y by A24, CAT_3:def_1 ; ::_thesis: verum end; supposeA26: y <> the Element of I ; ::_thesis: (doms F9) /. y = (I --> c) . y then A27: not y in { the Element of I} by TARSKI:def_1; A28: y in I \ { the Element of I} by A24, A26, ZFMISC_1:56; F9 /. y = F9 . y by A24, FUNCT_2:def_13 .= (G9 * p1) . y by A20, A22, A24, A27, FUNCT_4:def_1 .= (G9 * p1) /. y by A28, FUNCT_2:def_13 ; hence (doms F9) /. y = dom ((G9 * p1) /. y) by A24, CAT_3:def_1 .= (doms (G9 * p1)) /. y by A28, CAT_3:def_1 .= ((I \ { the Element of I}) --> c) /. y by A15, A17, A23, CAT_3:16 .= c by A24, A26, ZFMISC_1:56, CAT_3:2 .= (I --> c) . y by A24, FUNCOP_1:7 ; ::_thesis: verum end; end; end; hence (doms F9) . y = (I --> c) . y by A24, FUNCT_2:def_13; ::_thesis: verum end; then reconsider F9 = F9 as Projections_family of c,I by CAT_3:def_13, FUNCT_2:12; take c ; ::_thesis: ex F9 being Projections_family of c,I st ( cods F9 = F & c is_a_product_wrt F9 ) take F9 ; ::_thesis: ( cods F9 = F & c is_a_product_wrt F9 ) B35: now__::_thesis:_for_y_being_set_st_y_in_I_holds_ (cods_F9)_/._y_=_F_/._y let y be set ; ::_thesis: ( y in I implies (cods F9) /. y = F /. y ) assume A29: y in I ; ::_thesis: (cods F9) /. y = F /. y now__::_thesis:_(cods_F9)_/._y_=_F_/._y percases ( y = the Element of I or y <> the Element of I ) ; supposeA30: y = the Element of I ; ::_thesis: (cods F9) /. y = F /. y then A31: y in { the Element of I} by TARSKI:def_1; F9 /. y = F9 . y by A29, FUNCT_2:def_13 .= ( the Element of I .--> p2) . y by A20, A31, FUNCT_4:13 .= p2 by A31, FUNCOP_1:7 ; hence (cods F9) /. y = F /. y by A18, A29, A30, CAT_3:def_2; ::_thesis: verum end; supposeA32: y <> the Element of I ; ::_thesis: (cods F9) /. y = F /. y then A33: not y in { the Element of I} by TARSKI:def_1; A34: y in I \ { the Element of I} by A29, A32, ZFMISC_1:56; F9 /. y = F9 . y by A29, FUNCT_2:def_13 .= (G9 * p1) . y by A20, A22, A29, A33, FUNCT_4:def_1 .= (G9 * p1) /. y by A34, FUNCT_2:def_13 ; hence (cods F9) /. y = cod ((G9 * p1) /. y) by A29, CAT_3:def_2 .= (cods (G9 * p1)) /. y by A34, CAT_3:def_2 .= G /. y by A13, A17, A23, CAT_3:16 .= G . y by A34, FUNCT_2:def_13 .= F . y by A29, A32, ZFMISC_1:56, FUNCT_1:49 .= F /. y by A29, FUNCT_2:def_13 ; ::_thesis: verum end; end; end; hence (cods F9) /. y = F /. y ; ::_thesis: verum end; hence cods F9 = F by CAT_3:1; ::_thesis: c is_a_product_wrt F9 thus F9 is Projections_family of c,I ; :: according to CAT_3:def_14 ::_thesis: for b1 being Element of the carrier of C for b2 being Projections_family of b1,I holds ( not cods F9 = cods b2 or ex b3 being Element of the carrier' of C st ( b3 in Hom (b1,c) & ( for b4 being Element of the carrier' of C holds ( not b4 in Hom (b1,c) or ( ( ex b5 being set st ( b5 in I & not (F9 /. b5) (*) b4 = b2 /. b5 ) or b3 = b4 ) & ( not b3 = b4 or for b5 being set holds ( not b5 in I or (F9 /. b5) (*) b4 = b2 /. b5 ) ) ) ) ) ) ) let d be Object of C; ::_thesis: for b1 being Projections_family of d,I holds ( not cods F9 = cods b1 or ex b2 being Element of the carrier' of C st ( b2 in Hom (d,c) & ( for b3 being Element of the carrier' of C holds ( not b3 in Hom (d,c) or ( ( ex b4 being set st ( b4 in I & not (F9 /. b4) (*) b3 = b1 /. b4 ) or b2 = b3 ) & ( not b2 = b3 or for b4 being set holds ( not b4 in I or (F9 /. b4) (*) b3 = b1 /. b4 ) ) ) ) ) ) ) let F99 be Projections_family of d,I; ::_thesis: ( not cods F9 = cods F99 or ex b1 being Element of the carrier' of C st ( b1 in Hom (d,c) & ( for b2 being Element of the carrier' of C holds ( not b2 in Hom (d,c) or ( ( ex b3 being set st ( b3 in I & not (F9 /. b3) (*) b2 = F99 /. b3 ) or b1 = b2 ) & ( not b1 = b2 or for b3 being set holds ( not b3 in I or (F9 /. b3) (*) b2 = F99 /. b3 ) ) ) ) ) ) ) assume A36: cods F9 = cods F99 ; ::_thesis: ex b1 being Element of the carrier' of C st ( b1 in Hom (d,c) & ( for b2 being Element of the carrier' of C holds ( not b2 in Hom (d,c) or ( ( ex b3 being set st ( b3 in I & not (F9 /. b3) (*) b2 = F99 /. b3 ) or b1 = b2 ) & ( not b1 = b2 or for b3 being set holds ( not b3 in I or (F9 /. b3) (*) b2 = F99 /. b3 ) ) ) ) ) ) reconsider G99 = F99 | (I \ { the Element of I}) as Function of (I \ { the Element of I}), the carrier' of C by FUNCT_2:32; now__::_thesis:_for_y_being_set_st_y_in_I_\_{_the_Element_of_I}_holds_ (doms_G99)_/._y_=_((I_\_{_the_Element_of_I})_-->_d)_/._y let y be set ; ::_thesis: ( y in I \ { the Element of I} implies (doms G99) /. y = ((I \ { the Element of I}) --> d) /. y ) assume A37: y in I \ { the Element of I} ; ::_thesis: (doms G99) /. y = ((I \ { the Element of I}) --> d) /. y then G99 /. y = G99 . y by FUNCT_2:def_13 .= F99 . y by A37, FUNCT_1:49 .= F99 /. y by A37, FUNCT_2:def_13 ; hence (doms G99) /. y = dom (F99 /. y) by A37, CAT_3:def_1 .= d by A37, CAT_3:41 .= ((I \ { the Element of I}) --> d) /. y by A37, CAT_3:2 ; ::_thesis: verum end; then reconsider G99 = G99 as Projections_family of d,I \ { the Element of I} by CAT_3:def_13, CAT_3:1; now__::_thesis:_for_y_being_set_st_y_in_I_\_{_the_Element_of_I}_holds_ (cods_G9)_/._y_=_(cods_G99)_/._y let y be set ; ::_thesis: ( y in I \ { the Element of I} implies (cods G9) /. y = (cods G99) /. y ) assume A38: y in I \ { the Element of I} ; ::_thesis: (cods G9) /. y = (cods G99) /. y then A39: G /. y = G . y by FUNCT_2:def_13 .= F . y by A38, FUNCT_1:49 .= F /. y by A38, FUNCT_2:def_13 ; F99 /. y = F99 . y by A38, FUNCT_2:def_13 .= G99 . y by A38, FUNCT_1:49 .= G99 /. y by A38, FUNCT_2:def_13 ; hence (cods G9) /. y = cod (G99 /. y) by A13, A36, A38, A39, CAT_3:def_2, CAT_3:1, B35 .= (cods G99) /. y by A38, CAT_3:def_2 ; ::_thesis: verum end; then consider h9 being Morphism of C such that A40: h9 in Hom (d,a) and A41: for k being Morphism of C st k in Hom (d,a) holds ( ( for y being set st y in I \ { the Element of I} holds (G9 /. y) (*) k = G99 /. y ) iff h9 = k ) by A14, CAT_3:def_14, CAT_3:1; A42: the Element of I in { the Element of I} by TARSKI:def_1; set g = F99 /. the Element of I; A43: dom (F99 /. the Element of I) = d by A12, CARD_1:27, CAT_3:41; A44: F9 /. the Element of I = F9 . the Element of I by A12, CARD_1:27, FUNCT_2:def_13 .= ( the Element of I .--> p2) . the Element of I by A20, A42, FUNCT_4:13 .= p2 by A42, FUNCOP_1:7 ; then cod p2 = (cods F9) /. the Element of I by A12, CARD_1:27, CAT_3:def_2 .= cod (F99 /. the Element of I) by A12, A36, CARD_1:27, CAT_3:def_2 ; then F99 /. the Element of I in Hom (d,(cod p2)) by A43; then consider h being Morphism of C such that A45: h in Hom (d,c) and A46: for k being Morphism of C st k in Hom (d,c) holds ( ( p1 (*) k = h9 & p2 (*) k = F99 /. the Element of I ) iff h = k ) by A17, A19, A40, CAT_3:def_15; take h ; ::_thesis: ( h in Hom (d,c) & ( for b1 being Element of the carrier' of C holds ( not b1 in Hom (d,c) or ( ( ex b2 being set st ( b2 in I & not (F9 /. b2) (*) b1 = F99 /. b2 ) or h = b1 ) & ( not h = b1 or for b2 being set holds ( not b2 in I or (F9 /. b2) (*) b1 = F99 /. b2 ) ) ) ) ) ) thus h in Hom (d,c) by A45; ::_thesis: for b1 being Element of the carrier' of C holds ( not b1 in Hom (d,c) or ( ( ex b2 being set st ( b2 in I & not (F9 /. b2) (*) b1 = F99 /. b2 ) or h = b1 ) & ( not h = b1 or for b2 being set holds ( not b2 in I or (F9 /. b2) (*) b1 = F99 /. b2 ) ) ) ) let k be Morphism of C; ::_thesis: ( not k in Hom (d,c) or ( ( ex b1 being set st ( b1 in I & not (F9 /. b1) (*) k = F99 /. b1 ) or h = k ) & ( not h = k or for b1 being set holds ( not b1 in I or (F9 /. b1) (*) k = F99 /. b1 ) ) ) ) assume A47: k in Hom (d,c) ; ::_thesis: ( ( ex b1 being set st ( b1 in I & not (F9 /. b1) (*) k = F99 /. b1 ) or h = k ) & ( not h = k or for b1 being set holds ( not b1 in I or (F9 /. b1) (*) k = F99 /. b1 ) ) ) thus ( ( for y being set st y in I holds (F9 /. y) (*) k = F99 /. y ) implies h = k ) ::_thesis: ( not h = k or for b1 being set holds ( not b1 in I or (F9 /. b1) (*) k = F99 /. b1 ) ) proof A48: cod k = c by A47, CAT_1:1; then A49: cod (p1 (*) k) = a by A15, A17, CAT_1:17; assume A50: for y being set st y in I holds (F9 /. y) (*) k = F99 /. y ; ::_thesis: h = k A51: for y being set st y in I \ { the Element of I} holds (G9 /. y) (*) (p1 (*) k) = G99 /. y proof let y be set ; ::_thesis: ( y in I \ { the Element of I} implies (G9 /. y) (*) (p1 (*) k) = G99 /. y ) assume A52: y in I \ { the Element of I} ; ::_thesis: (G9 /. y) (*) (p1 (*) k) = G99 /. y then A53: not y in { the Element of I} by XBOOLE_0:def_5; A54: F9 /. y = F9 . y by A52, FUNCT_2:def_13 .= (G9 * p1) . y by A20, A22, A52, A53, FUNCT_4:def_1 .= (G9 * p1) /. y by A52, FUNCT_2:def_13 ; dom (G9 /. y) = a by A52, CAT_3:41; hence (G9 /. y) (*) (p1 (*) k) = ((G9 /. y) (*) p1) (*) k by A15, A17, A48, CAT_1:18 .= ((G9 * p1) /. y) (*) k by A52, CAT_3:def_5 .= F99 /. y by A50, A52, A54 .= F99 . y by A52, FUNCT_2:def_13 .= G99 . y by A52, FUNCT_1:49 .= G99 /. y by A52, FUNCT_2:def_13 ; ::_thesis: verum end; dom k = d by A47, CAT_1:1; then dom (p1 (*) k) = d by A15, A48, CAT_1:17; then p1 (*) k in Hom (d,a) by A49; then A55: p1 (*) k = h9 by A41, A51; p2 (*) k = F99 /. the Element of I by A12, A44, A50, CARD_1:27; hence h = k by A46, A47, A55; ::_thesis: verum end; assume A56: h = k ; ::_thesis: for b1 being set holds ( not b1 in I or (F9 /. b1) (*) k = F99 /. b1 ) let y be set ; ::_thesis: ( not y in I or (F9 /. y) (*) k = F99 /. y ) assume A57: y in I ; ::_thesis: (F9 /. y) (*) k = F99 /. y now__::_thesis:_(F9_/._y)_(*)_k_=_F99_/._y percases ( y = the Element of I or y <> the Element of I ) ; supposeA58: y = the Element of I ; ::_thesis: (F9 /. y) (*) k = F99 /. y then A59: y in { the Element of I} by TARSKI:def_1; F9 /. y = F9 . y by A57, FUNCT_2:def_13 .= ( the Element of I .--> p2) . y by A20, A59, FUNCT_4:13 .= p2 by A59, FUNCOP_1:7 ; hence (F9 /. y) (*) k = F99 /. y by A46, A47, A56, A58; ::_thesis: verum end; supposeA60: y <> the Element of I ; ::_thesis: (F9 /. y) (*) k = F99 /. y then A61: not y in { the Element of I} by TARSKI:def_1; A62: cod k = c by A47, CAT_1:1; A63: y in I \ { the Element of I} by A57, A60, ZFMISC_1:56; A64: dom (G9 /. y) = a by CAT_3:41, A57, A60, ZFMISC_1:56; F9 /. y = F9 . y by A57, FUNCT_2:def_13 .= (G9 * p1) . y by A20, A22, A57, A61, FUNCT_4:def_1 .= (G9 * p1) /. y by A63, FUNCT_2:def_13 .= (G9 /. y) (*) p1 by A63, CAT_3:def_5 ; hence (F9 /. y) (*) k = (G9 /. y) (*) (p1 (*) k) by A15, A17, A62, A64, CAT_1:18 .= (G9 /. y) (*) h9 by A46, A47, A56 .= G99 /. y by A40, A41, A63 .= G99 . y by A63, FUNCT_2:def_13 .= F99 . y by A57, A60, ZFMISC_1:56, FUNCT_1:49 .= F99 /. y by A57, FUNCT_2:def_13 ; ::_thesis: verum end; end; end; hence (F9 /. y) (*) k = F99 /. y ; ::_thesis: verum end; let I be finite set ; :: according to CAT_4:def_2 ::_thesis: for F being Function of I, the carrier of C ex a being Object of C ex F9 being Projections_family of a,I st ( cods F9 = F & a is_a_product_wrt F9 ) let F be Function of I, the carrier of C; ::_thesis: ex a being Object of C ex F9 being Projections_family of a,I st ( cods F9 = F & a is_a_product_wrt F9 ) A65: card I = card I ; A66: S1[ 0 ] proof let I be finite set ; ::_thesis: for F being Function of I, the carrier of C st card I = 0 holds ex a being Object of C ex F9 being Projections_family of a,I st ( cods F9 = F & a is_a_product_wrt F9 ) let F be Function of I, the carrier of C; ::_thesis: ( card I = 0 implies ex a being Object of C ex F9 being Projections_family of a,I st ( cods F9 = F & a is_a_product_wrt F9 ) ) assume card I = 0 ; ::_thesis: ex a being Object of C ex F9 being Projections_family of a,I st ( cods F9 = F & a is_a_product_wrt F9 ) then A67: I = {} ; {} is Function of {}, the carrier' of C by RELSET_1:12; then reconsider F9 = {} as Projections_family of a,I by A67, CAT_3:42; take a ; ::_thesis: ex F9 being Projections_family of a,I st ( cods F9 = F & a is_a_product_wrt F9 ) take F9 ; ::_thesis: ( cods F9 = F & a is_a_product_wrt F9 ) for x being set st x in I holds (cods F9) /. x = F /. x ; hence cods F9 = F by CAT_3:1; ::_thesis: a is_a_product_wrt F9 thus a is_a_product_wrt F9 by A8, A67, CAT_3:50; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A66, A10); hence ex a being Object of C ex F9 being Projections_family of a,I st ( cods F9 = F & a is_a_product_wrt F9 ) by A65; ::_thesis: verum end; definition attrc1 is strict ; struct ProdCatStr -> CatStr ; aggrProdCatStr(# carrier, carrier', Source, Target, Comp, TerminalObj, CatProd, Proj1, Proj2 #) -> ProdCatStr ; sel TerminalObj c1 -> Element of the carrier of c1; sel CatProd c1 -> Function of [: the carrier of c1, the carrier of c1:], the carrier of c1; sel Proj1 c1 -> Function of [: the carrier of c1, the carrier of c1:], the carrier' of c1; sel Proj2 c1 -> Function of [: the carrier of c1, the carrier of c1:], the carrier' of c1; end; registration cluster non empty non void for ProdCatStr ; existence ex b1 being ProdCatStr st ( not b1 is void & not b1 is empty ) proof set o = the set ; take ProdCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) ; ::_thesis: ( not ProdCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is void & not ProdCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is empty ) thus ( not ProdCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is void & not ProdCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is empty ) ; ::_thesis: verum end; end; definition let C be non empty non void ProdCatStr ; func [1] C -> Object of C equals :: CAT_4:def 3 the TerminalObj of C; correctness coherence the TerminalObj of C is Object of C; ; let a, b be Object of C; funca [x] b -> Object of C equals :: CAT_4:def 4 the CatProd of C . (a,b); correctness coherence the CatProd of C . (a,b) is Object of C; ; func pr1 (a,b) -> Morphism of C equals :: CAT_4:def 5 the Proj1 of C . (a,b); correctness coherence the Proj1 of C . (a,b) is Morphism of C; ; func pr2 (a,b) -> Morphism of C equals :: CAT_4:def 6 the Proj2 of C . (a,b); correctness coherence the Proj2 of C . (a,b) is Morphism of C; ; end; :: deftheorem defines [1] CAT_4:def_3_:_ for C being non empty non void ProdCatStr holds [1] C = the TerminalObj of C; :: deftheorem defines [x] CAT_4:def_4_:_ for C being non empty non void ProdCatStr for a, b being Object of C holds a [x] b = the CatProd of C . (a,b); :: deftheorem defines pr1 CAT_4:def_5_:_ for C being non empty non void ProdCatStr for a, b being Object of C holds pr1 (a,b) = the Proj1 of C . (a,b); :: deftheorem defines pr2 CAT_4:def_6_:_ for C being non empty non void ProdCatStr for a, b being Object of C holds pr2 (a,b) = the Proj2 of C . (a,b); definition let o, m be set ; func c1Cat (o,m) -> strict ProdCatStr equals :: CAT_4:def 7 ProdCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #); correctness coherence ProdCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #) is strict ProdCatStr ; ; end; :: deftheorem defines c1Cat CAT_4:def_7_:_ for o, m being set holds c1Cat (o,m) = ProdCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #); registration let o, m be set ; cluster c1Cat (o,m) -> non empty trivial non void trivial' strict ; coherence ( not c1Cat (o,m) is empty & c1Cat (o,m) is trivial & not c1Cat (o,m) is void & c1Cat (o,m) is trivial' ) ; end; theorem :: CAT_4:2 for o, m being set holds CatStr(# the carrier of (c1Cat (o,m)), the carrier' of (c1Cat (o,m)), the Source of (c1Cat (o,m)), the Target of (c1Cat (o,m)), the Comp of (c1Cat (o,m)) #) = 1Cat (o,m) ; Lm1a: for o, m being set holds c1Cat (o,m) is Category-like proof let o, m be set ; ::_thesis: c1Cat (o,m) is Category-like set C = c1Cat (o,m); set CP = the Comp of (c1Cat (o,m)); set CD = the Source of (c1Cat (o,m)); set CC = the Target of (c1Cat (o,m)); thus for f, g being Morphism of (c1Cat (o,m)) holds ( [g,f] in dom the Comp of (c1Cat (o,m)) iff dom g = cod f ) :: according to CAT_1:def_6 ::_thesis: verum proof let f, g be Morphism of (c1Cat (o,m)); ::_thesis: ( [g,f] in dom the Comp of (c1Cat (o,m)) iff dom g = cod f ) A1: dom the Comp of (c1Cat (o,m)) = {[m,m]} by FUNCOP_1:13; ( f = m & g = m ) by TARSKI:def_1; hence ( [g,f] in dom the Comp of (c1Cat (o,m)) iff dom g = cod f ) by A1, TARSKI:def_1; ::_thesis: verum end; end; registration cluster non empty non void V57() Category-like transitive associative reflexive with_identities strict for ProdCatStr ; existence ex b1 being non empty non void ProdCatStr st ( b1 is strict & b1 is Category-like & b1 is reflexive & b1 is transitive & b1 is associative & b1 is with_identities & not b1 is void & not b1 is empty ) proof ( c1Cat (0,1) is Category-like & c1Cat (0,1) is transitive & c1Cat (0,1) is reflexive & c1Cat (0,1) is associative & c1Cat (0,1) is with_identities ) by Lm1a; hence ex b1 being non empty non void ProdCatStr st ( b1 is strict & b1 is Category-like & b1 is reflexive & b1 is transitive & b1 is associative & b1 is with_identities & not b1 is void & not b1 is empty ) ; ::_thesis: verum end; end; registration let o, m be set ; cluster c1Cat (o,m) -> non empty non void Category-like transitive associative reflexive with_identities strict ; coherence ( c1Cat (o,m) is Category-like & c1Cat (o,m) is reflexive & c1Cat (o,m) is transitive & c1Cat (o,m) is associative & c1Cat (o,m) is with_identities & not c1Cat (o,m) is empty & not c1Cat (o,m) is void ) by Lm1a; end; theorem Th3: :: CAT_4:3 for o, m being set for a, b being Object of (c1Cat (o,m)) holds a = b proof let o, m be set ; ::_thesis: for a, b being Object of (c1Cat (o,m)) holds a = b let a, b be Object of (c1Cat (o,m)); ::_thesis: a = b a = o by TARSKI:def_1; hence a = b by TARSKI:def_1; ::_thesis: verum end; theorem Th4: :: CAT_4:4 for o, m being set for f, g being Morphism of (c1Cat (o,m)) holds f = g proof let o, m be set ; ::_thesis: for f, g being Morphism of (c1Cat (o,m)) holds f = g let f, g be Morphism of (c1Cat (o,m)); ::_thesis: f = g f = m by TARSKI:def_1; hence f = g by TARSKI:def_1; ::_thesis: verum end; theorem Th5: :: CAT_4:5 for o, m being set for a, b being Object of (c1Cat (o,m)) for f being Morphism of (c1Cat (o,m)) holds f in Hom (a,b) proof let o, m be set ; ::_thesis: for a, b being Object of (c1Cat (o,m)) for f being Morphism of (c1Cat (o,m)) holds f in Hom (a,b) let a, b be Object of (c1Cat (o,m)); ::_thesis: for f being Morphism of (c1Cat (o,m)) holds f in Hom (a,b) let f be Morphism of (c1Cat (o,m)); ::_thesis: f in Hom (a,b) cod f = o by TARSKI:def_1; then A1: cod f = b by TARSKI:def_1; dom f = o by TARSKI:def_1; then dom f = a by TARSKI:def_1; hence f in Hom (a,b) by A1; ::_thesis: verum end; theorem :: CAT_4:6 for o, m being set for a, b being Object of (c1Cat (o,m)) for f being Morphism of (c1Cat (o,m)) holds f is Morphism of a,b proof let o, m be set ; ::_thesis: for a, b being Object of (c1Cat (o,m)) for f being Morphism of (c1Cat (o,m)) holds f is Morphism of a,b let a, b be Object of (c1Cat (o,m)); ::_thesis: for f being Morphism of (c1Cat (o,m)) holds f is Morphism of a,b let f be Morphism of (c1Cat (o,m)); ::_thesis: f is Morphism of a,b f in Hom (a,b) by Th5; hence f is Morphism of a,b by CAT_1:def_5; ::_thesis: verum end; theorem :: CAT_4:7 for o, m being set for a, b being Object of (c1Cat (o,m)) holds Hom (a,b) <> {} by Th5; theorem Th8: :: CAT_4:8 for o, m being set for a being Object of (c1Cat (o,m)) holds a is terminal proof let o, m be set ; ::_thesis: for a being Object of (c1Cat (o,m)) holds a is terminal let a be Object of (c1Cat (o,m)); ::_thesis: a is terminal let b be Object of (c1Cat (o,m)); :: according to CAT_1:def_18 ::_thesis: ( not Hom (b,a) = {} & ex b1 being Morphism of b,a st for b2 being Morphism of b,a holds b1 = b2 ) set f = the Morphism of b,a; thus Hom (b,a) <> {} by Th5; ::_thesis: ex b1 being Morphism of b,a st for b2 being Morphism of b,a holds b1 = b2 take the Morphism of b,a ; ::_thesis: for b1 being Morphism of b,a holds the Morphism of b,a = b1 thus for b1 being Morphism of b,a holds the Morphism of b,a = b1 by Th4; ::_thesis: verum end; theorem Th9: :: CAT_4:9 for o, m being set for c being Object of (c1Cat (o,m)) for p1, p2 being Morphism of (c1Cat (o,m)) holds c is_a_product_wrt p1,p2 proof let o, m be set ; ::_thesis: for c being Object of (c1Cat (o,m)) for p1, p2 being Morphism of (c1Cat (o,m)) holds c is_a_product_wrt p1,p2 let c be Object of (c1Cat (o,m)); ::_thesis: for p1, p2 being Morphism of (c1Cat (o,m)) holds c is_a_product_wrt p1,p2 let p1, p2 be Morphism of (c1Cat (o,m)); ::_thesis: c is_a_product_wrt p1,p2 thus ( dom p1 = c & dom p2 = c ) by Th3; :: according to CAT_3:def_15 ::_thesis: for b1 being Element of the carrier of (c1Cat (o,m)) for b2, b3 being Element of the carrier' of (c1Cat (o,m)) holds ( not b2 in Hom (b1,(cod p1)) or not b3 in Hom (b1,(cod p2)) or ex b4 being Element of the carrier' of (c1Cat (o,m)) st ( b4 in Hom (b1,c) & ( for b5 being Element of the carrier' of (c1Cat (o,m)) holds ( not b5 in Hom (b1,c) or ( ( not p1 (*) b5 = b2 or not p2 (*) b5 = b3 or b4 = b5 ) & ( not b4 = b5 or ( p1 (*) b5 = b2 & p2 (*) b5 = b3 ) ) ) ) ) ) ) let d be Object of (c1Cat (o,m)); ::_thesis: for b1, b2 being Element of the carrier' of (c1Cat (o,m)) holds ( not b1 in Hom (d,(cod p1)) or not b2 in Hom (d,(cod p2)) or ex b3 being Element of the carrier' of (c1Cat (o,m)) st ( b3 in Hom (d,c) & ( for b4 being Element of the carrier' of (c1Cat (o,m)) holds ( not b4 in Hom (d,c) or ( ( not p1 (*) b4 = b1 or not p2 (*) b4 = b2 or b3 = b4 ) & ( not b3 = b4 or ( p1 (*) b4 = b1 & p2 (*) b4 = b2 ) ) ) ) ) ) ) let f, g be Morphism of (c1Cat (o,m)); ::_thesis: ( not f in Hom (d,(cod p1)) or not g in Hom (d,(cod p2)) or ex b1 being Element of the carrier' of (c1Cat (o,m)) st ( b1 in Hom (d,c) & ( for b2 being Element of the carrier' of (c1Cat (o,m)) holds ( not b2 in Hom (d,c) or ( ( not p1 (*) b2 = f or not p2 (*) b2 = g or b1 = b2 ) & ( not b1 = b2 or ( p1 (*) b2 = f & p2 (*) b2 = g ) ) ) ) ) ) ) assume that f in Hom (d,(cod p1)) and g in Hom (d,(cod p2)) ; ::_thesis: ex b1 being Element of the carrier' of (c1Cat (o,m)) st ( b1 in Hom (d,c) & ( for b2 being Element of the carrier' of (c1Cat (o,m)) holds ( not b2 in Hom (d,c) or ( ( not p1 (*) b2 = f or not p2 (*) b2 = g or b1 = b2 ) & ( not b1 = b2 or ( p1 (*) b2 = f & p2 (*) b2 = g ) ) ) ) ) ) take h = p1; ::_thesis: ( h in Hom (d,c) & ( for b1 being Element of the carrier' of (c1Cat (o,m)) holds ( not b1 in Hom (d,c) or ( ( not p1 (*) b1 = f or not p2 (*) b1 = g or h = b1 ) & ( not h = b1 or ( p1 (*) b1 = f & p2 (*) b1 = g ) ) ) ) ) ) thus h in Hom (d,c) by Th5; ::_thesis: for b1 being Element of the carrier' of (c1Cat (o,m)) holds ( not b1 in Hom (d,c) or ( ( not p1 (*) b1 = f or not p2 (*) b1 = g or h = b1 ) & ( not h = b1 or ( p1 (*) b1 = f & p2 (*) b1 = g ) ) ) ) thus for b1 being Element of the carrier' of (c1Cat (o,m)) holds ( not b1 in Hom (d,c) or ( ( not p1 (*) b1 = f or not p2 (*) b1 = g or h = b1 ) & ( not h = b1 or ( p1 (*) b1 = f & p2 (*) b1 = g ) ) ) ) by Th4; ::_thesis: verum end; definition let IT be non empty non void Category-like transitive associative reflexive with_identities ProdCatStr ; attrIT is Cartesian means :Def8: :: CAT_4:def 8 ( the TerminalObj of IT is terminal & ( for a, b being Object of IT holds ( cod ( the Proj1 of IT . (a,b)) = a & cod ( the Proj2 of IT . (a,b)) = b & the CatProd of IT . (a,b) is_a_product_wrt the Proj1 of IT . (a,b), the Proj2 of IT . (a,b) ) ) ); end; :: deftheorem Def8 defines Cartesian CAT_4:def_8_:_ for IT being non empty non void Category-like transitive associative reflexive with_identities ProdCatStr holds ( IT is Cartesian iff ( the TerminalObj of IT is terminal & ( for a, b being Object of IT holds ( cod ( the Proj1 of IT . (a,b)) = a & cod ( the Proj2 of IT . (a,b)) = b & the CatProd of IT . (a,b) is_a_product_wrt the Proj1 of IT . (a,b), the Proj2 of IT . (a,b) ) ) ) ); theorem Th10: :: CAT_4:10 for o, m being set holds c1Cat (o,m) is Cartesian proof let o, m be set ; ::_thesis: c1Cat (o,m) is Cartesian set 1PCat = c1Cat (o,m); thus the TerminalObj of (c1Cat (o,m)) is terminal by Th8; :: according to CAT_4:def_8 ::_thesis: for a, b being Object of (c1Cat (o,m)) holds ( cod ( the Proj1 of (c1Cat (o,m)) . (a,b)) = a & cod ( the Proj2 of (c1Cat (o,m)) . (a,b)) = b & the CatProd of (c1Cat (o,m)) . (a,b) is_a_product_wrt the Proj1 of (c1Cat (o,m)) . (a,b), the Proj2 of (c1Cat (o,m)) . (a,b) ) let a, b be Object of (c1Cat (o,m)); ::_thesis: ( cod ( the Proj1 of (c1Cat (o,m)) . (a,b)) = a & cod ( the Proj2 of (c1Cat (o,m)) . (a,b)) = b & the CatProd of (c1Cat (o,m)) . (a,b) is_a_product_wrt the Proj1 of (c1Cat (o,m)) . (a,b), the Proj2 of (c1Cat (o,m)) . (a,b) ) thus cod ( the Proj1 of (c1Cat (o,m)) . (a,b)) = a by Th3; ::_thesis: ( cod ( the Proj2 of (c1Cat (o,m)) . (a,b)) = b & the CatProd of (c1Cat (o,m)) . (a,b) is_a_product_wrt the Proj1 of (c1Cat (o,m)) . (a,b), the Proj2 of (c1Cat (o,m)) . (a,b) ) thus cod ( the Proj2 of (c1Cat (o,m)) . (a,b)) = b by Th3; ::_thesis: the CatProd of (c1Cat (o,m)) . (a,b) is_a_product_wrt the Proj1 of (c1Cat (o,m)) . (a,b), the Proj2 of (c1Cat (o,m)) . (a,b) thus the CatProd of (c1Cat (o,m)) . (a,b) is_a_product_wrt the Proj1 of (c1Cat (o,m)) . (a,b), the Proj2 of (c1Cat (o,m)) . (a,b) by Th9; ::_thesis: verum end; registration cluster non empty non void V57() Category-like transitive associative reflexive with_identities strict Cartesian for ProdCatStr ; existence ex b1 being non empty non void Category-like transitive associative reflexive with_identities ProdCatStr st ( b1 is strict & b1 is Cartesian ) proof c1Cat (0,1) is Cartesian by Th10; hence ex b1 being non empty non void Category-like transitive associative reflexive with_identities ProdCatStr st ( b1 is strict & b1 is Cartesian ) ; ::_thesis: verum end; end; definition mode Cartesian_category is non empty non void Category-like transitive associative reflexive with_identities Cartesian ProdCatStr ; end; theorem :: CAT_4:11 for C being Cartesian_category holds [1] C is terminal by Def8; theorem Th12: :: CAT_4:12 for C being Cartesian_category for a being Object of C for f1, f2 being Morphism of a, [1] C holds f1 = f2 proof let C be Cartesian_category; ::_thesis: for a being Object of C for f1, f2 being Morphism of a, [1] C holds f1 = f2 let a be Object of C; ::_thesis: for f1, f2 being Morphism of a, [1] C holds f1 = f2 let f1, f2 be Morphism of a, [1] C; ::_thesis: f1 = f2 [1] C is terminal by Def8; then consider f being Morphism of a, [1] C such that A1: for g being Morphism of a, [1] C holds f = g by CAT_1:def_18; thus f1 = f by A1 .= f2 by A1 ; ::_thesis: verum end; theorem Th13: :: CAT_4:13 for C being Cartesian_category for a being Object of C holds Hom (a,([1] C)) <> {} proof let C be Cartesian_category; ::_thesis: for a being Object of C holds Hom (a,([1] C)) <> {} let a be Object of C; ::_thesis: Hom (a,([1] C)) <> {} [1] C is terminal by Def8; hence Hom (a,([1] C)) <> {} by CAT_1:def_18; ::_thesis: verum end; definition let C be Cartesian_category; let a be Object of C; func term a -> Morphism of a, [1] C means :: CAT_4:def 9 verum; existence ex b1 being Morphism of a, [1] C st verum ; uniqueness for b1, b2 being Morphism of a, [1] C holds b1 = b2 by Th12; end; :: deftheorem defines term CAT_4:def_9_:_ for C being Cartesian_category for a being Object of C for b3 being Morphism of a, [1] C holds ( b3 = term a iff verum ); theorem Th14: :: CAT_4:14 for C being Cartesian_category for a being Object of C holds term a = term (a,([1] C)) proof let C be Cartesian_category; ::_thesis: for a being Object of C holds term a = term (a,([1] C)) let a be Object of C; ::_thesis: term a = term (a,([1] C)) [1] C is terminal by Def8; hence term a = term (a,([1] C)) by CAT_3:37; ::_thesis: verum end; theorem :: CAT_4:15 for C being Cartesian_category for a being Object of C holds ( dom (term a) = a & cod (term a) = [1] C ) proof let C be Cartesian_category; ::_thesis: for a being Object of C holds ( dom (term a) = a & cod (term a) = [1] C ) let a be Object of C; ::_thesis: ( dom (term a) = a & cod (term a) = [1] C ) ( [1] C is terminal & term a = term (a,([1] C)) ) by Def8, Th14; hence ( dom (term a) = a & cod (term a) = [1] C ) by CAT_3:35; ::_thesis: verum end; theorem :: CAT_4:16 for C being Cartesian_category for a being Object of C holds Hom (a,([1] C)) = {(term a)} proof let C be Cartesian_category; ::_thesis: for a being Object of C holds Hom (a,([1] C)) = {(term a)} let a be Object of C; ::_thesis: Hom (a,([1] C)) = {(term a)} for f2 being Morphism of a, [1] C holds term a = f2 by Th12; hence Hom (a,([1] C)) = {(term a)} by Th13, CAT_1:8; ::_thesis: verum end; theorem Th17: :: CAT_4:17 for C being Cartesian_category for a, b being Object of C holds ( dom (pr1 (a,b)) = a [x] b & cod (pr1 (a,b)) = a ) proof let C be Cartesian_category; ::_thesis: for a, b being Object of C holds ( dom (pr1 (a,b)) = a [x] b & cod (pr1 (a,b)) = a ) let a, b be Object of C; ::_thesis: ( dom (pr1 (a,b)) = a [x] b & cod (pr1 (a,b)) = a ) set p1 = the Proj1 of C . (a,b); set p2 = the Proj2 of C . (a,b); a [x] b is_a_product_wrt the Proj1 of C . (a,b), the Proj2 of C . (a,b) by Def8; hence ( dom (pr1 (a,b)) = a [x] b & cod (pr1 (a,b)) = a ) by Def8, CAT_3:def_15; ::_thesis: verum end; theorem Th18: :: CAT_4:18 for C being Cartesian_category for a, b being Object of C holds ( dom (pr2 (a,b)) = a [x] b & cod (pr2 (a,b)) = b ) proof let C be Cartesian_category; ::_thesis: for a, b being Object of C holds ( dom (pr2 (a,b)) = a [x] b & cod (pr2 (a,b)) = b ) let a, b be Object of C; ::_thesis: ( dom (pr2 (a,b)) = a [x] b & cod (pr2 (a,b)) = b ) set p1 = the Proj1 of C . (a,b); set p2 = the Proj2 of C . (a,b); a [x] b is_a_product_wrt the Proj1 of C . (a,b), the Proj2 of C . (a,b) by Def8; hence ( dom (pr2 (a,b)) = a [x] b & cod (pr2 (a,b)) = b ) by Def8, CAT_3:def_15; ::_thesis: verum end; definition let C be Cartesian_category; let a, b be Object of C; :: original: pr1 redefine func pr1 (a,b) -> Morphism of a [x] b,a; coherence pr1 (a,b) is Morphism of a [x] b,a proof ( dom (pr1 (a,b)) = a [x] b & cod (pr1 (a,b)) = a ) by Th17; hence pr1 (a,b) is Morphism of a [x] b,a by CAT_1:4; ::_thesis: verum end; :: original: pr2 redefine func pr2 (a,b) -> Morphism of a [x] b,b; coherence pr2 (a,b) is Morphism of a [x] b,b proof ( dom (pr2 (a,b)) = a [x] b & cod (pr2 (a,b)) = b ) by Th18; hence pr2 (a,b) is Morphism of a [x] b,b by CAT_1:4; ::_thesis: verum end; end; theorem Th19: :: CAT_4:19 for C being Cartesian_category for a, b being Object of C holds ( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) proof let C be Cartesian_category; ::_thesis: for a, b being Object of C holds ( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) let a, b be Object of C; ::_thesis: ( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) set c = the CatProd of C . (a,b); set p1 = the Proj1 of C . (a,b); set p2 = the Proj2 of C . (a,b); the CatProd of C . (a,b) is_a_product_wrt the Proj1 of C . (a,b), the Proj2 of C . (a,b) by Def8; then A1: ( dom ( the Proj1 of C . (a,b)) = the CatProd of C . (a,b) & dom ( the Proj2 of C . (a,b)) = the CatProd of C . (a,b) ) by CAT_3:def_15; ( cod ( the Proj1 of C . (a,b)) = a & cod ( the Proj2 of C . (a,b)) = b ) by Def8; hence ( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) by A1, CAT_1:1; ::_thesis: verum end; theorem :: CAT_4:20 for C being Cartesian_category for a, b being Object of C holds a [x] b is_a_product_wrt pr1 (a,b), pr2 (a,b) by Def8; theorem :: CAT_4:21 for C being Cartesian_category holds C is with_finite_product proof let C be Cartesian_category; ::_thesis: C is with_finite_product A1: for a, b being Object of C ex c being Object of C ex p1, p2 being Morphism of C st ( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 ) proof let a, b be Object of C; ::_thesis: ex c being Object of C ex p1, p2 being Morphism of C st ( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 ) take a [x] b ; ::_thesis: ex p1, p2 being Morphism of C st ( dom p1 = a [x] b & dom p2 = a [x] b & cod p1 = a & cod p2 = b & a [x] b is_a_product_wrt p1,p2 ) take pr1 (a,b) ; ::_thesis: ex p2 being Morphism of C st ( dom (pr1 (a,b)) = a [x] b & dom p2 = a [x] b & cod (pr1 (a,b)) = a & cod p2 = b & a [x] b is_a_product_wrt pr1 (a,b),p2 ) take pr2 (a,b) ; ::_thesis: ( dom (pr1 (a,b)) = a [x] b & dom (pr2 (a,b)) = a [x] b & cod (pr1 (a,b)) = a & cod (pr2 (a,b)) = b & a [x] b is_a_product_wrt pr1 (a,b), pr2 (a,b) ) thus ( dom (pr1 (a,b)) = a [x] b & dom (pr2 (a,b)) = a [x] b & cod (pr1 (a,b)) = a & cod (pr2 (a,b)) = b & a [x] b is_a_product_wrt pr1 (a,b), pr2 (a,b) ) by Def8, Th17, Th18; ::_thesis: verum end; [1] C is terminal by Def8; hence C is with_finite_product by A1, Th1; ::_thesis: verum end; theorem :: CAT_4:22 for C being Cartesian_category for a, b being Object of C st Hom (a,b) <> {} & Hom (b,a) <> {} holds ( pr1 (a,b) is retraction & pr2 (a,b) is retraction ) proof let C be Cartesian_category; ::_thesis: for a, b being Object of C st Hom (a,b) <> {} & Hom (b,a) <> {} holds ( pr1 (a,b) is retraction & pr2 (a,b) is retraction ) let a, b be Object of C; ::_thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} implies ( pr1 (a,b) is retraction & pr2 (a,b) is retraction ) ) X: ( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) by Th19; ( a [x] b is_a_product_wrt pr1 (a,b), pr2 (a,b) & cod (pr1 (a,b)) = a ) by Def8; hence ( Hom (a,b) <> {} & Hom (b,a) <> {} implies ( pr1 (a,b) is retraction & pr2 (a,b) is retraction ) ) by X, CAT_3:57; ::_thesis: verum end; definition let C be Cartesian_category; let a, b, c be Object of C; let f be Morphism of c,a; let g be Morphism of c,b; assume A1: ( Hom (c,a) <> {} & Hom (c,b) <> {} ) ; func<:f,g:> -> Morphism of c,a [x] b means :Def10: :: CAT_4:def 10 ( (pr1 (a,b)) * it = f & (pr2 (a,b)) * it = g ); existence ex b1 being Morphism of c,a [x] b st ( (pr1 (a,b)) * b1 = f & (pr2 (a,b)) * b1 = g ) proof A2: a [x] b is_a_product_wrt pr1 (a,b), pr2 (a,b) by Def8; ( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) by Th19; then consider h being Morphism of c,a [x] b such that A3: for h1 being Morphism of c,a [x] b holds ( ( (pr1 (a,b)) * h1 = f & (pr2 (a,b)) * h1 = g ) iff h = h1 ) by A1, A2, CAT_3:55; take h ; ::_thesis: ( (pr1 (a,b)) * h = f & (pr2 (a,b)) * h = g ) thus ( (pr1 (a,b)) * h = f & (pr2 (a,b)) * h = g ) by A3; ::_thesis: verum end; uniqueness for b1, b2 being Morphism of c,a [x] b st (pr1 (a,b)) * b1 = f & (pr2 (a,b)) * b1 = g & (pr1 (a,b)) * b2 = f & (pr2 (a,b)) * b2 = g holds b1 = b2 proof A4: a [x] b is_a_product_wrt pr1 (a,b), pr2 (a,b) by Def8; ( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) by Th19; then consider h being Morphism of c,a [x] b such that A5: for h1 being Morphism of c,a [x] b holds ( ( (pr1 (a,b)) * h1 = f & (pr2 (a,b)) * h1 = g ) iff h = h1 ) by A1, A4, CAT_3:55; let h1, h2 be Morphism of c,a [x] b; ::_thesis: ( (pr1 (a,b)) * h1 = f & (pr2 (a,b)) * h1 = g & (pr1 (a,b)) * h2 = f & (pr2 (a,b)) * h2 = g implies h1 = h2 ) assume that A6: ( (pr1 (a,b)) * h1 = f & (pr2 (a,b)) * h1 = g ) and A7: ( (pr1 (a,b)) * h2 = f & (pr2 (a,b)) * h2 = g ) ; ::_thesis: h1 = h2 h1 = h by A6, A5; hence h1 = h2 by A7, A5; ::_thesis: verum end; end; :: deftheorem Def10 defines <: CAT_4:def_10_:_ for C being Cartesian_category for a, b, c being Object of C for f being Morphism of c,a for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} holds for b7 being Morphism of c,a [x] b holds ( b7 = <:f,g:> iff ( (pr1 (a,b)) * b7 = f & (pr2 (a,b)) * b7 = g ) ); theorem Th23: :: CAT_4:23 for C being Cartesian_category for c, a, b being Object of C st Hom (c,a) <> {} & Hom (c,b) <> {} holds Hom (c,(a [x] b)) <> {} proof let C be Cartesian_category; ::_thesis: for c, a, b being Object of C st Hom (c,a) <> {} & Hom (c,b) <> {} holds Hom (c,(a [x] b)) <> {} let c, a, b be Object of C; ::_thesis: ( Hom (c,a) <> {} & Hom (c,b) <> {} implies Hom (c,(a [x] b)) <> {} ) A1: a [x] b is_a_product_wrt pr1 (a,b), pr2 (a,b) by Def8; ( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) by Th19; hence ( Hom (c,a) <> {} & Hom (c,b) <> {} implies Hom (c,(a [x] b)) <> {} ) by A1, CAT_3:55; ::_thesis: verum end; theorem Th24: :: CAT_4:24 for C being Cartesian_category for a, b being Object of C holds <:(pr1 (a,b)),(pr2 (a,b)):> = id (a [x] b) proof let C be Cartesian_category; ::_thesis: for a, b being Object of C holds <:(pr1 (a,b)),(pr2 (a,b)):> = id (a [x] b) let a, b be Object of C; ::_thesis: <:(pr1 (a,b)),(pr2 (a,b)):> = id (a [x] b) A1: Hom ((a [x] b),b) <> {} by Th19; then A2: (pr2 (a,b)) * (id (a [x] b)) = pr2 (a,b) by CAT_1:29; A3: Hom ((a [x] b),a) <> {} by Th19; then (pr1 (a,b)) * (id (a [x] b)) = pr1 (a,b) by CAT_1:29; hence <:(pr1 (a,b)),(pr2 (a,b)):> = id (a [x] b) by A3, A1, A2, Def10; ::_thesis: verum end; theorem Th25: :: CAT_4:25 for C being Cartesian_category for c, a, b, d being Object of C for f being Morphism of c,a for g being Morphism of c,b for h being Morphism of d,c st Hom (c,a) <> {} & Hom (c,b) <> {} & Hom (d,c) <> {} holds <:(f * h),(g * h):> = <:f,g:> * h proof let C be Cartesian_category; ::_thesis: for c, a, b, d being Object of C for f being Morphism of c,a for g being Morphism of c,b for h being Morphism of d,c st Hom (c,a) <> {} & Hom (c,b) <> {} & Hom (d,c) <> {} holds <:(f * h),(g * h):> = <:f,g:> * h let c, a, b, d be Object of C; ::_thesis: for f being Morphism of c,a for g being Morphism of c,b for h being Morphism of d,c st Hom (c,a) <> {} & Hom (c,b) <> {} & Hom (d,c) <> {} holds <:(f * h),(g * h):> = <:f,g:> * h let f be Morphism of c,a; ::_thesis: for g being Morphism of c,b for h being Morphism of d,c st Hom (c,a) <> {} & Hom (c,b) <> {} & Hom (d,c) <> {} holds <:(f * h),(g * h):> = <:f,g:> * h let g be Morphism of c,b; ::_thesis: for h being Morphism of d,c st Hom (c,a) <> {} & Hom (c,b) <> {} & Hom (d,c) <> {} holds <:(f * h),(g * h):> = <:f,g:> * h let h be Morphism of d,c; ::_thesis: ( Hom (c,a) <> {} & Hom (c,b) <> {} & Hom (d,c) <> {} implies <:(f * h),(g * h):> = <:f,g:> * h ) assume that A1: ( Hom (c,a) <> {} & Hom (c,b) <> {} ) and A2: Hom (d,c) <> {} ; ::_thesis: <:(f * h),(g * h):> = <:f,g:> * h A3: Hom (c,(a [x] b)) <> {} by A1, Th23; A4: Hom ((a [x] b),b) <> {} by Th19; ((pr2 (a,b)) * <:f,g:>) * h = g * h by A1, Def10; then A5: (pr2 (a,b)) * (<:f,g:> * h) = g * h by A2, A4, A3, CAT_1:25; A6: Hom ((a [x] b),a) <> {} by Th19; A7: ( Hom (d,a) <> {} & Hom (d,b) <> {} ) by A1, A2, CAT_1:24; ((pr1 (a,b)) * <:f,g:>) * h = f * h by A1, Def10; then (pr1 (a,b)) * (<:f,g:> * h) = f * h by A2, A6, A3, CAT_1:25; hence <:(f * h),(g * h):> = <:f,g:> * h by A5, A7, Def10; ::_thesis: verum end; theorem Th26: :: CAT_4:26 for C being Cartesian_category for c, a, b being Object of C for f, k being Morphism of c,a for g, h being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & <:f,g:> = <:k,h:> holds ( f = k & g = h ) proof let C be Cartesian_category; ::_thesis: for c, a, b being Object of C for f, k being Morphism of c,a for g, h being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & <:f,g:> = <:k,h:> holds ( f = k & g = h ) let c, a, b be Object of C; ::_thesis: for f, k being Morphism of c,a for g, h being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & <:f,g:> = <:k,h:> holds ( f = k & g = h ) let f, k be Morphism of c,a; ::_thesis: for g, h being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & <:f,g:> = <:k,h:> holds ( f = k & g = h ) let g, h be Morphism of c,b; ::_thesis: ( Hom (c,a) <> {} & Hom (c,b) <> {} & <:f,g:> = <:k,h:> implies ( f = k & g = h ) ) assume A1: ( Hom (c,a) <> {} & Hom (c,b) <> {} ) ; ::_thesis: ( not <:f,g:> = <:k,h:> or ( f = k & g = h ) ) then ( (pr1 (a,b)) * <:f,g:> = f & (pr2 (a,b)) * <:f,g:> = g ) by Def10; hence ( not <:f,g:> = <:k,h:> or ( f = k & g = h ) ) by A1, Def10; ::_thesis: verum end; theorem :: CAT_4:27 for C being Cartesian_category for c, a, b being Object of C for f being Morphism of c,a for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & ( f is monic or g is monic ) holds <:f,g:> is monic proof let C be Cartesian_category; ::_thesis: for c, a, b being Object of C for f being Morphism of c,a for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & ( f is monic or g is monic ) holds <:f,g:> is monic let c, a, b be Object of C; ::_thesis: for f being Morphism of c,a for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & ( f is monic or g is monic ) holds <:f,g:> is monic let f be Morphism of c,a; ::_thesis: for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & ( f is monic or g is monic ) holds <:f,g:> is monic let g be Morphism of c,b; ::_thesis: ( Hom (c,a) <> {} & Hom (c,b) <> {} & ( f is monic or g is monic ) implies <:f,g:> is monic ) assume that A1: Hom (c,a) <> {} and A2: Hom (c,b) <> {} and A3: ( f is monic or g is monic ) ; ::_thesis: <:f,g:> is monic A4: now__::_thesis:_(_g_is_monic_implies_for_d_being_Object_of_C for_f1,_f2_being_Morphism_of_d,c_st_Hom_(d,c)_<>_{}_&_<:f,g:>_*_f1_=_<:f,g:>_*_f2_holds_ f1_=_f2_) assume A5: g is monic ; ::_thesis: for d being Object of C for f1, f2 being Morphism of d,c st Hom (d,c) <> {} & <:f,g:> * f1 = <:f,g:> * f2 holds f1 = f2 let d be Object of C; ::_thesis: for f1, f2 being Morphism of d,c st Hom (d,c) <> {} & <:f,g:> * f1 = <:f,g:> * f2 holds f1 = f2 let f1, f2 be Morphism of d,c; ::_thesis: ( Hom (d,c) <> {} & <:f,g:> * f1 = <:f,g:> * f2 implies f1 = f2 ) assume that A6: Hom (d,c) <> {} and A7: <:f,g:> * f1 = <:f,g:> * f2 ; ::_thesis: f1 = f2 A8: ( Hom (d,a) <> {} & Hom (d,b) <> {} ) by A1, A2, A6, CAT_1:24; ( <:(f * f1),(g * f1):> = <:f,g:> * f1 & <:(f * f2),(g * f2):> = <:f,g:> * f2 ) by A1, A2, A6, Th25; then g * f1 = g * f2 by A7, A8, Th26; hence f1 = f2 by A2, A5, A6, CAT_1:31; ::_thesis: verum end; A9: now__::_thesis:_(_f_is_monic_implies_for_d_being_Object_of_C for_f1,_f2_being_Morphism_of_d,c_st_Hom_(d,c)_<>_{}_&_<:f,g:>_*_f1_=_<:f,g:>_*_f2_holds_ f1_=_f2_) assume A10: f is monic ; ::_thesis: for d being Object of C for f1, f2 being Morphism of d,c st Hom (d,c) <> {} & <:f,g:> * f1 = <:f,g:> * f2 holds f1 = f2 let d be Object of C; ::_thesis: for f1, f2 being Morphism of d,c st Hom (d,c) <> {} & <:f,g:> * f1 = <:f,g:> * f2 holds f1 = f2 let f1, f2 be Morphism of d,c; ::_thesis: ( Hom (d,c) <> {} & <:f,g:> * f1 = <:f,g:> * f2 implies f1 = f2 ) assume that A11: Hom (d,c) <> {} and A12: <:f,g:> * f1 = <:f,g:> * f2 ; ::_thesis: f1 = f2 A13: ( Hom (d,a) <> {} & Hom (d,b) <> {} ) by A1, A2, A11, CAT_1:24; ( <:(f * f1),(g * f1):> = <:f,g:> * f1 & <:(f * f2),(g * f2):> = <:f,g:> * f2 ) by A1, A2, A11, Th25; then f * f1 = f * f2 by A12, A13, Th26; hence f1 = f2 by A1, A10, A11, CAT_1:31; ::_thesis: verum end; Hom (c,(a [x] b)) <> {} by A1, A2, Th23; hence <:f,g:> is monic by A3, A9, A4, CAT_1:31; ::_thesis: verum end; theorem Th28: :: CAT_4:28 for C being Cartesian_category for a being Object of C holds ( Hom (a,(a [x] ([1] C))) <> {} & Hom (a,(([1] C) [x] a)) <> {} ) proof let C be Cartesian_category; ::_thesis: for a being Object of C holds ( Hom (a,(a [x] ([1] C))) <> {} & Hom (a,(([1] C) [x] a)) <> {} ) let a be Object of C; ::_thesis: ( Hom (a,(a [x] ([1] C))) <> {} & Hom (a,(([1] C) [x] a)) <> {} ) ( Hom (a,([1] C)) <> {} & Hom (a,a) <> {} ) by Th13; hence ( Hom (a,(a [x] ([1] C))) <> {} & Hom (a,(([1] C) [x] a)) <> {} ) by Th23; ::_thesis: verum end; definition let C be Cartesian_category; let a be Object of C; func lambda a -> Morphism of ([1] C) [x] a,a equals :: CAT_4:def 11 pr2 (([1] C),a); correctness coherence pr2 (([1] C),a) is Morphism of ([1] C) [x] a,a; ; func lambda' a -> Morphism of a,([1] C) [x] a equals :: CAT_4:def 12 <:(term a),(id a):>; correctness coherence <:(term a),(id a):> is Morphism of a,([1] C) [x] a; ; func rho a -> Morphism of a [x] ([1] C),a equals :: CAT_4:def 13 pr1 (a,([1] C)); correctness coherence pr1 (a,([1] C)) is Morphism of a [x] ([1] C),a; ; func rho' a -> Morphism of a,a [x] ([1] C) equals :: CAT_4:def 14 <:(id a),(term a):>; correctness coherence <:(id a),(term a):> is Morphism of a,a [x] ([1] C); ; end; :: deftheorem defines lambda CAT_4:def_11_:_ for C being Cartesian_category for a being Object of C holds lambda a = pr2 (([1] C),a); :: deftheorem defines lambda' CAT_4:def_12_:_ for C being Cartesian_category for a being Object of C holds lambda' a = <:(term a),(id a):>; :: deftheorem defines rho CAT_4:def_13_:_ for C being Cartesian_category for a being Object of C holds rho a = pr1 (a,([1] C)); :: deftheorem defines rho' CAT_4:def_14_:_ for C being Cartesian_category for a being Object of C holds rho' a = <:(id a),(term a):>; theorem Th29: :: CAT_4:29 for C being Cartesian_category for a being Object of C holds ( (lambda a) * (lambda' a) = id a & (lambda' a) * (lambda a) = id (([1] C) [x] a) & (rho a) * (rho' a) = id a & (rho' a) * (rho a) = id (a [x] ([1] C)) ) proof let C be Cartesian_category; ::_thesis: for a being Object of C holds ( (lambda a) * (lambda' a) = id a & (lambda' a) * (lambda a) = id (([1] C) [x] a) & (rho a) * (rho' a) = id a & (rho' a) * (rho a) = id (a [x] ([1] C)) ) let a be Object of C; ::_thesis: ( (lambda a) * (lambda' a) = id a & (lambda' a) * (lambda a) = id (([1] C) [x] a) & (rho a) * (rho' a) = id a & (rho' a) * (rho a) = id (a [x] ([1] C)) ) A1: (term a) * (pr2 (([1] C),a)) = pr1 (([1] C),a) by Th12; A2: ( Hom (a,([1] C)) <> {} & Hom (a,a) <> {} ) by Th13; hence id a = (lambda a) * (lambda' a) by Def10; ::_thesis: ( (lambda' a) * (lambda a) = id (([1] C) [x] a) & (rho a) * (rho' a) = id a & (rho' a) * (rho a) = id (a [x] ([1] C)) ) A3: Hom ((([1] C) [x] a),a) <> {} by Th19; then (id a) * (pr2 (([1] C),a)) = pr2 (([1] C),a) by CAT_1:28; then <:(term a),(id a):> * (pr2 (([1] C),a)) = <:(pr1 (([1] C),a)),(pr2 (([1] C),a)):> by A2, A3, A1, Th25; hence id (([1] C) [x] a) = (lambda' a) * (lambda a) by Th24; ::_thesis: ( (rho a) * (rho' a) = id a & (rho' a) * (rho a) = id (a [x] ([1] C)) ) thus id a = (rho a) * (rho' a) by A2, Def10; ::_thesis: (rho' a) * (rho a) = id (a [x] ([1] C)) A4: (term a) * (pr1 (a,([1] C))) = pr2 (a,([1] C)) by Th12; A5: Hom ((a [x] ([1] C)),a) <> {} by Th19; then (id a) * (pr1 (a,([1] C))) = pr1 (a,([1] C)) by CAT_1:28; then <:(id a),(term a):> * (pr1 (a,([1] C))) = <:(pr1 (a,([1] C))),(pr2 (a,([1] C))):> by A2, A5, A4, Th25; hence (rho' a) * (rho a) = id (a [x] ([1] C)) by Th24; ::_thesis: verum end; theorem :: CAT_4:30 for C being Cartesian_category for a being Object of C holds ( a,a [x] ([1] C) are_isomorphic & a,([1] C) [x] a are_isomorphic ) proof let C be Cartesian_category; ::_thesis: for a being Object of C holds ( a,a [x] ([1] C) are_isomorphic & a,([1] C) [x] a are_isomorphic ) let a be Object of C; ::_thesis: ( a,a [x] ([1] C) are_isomorphic & a,([1] C) [x] a are_isomorphic ) thus a,a [x] ([1] C) are_isomorphic ::_thesis: a,([1] C) [x] a are_isomorphic proof thus ( Hom (a,(a [x] ([1] C))) <> {} & Hom ((a [x] ([1] C)),a) <> {} ) by Th19, Th28; :: according to CAT_4:def_1 ::_thesis: ex f being Morphism of a,a [x] ([1] C) ex f9 being Morphism of a [x] ([1] C),a st ( f * f9 = id (a [x] ([1] C)) & f9 * f = id a ) take rho' a ; ::_thesis: ex f9 being Morphism of a [x] ([1] C),a st ( (rho' a) * f9 = id (a [x] ([1] C)) & f9 * (rho' a) = id a ) take rho a ; ::_thesis: ( (rho' a) * (rho a) = id (a [x] ([1] C)) & (rho a) * (rho' a) = id a ) thus ( (rho' a) * (rho a) = id (a [x] ([1] C)) & (rho a) * (rho' a) = id a ) by Th29; ::_thesis: verum end; thus ( Hom (a,(([1] C) [x] a)) <> {} & Hom ((([1] C) [x] a),a) <> {} ) by Th19, Th28; :: according to CAT_4:def_1 ::_thesis: ex f being Morphism of a,([1] C) [x] a ex f9 being Morphism of ([1] C) [x] a,a st ( f * f9 = id (([1] C) [x] a) & f9 * f = id a ) take lambda' a ; ::_thesis: ex f9 being Morphism of ([1] C) [x] a,a st ( (lambda' a) * f9 = id (([1] C) [x] a) & f9 * (lambda' a) = id a ) take lambda a ; ::_thesis: ( (lambda' a) * (lambda a) = id (([1] C) [x] a) & (lambda a) * (lambda' a) = id a ) thus ( (lambda' a) * (lambda a) = id (([1] C) [x] a) & (lambda a) * (lambda' a) = id a ) by Th29; ::_thesis: verum end; definition let C be Cartesian_category; let a, b be Object of C; func Switch (a,b) -> Morphism of a [x] b,b [x] a equals :: CAT_4:def 15 <:(pr2 (a,b)),(pr1 (a,b)):>; correctness coherence <:(pr2 (a,b)),(pr1 (a,b)):> is Morphism of a [x] b,b [x] a; ; end; :: deftheorem defines Switch CAT_4:def_15_:_ for C being Cartesian_category for a, b being Object of C holds Switch (a,b) = <:(pr2 (a,b)),(pr1 (a,b)):>; theorem Th31: :: CAT_4:31 for C being Cartesian_category for a, b being Object of C holds Hom ((a [x] b),(b [x] a)) <> {} proof let C be Cartesian_category; ::_thesis: for a, b being Object of C holds Hom ((a [x] b),(b [x] a)) <> {} let a, b be Object of C; ::_thesis: Hom ((a [x] b),(b [x] a)) <> {} ( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) by Th19; hence Hom ((a [x] b),(b [x] a)) <> {} by Th23; ::_thesis: verum end; theorem Th32: :: CAT_4:32 for C being Cartesian_category for a, b being Object of C holds (Switch (a,b)) * (Switch (b,a)) = id (b [x] a) proof let C be Cartesian_category; ::_thesis: for a, b being Object of C holds (Switch (a,b)) * (Switch (b,a)) = id (b [x] a) let a, b be Object of C; ::_thesis: (Switch (a,b)) * (Switch (b,a)) = id (b [x] a) A1: ( Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} ) by Th19; A2: ( Hom ((b [x] a),b) <> {} & Hom ((b [x] a),a) <> {} ) by Th19; then Hom ((b [x] a),(a [x] b)) <> {} by Th23; hence (Switch (a,b)) * (Switch (b,a)) = <:((pr2 (a,b)) * <:(pr2 (b,a)),(pr1 (b,a)):>),((pr1 (a,b)) * <:(pr2 (b,a)),(pr1 (b,a)):>):> by A1, Th25 .= <:(pr1 (b,a)),((pr1 (a,b)) * <:(pr2 (b,a)),(pr1 (b,a)):>):> by A2, Def10 .= <:(pr1 (b,a)),(pr2 (b,a)):> by A2, Def10 .= id (b [x] a) by Th24 ; ::_thesis: verum end; theorem :: CAT_4:33 for C being Cartesian_category for a, b being Object of C holds a [x] b,b [x] a are_isomorphic proof let C be Cartesian_category; ::_thesis: for a, b being Object of C holds a [x] b,b [x] a are_isomorphic let a, b be Object of C; ::_thesis: a [x] b,b [x] a are_isomorphic thus ( Hom ((a [x] b),(b [x] a)) <> {} & Hom ((b [x] a),(a [x] b)) <> {} ) by Th31; :: according to CAT_4:def_1 ::_thesis: ex f being Morphism of a [x] b,b [x] a ex f9 being Morphism of b [x] a,a [x] b st ( f * f9 = id (b [x] a) & f9 * f = id (a [x] b) ) take Switch (a,b) ; ::_thesis: ex f9 being Morphism of b [x] a,a [x] b st ( (Switch (a,b)) * f9 = id (b [x] a) & f9 * (Switch (a,b)) = id (a [x] b) ) take Switch (b,a) ; ::_thesis: ( (Switch (a,b)) * (Switch (b,a)) = id (b [x] a) & (Switch (b,a)) * (Switch (a,b)) = id (a [x] b) ) thus ( (Switch (a,b)) * (Switch (b,a)) = id (b [x] a) & (Switch (b,a)) * (Switch (a,b)) = id (a [x] b) ) by Th32; ::_thesis: verum end; definition let C be Cartesian_category; let a be Object of C; func Delta a -> Morphism of a,a [x] a equals :: CAT_4:def 16 <:(id a),(id a):>; correctness coherence <:(id a),(id a):> is Morphism of a,a [x] a; ; end; :: deftheorem defines Delta CAT_4:def_16_:_ for C being Cartesian_category for a being Object of C holds Delta a = <:(id a),(id a):>; theorem :: CAT_4:34 for C being Cartesian_category for a being Object of C holds Hom (a,(a [x] a)) <> {} proof let C be Cartesian_category; ::_thesis: for a being Object of C holds Hom (a,(a [x] a)) <> {} let a be Object of C; ::_thesis: Hom (a,(a [x] a)) <> {} Hom (a,a) <> {} ; hence Hom (a,(a [x] a)) <> {} by Th23; ::_thesis: verum end; theorem :: CAT_4:35 for C being Cartesian_category for a, b being Object of C for f being Morphism of a,b st Hom (a,b) <> {} holds <:f,f:> = (Delta b) * f proof let C be Cartesian_category; ::_thesis: for a, b being Object of C for f being Morphism of a,b st Hom (a,b) <> {} holds <:f,f:> = (Delta b) * f let a, b be Object of C; ::_thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds <:f,f:> = (Delta b) * f let f be Morphism of a,b; ::_thesis: ( Hom (a,b) <> {} implies <:f,f:> = (Delta b) * f ) assume A1: Hom (a,b) <> {} ; ::_thesis: <:f,f:> = (Delta b) * f ( Hom (b,b) <> {} & (id b) * f = f ) by A1, CAT_1:28; hence <:f,f:> = (Delta b) * f by A1, Th25; ::_thesis: verum end; definition let C be Cartesian_category; let a, b, c be Object of C; func Alpha (a,b,c) -> Morphism of (a [x] b) [x] c,a [x] (b [x] c) equals :: CAT_4:def 17 <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:>; correctness coherence <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:> is Morphism of (a [x] b) [x] c,a [x] (b [x] c); ; func Alpha' (a,b,c) -> Morphism of a [x] (b [x] c),(a [x] b) [x] c equals :: CAT_4:def 18 <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):>; correctness coherence <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):> is Morphism of a [x] (b [x] c),(a [x] b) [x] c; ; end; :: deftheorem defines Alpha CAT_4:def_17_:_ for C being Cartesian_category for a, b, c being Object of C holds Alpha (a,b,c) = <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:>; :: deftheorem defines Alpha' CAT_4:def_18_:_ for C being Cartesian_category for a, b, c being Object of C holds Alpha' (a,b,c) = <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):>; theorem Th36: :: CAT_4:36 for C being Cartesian_category for a, b, c being Object of C holds ( Hom (((a [x] b) [x] c),(a [x] (b [x] c))) <> {} & Hom ((a [x] (b [x] c)),((a [x] b) [x] c)) <> {} ) proof let C be Cartesian_category; ::_thesis: for a, b, c being Object of C holds ( Hom (((a [x] b) [x] c),(a [x] (b [x] c))) <> {} & Hom ((a [x] (b [x] c)),((a [x] b) [x] c)) <> {} ) let a, b, c be Object of C; ::_thesis: ( Hom (((a [x] b) [x] c),(a [x] (b [x] c))) <> {} & Hom ((a [x] (b [x] c)),((a [x] b) [x] c)) <> {} ) A1: Hom (((a [x] b) [x] c),(a [x] b)) <> {} by Th19; Hom ((a [x] b),b) <> {} by Th19; then A2: Hom (((a [x] b) [x] c),b) <> {} by A1, CAT_1:24; Hom ((a [x] b),a) <> {} by Th19; then A3: Hom (((a [x] b) [x] c),a) <> {} by A1, CAT_1:24; Hom (((a [x] b) [x] c),c) <> {} by Th19; then Hom (((a [x] b) [x] c),(b [x] c)) <> {} by A2, Th23; hence Hom (((a [x] b) [x] c),(a [x] (b [x] c))) <> {} by A3, Th23; ::_thesis: Hom ((a [x] (b [x] c)),((a [x] b) [x] c)) <> {} A4: Hom ((a [x] (b [x] c)),(b [x] c)) <> {} by Th19; Hom ((b [x] c),c) <> {} by Th19; then A5: Hom ((a [x] (b [x] c)),c) <> {} by A4, CAT_1:24; Hom ((b [x] c),b) <> {} by Th19; then A6: Hom ((a [x] (b [x] c)),b) <> {} by A4, CAT_1:24; Hom ((a [x] (b [x] c)),a) <> {} by Th19; then Hom ((a [x] (b [x] c)),(a [x] b)) <> {} by A6, Th23; hence Hom ((a [x] (b [x] c)),((a [x] b) [x] c)) <> {} by A5, Th23; ::_thesis: verum end; theorem Th37: :: CAT_4:37 for C being Cartesian_category for a, b, c being Object of C holds ( (Alpha (a,b,c)) * (Alpha' (a,b,c)) = id (a [x] (b [x] c)) & (Alpha' (a,b,c)) * (Alpha (a,b,c)) = id ((a [x] b) [x] c) ) proof let C be Cartesian_category; ::_thesis: for a, b, c being Object of C holds ( (Alpha (a,b,c)) * (Alpha' (a,b,c)) = id (a [x] (b [x] c)) & (Alpha' (a,b,c)) * (Alpha (a,b,c)) = id ((a [x] b) [x] c) ) let a, b, c be Object of C; ::_thesis: ( (Alpha (a,b,c)) * (Alpha' (a,b,c)) = id (a [x] (b [x] c)) & (Alpha' (a,b,c)) * (Alpha (a,b,c)) = id ((a [x] b) [x] c) ) set k = <:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>; set l = <:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>; set f = <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:>; set g = <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):>; A1: Hom (((a [x] b) [x] c),(a [x] b)) <> {} by Th19; A2: Hom ((a [x] b),b) <> {} by Th19; then A3: Hom (((a [x] b) [x] c),b) <> {} by A1, CAT_1:24; A4: Hom (((a [x] b) [x] c),c) <> {} by Th19; then A5: Hom (((a [x] b) [x] c),(b [x] c)) <> {} by A3, Th23; A6: Hom ((a [x] b),a) <> {} by Th19; then A7: Hom (((a [x] b) [x] c),a) <> {} by A1, CAT_1:24; A8: Hom ((a [x] (b [x] c)),(b [x] c)) <> {} by Th19; A9: Hom ((b [x] c),c) <> {} by Th19; then A10: Hom ((a [x] (b [x] c)),c) <> {} by A8, CAT_1:24; A11: Hom ((b [x] c),b) <> {} by Th19; then A12: Hom ((a [x] (b [x] c)),b) <> {} by A8, CAT_1:24; A13: Hom ((a [x] (b [x] c)),a) <> {} by Th19; then A14: Hom ((a [x] (b [x] c)),(a [x] b)) <> {} by A12, Th23; A15: Hom ((a [x] (b [x] c)),((a [x] b) [x] c)) <> {} by Th36; then ((pr2 (a,b)) * (pr1 ((a [x] b),c))) * <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):> = (pr2 (a,b)) * ((pr1 ((a [x] b),c)) * <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):>) by A1, A2, CAT_1:25 .= (pr2 (a,b)) * <:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):> by A10, A14, Def10 .= (pr1 (b,c)) * (pr2 (a,(b [x] c))) by A12, A13, Def10 ; then A16: <:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):> * <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):> = <:((pr1 (b,c)) * (pr2 (a,(b [x] c)))),((pr2 ((a [x] b),c)) * <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):>):> by A3, A4, A15, Th25 .= <:((pr1 (b,c)) * (pr2 (a,(b [x] c)))),((pr2 (b,c)) * (pr2 (a,(b [x] c)))):> by A10, A14, Def10 .= <:(pr1 (b,c)),(pr2 (b,c)):> * (pr2 (a,(b [x] c))) by A11, A8, A9, Th25 .= (id (b [x] c)) * (pr2 (a,(b [x] c))) by Th24 .= pr2 (a,(b [x] c)) by A8, CAT_1:28 ; A17: Hom (((a [x] b) [x] c),(a [x] (b [x] c))) <> {} by Th36; then ((pr1 (b,c)) * (pr2 (a,(b [x] c)))) * <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:> = (pr1 (b,c)) * ((pr2 (a,(b [x] c))) * <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:>) by A11, A8, CAT_1:25 .= (pr1 (b,c)) * <:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):> by A7, A5, Def10 .= (pr2 (a,b)) * (pr1 ((a [x] b),c)) by A3, A4, Def10 ; then A18: <:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):> * <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:> = <:((pr1 (a,(b [x] c))) * <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:>),((pr2 (a,b)) * (pr1 ((a [x] b),c))):> by A17, A12, A13, Th25 .= <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),((pr2 (a,b)) * (pr1 ((a [x] b),c))):> by A7, A5, Def10 .= <:(pr1 (a,b)),(pr2 (a,b)):> * (pr1 ((a [x] b),c)) by A6, A1, A2, Th25 .= (id (a [x] b)) * (pr1 ((a [x] b),c)) by Th24 .= pr1 ((a [x] b),c) by A1, CAT_1:28 ; ((pr1 (a,b)) * (pr1 ((a [x] b),c))) * <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):> = (pr1 (a,b)) * ((pr1 ((a [x] b),c)) * <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):>) by A6, A1, A15, CAT_1:25 .= (pr1 (a,b)) * <:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):> by A10, A14, Def10 .= pr1 (a,(b [x] c)) by A12, A13, Def10 ; hence (Alpha (a,b,c)) * (Alpha' (a,b,c)) = <:(pr1 (a,(b [x] c))),(pr2 (a,(b [x] c))):> by A7, A5, A15, A16, Th25 .= id (a [x] (b [x] c)) by Th24 ; ::_thesis: (Alpha' (a,b,c)) * (Alpha (a,b,c)) = id ((a [x] b) [x] c) ((pr2 (b,c)) * (pr2 (a,(b [x] c)))) * <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:> = (pr2 (b,c)) * ((pr2 (a,(b [x] c))) * <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:>) by A17, A8, A9, CAT_1:25 .= (pr2 (b,c)) * <:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):> by A7, A5, Def10 .= pr2 ((a [x] b),c) by A3, A4, Def10 ; hence (Alpha' (a,b,c)) * (Alpha (a,b,c)) = <:(pr1 ((a [x] b),c)),(pr2 ((a [x] b),c)):> by A17, A10, A14, A18, Th25 .= id ((a [x] b) [x] c) by Th24 ; ::_thesis: verum end; theorem :: CAT_4:38 for C being Cartesian_category for a, b, c being Object of C holds (a [x] b) [x] c,a [x] (b [x] c) are_isomorphic proof let C be Cartesian_category; ::_thesis: for a, b, c being Object of C holds (a [x] b) [x] c,a [x] (b [x] c) are_isomorphic let a, b, c be Object of C; ::_thesis: (a [x] b) [x] c,a [x] (b [x] c) are_isomorphic thus ( Hom (((a [x] b) [x] c),(a [x] (b [x] c))) <> {} & Hom ((a [x] (b [x] c)),((a [x] b) [x] c)) <> {} ) by Th36; :: according to CAT_4:def_1 ::_thesis: ex f being Morphism of (a [x] b) [x] c,a [x] (b [x] c) ex f9 being Morphism of a [x] (b [x] c),(a [x] b) [x] c st ( f * f9 = id (a [x] (b [x] c)) & f9 * f = id ((a [x] b) [x] c) ) take Alpha (a,b,c) ; ::_thesis: ex f9 being Morphism of a [x] (b [x] c),(a [x] b) [x] c st ( (Alpha (a,b,c)) * f9 = id (a [x] (b [x] c)) & f9 * (Alpha (a,b,c)) = id ((a [x] b) [x] c) ) take Alpha' (a,b,c) ; ::_thesis: ( (Alpha (a,b,c)) * (Alpha' (a,b,c)) = id (a [x] (b [x] c)) & (Alpha' (a,b,c)) * (Alpha (a,b,c)) = id ((a [x] b) [x] c) ) thus ( (Alpha (a,b,c)) * (Alpha' (a,b,c)) = id (a [x] (b [x] c)) & (Alpha' (a,b,c)) * (Alpha (a,b,c)) = id ((a [x] b) [x] c) ) by Th37; ::_thesis: verum end; definition let C be Cartesian_category; let a, b, c, d be Object of C; let f be Morphism of a,b; let g be Morphism of c,d; funcf [x] g -> Morphism of a [x] c,b [x] d equals :: CAT_4:def 19 <:(f * (pr1 (a,c))),(g * (pr2 (a,c))):>; correctness coherence <:(f * (pr1 (a,c))),(g * (pr2 (a,c))):> is Morphism of a [x] c,b [x] d; ; end; :: deftheorem defines [x] CAT_4:def_19_:_ for C being Cartesian_category for a, b, c, d being Object of C for f being Morphism of a,b for g being Morphism of c,d holds f [x] g = <:(f * (pr1 (a,c))),(g * (pr2 (a,c))):>; theorem :: CAT_4:39 for C being Cartesian_category for a, c, b, d being Object of C st Hom (a,c) <> {} & Hom (b,d) <> {} holds Hom ((a [x] b),(c [x] d)) <> {} proof let C be Cartesian_category; ::_thesis: for a, c, b, d being Object of C st Hom (a,c) <> {} & Hom (b,d) <> {} holds Hom ((a [x] b),(c [x] d)) <> {} let a, c, b, d be Object of C; ::_thesis: ( Hom (a,c) <> {} & Hom (b,d) <> {} implies Hom ((a [x] b),(c [x] d)) <> {} ) assume that A1: Hom (a,c) <> {} and A2: Hom (b,d) <> {} ; ::_thesis: Hom ((a [x] b),(c [x] d)) <> {} Hom ((a [x] b),b) <> {} by Th19; then A3: Hom ((a [x] b),d) <> {} by A2, CAT_1:24; Hom ((a [x] b),a) <> {} by Th19; then Hom ((a [x] b),c) <> {} by A1, CAT_1:24; hence Hom ((a [x] b),(c [x] d)) <> {} by A3, Th23; ::_thesis: verum end; theorem :: CAT_4:40 for C being Cartesian_category for a, b being Object of C holds (id a) [x] (id b) = id (a [x] b) proof let C be Cartesian_category; ::_thesis: for a, b being Object of C holds (id a) [x] (id b) = id (a [x] b) let a, b be Object of C; ::_thesis: (id a) [x] (id b) = id (a [x] b) Hom ((a [x] b),b) <> {} by Th19; then A1: (id b) * (pr2 (a,b)) = pr2 (a,b) by CAT_1:28; Hom ((a [x] b),a) <> {} by Th19; then (id a) * (pr1 (a,b)) = pr1 (a,b) by CAT_1:28; hence (id a) [x] (id b) = id (a [x] b) by A1, Th24; ::_thesis: verum end; theorem Th41: :: CAT_4:41 for C being Cartesian_category for a, b, c, d, e being Object of C for f being Morphism of a,b for h being Morphism of c,d for g being Morphism of e,a for k being Morphism of e,c st Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (e,c) <> {} holds (f [x] h) * <:g,k:> = <:(f * g),(h * k):> proof let C be Cartesian_category; ::_thesis: for a, b, c, d, e being Object of C for f being Morphism of a,b for h being Morphism of c,d for g being Morphism of e,a for k being Morphism of e,c st Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (e,c) <> {} holds (f [x] h) * <:g,k:> = <:(f * g),(h * k):> let a, b, c, d, e be Object of C; ::_thesis: for f being Morphism of a,b for h being Morphism of c,d for g being Morphism of e,a for k being Morphism of e,c st Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (e,c) <> {} holds (f [x] h) * <:g,k:> = <:(f * g),(h * k):> let f be Morphism of a,b; ::_thesis: for h being Morphism of c,d for g being Morphism of e,a for k being Morphism of e,c st Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (e,c) <> {} holds (f [x] h) * <:g,k:> = <:(f * g),(h * k):> let h be Morphism of c,d; ::_thesis: for g being Morphism of e,a for k being Morphism of e,c st Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (e,c) <> {} holds (f [x] h) * <:g,k:> = <:(f * g),(h * k):> let g be Morphism of e,a; ::_thesis: for k being Morphism of e,c st Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (e,c) <> {} holds (f [x] h) * <:g,k:> = <:(f * g),(h * k):> let k be Morphism of e,c; ::_thesis: ( Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (e,c) <> {} implies (f [x] h) * <:g,k:> = <:(f * g),(h * k):> ) assume that A1: Hom (a,b) <> {} and A2: Hom (c,d) <> {} and A3: ( Hom (e,a) <> {} & Hom (e,c) <> {} ) ; ::_thesis: (f [x] h) * <:g,k:> = <:(f * g),(h * k):> A4: Hom (e,(a [x] c)) <> {} by A3, Th23; A5: Hom ((a [x] c),c) <> {} by Th19; then A6: Hom ((a [x] c),d) <> {} by A2, CAT_1:24; A7: Hom ((a [x] c),a) <> {} by Th19; then A8: Hom ((a [x] c),b) <> {} by A1, CAT_1:24; (pr2 (a,c)) * <:g,k:> = k by A3, Def10; then A9: h * k = (h * (pr2 (a,c))) * <:g,k:> by A2, A4, A5, CAT_1:25; (pr1 (a,c)) * <:g,k:> = g by A3, Def10; then f * g = (f * (pr1 (a,c))) * <:g,k:> by A1, A4, A7, CAT_1:25; hence (f [x] h) * <:g,k:> = <:(f * g),(h * k):> by A4, A8, A6, A9, Th25; ::_thesis: verum end; theorem :: CAT_4:42 for C being Cartesian_category for c, a, b being Object of C for f being Morphism of c,a for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} holds <:f,g:> = (f [x] g) * (Delta c) proof let C be Cartesian_category; ::_thesis: for c, a, b being Object of C for f being Morphism of c,a for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} holds <:f,g:> = (f [x] g) * (Delta c) let c, a, b be Object of C; ::_thesis: for f being Morphism of c,a for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} holds <:f,g:> = (f [x] g) * (Delta c) let f be Morphism of c,a; ::_thesis: for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} holds <:f,g:> = (f [x] g) * (Delta c) let g be Morphism of c,b; ::_thesis: ( Hom (c,a) <> {} & Hom (c,b) <> {} implies <:f,g:> = (f [x] g) * (Delta c) ) assume that A1: Hom (c,a) <> {} and A2: Hom (c,b) <> {} ; ::_thesis: <:f,g:> = (f [x] g) * (Delta c) Hom (c,c) <> {} ; hence (f [x] g) * (Delta c) = <:(f * (id c)),(g * (id c)):> by A1, A2, Th41 .= <:f,(g * (id c)):> by A1, CAT_1:29 .= <:f,g:> by A2, CAT_1:29 ; ::_thesis: verum end; theorem :: CAT_4:43 for C being Cartesian_category for a, b, c, d, e, s being Object of C for f being Morphism of a,b for h being Morphism of c,d for g being Morphism of e,a for k being Morphism of s,c st Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (s,c) <> {} holds (f [x] h) * (g [x] k) = (f * g) [x] (h * k) proof let C be Cartesian_category; ::_thesis: for a, b, c, d, e, s being Object of C for f being Morphism of a,b for h being Morphism of c,d for g being Morphism of e,a for k being Morphism of s,c st Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (s,c) <> {} holds (f [x] h) * (g [x] k) = (f * g) [x] (h * k) let a, b, c, d, e, s be Object of C; ::_thesis: for f being Morphism of a,b for h being Morphism of c,d for g being Morphism of e,a for k being Morphism of s,c st Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (s,c) <> {} holds (f [x] h) * (g [x] k) = (f * g) [x] (h * k) let f be Morphism of a,b; ::_thesis: for h being Morphism of c,d for g being Morphism of e,a for k being Morphism of s,c st Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (s,c) <> {} holds (f [x] h) * (g [x] k) = (f * g) [x] (h * k) let h be Morphism of c,d; ::_thesis: for g being Morphism of e,a for k being Morphism of s,c st Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (s,c) <> {} holds (f [x] h) * (g [x] k) = (f * g) [x] (h * k) let g be Morphism of e,a; ::_thesis: for k being Morphism of s,c st Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (s,c) <> {} holds (f [x] h) * (g [x] k) = (f * g) [x] (h * k) let k be Morphism of s,c; ::_thesis: ( Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (s,c) <> {} implies (f [x] h) * (g [x] k) = (f * g) [x] (h * k) ) assume that A1: Hom (a,b) <> {} and A2: Hom (c,d) <> {} and A3: Hom (e,a) <> {} and A4: Hom (s,c) <> {} ; ::_thesis: (f [x] h) * (g [x] k) = (f * g) [x] (h * k) A5: Hom ((e [x] s),s) <> {} by Th19; then A6: Hom ((e [x] s),c) <> {} by A4, CAT_1:24; A7: Hom ((e [x] s),e) <> {} by Th19; then f * (g * (pr1 (e,s))) = (f * g) * (pr1 (e,s)) by A1, A3, CAT_1:25; then A8: (f * g) [x] (h * k) = <:(f * (g * (pr1 (e,s)))),(h * (k * (pr2 (e,s)))):> by A2, A4, A5, CAT_1:25; Hom ((e [x] s),a) <> {} by A3, A7, CAT_1:24; hence (f [x] h) * (g [x] k) = (f * g) [x] (h * k) by A1, A2, A6, A8, Th41; ::_thesis: verum end; begin definition let C be Category; attrC is with_finite_coproduct means :: CAT_4:def 20 for I being finite set for F being Function of I, the carrier of C ex a being Object of C ex F9 being Injections_family of a,I st ( doms F9 = F & a is_a_coproduct_wrt F9 ); end; :: deftheorem defines with_finite_coproduct CAT_4:def_20_:_ for C being Category holds ( C is with_finite_coproduct iff for I being finite set for F being Function of I, the carrier of C ex a being Object of C ex F9 being Injections_family of a,I st ( doms F9 = F & a is_a_coproduct_wrt F9 ) ); theorem Th44: :: CAT_4:44 for C being Category holds ( C is with_finite_coproduct iff ( ex a being Object of C st a is initial & ( for a, b being Object of C ex c being Object of C ex i1, i2 being Morphism of C st ( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) ) ) ) proof let C be Category; ::_thesis: ( C is with_finite_coproduct iff ( ex a being Object of C st a is initial & ( for a, b being Object of C ex c being Object of C ex i1, i2 being Morphism of C st ( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) ) ) ) thus ( C is with_finite_coproduct implies ( ex a being Object of C st a is initial & ( for a, b being Object of C ex c being Object of C ex i1, i2 being Morphism of C st ( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) ) ) ) ::_thesis: ( ex a being Object of C st a is initial & ( for a, b being Object of C ex c being Object of C ex i1, i2 being Morphism of C st ( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) ) implies C is with_finite_coproduct ) proof reconsider F = {} as Function of {}, the carrier of C by RELSET_1:12; A1: 0 in {0,1} by TARSKI:def_2; assume A2: for I being finite set for F being Function of I, the carrier of C ex a being Object of C ex F9 being Injections_family of a,I st ( doms F9 = F & a is_a_coproduct_wrt F9 ) ; :: according to CAT_4:def_20 ::_thesis: ( ex a being Object of C st a is initial & ( for a, b being Object of C ex c being Object of C ex i1, i2 being Morphism of C st ( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) ) ) then consider a being Object of C, F9 being Injections_family of a, {} such that doms F9 = F and A3: a is_a_coproduct_wrt F9 ; thus ex a being Object of C st a is initial by CAT_3:75, A3; ::_thesis: for a, b being Object of C ex c being Object of C ex i1, i2 being Morphism of C st ( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) let a, b be Object of C; ::_thesis: ex c being Object of C ex i1, i2 being Morphism of C st ( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) set F = (0,1) --> (a,b); consider c being Object of C, F9 being Injections_family of c,{0,1} such that A4: doms F9 = (0,1) --> (a,b) and A5: c is_a_coproduct_wrt F9 by A2; take c ; ::_thesis: ex i1, i2 being Morphism of C st ( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) take i1 = F9 /. 0; ::_thesis: ex i2 being Morphism of C st ( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) take i2 = F9 /. 1; ::_thesis: ( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) A6: 1 in {0,1} by TARSKI:def_2; then A7: i2 = F9 . 1 by FUNCT_2:def_13; ( ((0,1) --> (a,b)) /. 0 = a & ((0,1) --> (a,b)) /. 1 = b ) by CAT_3:3; hence ( dom i1 = a & dom i2 = b ) by A4, A1, A6, CAT_3:def_1; ::_thesis: ( cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) thus ( cod i1 = c & cod i2 = c ) by A1, A6, CAT_3:62; ::_thesis: c is_a_coproduct_wrt i1,i2 ( dom F9 = {0,1} & i1 = F9 . 0 ) by A1, FUNCT_2:def_1, FUNCT_2:def_13; then F9 = (0,1) --> (i1,i2) by A7, FUNCT_4:66; hence c is_a_coproduct_wrt i1,i2 by A5, CAT_3:79; ::_thesis: verum end; given a being Object of C such that A8: a is initial ; ::_thesis: ( ex a, b being Object of C st for c being Object of C for i1, i2 being Morphism of C holds ( not dom i1 = a or not dom i2 = b or not cod i1 = c or not cod i2 = c or not c is_a_coproduct_wrt i1,i2 ) or C is with_finite_coproduct ) defpred S1[ Nat] means for I being finite set for F being Function of I, the carrier of C st card I = \$1 holds ex a being Object of C ex F9 being Injections_family of a,I st ( doms F9 = F & a is_a_coproduct_wrt F9 ); assume A9: for a, b being Object of C ex c being Object of C ex i1, i2 being Morphism of C st ( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) ; ::_thesis: C is with_finite_coproduct A10: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A11: S1[n] ; ::_thesis: S1[n + 1] let I be finite set ; ::_thesis: for F being Function of I, the carrier of C st card I = n + 1 holds ex a being Object of C ex F9 being Injections_family of a,I st ( doms F9 = F & a is_a_coproduct_wrt F9 ) let F be Function of I, the carrier of C; ::_thesis: ( card I = n + 1 implies ex a being Object of C ex F9 being Injections_family of a,I st ( doms F9 = F & a is_a_coproduct_wrt F9 ) ) assume A12: card I = n + 1 ; ::_thesis: ex a being Object of C ex F9 being Injections_family of a,I st ( doms F9 = F & a is_a_coproduct_wrt F9 ) set x = the Element of I; reconsider Ix = I \ { the Element of I} as finite set ; reconsider sx = { the Element of I} as finite set ; reconsider G = F | (I \ { the Element of I}) as Function of (I \ { the Element of I}), the carrier of C by FUNCT_2:32; card Ix = (card I) - (card sx) by CARD_2:44, A12, CARD_1:27, ZFMISC_1:31 .= (card I) - 1 by CARD_1:30 .= n by A12, XCMPLX_1:26 ; then consider a being Object of C, G9 being Injections_family of a,I \ { the Element of I} such that A13: doms G9 = G and A14: a is_a_coproduct_wrt G9 by A11; set b = F /. the Element of I; consider c being Object of C, i1, i2 being Morphism of C such that A15: dom i1 = a and A16: dom i2 = F /. the Element of I and A17: cod i1 = c and A18: cod i2 = c and A19: c is_a_coproduct_wrt i1,i2 by A9; set F9 = (i1 * G9) +* ( the Element of I .--> i2); A20: dom ({ the Element of I} --> i2) = { the Element of I} by FUNCT_2:def_1; rng ((i1 * G9) +* ( the Element of I .--> i2)) c= (rng (i1 * G9)) \/ (rng ( the Element of I .--> i2)) by FUNCT_4:17; then A21: rng ((i1 * G9) +* ( the Element of I .--> i2)) c= the carrier' of C by XBOOLE_1:1; dom (i1 * G9) = I \ { the Element of I} by FUNCT_2:def_1; then A22: (dom (i1 * G9)) \/ (dom ( the Element of I .--> i2)) = I \/ { the Element of I} by A20, XBOOLE_1:39 .= I by A12, CARD_1:27, ZFMISC_1:40 ; then dom ((i1 * G9) +* ( the Element of I .--> i2)) = I by FUNCT_4:def_1; then reconsider F9 = (i1 * G9) +* ( the Element of I .--> i2) as Function of I, the carrier' of C by A21, FUNCT_2:def_1, RELSET_1:4; A23: cods G9 = (I \ { the Element of I}) --> a by CAT_3:def_16; now__::_thesis:_for_y_being_set_st_y_in_I_holds_ (cods_F9)_._y_=_(I_-->_c)_._y let y be set ; ::_thesis: ( y in I implies (cods F9) . y = (I --> c) . y ) assume A24: y in I ; ::_thesis: (cods F9) . y = (I --> c) . y now__::_thesis:_(I_-->_c)_._y_=_(cods_F9)_/._y percases ( y = the Element of I or y <> the Element of I ) ; suppose y = the Element of I ; ::_thesis: (I --> c) . y = (cods F9) /. y then A25: y in { the Element of I} by TARSKI:def_1; F9 /. y = F9 . y by A24, FUNCT_2:def_13 .= ( the Element of I .--> i2) . y by A20, A25, FUNCT_4:13 .= i2 by A25, FUNCOP_1:7 ; hence (I --> c) . y = cod (F9 /. y) by A18, A24, FUNCOP_1:7 .= (cods F9) /. y by A24, CAT_3:def_2 ; ::_thesis: verum end; supposeA26: y <> the Element of I ; ::_thesis: (cods F9) /. y = (I --> c) . y then A27: not y in { the Element of I} by TARSKI:def_1; A28: y in I \ { the Element of I} by A24, A26, ZFMISC_1:56; F9 /. y = F9 . y by A24, FUNCT_2:def_13 .= (i1 * G9) . y by A20, A22, A24, A27, FUNCT_4:def_1 .= (i1 * G9) /. y by A28, FUNCT_2:def_13 ; hence (cods F9) /. y = cod ((i1 * G9) /. y) by A24, CAT_3:def_2 .= (cods (i1 * G9)) /. y by A28, CAT_3:def_2 .= ((I \ { the Element of I}) --> c) /. y by A15, A17, A23, CAT_3:17 .= c by A24, A26, ZFMISC_1:56, CAT_3:2 .= (I --> c) . y by A24, FUNCOP_1:7 ; ::_thesis: verum end; end; end; hence (cods F9) . y = (I --> c) . y by A24, FUNCT_2:def_13; ::_thesis: verum end; then reconsider F9 = F9 as Injections_family of c,I by CAT_3:def_16, FUNCT_2:12; take c ; ::_thesis: ex F9 being Injections_family of c,I st ( doms F9 = F & c is_a_coproduct_wrt F9 ) take F9 ; ::_thesis: ( doms F9 = F & c is_a_coproduct_wrt F9 ) B35: now__::_thesis:_for_y_being_set_st_y_in_I_holds_ (doms_F9)_/._y_=_F_/._y let y be set ; ::_thesis: ( y in I implies (doms F9) /. y = F /. y ) assume A29: y in I ; ::_thesis: (doms F9) /. y = F /. y now__::_thesis:_(doms_F9)_/._y_=_F_/._y percases ( y = the Element of I or y <> the Element of I ) ; supposeA30: y = the Element of I ; ::_thesis: (doms F9) /. y = F /. y then A31: y in { the Element of I} by TARSKI:def_1; F9 /. y = F9 . y by A29, FUNCT_2:def_13 .= ( the Element of I .--> i2) . y by A20, A31, FUNCT_4:13 .= i2 by A31, FUNCOP_1:7 ; hence (doms F9) /. y = F /. y by A16, A29, A30, CAT_3:def_1; ::_thesis: verum end; supposeA32: y <> the Element of I ; ::_thesis: (doms F9) /. y = F /. y then A33: not y in { the Element of I} by TARSKI:def_1; A34: y in I \ { the Element of I} by A29, A32, ZFMISC_1:56; F9 /. y = F9 . y by A29, FUNCT_2:def_13 .= (i1 * G9) . y by A20, A22, A29, A33, FUNCT_4:def_1 .= (i1 * G9) /. y by A34, FUNCT_2:def_13 ; hence (doms F9) /. y = dom ((i1 * G9) /. y) by A29, CAT_3:def_1 .= (doms (i1 * G9)) /. y by A34, CAT_3:def_1 .= G /. y by A13, A15, A23, CAT_3:17 .= G . y by A34, FUNCT_2:def_13 .= F . y by A29, A32, ZFMISC_1:56, FUNCT_1:49 .= F /. y by A29, FUNCT_2:def_13 ; ::_thesis: verum end; end; end; hence (doms F9) /. y = F /. y ; ::_thesis: verum end; hence doms F9 = F by CAT_3:1; ::_thesis: c is_a_coproduct_wrt F9 thus F9 is Injections_family of c,I ; :: according to CAT_3:def_17 ::_thesis: for b1 being Element of the carrier of C for b2 being Injections_family of b1,I holds ( not doms F9 = doms b2 or ex b3 being Element of the carrier' of C st ( b3 in Hom (c,b1) & ( for b4 being Element of the carrier' of C holds ( not b4 in Hom (c,b1) or ( ( ex b5 being set st ( b5 in I & not b4 (*) (F9 /. b5) = b2 /. b5 ) or b3 = b4 ) & ( not b3 = b4 or for b5 being set holds ( not b5 in I or b4 (*) (F9 /. b5) = b2 /. b5 ) ) ) ) ) ) ) let d be Object of C; ::_thesis: for b1 being Injections_family of d,I holds ( not doms F9 = doms b1 or ex b2 being Element of the carrier' of C st ( b2 in Hom (c,d) & ( for b3 being Element of the carrier' of C holds ( not b3 in Hom (c,d) or ( ( ex b4 being set st ( b4 in I & not b3 (*) (F9 /. b4) = b1 /. b4 ) or b2 = b3 ) & ( not b2 = b3 or for b4 being set holds ( not b4 in I or b3 (*) (F9 /. b4) = b1 /. b4 ) ) ) ) ) ) ) let F99 be Injections_family of d,I; ::_thesis: ( not doms F9 = doms F99 or ex b1 being Element of the carrier' of C st ( b1 in Hom (c,d) & ( for b2 being Element of the carrier' of C holds ( not b2 in Hom (c,d) or ( ( ex b3 being set st ( b3 in I & not b2 (*) (F9 /. b3) = F99 /. b3 ) or b1 = b2 ) & ( not b1 = b2 or for b3 being set holds ( not b3 in I or b2 (*) (F9 /. b3) = F99 /. b3 ) ) ) ) ) ) ) assume A36: doms F9 = doms F99 ; ::_thesis: ex b1 being Element of the carrier' of C st ( b1 in Hom (c,d) & ( for b2 being Element of the carrier' of C holds ( not b2 in Hom (c,d) or ( ( ex b3 being set st ( b3 in I & not b2 (*) (F9 /. b3) = F99 /. b3 ) or b1 = b2 ) & ( not b1 = b2 or for b3 being set holds ( not b3 in I or b2 (*) (F9 /. b3) = F99 /. b3 ) ) ) ) ) ) reconsider G99 = F99 | (I \ { the Element of I}) as Function of (I \ { the Element of I}), the carrier' of C by FUNCT_2:32; now__::_thesis:_for_y_being_set_st_y_in_I_\_{_the_Element_of_I}_holds_ (cods_G99)_/._y_=_((I_\_{_the_Element_of_I})_-->_d)_/._y let y be set ; ::_thesis: ( y in I \ { the Element of I} implies (cods G99) /. y = ((I \ { the Element of I}) --> d) /. y ) assume A37: y in I \ { the Element of I} ; ::_thesis: (cods G99) /. y = ((I \ { the Element of I}) --> d) /. y then G99 /. y = G99 . y by FUNCT_2:def_13 .= F99 . y by A37, FUNCT_1:49 .= F99 /. y by A37, FUNCT_2:def_13 ; hence (cods G99) /. y = cod (F99 /. y) by A37, CAT_3:def_2 .= d by A37, CAT_3:62 .= ((I \ { the Element of I}) --> d) /. y by A37, CAT_3:2 ; ::_thesis: verum end; then reconsider G99 = G99 as Injections_family of d,I \ { the Element of I} by CAT_3:def_16, CAT_3:1; now__::_thesis:_for_y_being_set_st_y_in_I_\_{_the_Element_of_I}_holds_ (doms_G9)_/._y_=_(doms_G99)_/._y let y be set ; ::_thesis: ( y in I \ { the Element of I} implies (doms G9) /. y = (doms G99) /. y ) assume A38: y in I \ { the Element of I} ; ::_thesis: (doms G9) /. y = (doms G99) /. y then A39: G /. y = G . y by FUNCT_2:def_13 .= F . y by A38, FUNCT_1:49 .= F /. y by A38, FUNCT_2:def_13 ; F99 /. y = F99 . y by A38, FUNCT_2:def_13 .= G99 . y by A38, FUNCT_1:49 .= G99 /. y by A38, FUNCT_2:def_13 ; hence (doms G9) /. y = dom (G99 /. y) by A13, B35, A36, A38, A39, CAT_3:def_1, CAT_3:1 .= (doms G99) /. y by A38, CAT_3:def_1 ; ::_thesis: verum end; then consider h9 being Morphism of C such that A40: h9 in Hom (a,d) and A41: for k being Morphism of C st k in Hom (a,d) holds ( ( for y being set st y in I \ { the Element of I} holds k (*) (G9 /. y) = G99 /. y ) iff h9 = k ) by A14, CAT_3:def_17, CAT_3:1; A42: the Element of I in { the Element of I} by TARSKI:def_1; set g = F99 /. the Element of I; A43: cod (F99 /. the Element of I) = d by A12, CARD_1:27, CAT_3:62; A44: F9 /. the Element of I = F9 . the Element of I by A12, CARD_1:27, FUNCT_2:def_13 .= ( the Element of I .--> i2) . the Element of I by A20, A42, FUNCT_4:13 .= i2 by A42, FUNCOP_1:7 ; then dom i2 = (doms F9) /. the Element of I by A12, CARD_1:27, CAT_3:def_1 .= dom (F99 /. the Element of I) by A12, A36, CARD_1:27, CAT_3:def_1 ; then F99 /. the Element of I in Hom ((dom i2),d) by A43; then consider h being Morphism of C such that A45: h in Hom (c,d) and A46: for k being Morphism of C st k in Hom (c,d) holds ( ( k (*) i1 = h9 & k (*) i2 = F99 /. the Element of I ) iff h = k ) by A15, A19, A40, CAT_3:def_18; take h ; ::_thesis: ( h in Hom (c,d) & ( for b1 being Element of the carrier' of C holds ( not b1 in Hom (c,d) or ( ( ex b2 being set st ( b2 in I & not b1 (*) (F9 /. b2) = F99 /. b2 ) or h = b1 ) & ( not h = b1 or for b2 being set holds ( not b2 in I or b1 (*) (F9 /. b2) = F99 /. b2 ) ) ) ) ) ) thus h in Hom (c,d) by A45; ::_thesis: for b1 being Element of the carrier' of C holds ( not b1 in Hom (c,d) or ( ( ex b2 being set st ( b2 in I & not b1 (*) (F9 /. b2) = F99 /. b2 ) or h = b1 ) & ( not h = b1 or for b2 being set holds ( not b2 in I or b1 (*) (F9 /. b2) = F99 /. b2 ) ) ) ) let k be Morphism of C; ::_thesis: ( not k in Hom (c,d) or ( ( ex b1 being set st ( b1 in I & not k (*) (F9 /. b1) = F99 /. b1 ) or h = k ) & ( not h = k or for b1 being set holds ( not b1 in I or k (*) (F9 /. b1) = F99 /. b1 ) ) ) ) assume A47: k in Hom (c,d) ; ::_thesis: ( ( ex b1 being set st ( b1 in I & not k (*) (F9 /. b1) = F99 /. b1 ) or h = k ) & ( not h = k or for b1 being set holds ( not b1 in I or k (*) (F9 /. b1) = F99 /. b1 ) ) ) thus ( ( for y being set st y in I holds k (*) (F9 /. y) = F99 /. y ) implies h = k ) ::_thesis: ( not h = k or for b1 being set holds ( not b1 in I or k (*) (F9 /. b1) = F99 /. b1 ) ) proof A48: dom k = c by A47, CAT_1:1; then A49: dom (k (*) i1) = a by A15, A17, CAT_1:17; assume A50: for y being set st y in I holds k (*) (F9 /. y) = F99 /. y ; ::_thesis: h = k A51: for y being set st y in I \ { the Element of I} holds (k (*) i1) (*) (G9 /. y) = G99 /. y proof let y be set ; ::_thesis: ( y in I \ { the Element of I} implies (k (*) i1) (*) (G9 /. y) = G99 /. y ) assume A52: y in I \ { the Element of I} ; ::_thesis: (k (*) i1) (*) (G9 /. y) = G99 /. y then A53: not y in { the Element of I} by XBOOLE_0:def_5; A54: F9 /. y = F9 . y by A52, FUNCT_2:def_13 .= (i1 * G9) . y by A20, A22, A52, A53, FUNCT_4:def_1 .= (i1 * G9) /. y by A52, FUNCT_2:def_13 ; cod (G9 /. y) = a by A52, CAT_3:62; hence (k (*) i1) (*) (G9 /. y) = k (*) (i1 (*) (G9 /. y)) by A15, A17, A48, CAT_1:18 .= k (*) ((i1 * G9) /. y) by A52, CAT_3:def_6 .= F99 /. y by A50, A52, A54 .= F99 . y by A52, FUNCT_2:def_13 .= G99 . y by A52, FUNCT_1:49 .= G99 /. y by A52, FUNCT_2:def_13 ; ::_thesis: verum end; cod k = d by A47, CAT_1:1; then cod (k (*) i1) = d by A17, A48, CAT_1:17; then k (*) i1 in Hom (a,d) by A49; then A55: k (*) i1 = h9 by A41, A51; k (*) i2 = F99 /. the Element of I by A12, A44, A50, CARD_1:27; hence h = k by A46, A47, A55; ::_thesis: verum end; assume A56: h = k ; ::_thesis: for b1 being set holds ( not b1 in I or k (*) (F9 /. b1) = F99 /. b1 ) let y be set ; ::_thesis: ( not y in I or k (*) (F9 /. y) = F99 /. y ) assume A57: y in I ; ::_thesis: k (*) (F9 /. y) = F99 /. y now__::_thesis:_k_(*)_(F9_/._y)_=_F99_/._y percases ( y = the Element of I or y <> the Element of I ) ; supposeA58: y = the Element of I ; ::_thesis: k (*) (F9 /. y) = F99 /. y then A59: y in { the Element of I} by TARSKI:def_1; F9 /. y = F9 . y by A57, FUNCT_2:def_13 .= ( the Element of I .--> i2) . y by A20, A59, FUNCT_4:13 .= i2 by A59, FUNCOP_1:7 ; hence k (*) (F9 /. y) = F99 /. y by A46, A47, A56, A58; ::_thesis: verum end; supposeA60: y <> the Element of I ; ::_thesis: k (*) (F9 /. y) = F99 /. y then A61: not y in { the Element of I} by TARSKI:def_1; A62: dom k = c by A47, CAT_1:1; A63: y in I \ { the Element of I} by A57, A60, ZFMISC_1:56; A64: cod (G9 /. y) = a by CAT_3:62, A57, A60, ZFMISC_1:56; F9 /. y = F9 . y by A57, FUNCT_2:def_13 .= (i1 * G9) . y by A20, A22, A57, A61, FUNCT_4:def_1 .= (i1 * G9) /. y by A63, FUNCT_2:def_13 .= i1 (*) (G9 /. y) by A63, CAT_3:def_6 ; hence k (*) (F9 /. y) = (k (*) i1) (*) (G9 /. y) by A15, A17, A62, A64, CAT_1:18 .= h9 (*) (G9 /. y) by A46, A47, A56 .= G99 /. y by A40, A41, A63 .= G99 . y by A63, FUNCT_2:def_13 .= F99 . y by A57, A60, ZFMISC_1:56, FUNCT_1:49 .= F99 /. y by A57, FUNCT_2:def_13 ; ::_thesis: verum end; end; end; hence k (*) (F9 /. y) = F99 /. y ; ::_thesis: verum end; let I be finite set ; :: according to CAT_4:def_20 ::_thesis: for F being Function of I, the carrier of C ex a being Object of C ex F9 being Injections_family of a,I st ( doms F9 = F & a is_a_coproduct_wrt F9 ) let F be Function of I, the carrier of C; ::_thesis: ex a being Object of C ex F9 being Injections_family of a,I st ( doms F9 = F & a is_a_coproduct_wrt F9 ) A65: card I = card I ; A66: S1[ 0 ] proof let I be finite set ; ::_thesis: for F being Function of I, the carrier of C st card I = 0 holds ex a being Object of C ex F9 being Injections_family of a,I st ( doms F9 = F & a is_a_coproduct_wrt F9 ) let F be Function of I, the carrier of C; ::_thesis: ( card I = 0 implies ex a being Object of C ex F9 being Injections_family of a,I st ( doms F9 = F & a is_a_coproduct_wrt F9 ) ) assume card I = 0 ; ::_thesis: ex a being Object of C ex F9 being Injections_family of a,I st ( doms F9 = F & a is_a_coproduct_wrt F9 ) then A67: I = {} ; {} is Function of {}, the carrier' of C by RELSET_1:12; then reconsider F9 = {} as Injections_family of a,I by A67, CAT_3:63; take a ; ::_thesis: ex F9 being Injections_family of a,I st ( doms F9 = F & a is_a_coproduct_wrt F9 ) take F9 ; ::_thesis: ( doms F9 = F & a is_a_coproduct_wrt F9 ) for x being set st x in I holds (doms F9) /. x = F /. x ; hence doms F9 = F by CAT_3:1; ::_thesis: a is_a_coproduct_wrt F9 thus a is_a_coproduct_wrt F9 by A8, A67, CAT_3:75; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A66, A10); hence ex a being Object of C ex F9 being Injections_family of a,I st ( doms F9 = F & a is_a_coproduct_wrt F9 ) by A65; ::_thesis: verum end; definition attrc1 is strict ; struct CoprodCatStr -> CatStr ; aggrCoprodCatStr(# carrier, carrier', Source, Target, Comp, Initial, Coproduct, Incl1, Incl2 #) -> CoprodCatStr ; sel Initial c1 -> Element of the carrier of c1; sel Coproduct c1 -> Function of [: the carrier of c1, the carrier of c1:], the carrier of c1; sel Incl1 c1 -> Function of [: the carrier of c1, the carrier of c1:], the carrier' of c1; sel Incl2 c1 -> Function of [: the carrier of c1, the carrier of c1:], the carrier' of c1; end; registration cluster non empty non void for CoprodCatStr ; existence ex b1 being CoprodCatStr st ( not b1 is void & not b1 is empty ) proof set o = the set ; take CoprodCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) ; ::_thesis: ( not CoprodCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is void & not CoprodCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is empty ) thus ( not CoprodCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is void & not CoprodCatStr(# { the set },{ the set },( the set :-> the set ),( the set :-> the set ),(( the set , the set ) :-> the set ),(Extract the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ),(( the set , the set ) :-> the set ) #) is empty ) ; ::_thesis: verum end; end; definition let C be non empty non void CoprodCatStr ; func [[0]] C -> Object of C equals :: CAT_4:def 21 the Initial of C; correctness coherence the Initial of C is Object of C; ; let a, b be Object of C; funca + b -> Object of C equals :: CAT_4:def 22 the Coproduct of C . (a,b); correctness coherence the Coproduct of C . (a,b) is Object of C; ; func in1 (a,b) -> Morphism of C equals :: CAT_4:def 23 the Incl1 of C . (a,b); correctness coherence the Incl1 of C . (a,b) is Morphism of C; ; func in2 (a,b) -> Morphism of C equals :: CAT_4:def 24 the Incl2 of C . (a,b); correctness coherence the Incl2 of C . (a,b) is Morphism of C; ; end; :: deftheorem defines [[0]] CAT_4:def_21_:_ for C being non empty non void CoprodCatStr holds [[0]] C = the Initial of C; :: deftheorem defines + CAT_4:def_22_:_ for C being non empty non void CoprodCatStr for a, b being Object of C holds a + b = the Coproduct of C . (a,b); :: deftheorem defines in1 CAT_4:def_23_:_ for C being non empty non void CoprodCatStr for a, b being Object of C holds in1 (a,b) = the Incl1 of C . (a,b); :: deftheorem defines in2 CAT_4:def_24_:_ for C being non empty non void CoprodCatStr for a, b being Object of C holds in2 (a,b) = the Incl2 of C . (a,b); definition let o, m be set ; func c1Cat* (o,m) -> strict CoprodCatStr equals :: CAT_4:def 25 CoprodCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #); correctness coherence CoprodCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #) is strict CoprodCatStr ; ; end; :: deftheorem defines c1Cat* CAT_4:def_25_:_ for o, m being set holds c1Cat* (o,m) = CoprodCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #); theorem :: CAT_4:45 canceled; registration let o, m be set ; cluster c1Cat* (o,m) -> non empty trivial non void trivial' strict ; coherence ( not c1Cat* (o,m) is void & not c1Cat* (o,m) is empty & c1Cat* (o,m) is trivial & c1Cat* (o,m) is trivial' ) ; end; Lm2a: for o, m being set holds c1Cat* (o,m) is Category-like proof let o, m be set ; ::_thesis: c1Cat* (o,m) is Category-like set C = c1Cat* (o,m); set CP = the Comp of (c1Cat* (o,m)); set CD = the Source of (c1Cat* (o,m)); set CC = the Target of (c1Cat* (o,m)); thus for f, g being Morphism of (c1Cat* (o,m)) holds ( [g,f] in dom the Comp of (c1Cat* (o,m)) iff dom g = cod f ) :: according to CAT_1:def_6 ::_thesis: verum proof let f, g be Morphism of (c1Cat* (o,m)); ::_thesis: ( [g,f] in dom the Comp of (c1Cat* (o,m)) iff dom g = cod f ) A1: dom the Comp of (c1Cat* (o,m)) = {[m,m]} by FUNCOP_1:13; Y: ( f = m & g = m ) by TARSKI:def_1; thus ( [g,f] in dom the Comp of (c1Cat* (o,m)) implies dom g = cod f ) by ZFMISC_1:def_10; ::_thesis: ( dom g = cod f implies [g,f] in dom the Comp of (c1Cat* (o,m)) ) thus ( dom g = cod f implies [g,f] in dom the Comp of (c1Cat* (o,m)) ) by A1, Y, TARSKI:def_1; ::_thesis: verum end; end; registration cluster non empty non void V57() Category-like transitive associative reflexive with_identities strict for CoprodCatStr ; existence ex b1 being non empty non void CoprodCatStr st ( b1 is strict & b1 is Category-like & b1 is reflexive & b1 is transitive & b1 is associative & b1 is with_identities ) proof ( c1Cat* (0,1) is reflexive & c1Cat* (0,1) is transitive & c1Cat* (0,1) is associative & c1Cat* (0,1) is with_identities & c1Cat* (0,1) is Category-like ) by Lm2a; hence ex b1 being non empty non void CoprodCatStr st ( b1 is strict & b1 is Category-like & b1 is reflexive & b1 is transitive & b1 is associative & b1 is with_identities ) ; ::_thesis: verum end; end; registration let o, m be set ; cluster c1Cat* (o,m) -> non empty non void Category-like transitive associative reflexive with_identities strict ; coherence ( c1Cat* (o,m) is Category-like & c1Cat* (o,m) is reflexive & c1Cat* (o,m) is transitive & c1Cat* (o,m) is associative & c1Cat* (o,m) is with_identities & not c1Cat* (o,m) is void & not c1Cat* (o,m) is empty ) by Lm2a; end; theorem Th46: :: CAT_4:46 for o, m being set for a, b being Object of (c1Cat* (o,m)) holds a = b proof let o, m be set ; ::_thesis: for a, b being Object of (c1Cat* (o,m)) holds a = b let a, b be Object of (c1Cat* (o,m)); ::_thesis: a = b a = o by TARSKI:def_1; hence a = b by TARSKI:def_1; ::_thesis: verum end; theorem Th47: :: CAT_4:47 for o, m being set for f, g being Morphism of (c1Cat* (o,m)) holds f = g proof let o, m be set ; ::_thesis: for f, g being Morphism of (c1Cat* (o,m)) holds f = g let f, g be Morphism of (c1Cat* (o,m)); ::_thesis: f = g f = m by TARSKI:def_1; hence f = g by TARSKI:def_1; ::_thesis: verum end; theorem Th48: :: CAT_4:48 for o, m being set for a, b being Object of (c1Cat* (o,m)) for f being Morphism of (c1Cat* (o,m)) holds f in Hom (a,b) proof let o, m be set ; ::_thesis: for a, b being Object of (c1Cat* (o,m)) for f being Morphism of (c1Cat* (o,m)) holds f in Hom (a,b) let a, b be Object of (c1Cat* (o,m)); ::_thesis: for f being Morphism of (c1Cat* (o,m)) holds f in Hom (a,b) let f be Morphism of (c1Cat* (o,m)); ::_thesis: f in Hom (a,b) cod f = o by TARSKI:def_1; then A1: cod f = b by TARSKI:def_1; dom f = o by TARSKI:def_1; then dom f = a by TARSKI:def_1; hence f in Hom (a,b) by A1; ::_thesis: verum end; theorem :: CAT_4:49 for o, m being set for a, b being Object of (c1Cat* (o,m)) for f being Morphism of (c1Cat* (o,m)) holds f is Morphism of a,b proof let o, m be set ; ::_thesis: for a, b being Object of (c1Cat* (o,m)) for f being Morphism of (c1Cat* (o,m)) holds f is Morphism of a,b let a, b be Object of (c1Cat* (o,m)); ::_thesis: for f being Morphism of (c1Cat* (o,m)) holds f is Morphism of a,b let f be Morphism of (c1Cat* (o,m)); ::_thesis: f is Morphism of a,b f in Hom (a,b) by Th48; hence f is Morphism of a,b by CAT_1:def_5; ::_thesis: verum end; theorem :: CAT_4:50 for o, m being set for a, b being Object of (c1Cat* (o,m)) holds Hom (a,b) <> {} by Th48; theorem Th51: :: CAT_4:51 for o, m being set for a being Object of (c1Cat* (o,m)) holds a is initial proof let o, m be set ; ::_thesis: for a being Object of (c1Cat* (o,m)) holds a is initial let a be Object of (c1Cat* (o,m)); ::_thesis: a is initial let b be Object of (c1Cat* (o,m)); :: according to CAT_1:def_19 ::_thesis: ( not Hom (a,b) = {} & ex b1 being Morphism of a,b st for b2 being Morphism of a,b holds b1 = b2 ) set f = the Morphism of a,b; thus Hom (a,b) <> {} by Th48; ::_thesis: ex b1 being Morphism of a,b st for b2 being Morphism of a,b holds b1 = b2 take the Morphism of a,b ; ::_thesis: for b1 being Morphism of a,b holds the Morphism of a,b = b1 thus for b1 being Morphism of a,b holds the Morphism of a,b = b1 by Th47; ::_thesis: verum end; theorem Th52: :: CAT_4:52 for o, m being set for c being Object of (c1Cat* (o,m)) for i1, i2 being Morphism of (c1Cat* (o,m)) holds c is_a_coproduct_wrt i1,i2 proof let o, m be set ; ::_thesis: for c being Object of (c1Cat* (o,m)) for i1, i2 being Morphism of (c1Cat* (o,m)) holds c is_a_coproduct_wrt i1,i2 let c be Object of (c1Cat* (o,m)); ::_thesis: for i1, i2 being Morphism of (c1Cat* (o,m)) holds c is_a_coproduct_wrt i1,i2 let i1, i2 be Morphism of (c1Cat* (o,m)); ::_thesis: c is_a_coproduct_wrt i1,i2 thus ( cod i1 = c & cod i2 = c ) by Th46; :: according to CAT_3:def_18 ::_thesis: for b1 being Element of the carrier of (c1Cat* (o,m)) for b2, b3 being Element of the carrier' of (c1Cat* (o,m)) holds ( not b2 in Hom ((dom i1),b1) or not b3 in Hom ((dom i2),b1) or ex b4 being Element of the carrier' of (c1Cat* (o,m)) st ( b4 in Hom (c,b1) & ( for b5 being Element of the carrier' of (c1Cat* (o,m)) holds ( not b5 in Hom (c,b1) or ( ( not b5 (*) i1 = b2 or not b5 (*) i2 = b3 or b4 = b5 ) & ( not b4 = b5 or ( b5 (*) i1 = b2 & b5 (*) i2 = b3 ) ) ) ) ) ) ) let d be Object of (c1Cat* (o,m)); ::_thesis: for b1, b2 being Element of the carrier' of (c1Cat* (o,m)) holds ( not b1 in Hom ((dom i1),d) or not b2 in Hom ((dom i2),d) or ex b3 being Element of the carrier' of (c1Cat* (o,m)) st ( b3 in Hom (c,d) & ( for b4 being Element of the carrier' of (c1Cat* (o,m)) holds ( not b4 in Hom (c,d) or ( ( not b4 (*) i1 = b1 or not b4 (*) i2 = b2 or b3 = b4 ) & ( not b3 = b4 or ( b4 (*) i1 = b1 & b4 (*) i2 = b2 ) ) ) ) ) ) ) let f, g be Morphism of (c1Cat* (o,m)); ::_thesis: ( not f in Hom ((dom i1),d) or not g in Hom ((dom i2),d) or ex b1 being Element of the carrier' of (c1Cat* (o,m)) st ( b1 in Hom (c,d) & ( for b2 being Element of the carrier' of (c1Cat* (o,m)) holds ( not b2 in Hom (c,d) or ( ( not b2 (*) i1 = f or not b2 (*) i2 = g or b1 = b2 ) & ( not b1 = b2 or ( b2 (*) i1 = f & b2 (*) i2 = g ) ) ) ) ) ) ) assume that f in Hom ((dom i1),d) and g in Hom ((dom i2),d) ; ::_thesis: ex b1 being Element of the carrier' of (c1Cat* (o,m)) st ( b1 in Hom (c,d) & ( for b2 being Element of the carrier' of (c1Cat* (o,m)) holds ( not b2 in Hom (c,d) or ( ( not b2 (*) i1 = f or not b2 (*) i2 = g or b1 = b2 ) & ( not b1 = b2 or ( b2 (*) i1 = f & b2 (*) i2 = g ) ) ) ) ) ) take h = i1; ::_thesis: ( h in Hom (c,d) & ( for b1 being Element of the carrier' of (c1Cat* (o,m)) holds ( not b1 in Hom (c,d) or ( ( not b1 (*) i1 = f or not b1 (*) i2 = g or h = b1 ) & ( not h = b1 or ( b1 (*) i1 = f & b1 (*) i2 = g ) ) ) ) ) ) thus h in Hom (c,d) by Th48; ::_thesis: for b1 being Element of the carrier' of (c1Cat* (o,m)) holds ( not b1 in Hom (c,d) or ( ( not b1 (*) i1 = f or not b1 (*) i2 = g or h = b1 ) & ( not h = b1 or ( b1 (*) i1 = f & b1 (*) i2 = g ) ) ) ) thus for b1 being Element of the carrier' of (c1Cat* (o,m)) holds ( not b1 in Hom (c,d) or ( ( not b1 (*) i1 = f or not b1 (*) i2 = g or h = b1 ) & ( not h = b1 or ( b1 (*) i1 = f & b1 (*) i2 = g ) ) ) ) by Th47; ::_thesis: verum end; definition let IT be non empty non void Category-like transitive associative reflexive with_identities CoprodCatStr ; attrIT is Cocartesian means :Def26: :: CAT_4:def 26 ( the Initial of IT is initial & ( for a, b being Object of IT holds ( dom ( the Incl1 of IT . (a,b)) = a & dom ( the Incl2 of IT . (a,b)) = b & the Coproduct of IT . (a,b) is_a_coproduct_wrt the Incl1 of IT . (a,b), the Incl2 of IT . (a,b) ) ) ); end; :: deftheorem Def26 defines Cocartesian CAT_4:def_26_:_ for IT being non empty non void Category-like transitive associative reflexive with_identities CoprodCatStr holds ( IT is Cocartesian iff ( the Initial of IT is initial & ( for a, b being Object of IT holds ( dom ( the Incl1 of IT . (a,b)) = a & dom ( the Incl2 of IT . (a,b)) = b & the Coproduct of IT . (a,b) is_a_coproduct_wrt the Incl1 of IT . (a,b), the Incl2 of IT . (a,b) ) ) ) ); theorem Th53: :: CAT_4:53 for o, m being set holds c1Cat* (o,m) is Cocartesian proof let o, m be set ; ::_thesis: c1Cat* (o,m) is Cocartesian set 1PCat = c1Cat* (o,m); thus the Initial of (c1Cat* (o,m)) is initial by Th51; :: according to CAT_4:def_26 ::_thesis: for a, b being Object of (c1Cat* (o,m)) holds ( dom ( the Incl1 of (c1Cat* (o,m)) . (a,b)) = a & dom ( the Incl2 of (c1Cat* (o,m)) . (a,b)) = b & the Coproduct of (c1Cat* (o,m)) . (a,b) is_a_coproduct_wrt the Incl1 of (c1Cat* (o,m)) . (a,b), the Incl2 of (c1Cat* (o,m)) . (a,b) ) let a, b be Object of (c1Cat* (o,m)); ::_thesis: ( dom ( the Incl1 of (c1Cat* (o,m)) . (a,b)) = a & dom ( the Incl2 of (c1Cat* (o,m)) . (a,b)) = b & the Coproduct of (c1Cat* (o,m)) . (a,b) is_a_coproduct_wrt the Incl1 of (c1Cat* (o,m)) . (a,b), the Incl2 of (c1Cat* (o,m)) . (a,b) ) thus dom ( the Incl1 of (c1Cat* (o,m)) . (a,b)) = a by Th46; ::_thesis: ( dom ( the Incl2 of (c1Cat* (o,m)) . (a,b)) = b & the Coproduct of (c1Cat* (o,m)) . (a,b) is_a_coproduct_wrt the Incl1 of (c1Cat* (o,m)) . (a,b), the Incl2 of (c1Cat* (o,m)) . (a,b) ) thus dom ( the Incl2 of (c1Cat* (o,m)) . (a,b)) = b by Th46; ::_thesis: the Coproduct of (c1Cat* (o,m)) . (a,b) is_a_coproduct_wrt the Incl1 of (c1Cat* (o,m)) . (a,b), the Incl2 of (c1Cat* (o,m)) . (a,b) thus the Coproduct of (c1Cat* (o,m)) . (a,b) is_a_coproduct_wrt the Incl1 of (c1Cat* (o,m)) . (a,b), the Incl2 of (c1Cat* (o,m)) . (a,b) by Th52; ::_thesis: verum end; registration cluster non empty non void V57() Category-like transitive associative reflexive with_identities strict Cocartesian for CoprodCatStr ; existence ex b1 being non empty non void Category-like transitive associative reflexive with_identities CoprodCatStr st ( b1 is strict & b1 is Cocartesian ) proof c1Cat* (0,1) is Cocartesian by Th53; hence ex b1 being non empty non void Category-like transitive associative reflexive with_identities CoprodCatStr st ( b1 is strict & b1 is Cocartesian ) ; ::_thesis: verum end; end; definition mode Cocartesian_category is non empty non void Category-like transitive associative reflexive with_identities Cocartesian CoprodCatStr ; end; theorem :: CAT_4:54 for C being Cocartesian_category holds [[0]] C is initial by Def26; theorem Th55: :: CAT_4:55 for C being Cocartesian_category for a being Object of C for f1, f2 being Morphism of [[0]] C,a holds f1 = f2 proof let C be Cocartesian_category; ::_thesis: for a being Object of C for f1, f2 being Morphism of [[0]] C,a holds f1 = f2 let a be Object of C; ::_thesis: for f1, f2 being Morphism of [[0]] C,a holds f1 = f2 let f1, f2 be Morphism of [[0]] C,a; ::_thesis: f1 = f2 [[0]] C is initial by Def26; then consider f being Morphism of [[0]] C,a such that A1: for g being Morphism of [[0]] C,a holds f = g by CAT_1:def_19; thus f1 = f by A1 .= f2 by A1 ; ::_thesis: verum end; definition let C be Cocartesian_category; let a be Object of C; func init a -> Morphism of [[0]] C,a means :: CAT_4:def 27 verum; existence ex b1 being Morphism of [[0]] C,a st verum ; uniqueness for b1, b2 being Morphism of [[0]] C,a holds b1 = b2 by Th55; end; :: deftheorem defines init CAT_4:def_27_:_ for C being Cocartesian_category for a being Object of C for b3 being Morphism of [[0]] C,a holds ( b3 = init a iff verum ); theorem Th56: :: CAT_4:56 for C being Cocartesian_category for a being Object of C holds Hom (([[0]] C),a) <> {} proof let C be Cocartesian_category; ::_thesis: for a being Object of C holds Hom (([[0]] C),a) <> {} let a be Object of C; ::_thesis: Hom (([[0]] C),a) <> {} [[0]] C is initial by Def26; hence Hom (([[0]] C),a) <> {} by CAT_1:def_19; ::_thesis: verum end; theorem Th57: :: CAT_4:57 for C being Cocartesian_category for a being Object of C holds init a = init (([[0]] C),a) proof let C be Cocartesian_category; ::_thesis: for a being Object of C holds init a = init (([[0]] C),a) let a be Object of C; ::_thesis: init a = init (([[0]] C),a) [[0]] C is initial by Def26; hence init a = init (([[0]] C),a) by CAT_3:40; ::_thesis: verum end; theorem :: CAT_4:58 for C being Cocartesian_category for a being Object of C holds ( dom (init a) = [[0]] C & cod (init a) = a ) proof let C be Cocartesian_category; ::_thesis: for a being Object of C holds ( dom (init a) = [[0]] C & cod (init a) = a ) let a be Object of C; ::_thesis: ( dom (init a) = [[0]] C & cod (init a) = a ) ( [[0]] C is initial & init a = init (([[0]] C),a) ) by Def26, Th57; hence ( dom (init a) = [[0]] C & cod (init a) = a ) by CAT_3:38; ::_thesis: verum end; theorem :: CAT_4:59 for C being Cocartesian_category for a being Object of C holds Hom (([[0]] C),a) = {(init a)} proof let C be Cocartesian_category; ::_thesis: for a being Object of C holds Hom (([[0]] C),a) = {(init a)} let a be Object of C; ::_thesis: Hom (([[0]] C),a) = {(init a)} for f2 being Morphism of [[0]] C,a holds init a = f2 by Th55; hence Hom (([[0]] C),a) = {(init a)} by Th56, CAT_1:8; ::_thesis: verum end; theorem Th60: :: CAT_4:60 for C being Cocartesian_category for a, b being Object of C holds ( dom (in1 (a,b)) = a & cod (in1 (a,b)) = a + b ) proof let C be Cocartesian_category; ::_thesis: for a, b being Object of C holds ( dom (in1 (a,b)) = a & cod (in1 (a,b)) = a + b ) let a, b be Object of C; ::_thesis: ( dom (in1 (a,b)) = a & cod (in1 (a,b)) = a + b ) set i1 = the Incl1 of C . (a,b); set i2 = the Incl2 of C . (a,b); a + b is_a_coproduct_wrt the Incl1 of C . (a,b), the Incl2 of C . (a,b) by Def26; hence ( dom (in1 (a,b)) = a & cod (in1 (a,b)) = a + b ) by Def26, CAT_3:def_18; ::_thesis: verum end; theorem Th61: :: CAT_4:61 for C being Cocartesian_category for a, b being Object of C holds ( dom (in2 (a,b)) = b & cod (in2 (a,b)) = a + b ) proof let C be Cocartesian_category; ::_thesis: for a, b being Object of C holds ( dom (in2 (a,b)) = b & cod (in2 (a,b)) = a + b ) let a, b be Object of C; ::_thesis: ( dom (in2 (a,b)) = b & cod (in2 (a,b)) = a + b ) set i1 = the Incl1 of C . (a,b); set i2 = the Incl2 of C . (a,b); a + b is_a_coproduct_wrt the Incl1 of C . (a,b), the Incl2 of C . (a,b) by Def26; hence ( dom (in2 (a,b)) = b & cod (in2 (a,b)) = a + b ) by Def26, CAT_3:def_18; ::_thesis: verum end; theorem Th62: :: CAT_4:62 for C being Cocartesian_category for a, b being Object of C holds ( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} ) proof let C be Cocartesian_category; ::_thesis: for a, b being Object of C holds ( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} ) let a, b be Object of C; ::_thesis: ( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} ) set c = the Coproduct of C . (a,b); set i1 = the Incl1 of C . (a,b); set i2 = the Incl2 of C . (a,b); the Coproduct of C . (a,b) is_a_coproduct_wrt the Incl1 of C . (a,b), the Incl2 of C . (a,b) by Def26; then A1: ( cod ( the Incl1 of C . (a,b)) = the Coproduct of C . (a,b) & cod ( the Incl2 of C . (a,b)) = the Coproduct of C . (a,b) ) by CAT_3:def_18; ( dom ( the Incl1 of C . (a,b)) = a & dom ( the Incl2 of C . (a,b)) = b ) by Def26; hence ( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} ) by A1, CAT_1:1; ::_thesis: verum end; theorem :: CAT_4:63 for C being Cocartesian_category for a, b being Object of C holds a + b is_a_coproduct_wrt in1 (a,b), in2 (a,b) by Def26; theorem :: CAT_4:64 for C being Cocartesian_category holds C is with_finite_coproduct proof let C be Cocartesian_category; ::_thesis: C is with_finite_coproduct A1: for a, b being Object of C ex c being Object of C ex i1, i2 being Morphism of C st ( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) proof let a, b be Object of C; ::_thesis: ex c being Object of C ex i1, i2 being Morphism of C st ( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) take a + b ; ::_thesis: ex i1, i2 being Morphism of C st ( dom i1 = a & dom i2 = b & cod i1 = a + b & cod i2 = a + b & a + b is_a_coproduct_wrt i1,i2 ) take in1 (a,b) ; ::_thesis: ex i2 being Morphism of C st ( dom (in1 (a,b)) = a & dom i2 = b & cod (in1 (a,b)) = a + b & cod i2 = a + b & a + b is_a_coproduct_wrt in1 (a,b),i2 ) take in2 (a,b) ; ::_thesis: ( dom (in1 (a,b)) = a & dom (in2 (a,b)) = b & cod (in1 (a,b)) = a + b & cod (in2 (a,b)) = a + b & a + b is_a_coproduct_wrt in1 (a,b), in2 (a,b) ) thus ( dom (in1 (a,b)) = a & dom (in2 (a,b)) = b & cod (in1 (a,b)) = a + b & cod (in2 (a,b)) = a + b & a + b is_a_coproduct_wrt in1 (a,b), in2 (a,b) ) by Def26, Th60, Th61; ::_thesis: verum end; [[0]] C is initial by Def26; hence C is with_finite_coproduct by A1, Th44; ::_thesis: verum end; definition let C be Cocartesian_category; let a, b be Object of C; :: original: in1 redefine func in1 (a,b) -> Morphism of a,a + b; coherence in1 (a,b) is Morphism of a,a + b proof ( dom (in1 (a,b)) = a & cod (in1 (a,b)) = a + b ) by Th60; hence in1 (a,b) is Morphism of a,a + b by CAT_1:4; ::_thesis: verum end; :: original: in2 redefine func in2 (a,b) -> Morphism of b,a + b; coherence in2 (a,b) is Morphism of b,a + b proof ( dom (in2 (a,b)) = b & cod (in2 (a,b)) = a + b ) by Th61; hence in2 (a,b) is Morphism of b,a + b by CAT_1:4; ::_thesis: verum end; end; theorem :: CAT_4:65 for C being Cocartesian_category for a, b being Object of C st Hom (a,b) <> {} & Hom (b,a) <> {} holds ( in1 (a,b) is coretraction & in2 (a,b) is coretraction ) proof let C be Cocartesian_category; ::_thesis: for a, b being Object of C st Hom (a,b) <> {} & Hom (b,a) <> {} holds ( in1 (a,b) is coretraction & in2 (a,b) is coretraction ) let a, b be Object of C; ::_thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} implies ( in1 (a,b) is coretraction & in2 (a,b) is coretraction ) ) X: ( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} ) by Th62; ( a + b is_a_coproduct_wrt in1 (a,b), in2 (a,b) & dom (in1 (a,b)) = a ) by Def26; hence ( Hom (a,b) <> {} & Hom (b,a) <> {} implies ( in1 (a,b) is coretraction & in2 (a,b) is coretraction ) ) by X, CAT_3:82; ::_thesis: verum end; definition let C be Cocartesian_category; let a, b be Object of C; :: original: in1 redefine func in1 (a,b) -> Morphism of a,a + b; coherence in1 (a,b) is Morphism of a,a + b proof ( cod (in1 (a,b)) = a + b & dom (in1 (a,b)) = a ) by Th60; hence in1 (a,b) is Morphism of a,a + b ; ::_thesis: verum end; :: original: in2 redefine func in2 (a,b) -> Morphism of b,a + b; coherence in2 (a,b) is Morphism of b,a + b proof ( cod (in2 (a,b)) = a + b & dom (in2 (a,b)) = b ) by Th61; hence in2 (a,b) is Morphism of b,a + b ; ::_thesis: verum end; end; definition let C be Cocartesian_category; let a, b, c be Object of C; let f be Morphism of a,c; let g be Morphism of b,c; assume A1: ( Hom (a,c) <> {} & Hom (b,c) <> {} ) ; func[\$f,g\$] -> Morphism of a + b,c means :Def28: :: CAT_4:def 28 ( it * (in1 (a,b)) = f & it * (in2 (a,b)) = g ); existence ex b1 being Morphism of a + b,c st ( b1 * (in1 (a,b)) = f & b1 * (in2 (a,b)) = g ) proof A2: a + b is_a_coproduct_wrt in1 (a,b), in2 (a,b) by Def26; ( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} ) by Th62; then consider h being Morphism of a + b,c such that A3: for k being Morphism of a + b,c holds ( ( k * (in1 (a,b)) = f & k * (in2 (a,b)) = g ) iff h = k ) by A1, A2, CAT_3:81; take h ; ::_thesis: ( h * (in1 (a,b)) = f & h * (in2 (a,b)) = g ) thus ( h * (in1 (a,b)) = f & h * (in2 (a,b)) = g ) by A3; ::_thesis: verum end; uniqueness for b1, b2 being Morphism of a + b,c st b1 * (in1 (a,b)) = f & b1 * (in2 (a,b)) = g & b2 * (in1 (a,b)) = f & b2 * (in2 (a,b)) = g holds b1 = b2 proof A4: Hom (b,(a + b)) <> {} by Th62; ( a + b is_a_coproduct_wrt in1 (a,b), in2 (a,b) & Hom (a,(a + b)) <> {} ) by Def26, Th62; then consider h being Morphism of a + b,c such that A5: for k being Morphism of a + b,c holds ( ( k * (in1 (a,b)) = f & k * (in2 (a,b)) = g ) iff h = k ) by A1, A4, CAT_3:81; let h1, h2 be Morphism of a + b,c; ::_thesis: ( h1 * (in1 (a,b)) = f & h1 * (in2 (a,b)) = g & h2 * (in1 (a,b)) = f & h2 * (in2 (a,b)) = g implies h1 = h2 ) assume that A6: ( h1 * (in1 (a,b)) = f & h1 * (in2 (a,b)) = g ) and A7: ( h2 * (in1 (a,b)) = f & h2 * (in2 (a,b)) = g ) ; ::_thesis: h1 = h2 h1 = h by A6, A5; hence h1 = h2 by A7, A5; ::_thesis: verum end; end; :: deftheorem Def28 defines [\$ CAT_4:def_28_:_ for C being Cocartesian_category for a, b, c being Object of C for f being Morphism of a,c for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} holds for b7 being Morphism of a + b,c holds ( b7 = [\$f,g\$] iff ( b7 * (in1 (a,b)) = f & b7 * (in2 (a,b)) = g ) ); theorem Th66: :: CAT_4:66 for C being Cocartesian_category for a, c, b being Object of C st Hom (a,c) <> {} & Hom (b,c) <> {} holds Hom ((a + b),c) <> {} proof let C be Cocartesian_category; ::_thesis: for a, c, b being Object of C st Hom (a,c) <> {} & Hom (b,c) <> {} holds Hom ((a + b),c) <> {} let a, c, b be Object of C; ::_thesis: ( Hom (a,c) <> {} & Hom (b,c) <> {} implies Hom ((a + b),c) <> {} ) A1: a + b is_a_coproduct_wrt in1 (a,b), in2 (a,b) by Def26; ( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} ) by Th62; hence ( Hom (a,c) <> {} & Hom (b,c) <> {} implies Hom ((a + b),c) <> {} ) by A1, CAT_3:81; ::_thesis: verum end; theorem Th67: :: CAT_4:67 for C being Cocartesian_category for a, b being Object of C holds [\$(in1 (a,b)),(in2 (a,b))\$] = id (a + b) proof let C be Cocartesian_category; ::_thesis: for a, b being Object of C holds [\$(in1 (a,b)),(in2 (a,b))\$] = id (a + b) let a, b be Object of C; ::_thesis: [\$(in1 (a,b)),(in2 (a,b))\$] = id (a + b) A1: Hom (b,(a + b)) <> {} by Th62; then A2: (id (a + b)) * (in2 (a,b)) = in2 (a,b) by CAT_1:28; A3: Hom (a,(a + b)) <> {} by Th62; then (id (a + b)) * (in1 (a,b)) = in1 (a,b) by CAT_1:28; hence [\$(in1 (a,b)),(in2 (a,b))\$] = id (a + b) by A3, A1, A2, Def28; ::_thesis: verum end; theorem Th68: :: CAT_4:68 for C being Cocartesian_category for a, c, b, d being Object of C for f being Morphism of a,c for g being Morphism of b,c for h being Morphism of c,d st Hom (a,c) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds [\$(h * f),(h * g)\$] = h * [\$f,g\$] proof let C be Cocartesian_category; ::_thesis: for a, c, b, d being Object of C for f being Morphism of a,c for g being Morphism of b,c for h being Morphism of c,d st Hom (a,c) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds [\$(h * f),(h * g)\$] = h * [\$f,g\$] let a, c, b, d be Object of C; ::_thesis: for f being Morphism of a,c for g being Morphism of b,c for h being Morphism of c,d st Hom (a,c) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds [\$(h * f),(h * g)\$] = h * [\$f,g\$] let f be Morphism of a,c; ::_thesis: for g being Morphism of b,c for h being Morphism of c,d st Hom (a,c) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds [\$(h * f),(h * g)\$] = h * [\$f,g\$] let g be Morphism of b,c; ::_thesis: for h being Morphism of c,d st Hom (a,c) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds [\$(h * f),(h * g)\$] = h * [\$f,g\$] let h be Morphism of c,d; ::_thesis: ( Hom (a,c) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} implies [\$(h * f),(h * g)\$] = h * [\$f,g\$] ) assume that A1: ( Hom (a,c) <> {} & Hom (b,c) <> {} ) and A2: Hom (c,d) <> {} ; ::_thesis: [\$(h * f),(h * g)\$] = h * [\$f,g\$] A3: Hom ((a + b),c) <> {} by A1, Th66; A4: Hom (b,(a + b)) <> {} by Th62; h * ([\$f,g\$] * (in2 (a,b))) = h * g by A1, Def28; then A5: (h * [\$f,g\$]) * (in2 (a,b)) = h * g by A2, A4, A3, CAT_1:25; A6: Hom (a,(a + b)) <> {} by Th62; A7: ( Hom (a,d) <> {} & Hom (b,d) <> {} ) by A1, A2, CAT_1:24; h * ([\$f,g\$] * (in1 (a,b))) = h * f by A1, Def28; then (h * [\$f,g\$]) * (in1 (a,b)) = h * f by A2, A6, A3, CAT_1:25; hence [\$(h * f),(h * g)\$] = h * [\$f,g\$] by A5, A7, Def28; ::_thesis: verum end; theorem Th69: :: CAT_4:69 for C being Cocartesian_category for a, c, b being Object of C for f, k being Morphism of a,c for g, h being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & [\$f,g\$] = [\$k,h\$] holds ( f = k & g = h ) proof let C be Cocartesian_category; ::_thesis: for a, c, b being Object of C for f, k being Morphism of a,c for g, h being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & [\$f,g\$] = [\$k,h\$] holds ( f = k & g = h ) let a, c, b be Object of C; ::_thesis: for f, k being Morphism of a,c for g, h being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & [\$f,g\$] = [\$k,h\$] holds ( f = k & g = h ) let f, k be Morphism of a,c; ::_thesis: for g, h being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & [\$f,g\$] = [\$k,h\$] holds ( f = k & g = h ) let g, h be Morphism of b,c; ::_thesis: ( Hom (a,c) <> {} & Hom (b,c) <> {} & [\$f,g\$] = [\$k,h\$] implies ( f = k & g = h ) ) assume A1: ( Hom (a,c) <> {} & Hom (b,c) <> {} ) ; ::_thesis: ( not [\$f,g\$] = [\$k,h\$] or ( f = k & g = h ) ) then ( [\$f,g\$] * (in1 (a,b)) = f & [\$f,g\$] * (in2 (a,b)) = g ) by Def28; hence ( not [\$f,g\$] = [\$k,h\$] or ( f = k & g = h ) ) by A1, Def28; ::_thesis: verum end; theorem :: CAT_4:70 for C being Cocartesian_category for a, c, b being Object of C for f being Morphism of a,c for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & ( f is epi or g is epi ) holds [\$f,g\$] is epi proof let C be Cocartesian_category; ::_thesis: for a, c, b being Object of C for f being Morphism of a,c for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & ( f is epi or g is epi ) holds [\$f,g\$] is epi let a, c, b be Object of C; ::_thesis: for f being Morphism of a,c for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & ( f is epi or g is epi ) holds [\$f,g\$] is epi let f be Morphism of a,c; ::_thesis: for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & ( f is epi or g is epi ) holds [\$f,g\$] is epi let g be Morphism of b,c; ::_thesis: ( Hom (a,c) <> {} & Hom (b,c) <> {} & ( f is epi or g is epi ) implies [\$f,g\$] is epi ) assume that A1: Hom (a,c) <> {} and A2: Hom (b,c) <> {} and A3: ( f is epi or g is epi ) ; ::_thesis: [\$f,g\$] is epi A4: now__::_thesis:_(_g_is_epi_implies_for_d_being_Object_of_C for_f1,_f2_being_Morphism_of_c,d_st_Hom_(c,d)_<>_{}_&_f1_*_[\$f,g\$]_=_f2_*_[\$f,g\$]_holds_ f1_=_f2_) assume A5: g is epi ; ::_thesis: for d being Object of C for f1, f2 being Morphism of c,d st Hom (c,d) <> {} & f1 * [\$f,g\$] = f2 * [\$f,g\$] holds f1 = f2 let d be Object of C; ::_thesis: for f1, f2 being Morphism of c,d st Hom (c,d) <> {} & f1 * [\$f,g\$] = f2 * [\$f,g\$] holds f1 = f2 let f1, f2 be Morphism of c,d; ::_thesis: ( Hom (c,d) <> {} & f1 * [\$f,g\$] = f2 * [\$f,g\$] implies f1 = f2 ) assume that A6: Hom (c,d) <> {} and A7: f1 * [\$f,g\$] = f2 * [\$f,g\$] ; ::_thesis: f1 = f2 A8: ( Hom (a,d) <> {} & Hom (b,d) <> {} ) by A1, A2, A6, CAT_1:24; ( [\$(f1 * f),(f1 * g)\$] = f1 * [\$f,g\$] & [\$(f2 * f),(f2 * g)\$] = f2 * [\$f,g\$] ) by A1, A2, A6, Th68; then f1 * g = f2 * g by A7, A8, Th69; hence f1 = f2 by A2, A5, A6, CAT_1:36; ::_thesis: verum end; A9: now__::_thesis:_(_f_is_epi_implies_for_d_being_Object_of_C for_f1,_f2_being_Morphism_of_c,d_st_Hom_(c,d)_<>_{}_&_f1_*_[\$f,g\$]_=_f2_*_[\$f,g\$]_holds_ f1_=_f2_) assume A10: f is epi ; ::_thesis: for d being Object of C for f1, f2 being Morphism of c,d st Hom (c,d) <> {} & f1 * [\$f,g\$] = f2 * [\$f,g\$] holds f1 = f2 let d be Object of C; ::_thesis: for f1, f2 being Morphism of c,d st Hom (c,d) <> {} & f1 * [\$f,g\$] = f2 * [\$f,g\$] holds f1 = f2 let f1, f2 be Morphism of c,d; ::_thesis: ( Hom (c,d) <> {} & f1 * [\$f,g\$] = f2 * [\$f,g\$] implies f1 = f2 ) assume that A11: Hom (c,d) <> {} and A12: f1 * [\$f,g\$] = f2 * [\$f,g\$] ; ::_thesis: f1 = f2 A13: ( Hom (a,d) <> {} & Hom (b,d) <> {} ) by A1, A2, A11, CAT_1:24; ( [\$(f1 * f),(f1 * g)\$] = f1 * [\$f,g\$] & [\$(f2 * f),(f2 * g)\$] = f2 * [\$f,g\$] ) by A1, A2, A11, Th68; then f1 * f = f2 * f by A12, A13, Th69; hence f1 = f2 by A1, A10, A11, CAT_1:36; ::_thesis: verum end; Hom ((a + b),c) <> {} by A1, A2, Th66; hence [\$f,g\$] is epi by A3, A9, A4, CAT_1:36; ::_thesis: verum end; theorem :: CAT_4:71 for C being Cocartesian_category for a being Object of C holds ( a,a + ([[0]] C) are_isomorphic & a,([[0]] C) + a are_isomorphic ) proof 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: (in2 (([[0]] C),a)) * (init a) = in1 (([[0]] C),a) by Th55; A2: ( Hom (([[0]] C),a) <> {} & Hom (a,a) <> {} ) by Th56; thus a,a + ([[0]] C) are_isomorphic ::_thesis: a,([[0]] C) + a are_isomorphic proof thus A3: Hom (a,(a + ([[0]] C))) <> {} by Th62; :: according to CAT_4:def_1 ::_thesis: ( 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, Th66; ::_thesis: 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)); ::_thesis: 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)\$]; ::_thesis: ( g * f = id (a + ([[0]] C)) & f * g = id a ) A4: (in1 (a,([[0]] C))) * (init a) = in2 (a,([[0]] C)) by Th55; (in1 (a,([[0]] C))) * (id a) = in1 (a,([[0]] C)) by A3, CAT_1:29; then g * f = [\$(in1 (a,([[0]] C))),(in2 (a,([[0]] C)))\$] by A2, A3, A4, Th68; hence ( g * f = id (a + ([[0]] C)) & f * g = id a ) by A2, Def28, Th67; ::_thesis: verum end; thus A5: Hom (a,(([[0]] C) + a)) <> {} by Th62; :: according to CAT_4:def_1 ::_thesis: ( 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, Th66; ::_thesis: 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); ::_thesis: 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)\$]; ::_thesis: ( g * f = id (([[0]] C) + a) & f * g = id a ) (in2 (([[0]] C),a)) * (id a) = in2 (([[0]] C),a) by A5, CAT_1:29; then g * f = [\$(in1 (([[0]] C),a)),(in2 (([[0]] C),a))\$] by A2, A5, A1, Th68; hence ( g * f = id (([[0]] C) + a) & f * g = id a ) by A2, Def28, Th67; ::_thesis: verum end; theorem :: CAT_4:72 for C being Cocartesian_category for a, b being Object of C holds a + b,b + a are_isomorphic proof let C be Cocartesian_category; ::_thesis: for a, b being Object of C holds a + b,b + a are_isomorphic let a, b be Object of C; ::_thesis: a + b,b + a are_isomorphic A1: ( Hom (a,(b + a)) <> {} & Hom (b,(b + a)) <> {} ) by Th62; hence A2: Hom ((a + b),(b + a)) <> {} by Th66; :: according to CAT_4:def_1 ::_thesis: ( Hom ((b + a),(a + b)) <> {} & ex f being Morphism of a + b,b + a ex f9 being Morphism of b + a,a + b st ( f * f9 = id (b + a) & f9 * f = id (a + b) ) ) A3: ( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} ) by Th62; hence A4: Hom ((b + a),(a + b)) <> {} by Th66; ::_thesis: ex f being Morphism of a + b,b + a ex f9 being Morphism of b + a,a + b st ( f * f9 = id (b + a) & f9 * f = id (a + b) ) take f9 = [\$(in2 (b,a)),(in1 (b,a))\$]; ::_thesis: ex f9 being Morphism of b + a,a + b st ( f9 * f9 = id (b + a) & f9 * f9 = id (a + b) ) take f = [\$(in2 (a,b)),(in1 (a,b))\$]; ::_thesis: ( f9 * f = id (b + a) & f * f9 = id (a + b) ) thus f9 * f = [\$(f9 * (in2 (a,b))),(f9 * (in1 (a,b)))\$] by A2, A3, Th68 .= [\$(in1 (b,a)),(f9 * (in1 (a,b)))\$] by A1, Def28 .= [\$(in1 (b,a)),(in2 (b,a))\$] by A1, Def28 .= id (b + a) by Th67 ; ::_thesis: f * f9 = id (a + b) thus f * f9 = [\$(f * (in2 (b,a))),(f * (in1 (b,a)))\$] by A1, A4, Th68 .= [\$(in1 (a,b)),(f * (in1 (b,a)))\$] by A3, Def28 .= [\$(in1 (a,b)),(in2 (a,b))\$] by A3, Def28 .= id (a + b) by Th67 ; ::_thesis: verum end; theorem :: CAT_4:73 for C being Cocartesian_category for a, b, c being Object of C holds (a + b) + c,a + (b + c) are_isomorphic proof 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 Th62; A2: Hom (b,(b + c)) <> {} by Th62; then A3: Hom (b,(a + (b + c))) <> {} by A1, CAT_1:24; A4: Hom (a,(a + (b + c))) <> {} by Th62; then A5: Hom ((a + b),(a + (b + c))) <> {} by A3, Th66; A6: Hom (c,(b + c)) <> {} by Th62; then A7: Hom (c,(a + (b + c))) <> {} by A1, CAT_1:24; hence A8: Hom (((a + b) + c),(a + (b + c))) <> {} by A5, Th66; :: 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 Th62; A10: Hom (b,(a + b)) <> {} by Th62; then A11: Hom (b,((a + b) + c)) <> {} by A9, CAT_1:24; A12: Hom (c,((a + b) + c)) <> {} by Th62; then A13: Hom ((b + c),((a + b) + c)) <> {} by A11, Th66; A14: Hom (a,(a + b)) <> {} by Th62; then A15: Hom (a,((a + b) + c)) <> {} by A9, CAT_1:24; hence A16: Hom ((a + (b + c)),((a + b) + c)) <> {} by A13, Th66; ::_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, Th68 .= [\$((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, Th68 .= (in2 (a,(b + c))) * (id (b + c)) by Th67 .= 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, Th68 .= [\$((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, Th68 .= (in1 ((a + b),c)) * (id (a + b)) by Th67 .= 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, Th68 .= id (a + (b + c)) by Th67 ; ::_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, Th68 .= id ((a + b) + c) by Th67 ; ::_thesis: verum end; definition let C be Cocartesian_category; let a be Object of C; func nabla a -> Morphism of a + a,a equals :: CAT_4:def 29 [\$(id a),(id a)\$]; correctness coherence [\$(id a),(id a)\$] is Morphism of a + a,a; ; end; :: deftheorem defines nabla CAT_4:def_29_:_ for C being Cocartesian_category for a being Object of C holds nabla a = [\$(id a),(id a)\$]; definition let C be Cocartesian_category; let a, b, c, d be Object of C; let f be Morphism of a,c; let g be Morphism of b,d; funcf + g -> Morphism of a + b,c + d equals :: CAT_4:def 30 [\$((in1 (c,d)) * f),((in2 (c,d)) * g)\$]; correctness coherence [\$((in1 (c,d)) * f),((in2 (c,d)) * g)\$] is Morphism of a + b,c + d; ; end; :: deftheorem defines + CAT_4:def_30_:_ for C being Cocartesian_category for a, b, c, d being Object of C for f being Morphism of a,c for g being Morphism of b,d holds f + g = [\$((in1 (c,d)) * f),((in2 (c,d)) * g)\$]; theorem :: CAT_4:74 for C being Cocartesian_category for a, c, b, d being Object of C st Hom (a,c) <> {} & Hom (b,d) <> {} holds Hom ((a + b),(c + d)) <> {} proof let C be Cocartesian_category; ::_thesis: for a, c, b, d being Object of C st Hom (a,c) <> {} & Hom (b,d) <> {} holds Hom ((a + b),(c + d)) <> {} let a, c, b, d be Object of C; ::_thesis: ( Hom (a,c) <> {} & Hom (b,d) <> {} implies Hom ((a + b),(c + d)) <> {} ) assume that A1: Hom (a,c) <> {} and A2: Hom (b,d) <> {} ; ::_thesis: Hom ((a + b),(c + d)) <> {} Hom (d,(c + d)) <> {} by Th62; then A3: Hom (b,(c + d)) <> {} by A2, CAT_1:24; Hom (c,(c + d)) <> {} by Th62; then Hom (a,(c + d)) <> {} by A1, CAT_1:24; hence Hom ((a + b),(c + d)) <> {} by A3, Th66; ::_thesis: verum end; theorem :: CAT_4:75 for C being Cocartesian_category for a, b being Object of C holds (id a) + (id b) = id (a + b) proof let C be Cocartesian_category; ::_thesis: for a, b being Object of C holds (id a) + (id b) = id (a + b) let a, b be Object of C; ::_thesis: (id a) + (id b) = id (a + b) Hom (b,(a + b)) <> {} by Th62; then A1: (in2 (a,b)) * (id b) = in2 (a,b) by CAT_1:29; Hom (a,(a + b)) <> {} by Th62; then (in1 (a,b)) * (id a) = in1 (a,b) by CAT_1:29; hence (id a) + (id b) = id (a + b) by A1, Th67; ::_thesis: verum end; theorem Th76: :: CAT_4:76 for C being Cocartesian_category for a, c, b, d, e being Object of C for f being Morphism of a,c for h being Morphism of b,d for g being Morphism of c,e for k being Morphism of d,e st Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,e) <> {} holds [\$g,k\$] * (f + h) = [\$(g * f),(k * h)\$] proof let C be Cocartesian_category; ::_thesis: for a, c, b, d, e being Object of C for f being Morphism of a,c for h being Morphism of b,d for g being Morphism of c,e for k being Morphism of d,e st Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,e) <> {} holds [\$g,k\$] * (f + h) = [\$(g * f),(k * h)\$] let a, c, b, d, e be Object of C; ::_thesis: for f being Morphism of a,c for h being Morphism of b,d for g being Morphism of c,e for k being Morphism of d,e st Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,e) <> {} holds [\$g,k\$] * (f + h) = [\$(g * f),(k * h)\$] let f be Morphism of a,c; ::_thesis: for h being Morphism of b,d for g being Morphism of c,e for k being Morphism of d,e st Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,e) <> {} holds [\$g,k\$] * (f + h) = [\$(g * f),(k * h)\$] let h be Morphism of b,d; ::_thesis: for g being Morphism of c,e for k being Morphism of d,e st Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,e) <> {} holds [\$g,k\$] * (f + h) = [\$(g * f),(k * h)\$] let g be Morphism of c,e; ::_thesis: for k being Morphism of d,e st Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,e) <> {} holds [\$g,k\$] * (f + h) = [\$(g * f),(k * h)\$] let k be Morphism of d,e; ::_thesis: ( Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,e) <> {} implies [\$g,k\$] * (f + h) = [\$(g * f),(k * h)\$] ) assume that A1: Hom (a,c) <> {} and A2: Hom (b,d) <> {} and A3: ( Hom (c,e) <> {} & Hom (d,e) <> {} ) ; ::_thesis: [\$g,k\$] * (f + h) = [\$(g * f),(k * h)\$] A4: Hom ((c + d),e) <> {} by A3, Th66; A5: Hom (d,(c + d)) <> {} by Th62; then A6: Hom (b,(c + d)) <> {} by A2, CAT_1:24; A7: Hom (c,(c + d)) <> {} by Th62; then A8: Hom (a,(c + d)) <> {} by A1, CAT_1:24; [\$g,k\$] * (in2 (c,d)) = k by A3, Def28; then A9: k * h = [\$g,k\$] * ((in2 (c,d)) * h) by A2, A4, A5, CAT_1:25; [\$g,k\$] * (in1 (c,d)) = g by A3, Def28; then g * f = [\$g,k\$] * ((in1 (c,d)) * f) by A1, A4, A7, CAT_1:25; hence [\$g,k\$] * (f + h) = [\$(g * f),(k * h)\$] by A4, A8, A6, A9, Th68; ::_thesis: verum end; theorem :: CAT_4:77 for C being Cocartesian_category for a, c, b being Object of C for f being Morphism of a,c for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} holds (nabla c) * (f + g) = [\$f,g\$] proof let C be Cocartesian_category; ::_thesis: for a, c, b being Object of C for f being Morphism of a,c for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} holds (nabla c) * (f + g) = [\$f,g\$] let a, c, b be Object of C; ::_thesis: for f being Morphism of a,c for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} holds (nabla c) * (f + g) = [\$f,g\$] let f be Morphism of a,c; ::_thesis: for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} holds (nabla c) * (f + g) = [\$f,g\$] let g be Morphism of b,c; ::_thesis: ( Hom (a,c) <> {} & Hom (b,c) <> {} implies (nabla c) * (f + g) = [\$f,g\$] ) assume that A1: Hom (a,c) <> {} and A2: Hom (b,c) <> {} ; ::_thesis: (nabla c) * (f + g) = [\$f,g\$] Hom (c,c) <> {} ; hence (nabla c) * (f + g) = [\$((id c) * f),((id c) * g)\$] by A1, A2, Th76 .= [\$f,((id c) * g)\$] by A1, CAT_1:28 .= [\$f,g\$] by A2, CAT_1:28 ; ::_thesis: verum end; theorem :: CAT_4:78 for C being Cocartesian_category for a, c, b, d, e, s being Object of C for f being Morphism of a,c for h being Morphism of b,d for g being Morphism of c,e for k being Morphism of d,s st Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,s) <> {} holds (g + k) * (f + h) = (g * f) + (k * h) proof let C be Cocartesian_category; ::_thesis: for a, c, b, d, e, s being Object of C for f being Morphism of a,c for h being Morphism of b,d for g being Morphism of c,e for k being Morphism of d,s st Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,s) <> {} holds (g + k) * (f + h) = (g * f) + (k * h) let a, c, b, d, e, s be Object of C; ::_thesis: for f being Morphism of a,c for h being Morphism of b,d for g being Morphism of c,e for k being Morphism of d,s st Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,s) <> {} holds (g + k) * (f + h) = (g * f) + (k * h) let f be Morphism of a,c; ::_thesis: for h being Morphism of b,d for g being Morphism of c,e for k being Morphism of d,s st Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,s) <> {} holds (g + k) * (f + h) = (g * f) + (k * h) let h be Morphism of b,d; ::_thesis: for g being Morphism of c,e for k being Morphism of d,s st Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,s) <> {} holds (g + k) * (f + h) = (g * f) + (k * h) let g be Morphism of c,e; ::_thesis: for k being Morphism of d,s st Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,s) <> {} holds (g + k) * (f + h) = (g * f) + (k * h) let k be Morphism of d,s; ::_thesis: ( Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,s) <> {} implies (g + k) * (f + h) = (g * f) + (k * h) ) assume that A1: Hom (a,c) <> {} and A2: Hom (b,d) <> {} and A3: Hom (c,e) <> {} and A4: Hom (d,s) <> {} ; ::_thesis: (g + k) * (f + h) = (g * f) + (k * h) A5: Hom (s,(e + s)) <> {} by Th62; then A6: Hom (d,(e + s)) <> {} by A4, CAT_1:24; A7: Hom (e,(e + s)) <> {} by Th62; then ((in1 (e,s)) * g) * f = (in1 (e,s)) * (g * f) by A1, A3, CAT_1:25; then A8: (g * f) + (k * h) = [\$(((in1 (e,s)) * g) * f),(((in2 (e,s)) * k) * h)\$] by A2, A4, A5, CAT_1:25; Hom (c,(e + s)) <> {} by A3, A7, CAT_1:24; hence (g + k) * (f + h) = (g * f) + (k * h) by A1, A2, A6, A8, Th76; ::_thesis: verum end;