:: FUNCTOR1 semantic presentation begin registration cluster non empty transitive with_units reflexive for AltCatStr ; existence ex b1 being non empty AltCatStr st ( b1 is transitive & b1 is with_units & b1 is reflexive ) proof set C = the category; take the category ; ::_thesis: ( the category is transitive & the category is with_units & the category is reflexive ) thus ( the category is transitive & the category is with_units & the category is reflexive ) ; ::_thesis: verum end; end; registration let A be non empty reflexive AltCatStr ; cluster non empty reflexive for SubCatStr of A; existence ex b1 being SubCatStr of A st ( not b1 is empty & b1 is reflexive ) proof reconsider B = A as SubCatStr of A by ALTCAT_2:20; take B ; ::_thesis: ( not B is empty & B is reflexive ) thus ( not B is empty & B is reflexive ) ; ::_thesis: verum end; end; registration let C1, C2 be non empty reflexive AltCatStr ; let F be feasible FunctorStr over C1,C2; let A be non empty reflexive SubCatStr of C1; clusterF | A -> feasible ; coherence F | A is feasible ; end; begin registration let X be set ; cluster id X -> onto ; coherence id X is onto proof reconsider f = id X as Function of X,X ; rng f = X by RELAT_1:45; hence id X is onto by FUNCT_2:def_3; ::_thesis: verum end; end; theorem :: FUNCTOR1:1 for A being non empty set for B, C being non empty Subset of A for D being non empty Subset of B st C = D holds incl C = (incl B) * (incl D) proof let A be non empty set ; ::_thesis: for B, C being non empty Subset of A for D being non empty Subset of B st C = D holds incl C = (incl B) * (incl D) let B, C be non empty Subset of A; ::_thesis: for D being non empty Subset of B st C = D holds incl C = (incl B) * (incl D) let D be non empty Subset of B; ::_thesis: ( C = D implies incl C = (incl B) * (incl D) ) assume A1: C = D ; ::_thesis: incl C = (incl B) * (incl D) (incl B) * (incl D) = id (B /\ D) by FUNCT_1:22 .= incl C by A1, XBOOLE_1:28 ; hence incl C = (incl B) * (incl D) ; ::_thesis: verum end; theorem Th2: :: FUNCTOR1:2 for X, Y being set for f being Function of X,Y st f is bijective holds f " is Function of Y,X proof let X, Y be set ; ::_thesis: for f being Function of X,Y st f is bijective holds f " is Function of Y,X let f be Function of X,Y; ::_thesis: ( f is bijective implies f " is Function of Y,X ) assume A1: f is bijective ; ::_thesis: f " is Function of Y,X then rng f = Y by FUNCT_2:def_3; hence f " is Function of Y,X by A1, FUNCT_2:25; ::_thesis: verum end; theorem :: FUNCTOR1:3 for X, Y being set for Z being non empty set for f being Function of X,Y for g being Function of Y,Z st f is bijective & g is bijective holds ex h being Function of X,Z st ( h = g * f & h is bijective ) proof let X, Y be set ; ::_thesis: for Z being non empty set for f being Function of X,Y for g being Function of Y,Z st f is bijective & g is bijective holds ex h being Function of X,Z st ( h = g * f & h is bijective ) let Z be non empty set ; ::_thesis: for f being Function of X,Y for g being Function of Y,Z st f is bijective & g is bijective holds ex h being Function of X,Z st ( h = g * f & h is bijective ) let f be Function of X,Y; ::_thesis: for g being Function of Y,Z st f is bijective & g is bijective holds ex h being Function of X,Z st ( h = g * f & h is bijective ) let g be Function of Y,Z; ::_thesis: ( f is bijective & g is bijective implies ex h being Function of X,Z st ( h = g * f & h is bijective ) ) assume that A1: f is bijective and A2: g is bijective ; ::_thesis: ex h being Function of X,Z st ( h = g * f & h is bijective ) A3: rng g = Z by A2, FUNCT_2:def_3; then ( Y = {} iff Z = {} ) ; then reconsider h = g * f as Function of X,Z ; take h ; ::_thesis: ( h = g * f & h is bijective ) rng f = Y by A1, FUNCT_2:def_3; then rng (g * f) = Z by A3, FUNCT_2:14; then h is onto by FUNCT_2:def_3; hence ( h = g * f & h is bijective ) by A1, A2; ::_thesis: verum end; begin theorem Th4: :: FUNCTOR1:4 for A being non empty reflexive AltCatStr for B being non empty reflexive SubCatStr of A for C being non empty SubCatStr of A for D being non empty SubCatStr of B st C = D holds incl C = (incl B) * (incl D) proof let A be non empty reflexive AltCatStr ; ::_thesis: for B being non empty reflexive SubCatStr of A for C being non empty SubCatStr of A for D being non empty SubCatStr of B st C = D holds incl C = (incl B) * (incl D) let B be non empty reflexive SubCatStr of A; ::_thesis: for C being non empty SubCatStr of A for D being non empty SubCatStr of B st C = D holds incl C = (incl B) * (incl D) let C be non empty SubCatStr of A; ::_thesis: for D being non empty SubCatStr of B st C = D holds incl C = (incl B) * (incl D) let D be non empty SubCatStr of B; ::_thesis: ( C = D implies incl C = (incl B) * (incl D) ) assume A1: C = D ; ::_thesis: incl C = (incl B) * (incl D) set X = [: the carrier of B, the carrier of B:]; set Y = [: the carrier of D, the carrier of D:]; A2: the carrier of D c= the carrier of B by ALTCAT_2:def_11; then A3: [: the carrier of D, the carrier of D:] c= [: the carrier of B, the carrier of B:] by ZFMISC_1:96; for i being set st i in [: the carrier of D, the carrier of D:] holds the MorphMap of (incl C) . i = (( the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D)) . i proof set dom2 = dom the MorphMap of (incl D); set dom1 = dom ( the MorphMap of (incl B) * the ObjectMap of (incl D)); set XX = the Arrows of B; set YY = the Arrows of D; let i be set ; ::_thesis: ( i in [: the carrier of D, the carrier of D:] implies the MorphMap of (incl C) . i = (( the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D)) . i ) A4: the MorphMap of (incl C) . i = (id the Arrows of C) . i by FUNCTOR0:def_28; A5: ( dom (( the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D)) = (dom the MorphMap of (incl D)) /\ (dom ( the MorphMap of (incl B) * the ObjectMap of (incl D))) & dom the MorphMap of (incl D) = [: the carrier of D, the carrier of D:] ) by PARTFUN1:def_2, PBOOLE:def_19; A6: dom ( the MorphMap of (incl B) * the ObjectMap of (incl D)) = dom ( the MorphMap of (incl B) * (id [: the carrier of D, the carrier of D:])) by FUNCTOR0:def_28 .= (dom the MorphMap of (incl B)) /\ [: the carrier of D, the carrier of D:] by FUNCT_1:19 .= [: the carrier of B, the carrier of B:] /\ [: the carrier of D, the carrier of D:] by PARTFUN1:def_2 .= [: the carrier of D, the carrier of D:] by A2, XBOOLE_1:28, ZFMISC_1:96 ; assume A7: i in [: the carrier of D, the carrier of D:] ; ::_thesis: the MorphMap of (incl C) . i = (( the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D)) . i then A8: i in dom (id [: the carrier of D, the carrier of D:]) ; the Arrows of D cc= the Arrows of B by ALTCAT_2:def_11; then A9: the Arrows of D . i c= the Arrows of B . i by A7, ALTCAT_2:def_2; A10: ( the MorphMap of (incl B) * the ObjectMap of (incl D)) . i = ( the MorphMap of (incl B) * (id [: the carrier of D, the carrier of D:])) . i by FUNCTOR0:def_28 .= the MorphMap of (incl B) . ((id [: the carrier of D, the carrier of D:]) . i) by A8, FUNCT_1:13 .= the MorphMap of (incl B) . i by A7, FUNCT_1:18 ; ( the MorphMap of (incl B) . i = (id the Arrows of B) . i & the MorphMap of (incl D) . i = (id the Arrows of D) . i ) by FUNCTOR0:def_28; then ( the MorphMap of (incl B) . i) * ( the MorphMap of (incl D) . i) = ((id the Arrows of B) . i) * (id ( the Arrows of D . i)) by A7, MSUALG_3:def_1 .= (id ( the Arrows of B . i)) * (id ( the Arrows of D . i)) by A3, A7, MSUALG_3:def_1 .= id (( the Arrows of B . i) /\ ( the Arrows of D . i)) by FUNCT_1:22 .= id ( the Arrows of D . i) by A9, XBOOLE_1:28 .= the MorphMap of (incl C) . i by A1, A7, A4, MSUALG_3:def_1 ; hence the MorphMap of (incl C) . i = (( the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D)) . i by A7, A10, A5, A6, PBOOLE:def_19; ::_thesis: verum end; then A11: the MorphMap of (incl C) = ( the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D) by A1, PBOOLE:3; the ObjectMap of (incl C) = id [: the carrier of D, the carrier of D:] by A1, FUNCTOR0:def_28 .= id ([: the carrier of B, the carrier of B:] /\ [: the carrier of D, the carrier of D:]) by A2, XBOOLE_1:28, ZFMISC_1:96 .= (id [: the carrier of B, the carrier of B:]) * (id [: the carrier of D, the carrier of D:]) by FUNCT_1:22 .= (id [: the carrier of B, the carrier of B:]) * the ObjectMap of (incl D) by FUNCTOR0:def_28 .= the ObjectMap of (incl B) * the ObjectMap of (incl D) by FUNCTOR0:def_28 ; hence incl C = (incl B) * (incl D) by A1, A11, FUNCTOR0:def_36; ::_thesis: verum end; theorem Th5: :: FUNCTOR1:5 for A, B being non empty AltCatStr for F being FunctorStr over A,B st F is bijective holds ( the ObjectMap of F is bijective & the MorphMap of F is "1-1" ) proof let A, B be non empty AltCatStr ; ::_thesis: for F being FunctorStr over A,B st F is bijective holds ( the ObjectMap of F is bijective & the MorphMap of F is "1-1" ) let F be FunctorStr over A,B; ::_thesis: ( F is bijective implies ( the ObjectMap of F is bijective & the MorphMap of F is "1-1" ) ) assume A1: F is bijective ; ::_thesis: ( the ObjectMap of F is bijective & the MorphMap of F is "1-1" ) then A2: F is injective by FUNCTOR0:def_35; then F is one-to-one by FUNCTOR0:def_33; then A3: the ObjectMap of F is one-to-one by FUNCTOR0:def_6; F is surjective by A1, FUNCTOR0:def_35; then F is onto by FUNCTOR0:def_34; then A4: the ObjectMap of F is onto by FUNCTOR0:def_7; F is faithful by A2, FUNCTOR0:def_33; hence ( the ObjectMap of F is bijective & the MorphMap of F is "1-1" ) by A3, A4, FUNCTOR0:def_30; ::_thesis: verum end; theorem Th6: :: FUNCTOR1:6 for C1 being non empty AltGraph for C2, C3 being non empty reflexive AltGraph for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is one-to-one & G is one-to-one holds G * F is one-to-one proof let C1 be non empty AltGraph ; ::_thesis: for C2, C3 being non empty reflexive AltGraph for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is one-to-one & G is one-to-one holds G * F is one-to-one let C2, C3 be non empty reflexive AltGraph ; ::_thesis: for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is one-to-one & G is one-to-one holds G * F is one-to-one let F be feasible FunctorStr over C1,C2; ::_thesis: for G being FunctorStr over C2,C3 st F is one-to-one & G is one-to-one holds G * F is one-to-one let G be FunctorStr over C2,C3; ::_thesis: ( F is one-to-one & G is one-to-one implies G * F is one-to-one ) assume ( F is one-to-one & G is one-to-one ) ; ::_thesis: G * F is one-to-one then A1: ( the ObjectMap of F is one-to-one & the ObjectMap of G is one-to-one ) by FUNCTOR0:def_6; the ObjectMap of (G * F) = the ObjectMap of G * the ObjectMap of F by FUNCTOR0:def_36; hence the ObjectMap of (G * F) is one-to-one by A1; :: according to FUNCTOR0:def_6 ::_thesis: verum end; theorem Th7: :: FUNCTOR1:7 for C1 being non empty AltGraph for C2, C3 being non empty reflexive AltGraph for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is faithful & G is faithful holds G * F is faithful proof let C1 be non empty AltGraph ; ::_thesis: for C2, C3 being non empty reflexive AltGraph for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is faithful & G is faithful holds G * F is faithful let C2, C3 be non empty reflexive AltGraph ; ::_thesis: for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is faithful & G is faithful holds G * F is faithful let F be feasible FunctorStr over C1,C2; ::_thesis: for G being FunctorStr over C2,C3 st F is faithful & G is faithful holds G * F is faithful let G be FunctorStr over C2,C3; ::_thesis: ( F is faithful & G is faithful implies G * F is faithful ) assume that A1: F is faithful and A2: G is faithful ; ::_thesis: G * F is faithful set MMG = the MorphMap of G; A3: the MorphMap of G is "1-1" by A2, FUNCTOR0:def_30; set MMF = the MorphMap of F; set CC2 = [: the carrier of C2, the carrier of C2:]; set CC1 = [: the carrier of C1, the carrier of C1:]; reconsider MMGF = the MorphMap of (G * F) as ManySortedFunction of [: the carrier of C1, the carrier of C1:] ; reconsider OMF = the ObjectMap of F as Function of [: the carrier of C1, the carrier of C1:],[: the carrier of C2, the carrier of C2:] ; A4: MMGF = ( the MorphMap of G * OMF) ** the MorphMap of F by FUNCTOR0:def_36; A5: the MorphMap of F is "1-1" by A1, FUNCTOR0:def_30; for i being set st i in [: the carrier of C1, the carrier of C1:] holds MMGF . i is one-to-one proof let i be set ; ::_thesis: ( i in [: the carrier of C1, the carrier of C1:] implies MMGF . i is one-to-one ) assume A6: i in [: the carrier of C1, the carrier of C1:] ; ::_thesis: MMGF . i is one-to-one then i in dom (( the MorphMap of G * OMF) ** the MorphMap of F) by PARTFUN1:def_2; then A7: MMGF . i = (( the MorphMap of G * OMF) . i) * ( the MorphMap of F . i) by A4, PBOOLE:def_19 .= ( the MorphMap of G . (OMF . i)) * ( the MorphMap of F . i) by A6, FUNCT_2:15 ; OMF . i in [: the carrier of C2, the carrier of C2:] by A6, FUNCT_2:5; then A8: the MorphMap of G . (OMF . i) is one-to-one by A3, MSUALG_3:1; the MorphMap of F . i is one-to-one by A5, A6, MSUALG_3:1; hence MMGF . i is one-to-one by A7, A8; ::_thesis: verum end; hence the MorphMap of (G * F) is "1-1" by MSUALG_3:1; :: according to FUNCTOR0:def_30 ::_thesis: verum end; theorem Th8: :: FUNCTOR1:8 for C1 being non empty AltGraph for C2, C3 being non empty reflexive AltGraph for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is onto & G is onto holds G * F is onto proof let C1 be non empty AltGraph ; ::_thesis: for C2, C3 being non empty reflexive AltGraph for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is onto & G is onto holds G * F is onto let C2, C3 be non empty reflexive AltGraph ; ::_thesis: for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is onto & G is onto holds G * F is onto let F be feasible FunctorStr over C1,C2; ::_thesis: for G being FunctorStr over C2,C3 st F is onto & G is onto holds G * F is onto let G be FunctorStr over C2,C3; ::_thesis: ( F is onto & G is onto implies G * F is onto ) assume that A1: F is onto and A2: G is onto ; ::_thesis: G * F is onto set CC3 = [: the carrier of C3, the carrier of C3:]; set CC2 = [: the carrier of C2, the carrier of C2:]; reconsider OMG = the ObjectMap of G as Function of [: the carrier of C2, the carrier of C2:],[: the carrier of C3, the carrier of C3:] ; OMG is onto by A2, FUNCTOR0:def_7; then A3: rng OMG = [: the carrier of C3, the carrier of C3:] by FUNCT_2:def_3; set CC1 = [: the carrier of C1, the carrier of C1:]; reconsider OMF = the ObjectMap of F as Function of [: the carrier of C1, the carrier of C1:],[: the carrier of C2, the carrier of C2:] ; OMF is onto by A1, FUNCTOR0:def_7; then rng OMF = [: the carrier of C2, the carrier of C2:] by FUNCT_2:def_3; then rng (OMG * OMF) = [: the carrier of C3, the carrier of C3:] by A3, FUNCT_2:14; then OMG * OMF is onto by FUNCT_2:def_3; hence the ObjectMap of (G * F) is onto by FUNCTOR0:def_36; :: according to FUNCTOR0:def_7 ::_thesis: verum end; theorem Th9: :: FUNCTOR1:9 for C1 being non empty AltGraph for C2, C3 being non empty reflexive AltGraph for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is full & G is full holds G * F is full proof let C1 be non empty AltGraph ; ::_thesis: for C2, C3 being non empty reflexive AltGraph for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is full & G is full holds G * F is full let C2, C3 be non empty reflexive AltGraph ; ::_thesis: for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is full & G is full holds G * F is full let F be feasible FunctorStr over C1,C2; ::_thesis: for G being FunctorStr over C2,C3 st F is full & G is full holds G * F is full let G be FunctorStr over C2,C3; ::_thesis: ( F is full & G is full implies G * F is full ) assume that A1: F is full and A2: G is full ; ::_thesis: G * F is full set CC3 = [: the carrier of C3, the carrier of C3:]; set CC2 = [: the carrier of C2, the carrier of C2:]; set CC1 = [: the carrier of C1, the carrier of C1:]; reconsider OMF = the ObjectMap of F as Function of [: the carrier of C1, the carrier of C1:],[: the carrier of C2, the carrier of C2:] ; reconsider OMG = the ObjectMap of G as Function of [: the carrier of C2, the carrier of C2:],[: the carrier of C3, the carrier of C3:] ; consider MMF being ManySortedFunction of the Arrows of C1, the Arrows of C2 * the ObjectMap of F such that A3: MMF = the MorphMap of F and A4: MMF is "onto" by A1, FUNCTOR0:def_32; consider MMG being ManySortedFunction of the Arrows of C2, the Arrows of C3 * the ObjectMap of G such that A5: MMG = the MorphMap of G and A6: MMG is "onto" by A2, FUNCTOR0:def_32; ex f being ManySortedFunction of the Arrows of C1, the Arrows of C3 * the ObjectMap of (G * F) st ( f = the MorphMap of (G * F) & f is "onto" ) proof reconsider MMGF = the MorphMap of (G * F) as ManySortedFunction of the Arrows of C1, the Arrows of C3 * the ObjectMap of (G * F) by FUNCTOR0:def_4; take MMGF ; ::_thesis: ( MMGF = the MorphMap of (G * F) & MMGF is "onto" ) A7: MMGF = (MMG * OMF) ** MMF by A3, A5, FUNCTOR0:def_36; for i being set st i in [: the carrier of C1, the carrier of C1:] holds rng (MMGF . i) = ( the Arrows of C3 * the ObjectMap of (G * F)) . i proof let i be set ; ::_thesis: ( i in [: the carrier of C1, the carrier of C1:] implies rng (MMGF . i) = ( the Arrows of C3 * the ObjectMap of (G * F)) . i ) assume A8: i in [: the carrier of C1, the carrier of C1:] ; ::_thesis: rng (MMGF . i) = ( the Arrows of C3 * the ObjectMap of (G * F)) . i then reconsider MMGI = MMG . (OMF . i) as Function of ( the Arrows of C2 . (OMF . i)),(( the Arrows of C3 * the ObjectMap of G) . (OMF . i)) by FUNCT_2:5, PBOOLE:def_15; A9: OMF . i in [: the carrier of C2, the carrier of C2:] by A8, FUNCT_2:5; A10: rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i)) proof percases ( rng MMGI = {} or rng MMGI <> {} ) ; supposeA11: rng MMGI = {} ; ::_thesis: rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i)) rng ({} * (MMF . i)) = {} ; hence rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i)) by A11, RELAT_1:41; ::_thesis: verum end; supposeA12: rng MMGI <> {} ; ::_thesis: rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i)) rng MMGI = ( the Arrows of C3 * the ObjectMap of G) . (OMF . i) by A6, A9, MSUALG_3:def_3; then dom MMGI = the Arrows of C2 . (OMF . i) by A12, FUNCT_2:def_1; then dom MMGI = ( the Arrows of C2 * OMF) . i by A8, FUNCT_2:15 .= rng (MMF . i) by A4, A8, MSUALG_3:def_3 ; hence rng ((MMG . (OMF . i)) * (MMF . i)) = rng (MMG . (OMF . i)) by RELAT_1:28; ::_thesis: verum end; end; end; i in dom ((MMG * OMF) ** MMF) by A8, PARTFUN1:def_2; then rng (MMGF . i) = rng (((MMG * OMF) . i) * (MMF . i)) by A7, PBOOLE:def_19 .= rng (MMG . (OMF . i)) by A8, A10, FUNCT_2:15 .= ( the Arrows of C3 * the ObjectMap of G) . (OMF . i) by A6, A9, MSUALG_3:def_3 .= the Arrows of C3 . (OMG . (OMF . i)) by A8, FUNCT_2:5, FUNCT_2:15 .= the Arrows of C3 . ((OMG * OMF) . i) by A8, FUNCT_2:15 .= the Arrows of C3 . ( the ObjectMap of (G * F) . i) by FUNCTOR0:def_36 .= ( the Arrows of C3 * the ObjectMap of (G * F)) . i by A8, FUNCT_2:15 ; hence rng (MMGF . i) = ( the Arrows of C3 * the ObjectMap of (G * F)) . i ; ::_thesis: verum end; hence ( MMGF = the MorphMap of (G * F) & MMGF is "onto" ) by MSUALG_3:def_3; ::_thesis: verum end; hence G * F is full by FUNCTOR0:def_32; ::_thesis: verum end; theorem Th10: :: FUNCTOR1:10 for C1 being non empty AltGraph for C2, C3 being non empty reflexive AltGraph for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is injective & G is injective holds G * F is injective proof let C1 be non empty AltGraph ; ::_thesis: for C2, C3 being non empty reflexive AltGraph for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is injective & G is injective holds G * F is injective let C2, C3 be non empty reflexive AltGraph ; ::_thesis: for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is injective & G is injective holds G * F is injective let F be feasible FunctorStr over C1,C2; ::_thesis: for G being FunctorStr over C2,C3 st F is injective & G is injective holds G * F is injective let G be FunctorStr over C2,C3; ::_thesis: ( F is injective & G is injective implies G * F is injective ) assume A1: ( F is injective & G is injective ) ; ::_thesis: G * F is injective then ( F is faithful & G is faithful ) by FUNCTOR0:def_33; then A2: G * F is faithful by Th7; ( F is one-to-one & G is one-to-one ) by A1, FUNCTOR0:def_33; then G * F is one-to-one by Th6; hence G * F is injective by A2, FUNCTOR0:def_33; ::_thesis: verum end; theorem Th11: :: FUNCTOR1:11 for C1 being non empty AltGraph for C2, C3 being non empty reflexive AltGraph for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is surjective & G is surjective holds G * F is surjective proof let C1 be non empty AltGraph ; ::_thesis: for C2, C3 being non empty reflexive AltGraph for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is surjective & G is surjective holds G * F is surjective let C2, C3 be non empty reflexive AltGraph ; ::_thesis: for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is surjective & G is surjective holds G * F is surjective let F be feasible FunctorStr over C1,C2; ::_thesis: for G being FunctorStr over C2,C3 st F is surjective & G is surjective holds G * F is surjective let G be FunctorStr over C2,C3; ::_thesis: ( F is surjective & G is surjective implies G * F is surjective ) assume A1: ( F is surjective & G is surjective ) ; ::_thesis: G * F is surjective then ( F is onto & G is onto ) by FUNCTOR0:def_34; then A2: G * F is onto by Th8; ( F is full & G is full ) by A1, FUNCTOR0:def_34; then G * F is full by Th9; hence G * F is surjective by A2, FUNCTOR0:def_34; ::_thesis: verum end; theorem Th12: :: FUNCTOR1:12 for C1 being non empty AltGraph for C2, C3 being non empty reflexive AltGraph for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is bijective & G is bijective holds G * F is bijective proof let C1 be non empty AltGraph ; ::_thesis: for C2, C3 being non empty reflexive AltGraph for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is bijective & G is bijective holds G * F is bijective let C2, C3 be non empty reflexive AltGraph ; ::_thesis: for F being feasible FunctorStr over C1,C2 for G being FunctorStr over C2,C3 st F is bijective & G is bijective holds G * F is bijective let F be feasible FunctorStr over C1,C2; ::_thesis: for G being FunctorStr over C2,C3 st F is bijective & G is bijective holds G * F is bijective let G be FunctorStr over C2,C3; ::_thesis: ( F is bijective & G is bijective implies G * F is bijective ) assume A1: ( F is bijective & G is bijective ) ; ::_thesis: G * F is bijective then ( F is surjective & G is surjective ) by FUNCTOR0:def_35; then A2: G * F is surjective by Th11; ( F is injective & G is injective ) by A1, FUNCTOR0:def_35; then G * F is injective by Th10; hence G * F is bijective by A2, FUNCTOR0:def_35; ::_thesis: verum end; begin theorem :: FUNCTOR1:13 for A, I being non empty reflexive AltCatStr for B being non empty reflexive SubCatStr of A for C being non empty SubCatStr of A for D being non empty SubCatStr of B st C = D holds for F being FunctorStr over A,I holds F | C = (F | B) | D proof let A, I be non empty reflexive AltCatStr ; ::_thesis: for B being non empty reflexive SubCatStr of A for C being non empty SubCatStr of A for D being non empty SubCatStr of B st C = D holds for F being FunctorStr over A,I holds F | C = (F | B) | D let B be non empty reflexive SubCatStr of A; ::_thesis: for C being non empty SubCatStr of A for D being non empty SubCatStr of B st C = D holds for F being FunctorStr over A,I holds F | C = (F | B) | D let C be non empty SubCatStr of A; ::_thesis: for D being non empty SubCatStr of B st C = D holds for F being FunctorStr over A,I holds F | C = (F | B) | D let D be non empty SubCatStr of B; ::_thesis: ( C = D implies for F being FunctorStr over A,I holds F | C = (F | B) | D ) assume A1: C = D ; ::_thesis: for F being FunctorStr over A,I holds F | C = (F | B) | D let F be FunctorStr over A,I; ::_thesis: F | C = (F | B) | D thus F | C = F * ((incl B) * (incl D)) by A1, Th4 .= (F | B) | D by FUNCTOR0:32 ; ::_thesis: verum end; theorem :: FUNCTOR1:14 for A being non empty AltCatStr for B being non empty SubCatStr of A holds ( B is full iff incl B is full ) proof let A be non empty AltCatStr ; ::_thesis: for B being non empty SubCatStr of A holds ( B is full iff incl B is full ) let B be non empty SubCatStr of A; ::_thesis: ( B is full iff incl B is full ) hereby ::_thesis: ( incl B is full implies B is full ) ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of [: the carrier of B, the carrier of B:],I29 st ( the ObjectMap of (incl B) = f9 & the Arrows of A = B9 & the MorphMap of (incl B) is ManySortedFunction of the Arrows of B,B9 * f9 ) by FUNCTOR0:def_3; then reconsider f = the MorphMap of (incl B) as ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (incl B) ; set I = [: the carrier of B, the carrier of B:]; ( the carrier of B c= the carrier of A & dom the Arrows of A = [: the carrier of A, the carrier of A:] ) by ALTCAT_2:def_11, PARTFUN1:def_2; then A1: (dom the Arrows of A) /\ [: the carrier of B, the carrier of B:] = [: the carrier of B, the carrier of B:] by XBOOLE_1:28, ZFMISC_1:96; assume A2: B is full ; ::_thesis: incl B is full f is "onto" proof let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in [: the carrier of B, the carrier of B:] or rng (f . i) = ( the Arrows of A * the ObjectMap of (incl B)) . i ) assume A3: i in [: the carrier of B, the carrier of B:] ; ::_thesis: rng (f . i) = ( the Arrows of A * the ObjectMap of (incl B)) . i the Arrows of B = the Arrows of A || the carrier of B by A2, ALTCAT_2:def_13; then A4: the Arrows of B . i = the Arrows of A . i by A3, FUNCT_1:49; rng (f . i) = rng ((id the Arrows of B) . i) by FUNCTOR0:def_28 .= rng (id ( the Arrows of B . i)) by A3, MSUALG_3:def_1 .= the Arrows of A . i by A4 .= ( the Arrows of A * (id [: the carrier of B, the carrier of B:])) . i by A1, A3, FUNCT_1:20 .= ( the Arrows of A * the ObjectMap of (incl B)) . i by FUNCTOR0:def_28 ; hence rng (f . i) = ( the Arrows of A * the ObjectMap of (incl B)) . i ; ::_thesis: verum end; hence incl B is full by FUNCTOR0:def_32; ::_thesis: verum end; set I = [: the carrier of B, the carrier of B:]; A5: the carrier of B c= the carrier of A by ALTCAT_2:def_11; then A6: [: the carrier of B, the carrier of B:] c= [: the carrier of A, the carrier of A:] by ZFMISC_1:96; dom the Arrows of A = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2; then A7: (dom the Arrows of A) /\ [: the carrier of B, the carrier of B:] = [: the carrier of B, the carrier of B:] by A5, XBOOLE_1:28, ZFMISC_1:96; then dom ( the Arrows of A | [: the carrier of B, the carrier of B:]) = [: the carrier of B, the carrier of B:] by RELAT_1:61; then reconsider XX = the Arrows of A || the carrier of B as ManySortedSet of [: the carrier of B, the carrier of B:] by PARTFUN1:def_2; assume A8: incl B is full ; ::_thesis: B is full A9: XX c= the Arrows of B proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in [: the carrier of B, the carrier of B:] or XX . i c= the Arrows of B . i ) assume A10: i in [: the carrier of B, the carrier of B:] ; ::_thesis: XX . i c= the Arrows of B . i let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in XX . i or x in the Arrows of B . i ) assume A11: x in XX . i ; ::_thesis: x in the Arrows of B . i x in the Arrows of B . i proof consider f being ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (incl B) such that A12: f = the MorphMap of (incl B) and A13: f is "onto" by A8, FUNCTOR0:def_32; f = id the Arrows of B by A12, FUNCTOR0:def_28; then A14: rng ((id the Arrows of B) . i) = ( the Arrows of A * the ObjectMap of (incl B)) . i by A10, A13, MSUALG_3:def_3 .= ( the Arrows of A * (id [: the carrier of B, the carrier of B:])) . i by FUNCTOR0:def_28 .= the Arrows of A . i by A7, A10, FUNCT_1:20 ; consider y, z being set such that y in the carrier of A and z in the carrier of A and A15: i = [y,z] by A6, A10, ZFMISC_1:84; ( y in the carrier of B & z in the carrier of B ) by A10, A15, ZFMISC_1:87; then A16: XX . (y,z) = the Arrows of A . (y,z) by A5, ALTCAT_1:5; rng ((id the Arrows of B) . i) = rng (id ( the Arrows of B . i)) by A10, MSUALG_3:def_1 .= the Arrows of B . i ; hence x in the Arrows of B . i by A11, A15, A16, A14; ::_thesis: verum end; hence x in the Arrows of B . i ; ::_thesis: verum end; the Arrows of B c= XX proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in [: the carrier of B, the carrier of B:] or the Arrows of B . i c= XX . i ) assume A17: i in [: the carrier of B, the carrier of B:] ; ::_thesis: the Arrows of B . i c= XX . i then consider y, z being set such that y in the carrier of A and z in the carrier of A and A18: i = [y,z] by A6, ZFMISC_1:84; ( y in the carrier of B & z in the carrier of B ) by A17, A18, ZFMISC_1:87; then A19: XX . (y,z) = the Arrows of A . (y,z) by A5, ALTCAT_1:5; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Arrows of B . i or x in XX . i ) assume A20: x in the Arrows of B . i ; ::_thesis: x in XX . i the Arrows of B cc= the Arrows of A by ALTCAT_2:def_11; then the Arrows of B . (y,z) c= the Arrows of A . (y,z) by A17, A18, ALTCAT_2:def_2; hence x in XX . i by A18, A20, A19; ::_thesis: verum end; hence the Arrows of B = the Arrows of A || the carrier of B by A9, PBOOLE:146; :: according to ALTCAT_2:def_13 ::_thesis: verum end; begin theorem :: FUNCTOR1:15 for C1, C2 being non empty AltCatStr for F being Covariant FunctorStr over C1,C2 holds ( F is full iff for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is onto ) proof let C1, C2 be non empty AltCatStr ; ::_thesis: for F being Covariant FunctorStr over C1,C2 holds ( F is full iff for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is onto ) let F be Covariant FunctorStr over C1,C2; ::_thesis: ( F is full iff for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is onto ) set I = [: the carrier of C1, the carrier of C1:]; hereby ::_thesis: ( ( for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is onto ) implies F is full ) assume F is full ; ::_thesis: for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is onto then consider f being ManySortedFunction of the Arrows of C1, the Arrows of C2 * the ObjectMap of F such that A1: f = the MorphMap of F and A2: f is "onto" by FUNCTOR0:def_32; let o1, o2 be object of C1; ::_thesis: Morph-Map (F,o1,o2) is onto A3: [o1,o2] in [: the carrier of C1, the carrier of C1:] by ZFMISC_1:87; then A4: [o1,o2] in dom the ObjectMap of F by FUNCT_2:def_1; rng (f . [o1,o2]) = ( the Arrows of C2 * the ObjectMap of F) . [o1,o2] by A2, A3, MSUALG_3:def_3; then rng (Morph-Map (F,o1,o2)) = the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) by A1, A4, FUNCT_1:13 .= the Arrows of C2 . ((F . o1),(F . o2)) by FUNCTOR0:22 .= <^(F . o1),(F . o2)^> by ALTCAT_1:def_1 ; hence Morph-Map (F,o1,o2) is onto by FUNCT_2:def_3; ::_thesis: verum end; ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of [: the carrier of C1, the carrier of C1:],I29 st ( the ObjectMap of F = f9 & the Arrows of C2 = B9 & the MorphMap of F is ManySortedFunction of the Arrows of C1,B9 * f9 ) by FUNCTOR0:def_3; then reconsider f = the MorphMap of F as ManySortedFunction of the Arrows of C1, the Arrows of C2 * the ObjectMap of F ; assume A5: for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is onto ; ::_thesis: F is full f is "onto" proof let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in [: the carrier of C1, the carrier of C1:] or rng (f . i) = ( the Arrows of C2 * the ObjectMap of F) . i ) assume i in [: the carrier of C1, the carrier of C1:] ; ::_thesis: rng (f . i) = ( the Arrows of C2 * the ObjectMap of F) . i then consider o1, o2 being set such that A6: ( o1 in the carrier of C1 & o2 in the carrier of C1 ) and A7: i = [o1,o2] by ZFMISC_1:84; reconsider o1 = o1, o2 = o2 as object of C1 by A6; [o1,o2] in [: the carrier of C1, the carrier of C1:] by ZFMISC_1:87; then A8: [o1,o2] in dom the ObjectMap of F by FUNCT_2:def_1; Morph-Map (F,o1,o2) is onto by A5; then rng (Morph-Map (F,o1,o2)) = <^(F . o1),(F . o2)^> by FUNCT_2:def_3 .= the Arrows of C2 . ((F . o1),(F . o2)) by ALTCAT_1:def_1 .= the Arrows of C2 . ( the ObjectMap of F . (o1,o2)) by FUNCTOR0:22 .= ( the Arrows of C2 * the ObjectMap of F) . (o1,o2) by A8, FUNCT_1:13 ; hence rng (f . i) = ( the Arrows of C2 * the ObjectMap of F) . i by A7; ::_thesis: verum end; hence ex f being ManySortedFunction of the Arrows of C1, the Arrows of C2 * the ObjectMap of F st ( f = the MorphMap of F & f is "onto" ) ; :: according to FUNCTOR0:def_32 ::_thesis: verum end; theorem :: FUNCTOR1:16 for C1, C2 being non empty AltCatStr for F being Covariant FunctorStr over C1,C2 holds ( F is faithful iff for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is one-to-one ) proof let C1, C2 be non empty AltCatStr ; ::_thesis: for F being Covariant FunctorStr over C1,C2 holds ( F is faithful iff for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is one-to-one ) let F be Covariant FunctorStr over C1,C2; ::_thesis: ( F is faithful iff for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is one-to-one ) set I = [: the carrier of C1, the carrier of C1:]; hereby ::_thesis: ( ( for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is one-to-one ) implies F is faithful ) assume F is faithful ; ::_thesis: for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is one-to-one then A1: the MorphMap of F is "1-1" by FUNCTOR0:def_30; let o1, o2 be object of C1; ::_thesis: Morph-Map (F,o1,o2) is one-to-one ( [o1,o2] in [: the carrier of C1, the carrier of C1:] & dom the MorphMap of F = [: the carrier of C1, the carrier of C1:] ) by PARTFUN1:def_2, ZFMISC_1:87; hence Morph-Map (F,o1,o2) is one-to-one by A1, MSUALG_3:def_2; ::_thesis: verum end; assume A2: for o1, o2 being object of C1 holds Morph-Map (F,o1,o2) is one-to-one ; ::_thesis: F is faithful let i be set ; :: according to MSUALG_3:def_2,FUNCTOR0:def_30 ::_thesis: for b1 being set holds ( not i in dom the MorphMap of F or not the MorphMap of F . i = b1 or b1 is one-to-one ) let f be Function; ::_thesis: ( not i in dom the MorphMap of F or not the MorphMap of F . i = f or f is one-to-one ) assume that A3: i in dom the MorphMap of F and A4: the MorphMap of F . i = f ; ::_thesis: f is one-to-one dom the MorphMap of F = [: the carrier of C1, the carrier of C1:] by PARTFUN1:def_2; then consider o1, o2 being set such that A5: ( o1 in the carrier of C1 & o2 in the carrier of C1 ) and A6: i = [o1,o2] by A3, ZFMISC_1:84; reconsider o1 = o1, o2 = o2 as object of C1 by A5; the MorphMap of F . (o1,o2) = Morph-Map (F,o1,o2) ; hence f is one-to-one by A2, A4, A6; ::_thesis: verum end; begin theorem :: FUNCTOR1:17 for A being non empty transitive with_units AltCatStr holds (id A) " = id A proof let A be non empty transitive with_units AltCatStr ; ::_thesis: (id A) " = id A set CCA = [: the carrier of A, the carrier of A:]; consider f being ManySortedFunction of the Arrows of A, the Arrows of A * the ObjectMap of (id A) such that A1: f = the MorphMap of (id A) and A2: the MorphMap of ((id A) ") = (f "") * ( the ObjectMap of (id A) ") by FUNCTOR0:def_38; A3: for i being set st i in [: the carrier of A, the carrier of A:] holds (id the Arrows of A) . i is one-to-one proof let i be set ; ::_thesis: ( i in [: the carrier of A, the carrier of A:] implies (id the Arrows of A) . i is one-to-one ) assume A4: i in [: the carrier of A, the carrier of A:] ; ::_thesis: (id the Arrows of A) . i is one-to-one id ( the Arrows of A . i) is one-to-one ; hence (id the Arrows of A) . i is one-to-one by A4, MSUALG_3:def_1; ::_thesis: verum end; the MorphMap of (id A) = id the Arrows of A by FUNCTOR0:def_29; then A5: the MorphMap of (id A) is "1-1" by A3, MSUALG_3:1; for i being set st i in [: the carrier of A, the carrier of A:] holds rng (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i proof dom the Arrows of A = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2; then A6: (dom the Arrows of A) /\ [: the carrier of A, the carrier of A:] = [: the carrier of A, the carrier of A:] ; let i be set ; ::_thesis: ( i in [: the carrier of A, the carrier of A:] implies rng (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i ) assume A7: i in [: the carrier of A, the carrier of A:] ; ::_thesis: rng (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i rng (f . i) = rng ((id the Arrows of A) . i) by A1, FUNCTOR0:def_29 .= rng (id ( the Arrows of A . i)) by A7, MSUALG_3:def_1 .= the Arrows of A . i .= ( the Arrows of A * (id [: the carrier of A, the carrier of A:])) . i by A7, A6, FUNCT_1:20 .= ( the Arrows of A * the ObjectMap of (id A)) . i by FUNCTOR0:def_29 ; hence rng (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i ; ::_thesis: verum end; then A8: f is "onto" by MSUALG_3:def_3; for i being set st i in [: the carrier of A, the carrier of A:] holds (f "") . i = f . i proof let i be set ; ::_thesis: ( i in [: the carrier of A, the carrier of A:] implies (f "") . i = f . i ) assume A9: i in [: the carrier of A, the carrier of A:] ; ::_thesis: (f "") . i = f . i then (f "") . i = ( the MorphMap of (id A) . i) " by A1, A5, A8, MSUALG_3:def_4 .= ((id the Arrows of A) . i) " by FUNCTOR0:def_29 .= (id ( the Arrows of A . i)) " by A9, MSUALG_3:def_1 .= id ( the Arrows of A . i) by FUNCT_1:45 .= (id the Arrows of A) . i by A9, MSUALG_3:def_1 .= f . i by A1, FUNCTOR0:def_29 ; hence (f "") . i = f . i ; ::_thesis: verum end; then A10: f "" = f by PBOOLE:3; for i being set st i in [: the carrier of A, the carrier of A:] holds ( the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:])) . i = the MorphMap of (id A) . i proof dom the MorphMap of (id A) = [: the carrier of A, the carrier of A:] by PARTFUN1:def_2; then A11: (dom the MorphMap of (id A)) /\ [: the carrier of A, the carrier of A:] = [: the carrier of A, the carrier of A:] ; let i be set ; ::_thesis: ( i in [: the carrier of A, the carrier of A:] implies ( the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:])) . i = the MorphMap of (id A) . i ) assume i in [: the carrier of A, the carrier of A:] ; ::_thesis: ( the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:])) . i = the MorphMap of (id A) . i hence ( the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:])) . i = the MorphMap of (id A) . i by A11, FUNCT_1:20; ::_thesis: verum end; then A12: the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:]) = the MorphMap of (id A) by PBOOLE:3; A13: the ObjectMap of ((id A) ") = the ObjectMap of (id A) " by FUNCTOR0:def_38; then the ObjectMap of ((id A) ") = (id [: the carrier of A, the carrier of A:]) " by FUNCTOR0:def_29 .= id [: the carrier of A, the carrier of A:] by FUNCT_1:45 .= the ObjectMap of (id A) by FUNCTOR0:def_29 ; hence (id A) " = id A by A13, A1, A2, A10, A12, FUNCTOR0:def_29; ::_thesis: verum end; theorem :: FUNCTOR1:18 for A, B being non empty transitive with_units reflexive AltCatStr for F being feasible FunctorStr over A,B st F is bijective holds for G being feasible FunctorStr over B,A st FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " holds F * G = id B proof let A, B be non empty transitive with_units reflexive AltCatStr ; ::_thesis: for F being feasible FunctorStr over A,B st F is bijective holds for G being feasible FunctorStr over B,A st FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " holds F * G = id B set I1 = [: the carrier of A, the carrier of A:]; set I2 = [: the carrier of B, the carrier of B:]; let F be feasible FunctorStr over A,B; ::_thesis: ( F is bijective implies for G being feasible FunctorStr over B,A st FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " holds F * G = id B ) assume A1: F is bijective ; ::_thesis: for G being feasible FunctorStr over B,A st FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " holds F * G = id B consider k being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that A2: k = the MorphMap of F and A3: the MorphMap of (F ") = (k "") * ( the ObjectMap of F ") by A1, FUNCTOR0:def_38; F is injective by A1, FUNCTOR0:def_35; then F is one-to-one by FUNCTOR0:def_33; then A4: the ObjectMap of F is one-to-one by FUNCTOR0:def_6; set OM = the ObjectMap of F; F is surjective by A1, FUNCTOR0:def_35; then F is onto by FUNCTOR0:def_34; then the ObjectMap of F is onto by FUNCTOR0:def_7; then A5: rng the ObjectMap of F = [: the carrier of B, the carrier of B:] by FUNCT_2:def_3; F is injective by A1, FUNCTOR0:def_35; then A6: F is faithful by FUNCTOR0:def_33; then A7: the MorphMap of F is "1-1" by FUNCTOR0:def_30; F is surjective by A1, FUNCTOR0:def_35; then ( F is full & F is onto ) by FUNCTOR0:def_34; then consider f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that A8: f = the MorphMap of F and A9: f is "onto" by FUNCTOR0:def_32; let G be feasible FunctorStr over B,A; ::_thesis: ( FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " implies F * G = id B ) assume A10: FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " ; ::_thesis: F * G = id B A11: the ObjectMap of G = the ObjectMap of F " by A1, A10, FUNCTOR0:def_38; FunctorStr(# the ObjectMap of G, the MorphMap of G #) is bijective by A1, A10, FUNCTOR0:35; then FunctorStr(# the ObjectMap of G, the MorphMap of G #) is surjective by FUNCTOR0:def_35; then ( FunctorStr(# the ObjectMap of G, the MorphMap of G #) is full & FunctorStr(# the ObjectMap of G, the MorphMap of G #) is onto ) by FUNCTOR0:def_34; then A12: the ObjectMap of G is onto by FUNCTOR0:def_7; set OMG = the ObjectMap of G; A13: dom the ObjectMap of F = [: the carrier of A, the carrier of A:] by FUNCT_2:def_1; reconsider OM = the ObjectMap of F as bifunction of the carrier of A, the carrier of B ; A14: [: the carrier of B, the carrier of B:] = dom ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) by PARTFUN1:def_2; A15: for i being set st i in [: the carrier of B, the carrier of B:] holds ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i proof let i be set ; ::_thesis: ( i in [: the carrier of B, the carrier of B:] implies ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i ) assume A16: i in [: the carrier of B, the carrier of B:] ; ::_thesis: ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i A17: dom the ObjectMap of G = [: the carrier of B, the carrier of B:] by FUNCT_2:def_1; then A18: (f * the ObjectMap of G) . i = k . ( the ObjectMap of G . i) by A2, A8, A16, FUNCT_1:13; rng the ObjectMap of G = [: the carrier of A, the carrier of A:] by A12, FUNCT_2:def_3; then A19: the ObjectMap of G . i in [: the carrier of A, the carrier of A:] by A16, A17, FUNCT_1:def_3; then A20: rng (f . ( the ObjectMap of G . i)) = ( the Arrows of B * the ObjectMap of F) . ( the ObjectMap of G . i) by A9, MSUALG_3:def_3 .= the Arrows of B . ( the ObjectMap of F . ( the ObjectMap of G . i)) by A13, A19, FUNCT_1:13 ; A21: the ObjectMap of F . ( the ObjectMap of G . i) = (OM * (OM ")) . i by A11, A16, A17, FUNCT_1:13 .= (id [: the carrier of B, the carrier of B:]) . i by A4, A5, FUNCT_1:39 .= i by A16, FUNCT_1:18 ; ( f is "1-1" & dom f = [: the carrier of A, the carrier of A:] ) by A6, A8, FUNCTOR0:def_30, PARTFUN1:def_2; then A22: f . ( the ObjectMap of G . i) is one-to-one by A19, MSUALG_3:def_2; ((k "") * the ObjectMap of G) . i = (k "") . ( the ObjectMap of G . i) by A16, A17, FUNCT_1:13 .= (k . ( the ObjectMap of G . i)) " by A7, A2, A8, A9, A19, MSUALG_3:def_4 ; then ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (f . ( the ObjectMap of G . i)) * ((f . ( the ObjectMap of G . i)) ") by A2, A8, A14, A16, A18, PBOOLE:def_19 .= id ( the Arrows of B . i) by A22, A20, A21, FUNCT_1:39 .= (id the Arrows of B) . i by A16, MSUALG_3:def_1 ; hence ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i ; ::_thesis: verum end; the MorphMap of (F * G) = (f * the ObjectMap of G) ** ((k "") * the ObjectMap of G) by A10, A3, A8, A11, FUNCTOR0:def_36; then A23: the MorphMap of (F * G) = id the Arrows of B by A15, PBOOLE:3; the ObjectMap of (F * G) = the ObjectMap of F * the ObjectMap of G by FUNCTOR0:def_36; then the ObjectMap of (F * G) = the ObjectMap of F * ( the ObjectMap of F ") by A1, A10, FUNCTOR0:def_38; then the ObjectMap of (F * G) = id [: the carrier of B, the carrier of B:] by A4, A5, FUNCT_1:39; hence F * G = id B by A23, FUNCTOR0:def_29; ::_thesis: verum end; Lm1: for I being set for A, B being ManySortedSet of I st A is_transformable_to B holds for H being ManySortedFunction of A,B for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds ( H ** H1 = id B & H1 ** H = id A ) proof let I be set ; ::_thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds for H being ManySortedFunction of A,B for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds ( H ** H1 = id B & H1 ** H = id A ) let A, B be ManySortedSet of I; ::_thesis: ( A is_transformable_to B implies for H being ManySortedFunction of A,B for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds ( H ** H1 = id B & H1 ** H = id A ) ) assume A1: A is_transformable_to B ; ::_thesis: for H being ManySortedFunction of A,B for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds ( H ** H1 = id B & H1 ** H = id A ) let H be ManySortedFunction of A,B; ::_thesis: for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds ( H ** H1 = id B & H1 ** H = id A ) let H1 be ManySortedFunction of B,A; ::_thesis: ( H is "1-1" & H is "onto" & H1 = H "" implies ( H ** H1 = id B & H1 ** H = id A ) ) assume that A2: ( H is "1-1" & H is "onto" ) and A3: H1 = H "" ; ::_thesis: ( H ** H1 = id B & H1 ** H = id A ) reconsider F1 = H ** H1 as ManySortedFunction of I ; A4: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (H_**_H1)_._i_=_id_(B_._i) let i be set ; ::_thesis: ( i in I implies (H ** H1) . i = id (B . i) ) assume A5: i in I ; ::_thesis: (H ** H1) . i = id (B . i) then reconsider h = H . i as Function of (A . i),(B . i) by PBOOLE:def_15; reconsider h1 = H1 . i as Function of (B . i),(A . i) by A5, PBOOLE:def_15; i in dom H by A5, PARTFUN1:def_2; then A6: h is one-to-one by A2, MSUALG_3:def_2; h1 = h " by A2, A3, A5, MSUALG_3:def_4; then h * h1 = id (rng h) by A6, FUNCT_1:39; then h * h1 = id (B . i) by A2, A5, MSUALG_3:def_3; hence (H ** H1) . i = id (B . i) by A5, MSUALG_3:2; ::_thesis: verum end; now__::_thesis:_for_i_being_set_st_i_in_I_holds_ F1_._i_is_Function_of_(B_._i),(B_._i) let i be set ; ::_thesis: ( i in I implies F1 . i is Function of (B . i),(B . i) ) assume i in I ; ::_thesis: F1 . i is Function of (B . i),(B . i) then F1 . i = id (B . i) by A4; hence F1 . i is Function of (B . i),(B . i) ; ::_thesis: verum end; then A7: F1 is ManySortedFunction of B,B by PBOOLE:def_15; reconsider F = H1 ** H as ManySortedFunction of I ; A8: for i being set st i in I holds (H1 ** H) . i = id (A . i) proof let i be set ; ::_thesis: ( i in I implies (H1 ** H) . i = id (A . i) ) assume A9: i in I ; ::_thesis: (H1 ** H) . i = id (A . i) then reconsider h = H . i as Function of (A . i),(B . i) by PBOOLE:def_15; reconsider h1 = H1 . i as Function of (B . i),(A . i) by A9, PBOOLE:def_15; i in dom H by A9, PARTFUN1:def_2; then A10: h is one-to-one by A2, MSUALG_3:def_2; ( B . i = {} implies A . i = {} ) by A1, A9, PZFMISC1:def_3; then A11: dom h = A . i by FUNCT_2:def_1; h1 = h " by A2, A3, A9, MSUALG_3:def_4; then h1 * h = id (A . i) by A10, A11, FUNCT_1:39; hence (H1 ** H) . i = id (A . i) by A9, MSUALG_3:2; ::_thesis: verum end; now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (H1_**_H)_._i_is_Function_of_(A_._i),(A_._i) let i be set ; ::_thesis: ( i in I implies (H1 ** H) . i is Function of (A . i),(A . i) ) assume i in I ; ::_thesis: (H1 ** H) . i is Function of (A . i),(A . i) then (H1 ** H) . i = id (A . i) by A8; hence (H1 ** H) . i is Function of (A . i),(A . i) ; ::_thesis: verum end; then reconsider F = F as ManySortedFunction of A,A by PBOOLE:def_15; F = id A by A8, MSUALG_3:def_1; hence ( H ** H1 = id B & H1 ** H = id A ) by A4, A7, MSUALG_3:def_1; ::_thesis: verum end; theorem :: FUNCTOR1:19 for A, B being non empty transitive with_units reflexive AltCatStr for F being feasible FunctorStr over A,B st F is bijective holds (F ") * F = id A proof let A, B be non empty transitive with_units reflexive AltCatStr ; ::_thesis: for F being feasible FunctorStr over A,B st F is bijective holds (F ") * F = id A set I1 = [: the carrier of A, the carrier of A:]; let F be feasible FunctorStr over A,B; ::_thesis: ( F is bijective implies (F ") * F = id A ) assume A1: F is bijective ; ::_thesis: (F ") * F = id A consider f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that A2: f = the MorphMap of F and A3: the MorphMap of (F ") = (f "") * ( the ObjectMap of F ") by A1, FUNCTOR0:def_38; set OM = the ObjectMap of F; A4: dom the ObjectMap of F = [: the carrier of A, the carrier of A:] by FUNCT_2:def_1; A5: the Arrows of A is_transformable_to the Arrows of B * the ObjectMap of F proof let i be set ; :: according to PZFMISC1:def_3 ::_thesis: ( not i in [: the carrier of A, the carrier of A:] or not ( the Arrows of B * the ObjectMap of F) . i = {} or the Arrows of A . i = {} ) assume A6: i in [: the carrier of A, the carrier of A:] ; ::_thesis: ( not ( the Arrows of B * the ObjectMap of F) . i = {} or the Arrows of A . i = {} ) then consider o1, o2 being set such that A7: ( o1 in the carrier of A & o2 in the carrier of A ) and A8: i = [o1,o2] by ZFMISC_1:84; reconsider o1 = o1, o2 = o2 as object of A by A7; A9: the Arrows of A . i = the Arrows of A . (o1,o2) by A8 .= <^o1,o2^> by ALTCAT_1:def_1 ; assume ( the Arrows of B * the ObjectMap of F) . i = {} ; ::_thesis: the Arrows of A . i = {} then the Arrows of B . ( the ObjectMap of F . (o1,o2)) = {} by A6, A8, FUNCT_2:15; hence the Arrows of A . i = {} by A9, FUNCTOR0:def_11; ::_thesis: verum end; F is injective by A1, FUNCTOR0:def_35; then F is faithful by FUNCTOR0:def_33; then A10: the MorphMap of F is "1-1" by FUNCTOR0:def_30; for i being set st i in [: the carrier of A, the carrier of A:] holds ((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . i proof let i be set ; ::_thesis: ( i in [: the carrier of A, the carrier of A:] implies ((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . i ) assume A11: i in [: the carrier of A, the carrier of A:] ; ::_thesis: ((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . i then ((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . ((id [: the carrier of A, the carrier of A:]) . i) by FUNCT_2:15 .= (f "") . i by A11, FUNCT_1:18 ; hence ((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . i ; ::_thesis: verum end; then A12: (f "") * (id [: the carrier of A, the carrier of A:]) = f "" by PBOOLE:3; F is injective by A1, FUNCTOR0:def_35; then F is one-to-one by FUNCTOR0:def_33; then A13: the ObjectMap of F is one-to-one by FUNCTOR0:def_6; the ObjectMap of ((F ") * F) = the ObjectMap of (F ") * the ObjectMap of F by FUNCTOR0:def_36; then the ObjectMap of ((F ") * F) = ( the ObjectMap of F ") * the ObjectMap of F by A1, FUNCTOR0:def_38; then A14: the ObjectMap of ((F ") * F) = id [: the carrier of A, the carrier of A:] by A13, A4, FUNCT_1:39; F is surjective by A1, FUNCTOR0:def_35; then ( F is full & F is onto ) by FUNCTOR0:def_34; then A15: ex k being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( k = the MorphMap of F & k is "onto" ) by FUNCTOR0:def_32; the MorphMap of ((F ") * F) = (((f "") * ( the ObjectMap of F ")) * the ObjectMap of F) ** f by A2, A3, FUNCTOR0:def_36 .= ((f "") * (( the ObjectMap of F ") * the ObjectMap of F)) ** f by RELAT_1:36 ; then the MorphMap of ((F ") * F) = ((f "") * (id [: the carrier of A, the carrier of A:])) ** f by A13, A4, FUNCT_1:39; then the MorphMap of ((F ") * F) = id the Arrows of A by A5, A2, A10, A15, A12, Lm1; hence (F ") * F = id A by A14, FUNCTOR0:def_29; ::_thesis: verum end; theorem :: FUNCTOR1:20 for A, B being non empty transitive with_units reflexive AltCatStr for F being feasible FunctorStr over A,B st F is bijective holds (F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #) proof let A, B be non empty transitive with_units reflexive AltCatStr ; ::_thesis: for F being feasible FunctorStr over A,B st F is bijective holds (F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #) set CCA = [: the carrier of A, the carrier of A:]; set CCB = [: the carrier of B, the carrier of B:]; let F be feasible FunctorStr over A,B; ::_thesis: ( F is bijective implies (F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #) ) assume A1: F is bijective ; ::_thesis: (F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #) A2: F is injective by A1, FUNCTOR0:def_35; then F is one-to-one by FUNCTOR0:def_33; then A3: the ObjectMap of F is one-to-one by FUNCTOR0:def_6; A4: F " is bijective by A1, FUNCTOR0:35; then F " is surjective by FUNCTOR0:def_35; then A5: F " is full by FUNCTOR0:def_34; F " is injective by A4, FUNCTOR0:def_35; then A6: F " is faithful by FUNCTOR0:def_33; A7: the ObjectMap of (F ") " = ( the ObjectMap of F ") " by A1, FUNCTOR0:def_38 .= the ObjectMap of F by A3, FUNCT_1:43 ; F is faithful by A2, FUNCTOR0:def_33; then A8: the MorphMap of F is "1-1" by FUNCTOR0:def_30; A9: F is surjective by A1, FUNCTOR0:def_35; then F is onto by FUNCTOR0:def_34; then the ObjectMap of F is onto by FUNCTOR0:def_7; then A10: rng the ObjectMap of F = [: the carrier of B, the carrier of B:] by FUNCT_2:def_3; A11: F is full by A9, FUNCTOR0:def_34; the MorphMap of ((F ") ") = the MorphMap of F proof A12: ex kk being ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") st ( kk = the MorphMap of (F ") & kk is "onto" ) by A5, FUNCTOR0:def_32; A13: ex k being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st ( k = the MorphMap of F & k is "onto" ) by A11, FUNCTOR0:def_32; consider f being ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") such that A14: f = the MorphMap of (F ") and A15: the MorphMap of ((F ") ") = (f "") * ( the ObjectMap of (F ") ") by A4, FUNCTOR0:def_38; consider g being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that A16: g = the MorphMap of F and A17: the MorphMap of (F ") = (g "") * ( the ObjectMap of F ") by A1, FUNCTOR0:def_38; A18: f is "1-1" by A6, A14, FUNCTOR0:def_30; for i being set st i in [: the carrier of A, the carrier of A:] holds ((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i proof A19: the ObjectMap of F " is Function of [: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:] by A3, A10, FUNCT_2:25; let i be set ; ::_thesis: ( i in [: the carrier of A, the carrier of A:] implies ((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i ) assume A20: i in [: the carrier of A, the carrier of A:] ; ::_thesis: ((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i then A21: the ObjectMap of F . i in [: the carrier of B, the carrier of B:] by FUNCT_2:5; the ObjectMap of F " is Function of [: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:] by A3, A10, FUNCT_2:25; then A22: ( the ObjectMap of F ") . ( the ObjectMap of F . i) in [: the carrier of A, the carrier of A:] by A21, FUNCT_2:5; A23: g . i is one-to-one by A8, A16, A20, MSUALG_3:1; ((f "") * ( the ObjectMap of (F ") ")) . i = (f "") . ( the ObjectMap of F . i) by A7, A20, FUNCT_2:15 .= ( the MorphMap of (F ") . ( the ObjectMap of F . i)) " by A14, A12, A18, A21, MSUALG_3:def_4 .= ((g "") . (( the ObjectMap of F ") . ( the ObjectMap of F . i))) " by A17, A20, A19, FUNCT_2:5, FUNCT_2:15 .= ((g . (( the ObjectMap of F ") . ( the ObjectMap of F . i))) ") " by A8, A16, A13, A22, MSUALG_3:def_4 .= ((g . i) ") " by A3, A20, FUNCT_2:26 .= the MorphMap of F . i by A16, A23, FUNCT_1:43 ; hence ((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i ; ::_thesis: verum end; hence the MorphMap of ((F ") ") = the MorphMap of F by A15, PBOOLE:3; ::_thesis: verum end; hence (F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #) by A4, A7, FUNCTOR0:def_38; ::_thesis: verum end; theorem :: FUNCTOR1:21 for A, B, C being non empty transitive with_units reflexive AltCatStr for G being feasible FunctorStr over A,B for F being feasible FunctorStr over B,C for GI being feasible FunctorStr over B,A for FI being feasible FunctorStr over C,B st F is bijective & G is bijective & FunctorStr(# the ObjectMap of GI, the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI, the MorphMap of FI #) = F " holds (F * G) " = GI * FI proof let A, B, C be non empty transitive with_units reflexive AltCatStr ; ::_thesis: for G being feasible FunctorStr over A,B for F being feasible FunctorStr over B,C for GI being feasible FunctorStr over B,A for FI being feasible FunctorStr over C,B st F is bijective & G is bijective & FunctorStr(# the ObjectMap of GI, the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI, the MorphMap of FI #) = F " holds (F * G) " = GI * FI let G be feasible FunctorStr over A,B; ::_thesis: for F being feasible FunctorStr over B,C for GI being feasible FunctorStr over B,A for FI being feasible FunctorStr over C,B st F is bijective & G is bijective & FunctorStr(# the ObjectMap of GI, the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI, the MorphMap of FI #) = F " holds (F * G) " = GI * FI let F be feasible FunctorStr over B,C; ::_thesis: for GI being feasible FunctorStr over B,A for FI being feasible FunctorStr over C,B st F is bijective & G is bijective & FunctorStr(# the ObjectMap of GI, the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI, the MorphMap of FI #) = F " holds (F * G) " = GI * FI let GI be feasible FunctorStr over B,A; ::_thesis: for FI being feasible FunctorStr over C,B st F is bijective & G is bijective & FunctorStr(# the ObjectMap of GI, the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI, the MorphMap of FI #) = F " holds (F * G) " = GI * FI let FI be feasible FunctorStr over C,B; ::_thesis: ( F is bijective & G is bijective & FunctorStr(# the ObjectMap of GI, the MorphMap of GI #) = G " & FunctorStr(# the ObjectMap of FI, the MorphMap of FI #) = F " implies (F * G) " = GI * FI ) assume that A1: F is bijective and A2: G is bijective and A3: FunctorStr(# the ObjectMap of GI, the MorphMap of GI #) = G " and A4: FunctorStr(# the ObjectMap of FI, the MorphMap of FI #) = F " ; ::_thesis: (F * G) " = GI * FI reconsider MF = the MorphMap of F as ManySortedFunction of the Arrows of B, the Arrows of C * the ObjectMap of F by FUNCTOR0:def_4; A5: MF is "1-1" by A1, Th5; set OG = the ObjectMap of G; set CB = [: the carrier of B, the carrier of B:]; set CA = [: the carrier of A, the carrier of A:]; reconsider OGI = the ObjectMap of G " as Function of [: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:] by A2, Th2, Th5; set CC = [: the carrier of C, the carrier of C:]; set OF = the ObjectMap of F; reconsider OFI = the ObjectMap of F " as Function of [: the carrier of C, the carrier of C:],[: the carrier of B, the carrier of B:] by A1, Th2, Th5; reconsider MFG = the MorphMap of (F * G) as ManySortedFunction of the Arrows of A, the Arrows of C * the ObjectMap of (F * G) by FUNCTOR0:def_4; reconsider OG = the ObjectMap of G as Function of [: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:] ; reconsider OFG = the ObjectMap of (F * G) as Function of [: the carrier of A, the carrier of A:],[: the carrier of C, the carrier of C:] ; reconsider MG = the MorphMap of G as ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of G by FUNCTOR0:def_4; A6: MG is "1-1" by A2, Th5; F is surjective by A1, FUNCTOR0:def_35; then F is full by FUNCTOR0:def_34; then A7: ex mf being ManySortedFunction of the Arrows of B, the Arrows of C * the ObjectMap of F st ( mf = the MorphMap of F & mf is "onto" ) by FUNCTOR0:def_32; F is injective by A1, FUNCTOR0:def_35; then F is one-to-one by FUNCTOR0:def_33; then A8: the ObjectMap of F is one-to-one by FUNCTOR0:def_6; A9: G is surjective by A2, FUNCTOR0:def_35; then G is onto by FUNCTOR0:def_34; then A10: the ObjectMap of G is onto by FUNCTOR0:def_7; G is full by A9, FUNCTOR0:def_34; then A11: ex mg being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of G st ( mg = the MorphMap of G & mg is "onto" ) by FUNCTOR0:def_32; G is injective by A2, FUNCTOR0:def_35; then G is one-to-one by FUNCTOR0:def_33; then A12: the ObjectMap of G is one-to-one by FUNCTOR0:def_6; A13: F * G is bijective by A1, A2, Th12; then F * G is surjective by FUNCTOR0:def_35; then F * G is full by FUNCTOR0:def_34; then A14: ex mfg being ManySortedFunction of the Arrows of A, the Arrows of C * the ObjectMap of (F * G) st ( mfg = the MorphMap of (F * G) & mfg is "onto" ) by FUNCTOR0:def_32; A15: MFG is "1-1" by A13, Th5; A16: the MorphMap of ((F * G) ") = the MorphMap of (GI * FI) proof consider f being ManySortedFunction of the Arrows of A, the Arrows of C * the ObjectMap of (F * G) such that A17: f = the MorphMap of (F * G) and A18: the MorphMap of ((F * G) ") = (f "") * ( the ObjectMap of (F * G) ") by A13, FUNCTOR0:def_38; A19: rng the ObjectMap of G = [: the carrier of B, the carrier of B:] by A10, FUNCT_2:def_3; for i being set st i in [: the carrier of C, the carrier of C:] holds ((f "") * ( the ObjectMap of (F * G) ")) . i = (( the MorphMap of (G ") * the ObjectMap of (F ")) ** the MorphMap of (F ")) . i proof A20: ( ex x1 being ManySortedFunction of the Arrows of B, the Arrows of C * the ObjectMap of F st ( x1 = the MorphMap of F & the MorphMap of (F ") = (x1 "") * ( the ObjectMap of F ") ) & ex x1 being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of G st ( x1 = the MorphMap of G & the MorphMap of (G ") = (x1 "") * ( the ObjectMap of G ") ) ) by A1, A2, FUNCTOR0:def_38; A21: ( the ObjectMap of F " = the ObjectMap of (F ") & dom ((((MG "") * OGI) * OFI) ** ((MF "") * OFI)) = [: the carrier of C, the carrier of C:] ) by A1, FUNCTOR0:def_38, PARTFUN1:def_2; A22: OG * (OG ") = id [: the carrier of B, the carrier of B:] by A12, A19, FUNCT_2:29; A23: OFG " = ( the ObjectMap of F * OG) " by FUNCTOR0:def_36 .= (OG ") * ( the ObjectMap of F ") by A8, A12, FUNCT_1:44 ; let i be set ; ::_thesis: ( i in [: the carrier of C, the carrier of C:] implies ((f "") * ( the ObjectMap of (F * G) ")) . i = (( the MorphMap of (G ") * the ObjectMap of (F ")) ** the MorphMap of (F ")) . i ) assume A24: i in [: the carrier of C, the carrier of C:] ; ::_thesis: ((f "") * ( the ObjectMap of (F * G) ")) . i = (( the MorphMap of (G ") * the ObjectMap of (F ")) ** the MorphMap of (F ")) . i A25: ((MF . (OG . (((OG ") * ( the ObjectMap of F ")) . i))) * (MG . ((OFG ") . i))) " = ((MF . (OG . (OGI . (OFI . i)))) * (MG . ((OFG ") . i))) " by A24, FUNCT_2:15 .= ((MF . ((OG * OGI) . (OFI . i))) * (MG . ((OFG ") . i))) " by A24, FUNCT_2:5, FUNCT_2:15 .= ((MF . (((id [: the carrier of B, the carrier of B:]) * OFI) . i)) * (MG . ((OFG ") . i))) " by A24, A22, FUNCT_2:15 .= ((MF . (( the ObjectMap of F ") . i)) * (MG . ((OGI * OFI) . i))) " by A23, FUNCT_2:17 ; OFG " is Function of [: the carrier of C, the carrier of C:],[: the carrier of A, the carrier of A:] by A13, Th2, Th5; then A26: ( dom ((MF * OG) ** MG) = [: the carrier of A, the carrier of A:] & (OFG ") . i in [: the carrier of A, the carrier of A:] ) by A24, FUNCT_2:5, PARTFUN1:def_2; A27: the ObjectMap of (F * G) " is Function of [: the carrier of C, the carrier of C:],[: the carrier of A, the carrier of A:] by A13, Th2, Th5; then A28: ( the ObjectMap of (F * G) ") . i in [: the carrier of A, the carrier of A:] by A24, FUNCT_2:5; i in dom ( the ObjectMap of (F * G) ") by A24, A27, FUNCT_2:def_1; then A29: ((f "") * ( the ObjectMap of (F * G) ")) . i = (MFG "") . (( the ObjectMap of (F * G) ") . i) by A17, FUNCT_1:13 .= (MFG . (( the ObjectMap of (F * G) ") . i)) " by A14, A15, A28, MSUALG_3:def_4 .= (((MF * OG) ** MG) . ((OFG ") . i)) " by FUNCTOR0:def_36 .= (((MF * OG) . ((OFG ") . i)) * (MG . ((OFG ") . i))) " by A26, PBOOLE:def_19 .= ((MF . (OG . (((OG ") * ( the ObjectMap of F ")) . i))) * (MG . ((OFG ") . i))) " by A24, A27, A23, FUNCT_2:5, FUNCT_2:15 ; A30: OFI . i in [: the carrier of B, the carrier of B:] by A24, FUNCT_2:5; then A31: MF . (OFI . i) is one-to-one by A5, MSUALG_3:1; A32: OGI . (OFI . i) in [: the carrier of A, the carrier of A:] by A30, FUNCT_2:5; then A33: MG . (OGI . (OFI . i)) is one-to-one by A6, MSUALG_3:1; ((MF . (( the ObjectMap of F ") . i)) * (MG . ((OGI * OFI) . i))) " = ((MF . (( the ObjectMap of F ") . i)) * (MG . (OGI . (OFI . i)))) " by A24, FUNCT_2:15 .= ((MG . (OGI . (OFI . i))) ") * ((MF . (OFI . i)) ") by A33, A31, FUNCT_1:44 .= ((MG "") . (OGI . (OFI . i))) * ((MF . (( the ObjectMap of F ") . i)) ") by A11, A6, A32, MSUALG_3:def_4 .= (((MG "") * OGI) . (OFI . i)) * ((MF . (( the ObjectMap of F ") . i)) ") by A24, FUNCT_2:5, FUNCT_2:15 .= ((((MG "") * OGI) * OFI) . i) * ((MF . (OFI . i)) ") by A24, FUNCT_2:15 .= ((((MG "") * OGI) * OFI) . i) * ((MF "") . (OFI . i)) by A5, A7, A30, MSUALG_3:def_4 .= ((((MG "") * OGI) * OFI) . i) * (((MF "") * OFI) . i) by A24, FUNCT_2:15 ; hence ((f "") * ( the ObjectMap of (F * G) ")) . i = (( the MorphMap of (G ") * the ObjectMap of (F ")) ** the MorphMap of (F ")) . i by A20, A24, A21, A29, A25, PBOOLE:def_19; ::_thesis: verum end; then the MorphMap of ((F * G) ") = ( the MorphMap of GI * the ObjectMap of FI) ** the MorphMap of FI by A3, A4, A18, PBOOLE:3 .= the MorphMap of (GI * FI) by FUNCTOR0:def_36 ; hence the MorphMap of ((F * G) ") = the MorphMap of (GI * FI) ; ::_thesis: verum end; the ObjectMap of ((F * G) ") = the ObjectMap of (F * G) " by A13, FUNCTOR0:def_38 .= ( the ObjectMap of F * the ObjectMap of G) " by FUNCTOR0:def_36 .= ( the ObjectMap of G ") * ( the ObjectMap of F ") by A8, A12, FUNCT_1:44 .= the ObjectMap of GI * ( the ObjectMap of F ") by A2, A3, FUNCTOR0:def_38 .= the ObjectMap of GI * the ObjectMap of FI by A1, A4, FUNCTOR0:def_38 .= the ObjectMap of (GI * FI) by FUNCTOR0:def_36 ; hence (F * G) " = GI * FI by A16; ::_thesis: verum end;