yellow20.miz

    begin

    reserve x,y for set;

    theorem :: YELLOW20:1



     Th1: for A,B be transitive with_units non empty AltCatStr holds for F be feasible reflexive FunctorStr over A, B st F is coreflexive bijective holds for a be Object of A, b be Object of B holds (F . a) = b iff ((F " ) . b) = a

    proof

      let A,B be transitive with_units non empty AltCatStr;

      let F be feasible reflexive FunctorStr over A, B such that

       A1: F is coreflexive bijective;

      reconsider G = (F " ) as feasible reflexive FunctorStr over B, A by A1, FUNCTOR0: 35, FUNCTOR0: 36;

      let a be Object of A, b be Object of B;

      ((F " ) * F) = ( id A) by A1, FUNCTOR1: 19;

      then a = (((F " ) * F) . a) by FUNCTOR0: 29;

      hence (F . a) = b implies ((F " ) . b) = a by FUNCTOR0: 33;

      (F * G) = ( id B) by A1, FUNCTOR1: 18;

      then b = ((F * G) . b) by FUNCTOR0: 29;

      hence thesis by FUNCTOR0: 33;

    end;

    theorem :: YELLOW20:2



     Th2: for A,B be transitive with_units non empty AltCatStr holds for F be Covariant feasible FunctorStr over A, B holds for G be Covariant feasible FunctorStr over B, A st F is bijective & G = (F " ) holds for a1,a2 be Object of A st <^a1, a2^> <> {} holds for f be Morphism of a1, a2, g be Morphism of (F . a1), (F . a2) holds (F . f) = g iff (G . g) = f

    proof

      let A,B be transitive with_units non empty AltCatStr;

      let F be Covariant feasible FunctorStr over A, B;

      let G be Covariant feasible FunctorStr over B, A such that

       A1: F is bijective and

       A2: G = (F " );

      let a1,a2 be Object of A such that

       A3: <^a1, a2^> <> {} ;



       A4: <^(F . a1), (F . a2)^> <> {} by A3, FUNCTOR0:def 18;

      F is surjective by A1;

      then F is onto;

      then F is reflexive coreflexive by FUNCTOR0: 44;

      then

       A5: (G . (F . a1)) = a1 & (G . (F . a2)) = a2 by A1, A2, Th1;

      let f be Morphism of a1, a2, g be Morphism of (F . a1), (F . a2);

      ((F " ) * F) = ( id A) by A1, FUNCTOR1: 19;

      then f = ((G * F) . f) by A2, A3, FUNCTOR0: 31;

      hence (F . f) = g implies (G . g) = f by A3, FUNCTOR3: 6;

      (F * G) = ( id B) by A1, A2, FUNCTOR1: 18;

      then g = ((F * G) . g) by A4, FUNCTOR0: 31;

      hence thesis by A4, A5, FUNCTOR3: 6;

    end;

    theorem :: YELLOW20:3



     Th3: for A,B be transitive with_units non empty AltCatStr holds for F be Contravariant feasible FunctorStr over A, B holds for G be Contravariant feasible FunctorStr over B, A st F is bijective & G = (F " ) holds for a1,a2 be Object of A st <^a1, a2^> <> {} holds for f be Morphism of a1, a2, g be Morphism of (F . a2), (F . a1) holds (F . f) = g iff (G . g) = f

    proof

      let A,B be transitive with_units non empty AltCatStr;

      let F be Contravariant feasible FunctorStr over A, B;

      let G be Contravariant feasible FunctorStr over B, A such that

       A1: F is bijective and

       A2: G = (F " );

      let a1,a2 be Object of A such that

       A3: <^a1, a2^> <> {} ;



       A4: <^(F . a2), (F . a1)^> <> {} by A3, FUNCTOR0:def 19;

      F is surjective by A1;

      then F is onto;

      then F is reflexive coreflexive by FUNCTOR0: 45;

      then

       A5: (G . (F . a1)) = a1 & (G . (F . a2)) = a2 by A1, A2, Th1;

      let f be Morphism of a1, a2, g be Morphism of (F . a2), (F . a1);

      ((F " ) * F) = ( id A) by A1, FUNCTOR1: 19;

      then f = ((G * F) . f) by A2, A3, FUNCTOR0: 31;

      hence (F . f) = g implies (G . g) = f by A3, FUNCTOR3: 7;

      (F * G) = ( id B) by A1, A2, FUNCTOR1: 18;

      then g = ((F * G) . g) by A4, FUNCTOR0: 31;

      hence thesis by A4, A5, FUNCTOR3: 7;

    end;

    theorem :: YELLOW20:4



     Th4: for A,B be category, F be Functor of A, B st F is bijective holds for G be Functor of B, A st (F * G) = ( id B) holds the FunctorStr of G = (F " )

    proof

      let A,B be category, F be Functor of A, B;

      assume

       A1: F is bijective;

      then

      reconsider FF = (F " ) as feasible FunctorStr over B, A by FUNCTOR0: 35;



       A2: ((F " ) * F) = ( id A) by A1, FUNCTOR1: 19;

      let G be Functor of B, A;

      assume (F * G) = ( id B);



      then (( id A) * G) = (FF * ( id B)) by A2, FUNCTOR0: 32

      .= (F " ) by FUNCTOR3: 5;

      hence thesis by FUNCTOR3: 4;

    end;

    theorem :: YELLOW20:5



     Th5: for A,B be category, F be Functor of A, B st F is bijective holds for G be Functor of B, A st (G * F) = ( id A) holds the FunctorStr of G = (F " )

    proof

      let A,B be category, F be Functor of A, B;

      assume

       A1: F is bijective;

      then

      reconsider FF = (F " ) as feasible FunctorStr over B, A by FUNCTOR0: 35;



       A2: (F * FF) = ( id B) by A1, FUNCTOR1: 18;

      let G be Functor of B, A;

      assume (G * F) = ( id A);



      then (( id A) * FF) = (G * ( id B)) by A2, FUNCTOR0: 32

      .= the FunctorStr of G by FUNCTOR3: 5;

      hence thesis by FUNCTOR3: 4;

    end;

    theorem :: YELLOW20:6

    for A,B be category, F be covariant Functor of A, B st F is bijective holds for G be covariant Functor of B, A st (for b be Object of B holds (F . (G . b)) = b) & (for a,b be Object of B st <^a, b^> <> {} holds for f be Morphism of a, b holds (F . (G . f)) = f) holds the FunctorStr of G = (F " )

    proof

      let A,B be category, F be covariant Functor of A, B such that

       A1: F is bijective;

      let G be covariant Functor of B, A such that

       A2: for b be Object of B holds (F . (G . b)) = b and

       A3: for a,b be Object of B st <^a, b^> <> {} holds for f be Morphism of a, b holds (F . (G . f)) = f;

       A4:

      now

        let a,b be Object of B such that

         A5: <^a, b^> <> {} ;

        let f be Morphism of a, b;



        thus ((F * G) . f) = (F . (G . f)) by A5, FUNCTOR3: 6

        .= f by A3, A5

        .= (( id B) . f) by A5, FUNCTOR0: 31;

      end;

      now

        let b be Object of B;



        thus ((F * G) . b) = (F . (G . b)) by FUNCTOR0: 33

        .= b by A2

        .= (( id B) . b) by FUNCTOR0: 29;

      end;

      hence thesis by A1, A4, Th4, YELLOW18: 1;

    end;

    theorem :: YELLOW20:7

    for A,B be category, F be contravariant Functor of A, B st F is bijective holds for G be contravariant Functor of B, A st (for b be Object of B holds (F . (G . b)) = b) & (for a,b be Object of B st <^a, b^> <> {} holds for f be Morphism of a, b holds (F . (G . f)) = f) holds the FunctorStr of G = (F " )

    proof

      let A,B be category, F be contravariant Functor of A, B such that

       A1: F is bijective;

      let G be contravariant Functor of B, A such that

       A2: for b be Object of B holds (F . (G . b)) = b and

       A3: for a,b be Object of B st <^a, b^> <> {} holds for f be Morphism of a, b holds (F . (G . f)) = f;

       A4:

      now

        let a,b be Object of B such that

         A5: <^a, b^> <> {} ;

        let f be Morphism of a, b;



        thus ((F * G) . f) = (F . (G . f)) by A5, FUNCTOR3: 7

        .= f by A3, A5

        .= (( id B) . f) by A5, FUNCTOR0: 31;

      end;

      now

        let b be Object of B;



        thus ((F * G) . b) = (F . (G . b)) by FUNCTOR0: 33

        .= b by A2

        .= (( id B) . b) by FUNCTOR0: 29;

      end;

      hence thesis by A1, A4, Th4, YELLOW18: 1;

    end;

    theorem :: YELLOW20:8

    for A,B be category, F be covariant Functor of A, B st F is bijective holds for G be covariant Functor of B, A st (for a be Object of A holds (G . (F . a)) = a) & (for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds (G . (F . f)) = f) holds the FunctorStr of G = (F " )

    proof

      let A,B be category, F be covariant Functor of A, B such that

       A1: F is bijective;

      let G be covariant Functor of B, A such that

       A2: for b be Object of A holds (G . (F . b)) = b and

       A3: for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds (G . (F . f)) = f;

       A4:

      now

        let a,b be Object of A such that

         A5: <^a, b^> <> {} ;

        let f be Morphism of a, b;



        thus ((G * F) . f) = (G . (F . f)) by A5, FUNCTOR3: 6

        .= f by A3, A5

        .= (( id A) . f) by A5, FUNCTOR0: 31;

      end;

      now

        let b be Object of A;



        thus ((G * F) . b) = (G . (F . b)) by FUNCTOR0: 33

        .= b by A2

        .= (( id A) . b) by FUNCTOR0: 29;

      end;

      hence thesis by A1, A4, Th5, YELLOW18: 1;

    end;

    theorem :: YELLOW20:9

    for A,B be category, F be contravariant Functor of A, B st F is bijective holds for G be contravariant Functor of B, A st (for a be Object of A holds (G . (F . a)) = a) & (for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds (G . (F . f)) = f) holds the FunctorStr of G = (F " )

    proof

      let A,B be category, F be contravariant Functor of A, B such that

       A1: F is bijective;

      let G be contravariant Functor of B, A such that

       A2: for b be Object of A holds (G . (F . b)) = b and

       A3: for a,b be Object of A st <^a, b^> <> {} holds for f be Morphism of a, b holds (G . (F . f)) = f;

       A4:

      now

        let a,b be Object of A such that

         A5: <^a, b^> <> {} ;

        let f be Morphism of a, b;



        thus ((G * F) . f) = (G . (F . f)) by A5, FUNCTOR3: 7

        .= f by A3, A5

        .= (( id A) . f) by A5, FUNCTOR0: 31;

      end;

      now

        let b be Object of A;



        thus ((G * F) . b) = (G . (F . b)) by FUNCTOR0: 33

        .= b by A2

        .= (( id A) . b) by FUNCTOR0: 29;

      end;

      hence thesis by A1, A4, Th5, YELLOW18: 1;

    end;

    begin

    definition

      let A,B be AltCatStr;

      :: YELLOW20:def1

      pred A,B have_the_same_composition means for a1,a2,a3 be object holds (the Comp of A . [a1, a2, a3]) tolerates (the Comp of B . [a1, a2, a3]);

      symmetry ;

    end

    theorem :: YELLOW20:10



     Th10: for A,B be AltCatStr holds (A,B) have_the_same_composition iff for a1,a2,a3,x be object st x in ( dom (the Comp of A . [a1, a2, a3])) & x in ( dom (the Comp of B . [a1, a2, a3])) holds ((the Comp of A . [a1, a2, a3]) . x) = ((the Comp of B . [a1, a2, a3]) . x)

    proof

      let A,B be AltCatStr;

      hereby

        assume

         A1: (A,B) have_the_same_composition ;

        let a1,a2,a3,x be object;

        assume x in ( dom (the Comp of A . [a1, a2, a3])) & x in ( dom (the Comp of B . [a1, a2, a3]));

        then

         A2: x in (( dom (the Comp of A . [a1, a2, a3])) /\ ( dom (the Comp of B . [a1, a2, a3]))) by XBOOLE_0:def 4;

        (the Comp of A . [a1, a2, a3]) tolerates (the Comp of B . [a1, a2, a3]) by A1;

        hence ((the Comp of A . [a1, a2, a3]) . x) = ((the Comp of B . [a1, a2, a3]) . x) by A2;

      end;

      assume

       A3: for a1,a2,a3,x be object st x in ( dom (the Comp of A . [a1, a2, a3])) & x in ( dom (the Comp of B . [a1, a2, a3])) holds ((the Comp of A . [a1, a2, a3]) . x) = ((the Comp of B . [a1, a2, a3]) . x);

      let a1,a2,a3,x be object;

      assume x in (( dom (the Comp of A . [a1, a2, a3])) /\ ( dom (the Comp of B . [a1, a2, a3])));

      then x in ( dom (the Comp of A . [a1, a2, a3])) & x in ( dom (the Comp of B . [a1, a2, a3])) by XBOOLE_0:def 4;

      hence thesis by A3;

    end;

    theorem :: YELLOW20:11



     Th11: for A,B be transitive non empty AltCatStr holds (A,B) have_the_same_composition iff for a1,a2,a3 be Object of A st <^a1, a2^> <> {} & <^a2, a3^> <> {} holds for b1,b2,b3 be Object of B st <^b1, b2^> <> {} & <^b2, b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds for f1 be Morphism of a1, a2, g1 be Morphism of b1, b2 st g1 = f1 holds for f2 be Morphism of a2, a3, g2 be Morphism of b2, b3 st g2 = f2 holds (f2 * f1) = (g2 * g1)

    proof

      let A,B be transitive non empty AltCatStr;

      hereby

        assume

         A1: (A,B) have_the_same_composition ;

        let a1,a2,a3 be Object of A such that

         A2: <^a1, a2^> <> {} & <^a2, a3^> <> {} ;

        let b1,b2,b3 be Object of B such that

         A3: <^b1, b2^> <> {} & <^b2, b3^> <> {} and

         A4: b1 = a1 & b2 = a2 & b3 = a3;

        let f1 be Morphism of a1, a2, g1 be Morphism of b1, b2 such that

         A5: g1 = f1;

        let f2 be Morphism of a2, a3, g2 be Morphism of b2, b3 such that

         A6: g2 = f2;

         <^b1, b3^> <> {} by A3, ALTCAT_1:def 2;

        then ( dom (the Comp of B . (b1,b2,b3))) = [: <^b2, b3^>, <^b1, b2^>:] by FUNCT_2:def 1;

        then

         A7: [g2, g1] in ( dom (the Comp of B . (b1,b2,b3))) by A3, ZFMISC_1:def 2;

         <^a1, a3^> <> {} by A2, ALTCAT_1:def 2;

        then ( dom (the Comp of A . (a1,a2,a3))) = [: <^a2, a3^>, <^a1, a2^>:] by FUNCT_2:def 1;

        then

         A8: [f2, f1] in ( dom (the Comp of A . (a1,a2,a3))) by A2, ZFMISC_1:def 2;



         A9: (the Comp of A . (a1,a2,a3)) = (the Comp of A . [a1, a2, a3]) & (the Comp of B . (b1,b2,b3)) = (the Comp of B . [b1, b2, b3]) by MULTOP_1:def 1;



        thus (f2 * f1) = ((the Comp of A . (a1,a2,a3)) . (f2,f1)) by A2, ALTCAT_1:def 8

        .= ((the Comp of B . (b1,b2,b3)) . (g2,g1)) by A1, A4, A5, A6, A9, A8, A7, Th10

        .= (g2 * g1) by A3, ALTCAT_1:def 8;

      end;

      assume

       A10: for a1,a2,a3 be Object of A st <^a1, a2^> <> {} & <^a2, a3^> <> {} holds for b1,b2,b3 be Object of B st <^b1, b2^> <> {} & <^b2, b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds for f1 be Morphism of a1, a2, g1 be Morphism of b1, b2 st g1 = f1 holds for f2 be Morphism of a2, a3, g2 be Morphism of b2, b3 st g2 = f2 holds (f2 * f1) = (g2 * g1);

      let a1,a2,a3,x be object;

      assume

       A11: x in (( dom (the Comp of A . [a1, a2, a3])) /\ ( dom (the Comp of B . [a1, a2, a3])));

      then

       A12: x in ( dom (the Comp of A . [a1, a2, a3])) by XBOOLE_0:def 4;

      then [a1, a2, a3] in ( dom the Comp of A) by FUNCT_1:def 2, RELAT_1: 38;

      then

       A13: [a1, a2, a3] in [:the carrier of A, the carrier of A, the carrier of A:];



       A14: x in ( dom (the Comp of B . [a1, a2, a3])) by A11, XBOOLE_0:def 4;

      then [a1, a2, a3] in ( dom the Comp of B) by FUNCT_1:def 2, RELAT_1: 38;

      then

       A15: [a1, a2, a3] in [:the carrier of B, the carrier of B, the carrier of B:];

      reconsider a1, a2, a3 as Object of A by A13, MCART_1: 69;

      reconsider b1 = a1, b2 = a2, b3 = a3 as Object of B by A15, MCART_1: 69;



       A16: (the Comp of A . (a1,a2,a3)) = (the Comp of A . [a1, a2, a3]) by MULTOP_1:def 1;

      then [: <^a2, a3^>, <^a1, a2^>:] <> {} implies <^a1, a3^> <> {} by A11, XBOOLE_0:def 4;

      then ( dom (the Comp of A . (a1,a2,a3))) = [: <^a2, a3^>, <^a1, a2^>:] by FUNCT_2:def 1;

      then

      consider f2,f1 be object such that

       A17: f2 in <^a2, a3^> and

       A18: f1 in <^a1, a2^> and

       A19: x = [f2, f1] by A12, A16, ZFMISC_1:def 2;

      reconsider f1 as Morphism of a1, a2 by A18;

      reconsider f2 as Morphism of a2, a3 by A17;



       A20: (the Comp of B . (b1,b2,b3)) = (the Comp of B . [b1, b2, b3]) by MULTOP_1:def 1;

      then [: <^b2, b3^>, <^b1, b2^>:] <> {} implies <^b1, b3^> <> {} by A11, XBOOLE_0:def 4;

      then

       A21: ( dom (the Comp of B . (b1,b2,b3))) = [: <^b2, b3^>, <^b1, b2^>:] by FUNCT_2:def 1;

      then

       A22: f1 in <^b1, b2^> & f2 in <^b2, b3^> by A14, A20, A19, ZFMISC_1: 87;

      reconsider g2 = f2 as Morphism of b2, b3 by A14, A20, A21, A19, ZFMISC_1: 87;

      reconsider g1 = f1 as Morphism of b1, b2 by A14, A20, A21, A19, ZFMISC_1: 87;

      ((the Comp of A . [a1, a2, a3]) . x) = ((the Comp of A . (a1,a2,a3)) . (f2,f1)) by A19, MULTOP_1:def 1

      .= (f2 * f1) by A17, A18, ALTCAT_1:def 8

      .= (g2 * g1) by A10, A17, A18, A22

      .= ((the Comp of B . (b1,b2,b3)) . (g2,g1)) by A22, ALTCAT_1:def 8;

      hence thesis by A19, MULTOP_1:def 1;

    end;

    theorem :: YELLOW20:12

    for A,B be para-functional semi-functional category holds (A,B) have_the_same_composition

    proof

      let A,B be para-functional semi-functional category;

      now

        let a1,a2,a3 be Object of A such that

         A1: <^a1, a2^> <> {} and

         A2: <^a2, a3^> <> {} ;

        let b1,b2,b3 be Object of B such that

         A3: <^b1, b2^> <> {} & <^b2, b3^> <> {} and b1 = a1 and b2 = a2 and b3 = a3;

        let f1 be Morphism of a1, a2, g1 be Morphism of b1, b2 such that

         A4: g1 = f1;

        reconsider f = f1 as Function of ( the_carrier_of a1), ( the_carrier_of a2) by A1, YELLOW18: 34;

        let f2 be Morphism of a2, a3, g2 be Morphism of b2, b3 such that

         A5: g2 = f2;



         A6: <^b1, b3^> <> {} by A3, ALTCAT_1:def 2;

        reconsider g = f2 as Function of ( the_carrier_of a2), ( the_carrier_of a3) by A2, YELLOW18: 34;

         <^a1, a3^> <> {} by A1, A2, ALTCAT_1:def 2;



        hence (f2 * f1) = (g * f) by A1, A2, ALTCAT_1:def 12

        .= (g2 * g1) by A3, A4, A5, A6, ALTCAT_1:def 12;

      end;

      hence thesis by Th11;

    end;

    definition

      let f,g be Function;

      :: YELLOW20:def2

      func Intersect (f,g) -> Function means

      : Def2: ( dom it ) = (( dom f) /\ ( dom g)) & for x be object st x in (( dom f) /\ ( dom g)) holds (it . x) = ((f . x) /\ (g . x));

      existence

      proof

        deffunc F( object) = ((f . $1) /\ (g . $1));

        thus ex h be Function st ( dom h) = (( dom f) /\ ( dom g)) & for x be object st x in (( dom f) /\ ( dom g)) holds (h . x) = F(x) from FUNCT_1:sch 3;

      end;

      uniqueness

      proof

        let f1,f2 be Function such that

         A1: ( dom f1) = (( dom f) /\ ( dom g)) and

         A2: for x be object st x in (( dom f) /\ ( dom g)) holds (f1 . x) = ((f . x) /\ (g . x)) and

         A3: ( dom f2) = (( dom f) /\ ( dom g)) and

         A4: for x be object st x in (( dom f) /\ ( dom g)) holds (f2 . x) = ((f . x) /\ (g . x));

        now

          let x be object;

          assume

           A5: x in (( dom f) /\ ( dom g));

          then (f1 . x) = ((f . x) /\ (g . x)) by A2;

          hence (f1 . x) = (f2 . x) by A4, A5;

        end;

        hence thesis by A1, A3, FUNCT_1: 2;

      end;

      commutativity ;

    end

    theorem :: YELLOW20:13

    for I be set, A,B be ManySortedSet of I holds ( Intersect (A,B)) = (A (/\) B)

    proof

      let I be set, A,B be ManySortedSet of I;



       A1: ( dom A) = I & ( dom B) = I by PARTFUN1:def 2;

      then ( dom ( Intersect (A,B))) = (I /\ I) by Def2;

      then

      reconsider AB = ( Intersect (A,B)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

      (I /\ I) = I;

      then for i be object st i in I holds (AB . i) = ((A . i) /\ (B . i)) by A1, Def2;

      hence thesis by PBOOLE:def 5;

    end;

    theorem :: YELLOW20:14



     Th14: for I,J be set holds for A be ManySortedSet of I, B be ManySortedSet of J holds ( Intersect (A,B)) is ManySortedSet of (I /\ J)

    proof

      let I,J be set, A be ManySortedSet of I, B be ManySortedSet of J;

      ( dom A) = I & ( dom B) = J by PARTFUN1:def 2;

      then ( dom ( Intersect (A,B))) = (I /\ J) by Def2;

      hence thesis by PARTFUN1:def 2, RELAT_1:def 18;

    end;

    theorem :: YELLOW20:15



     Th15: for I,J be set holds for A be ManySortedSet of I, B be Function holds for C be ManySortedSet of J st C = ( Intersect (A,B)) holds C cc= A

    proof

      let I,J be set, A be ManySortedSet of I, B be Function;

      let C be ManySortedSet of J such that

       A1: C = ( Intersect (A,B));



       A2: ( dom A) = I by PARTFUN1:def 2;

      ( dom C) = J by PARTFUN1:def 2;

      then

       A3: J = (I /\ ( dom B)) by A1, A2, Def2;

      hence J c= I by XBOOLE_1: 17;

      let i be set;

      assume i in J;

      then (C . i) = ((A . i) /\ (B . i)) by A1, A2, A3, Def2;

      hence thesis by XBOOLE_1: 17;

    end;

    theorem :: YELLOW20:16



     Th16: for I1,I2 be set holds for A1,B1 be ManySortedSet of I1 holds for A2,B2 be ManySortedSet of I2 holds for A,B be ManySortedSet of (I1 /\ I2) st A = ( Intersect (A1,A2)) & B = ( Intersect (B1,B2)) holds for F be ManySortedFunction of A1, B1 holds for G be ManySortedFunction of A2, B2 st for x be set st x in ( dom F) & x in ( dom G) holds (F . x) tolerates (G . x) holds ( Intersect (F,G)) is ManySortedFunction of A, B

    proof

      let I1,I2 be set;

      let A1,B1 be ManySortedSet of I1;

      let A2,B2 be ManySortedSet of I2;

      let A,B be ManySortedSet of (I1 /\ I2) such that

       A1: A = ( Intersect (A1,A2)) & B = ( Intersect (B1,B2));

      let F be ManySortedFunction of A1, B1;

      let G be ManySortedFunction of A2, B2 such that

       A2: for x be set st x in ( dom F) & x in ( dom G) holds (F . x) tolerates (G . x);



       A3: ( dom B1) = I1 & ( dom B2) = I2 by PARTFUN1:def 2;

      reconsider H = ( Intersect (F,G)) as ManySortedSet of (I1 /\ I2) by Th14;



       A4: ( dom F) = I1 & ( dom G) = I2 by PARTFUN1:def 2;



       A5: ( dom A1) = I1 & ( dom A2) = I2 by PARTFUN1:def 2;

      H is ManySortedFunction of A, B

      proof

        let i be object;

        assume

         A6: i in (I1 /\ I2);

        then

         A7: (H . i) = ((F . i) /\ (G . i)) by A4, Def2;



         A8: i in I2 by A6, XBOOLE_0:def 4;

        then

         A9: (G . i) is Function of (A2 . i), (B2 . i) by PBOOLE:def 15;



         A10: (A . i) = ((A1 . i) /\ (A2 . i)) & (B . i) = ((B1 . i) /\ (B2 . i)) by A1, A5, A3, A6, Def2;



         A11: i in I1 by A6, XBOOLE_0:def 4;

        then (F . i) is Function of (A1 . i), (B1 . i) by PBOOLE:def 15;

        hence thesis by A2, A4, A11, A8, A10, A7, A9, FUNCT_2: 120;

      end;

      hence thesis;

    end;

    theorem :: YELLOW20:17



     Th17: for I,J be set holds for F be ManySortedSet of [:I, I:] holds for G be ManySortedSet of [:J, J:] holds ex H be ManySortedSet of [:(I /\ J), (I /\ J):] st H = ( Intersect (F,G)) & ( Intersect ( {|F|}, {|G|})) = {|H|}

    proof

      let I,J be set;

      let F be ManySortedSet of [:I, I:];

      let G be ManySortedSet of [:J, J:];



       A1: [:(I /\ J), (I /\ J):] = ( [:I, I:] /\ [:J, J:]) by ZFMISC_1: 100;

      then

      reconsider H = ( Intersect (F,G)) as ManySortedSet of [:(I /\ J), (I /\ J):] by Th14;

       [:I, I, I:] = [: [:I, I:], I:] & [:J, J, J:] = [: [:J, J:], J:] by ZFMISC_1:def 3;



      then

       A2: ( [:I, I, I:] /\ [:J, J, J:]) = [: [:(I /\ J), (I /\ J):], (I /\ J):] by A1, ZFMISC_1: 100

      .= [:(I /\ J), (I /\ J), (I /\ J):] by ZFMISC_1:def 3;



       A3: ( dom F) = [:I, I:] & ( dom G) = [:J, J:] by PARTFUN1:def 2;

       A4:

      now

        let x be object;

        assume

         A5: x in ( [:I, I, I:] /\ [:J, J, J:]);

        then

         A6: x in [:J, J, J:] by XBOOLE_0:def 4;

        x in [:I, I, I:] by A5, XBOOLE_0:def 4;

        then

        consider a,b,c be object such that

         A7: a in I and

         A8: b in I and

         A9: c in I and

         A10: x = [a, b, c] by MCART_1: 68;



         A11: c in J by A6, A10, MCART_1: 69;

        then

         A12: c in (I /\ J) by A9, XBOOLE_0:def 4;



         A13: a in J by A6, A10, MCART_1: 69;

        then

         A14: a in (I /\ J) by A7, XBOOLE_0:def 4;

        then

         A15: [a, c] in [:(I /\ J), (I /\ J):] by A12, ZFMISC_1: 87;



         A16: b in J by A6, A10, MCART_1: 69;

        then

         A17: ( {|G|} . (a,b,c)) = (G . (a,c)) by A13, A11, ALTCAT_1:def 3;



         A18: ( {|F|} . (a,b,c)) = (F . (a,c)) by A7, A8, A9, ALTCAT_1:def 3;

        b in (I /\ J) by A8, A16, XBOOLE_0:def 4;

        then ( {|H|} . (a,b,c)) = (H . (a,c)) by A14, A12, ALTCAT_1:def 3;



        hence ( {|H|} . x) = (H . [a, c]) by A10, MULTOP_1:def 1

        .= ((F . (a,c)) /\ (G . [a, c])) by A1, A3, A15, Def2

        .= (( {|F|} . x) /\ (G . (a,c))) by A10, A18, MULTOP_1:def 1

        .= (( {|F|} . x) /\ ( {|G|} . x)) by A10, A17, MULTOP_1:def 1;

      end;

      take H;

      thus H = ( Intersect (F,G));



       A19: ( dom {|H|}) = [:(I /\ J), (I /\ J), (I /\ J):] by PARTFUN1:def 2;

      ( dom {|F|}) = [:I, I, I:] & ( dom {|G|}) = [:J, J, J:] by PARTFUN1:def 2;

      hence thesis by A19, A2, A4, Def2;

    end;

    theorem :: YELLOW20:18



     Th18: for I,J be set holds for F1,F2 be ManySortedSet of [:I, I:] holds for G1,G2 be ManySortedSet of [:J, J:] holds ex H1,H2 be ManySortedSet of [:(I /\ J), (I /\ J):] st H1 = ( Intersect (F1,G1)) & H2 = ( Intersect (F2,G2)) & ( Intersect ( {|F1, F2|}, {|G1, G2|})) = {|H1, H2|}

    proof

      let I,J be set;

      let F1,F2 be ManySortedSet of [:I, I:];

      let G1,G2 be ManySortedSet of [:J, J:];



       A1: ( dom F2) = [:I, I:] & ( dom G2) = [:J, J:] by PARTFUN1:def 2;



       A2: [:(I /\ J), (I /\ J):] = ( [:I, I:] /\ [:J, J:]) by ZFMISC_1: 100;

      then

      reconsider H1 = ( Intersect (F1,G1)), H2 = ( Intersect (F2,G2)) as ManySortedSet of [:(I /\ J), (I /\ J):] by Th14;

       [:I, I, I:] = [: [:I, I:], I:] & [:J, J, J:] = [: [:J, J:], J:] by ZFMISC_1:def 3;



      then

       A3: ( [:I, I, I:] /\ [:J, J, J:]) = [: [:(I /\ J), (I /\ J):], (I /\ J):] by A2, ZFMISC_1: 100

      .= [:(I /\ J), (I /\ J), (I /\ J):] by ZFMISC_1:def 3;



       A4: ( dom F1) = [:I, I:] & ( dom G1) = [:J, J:] by PARTFUN1:def 2;

       A5:

      now

        let x be object;

        assume

         A6: x in ( [:I, I, I:] /\ [:J, J, J:]);

        then

         A7: x in [:J, J, J:] by XBOOLE_0:def 4;

        x in [:I, I, I:] by A6, XBOOLE_0:def 4;

        then

        consider a,b,c be object such that

         A8: a in I and

         A9: b in I and

         A10: c in I and

         A11: x = [a, b, c] by MCART_1: 68;



         A12: b in J by A7, A11, MCART_1: 69;

        then

         A13: b in (I /\ J) by A9, XBOOLE_0:def 4;



         A14: c in J by A7, A11, MCART_1: 69;

        then

         A15: c in (I /\ J) by A10, XBOOLE_0:def 4;

        then

         A16: [b, c] in [:(I /\ J), (I /\ J):] by A13, ZFMISC_1: 87;



         A17: a in J by A7, A11, MCART_1: 69;

        then

         A18: a in (I /\ J) by A8, XBOOLE_0:def 4;

        then

         A19: [a, b] in [:(I /\ J), (I /\ J):] by A13, ZFMISC_1: 87;



         A20: ( {|F1, F2|} . (a,b,c)) = [:(F2 . (b,c)), (F1 . (a,b)):] by A8, A9, A10, ALTCAT_1:def 4;



         A21: ( {|G1, G2|} . (a,b,c)) = [:(G2 . (b,c)), (G1 . (a,b)):] by A17, A12, A14, ALTCAT_1:def 4;

        ( {|H1, H2|} . (a,b,c)) = [:(H2 . (b,c)), (H1 . (a,b)):] by A18, A13, A15, ALTCAT_1:def 4;



        hence ( {|H1, H2|} . x) = [:(H2 . (b,c)), (H1 . (a,b)):] by A11, MULTOP_1:def 1

        .= [:((F2 . [b, c]) /\ (G2 . [b, c])), (H1 . (a,b)):] by A2, A1, A16, Def2

        .= [:((F2 . [b, c]) /\ (G2 . [b, c])), ((F1 . [a, b]) /\ (G1 . [a, b])):] by A2, A4, A19, Def2

        .= ( [:(F2 . [b, c]), (F1 . [a, b]):] /\ [:(G2 . [b, c]), (G1 . [a, b]):]) by ZFMISC_1: 100

        .= (( {|F1, F2|} . x) /\ [:(G2 . [b, c]), (G1 . [a, b]):]) by A11, A20, MULTOP_1:def 1

        .= (( {|F1, F2|} . x) /\ ( {|G1, G2|} . x)) by A11, A21, MULTOP_1:def 1;

      end;

      take H1, H2;

      thus H1 = ( Intersect (F1,G1)) & H2 = ( Intersect (F2,G2));



       A22: ( dom {|H1, H2|}) = [:(I /\ J), (I /\ J), (I /\ J):] by PARTFUN1:def 2;

      ( dom {|F1, F2|}) = [:I, I, I:] & ( dom {|G1, G2|}) = [:J, J, J:] by PARTFUN1:def 2;

      hence thesis by A22, A3, A5, Def2;

    end;

    definition

      let A,B be AltCatStr;

      :: YELLOW20:def3

      func Intersect (A,B) -> strict AltCatStr means

      : Def3: the carrier of it = (the carrier of A /\ the carrier of B) & the Arrows of it = ( Intersect (the Arrows of A,the Arrows of B)) & the Comp of it = ( Intersect (the Comp of A,the Comp of B));

      existence

      proof

         A2:

        now

          let x be set;

          assume

           A3: x in ( dom the Comp of A);

          assume x in ( dom the Comp of B);

          ex a1,a2,a3 be object st a1 in the carrier of A & a2 in the carrier of A & a3 in the carrier of A & x = [a1, a2, a3] by A3, MCART_1: 68;

          hence (the Comp of A . x) tolerates (the Comp of B . x) by A1;

        end;

        set Cr = (the carrier of A /\ the carrier of B);



         A4: [:the carrier of B, the carrier of B, the carrier of B:] = [: [:the carrier of B, the carrier of B:], the carrier of B:] by ZFMISC_1:def 3;

         [:Cr, Cr:] = ( [:the carrier of A, the carrier of A:] /\ [:the carrier of B, the carrier of B:]) & [:the carrier of A, the carrier of A, the carrier of A:] = [: [:the carrier of A, the carrier of A:], the carrier of A:] by ZFMISC_1: 100, ZFMISC_1:def 3;



        then

         A5: ( [:the carrier of A, the carrier of A, the carrier of A:] /\ [:the carrier of B, the carrier of B, the carrier of B:]) = [: [:Cr, Cr:], Cr:] by A4, ZFMISC_1: 100

        .= [:Cr, Cr, Cr:] by ZFMISC_1:def 3;

        consider Ar be ManySortedSet of [:Cr, Cr:] such that

         A6: Ar = ( Intersect (the Arrows of A,the Arrows of B)) and

         A7: ( Intersect ( {|the Arrows of A|}, {|the Arrows of B|})) = {|Ar|} by Th17;

        ex Ar1,Ar2 be ManySortedSet of [:Cr, Cr:] st Ar1 = ( Intersect (the Arrows of A,the Arrows of B)) & Ar2 = ( Intersect (the Arrows of A,the Arrows of B)) & ( Intersect ( {|the Arrows of A, the Arrows of A|}, {|the Arrows of B, the Arrows of B|})) = {|Ar1, Ar2|} by Th18;

        then

        reconsider Cm = ( Intersect (the Comp of A,the Comp of B)) as ManySortedFunction of {|Ar, Ar|}, {|Ar|} by A6, A7, A5, A2, Th16;

        take AltCatStr (# Cr, Ar, Cm #);

        thus thesis by A6;

      end;

      uniqueness ;

    end

    theorem :: YELLOW20:19

    for A,B be AltCatStr st (A,B) have_the_same_composition holds ( Intersect (A,B)) = ( Intersect (B,A))

    proof

      let A,B be AltCatStr;

      set AB = ( Intersect (A,B));

      assume

       A1: (A,B) have_the_same_composition ;

      then

       A2: the Comp of AB = ( Intersect (the Comp of A,the Comp of B)) by Def3;

      the carrier of AB = (the carrier of A /\ the carrier of B) & the Arrows of AB = ( Intersect (the Arrows of A,the Arrows of B)) by A1, Def3;

      hence thesis by A1, A2, Def3;

    end;

    theorem :: YELLOW20:20



     Th20: for A,B be AltCatStr st (A,B) have_the_same_composition holds ( Intersect (A,B)) is SubCatStr of A

    proof

      let A,B be AltCatStr;

      set AB = ( Intersect (A,B));

      assume

       A1: (A,B) have_the_same_composition ;

      then

       A2: the Comp of AB = ( Intersect (the Comp of A,the Comp of B)) by Def3;

      the carrier of AB = (the carrier of A /\ the carrier of B) & the Arrows of AB = ( Intersect (the Arrows of A,the Arrows of B)) by A1, Def3;

      hence the carrier of AB c= the carrier of A & the Arrows of AB cc= the Arrows of A & the Comp of AB cc= the Comp of A by A2, Th15, XBOOLE_1: 17;

    end;

    theorem :: YELLOW20:21



     Th21: for A,B be AltCatStr st (A,B) have_the_same_composition holds for a1,a2 be Object of A, b1,b2 be Object of B holds for o1,o2 be Object of ( Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 holds <^o1, o2^> = ( <^a1, a2^> /\ <^b1, b2^>)

    proof

      let A,B be AltCatStr such that

       A1: (A,B) have_the_same_composition ;

      the carrier of ( Intersect (A,B)) = (the carrier of A /\ the carrier of B) by A1, Def3;

      then

       A2: [:the carrier of ( Intersect (A,B)), the carrier of ( Intersect (A,B)):] = ( [:the carrier of A, the carrier of A:] /\ [:the carrier of B, the carrier of B:]) by ZFMISC_1: 100;

      let a1,a2 be Object of A, b1,b2 be Object of B;

      let o1,o2 be Object of ( Intersect (A,B)) such that

       A3: o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2;

       A4:

      now

        assume the carrier of A <> {} & the carrier of B <> {} ;

        then [a1, a2] in [:the carrier of A, the carrier of A:] & [b1, b2] in [:the carrier of B, the carrier of B:] by ZFMISC_1:def 2;

        hence [o1, o2] in [:the carrier of ( Intersect (A,B)), the carrier of ( Intersect (A,B)):] by A3, A2, XBOOLE_0:def 4;

      end;



       A5: ( dom the Arrows of A) = [:the carrier of A, the carrier of A:] & ( dom the Arrows of B) = [:the carrier of B, the carrier of B:] by PARTFUN1:def 2;

       A6:

      now

        assume the carrier of A = {} or the carrier of B = {} ;

        then

         A7: [:the carrier of A, the carrier of A:] = {} or [:the carrier of B, the carrier of B:] = {} by ZFMISC_1: 90;

        then (the Arrows of A . [a1, a2]) = {} or (the Arrows of B . [b1, b2]) = {} ;

        hence ((the Arrows of A . [a1, a2]) /\ (the Arrows of B . [b1, b2])) = {} & (the Arrows of ( Intersect (A,B)) . [o1, o2]) = {} by A2, A7;

      end;

      the Arrows of ( Intersect (A,B)) = ( Intersect (the Arrows of A,the Arrows of B)) by A1, Def3;

      hence thesis by A3, A2, A5, A4, A6, Def2;

    end;

    theorem :: YELLOW20:22



     Th22: for A,B be transitive AltCatStr st (A,B) have_the_same_composition holds ( Intersect (A,B)) is transitive

    proof

      let A,B be transitive AltCatStr;

      set AB = ( Intersect (A,B));

      assume

       A1: (A,B) have_the_same_composition ;

      then

       A2: the carrier of AB = (the carrier of A /\ the carrier of B) by Def3;

      let o1,o2,o3 be Object of AB such that

       A3: <^o1, o2^> <> {} and

       A4: <^o2, o3^> <> {} ;

      ( dom the Arrows of AB) = [:the carrier of AB, the carrier of AB:] & [o1, o2] in ( dom the Arrows of AB) by A3, FUNCT_1:def 2, PARTFUN1:def 2;

      then

       A5: o1 in the carrier of AB by ZFMISC_1: 87;

      then

      reconsider A, B as non empty transitive AltCatStr by A2, XBOOLE_0:def 4;

      reconsider b1 = o1, b2 = o2, b3 = o3 as Object of B by A2, A5, XBOOLE_0:def 4;

      reconsider a1 = o1, a2 = o2, a3 = o3 as Object of A by A2, A5, XBOOLE_0:def 4;

      set f = the Morphism of o1, o2, g = the Morphism of o2, o3;



       A6: <^o2, o3^> = ( <^a2, a3^> /\ <^b2, b3^>) by A1, Th21;

      then

       A7: g in <^a2, a3^> & g in <^b2, b3^> by A4, XBOOLE_0:def 4;



       A8: <^o1, o2^> = ( <^a1, a2^> /\ <^b1, b2^>) by A1, Th21;

      then

      reconsider f1 = f as Morphism of a1, a2 by A3, XBOOLE_0:def 4;

      reconsider g2 = g as Morphism of b2, b3 by A4, A6, XBOOLE_0:def 4;

      reconsider g1 = g as Morphism of a2, a3 by A4, A6, XBOOLE_0:def 4;

      reconsider f2 = f as Morphism of b1, b2 by A3, A8, XBOOLE_0:def 4;

      f in <^a1, a2^> & f in <^b1, b2^> by A3, A8, XBOOLE_0:def 4;

      then

       A9: (g1 * f1) = (g2 * f2) by A1, A7, Th11;



       A10: <^b2, b3^> <> {} by A4, A6;



       A11: <^a2, a3^> <> {} by A4, A6;

       <^b1, b2^> <> {} by A3, A8;

      then

       A12: <^b1, b3^> <> {} by A10, ALTCAT_1:def 2;

       <^a1, a2^> <> {} by A3, A8;

      then

       A13: <^a1, a3^> <> {} by A11, ALTCAT_1:def 2;

       <^o1, o3^> = ( <^a1, a3^> /\ <^b1, b3^>) by A1, Th21;

      hence thesis by A13, A12, A9, XBOOLE_0:def 4;

    end;

    theorem :: YELLOW20:23



     Th23: for A,B be AltCatStr st (A,B) have_the_same_composition holds for a1,a2 be Object of A, b1,b2 be Object of B holds for o1,o2 be Object of ( Intersect (A,B)) st o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2 & <^a1, a2^> <> {} & <^b1, b2^> <> {} holds for f be Morphism of a1, a2, g be Morphism of b1, b2 st f = g holds f in <^o1, o2^>

    proof

      let A,B be AltCatStr such that

       A1: (A,B) have_the_same_composition ;

      let a1,a2 be Object of A, b1,b2 be Object of B;

      let o1,o2 be Object of ( Intersect (A,B));

      assume o1 = a1 & o1 = b1 & o2 = a2 & o2 = b2;

      then <^o1, o2^> = ( <^a1, a2^> /\ <^b1, b2^>) by A1, Th21;

      hence thesis by XBOOLE_0:def 4;

    end;

    theorem :: YELLOW20:24

    for A,B be with_units non empty AltCatStr st (A,B) have_the_same_composition holds for a be Object of A, b be Object of B holds for o be Object of ( Intersect (A,B)) st o = a & o = b & ( idm a) = ( idm b) holds ( idm a) in <^o, o^> by Th23;

    theorem :: YELLOW20:25

    for A,B be category st (A,B) have_the_same_composition & ( Intersect (A,B)) is non empty & for a be Object of A, b be Object of B st a = b holds ( idm a) = ( idm b) holds ( Intersect (A,B)) is subcategory of A

    proof

      let A,B be category such that

       A1: (A,B) have_the_same_composition and

       A2: ( Intersect (A,B)) is non empty and

       A3: for a be Object of A, b be Object of B st a = b holds ( idm a) = ( idm b);

      reconsider AB = ( Intersect (A,B)) as transitive non empty SubCatStr of A by A1, A2, Th20, Th22;



       A4: the carrier of AB = (the carrier of A /\ the carrier of B) by A1, Def3;

      now

        let o be Object of AB, a be Object of A;

        reconsider b = o as Object of B by A4, XBOOLE_0:def 4;

        assume

         A5: o = a;

        then ( idm a) = ( idm b) by A3;

        hence ( idm a) in <^o, o^> by A1, A5, Th23;

      end;

      hence thesis by ALTCAT_2:def 14;

    end;

    begin

    scheme :: YELLOW20:sch1

    SubcategoryUniq { A() -> category , B1,B2() -> non empty subcategory of A() , P[ set], Q[ set, set, set] } :

the AltCatStr of B1() = the AltCatStr of B2()

      provided

       A1: for a be Object of A() holds a is Object of B1() iff P[a]

       and

       A2: for a,b be Object of A(), a9,b9 be Object of B1() st a9 = a & b9 = b & <^a, b^> <> {} holds for f be Morphism of a, b holds f in <^a9, b9^> iff Q[a, b, f]

       and

       A3: for a be Object of A() holds a is Object of B2() iff P[a]

       and

       A4: for a,b be Object of A(), a9,b9 be Object of B2() st a9 = a & b9 = b & <^a, b^> <> {} holds for f be Morphism of a, b holds f in <^a9, b9^> iff Q[a, b, f];



       A5: the carrier of B1() c= the carrier of A() by ALTCAT_2:def 11;



       A6: the carrier of B2() c= the carrier of A() by ALTCAT_2:def 11;



       A7: the carrier of B1() = the carrier of B2()

      proof

        hereby

          let x be object;

          assume x in the carrier of B1();

          then

          reconsider a = x as Object of B1();

          reconsider a as Object of A() by A5;

          P[a] by A1;

          then a is Object of B2() by A3;

          hence x in the carrier of B2();

        end;

        let x be object;

        assume x in the carrier of B2();

        then

        reconsider a = x as Object of B2();

        reconsider a as Object of A() by A6;

        P[a] by A3;

        then a is Object of B1() by A1;

        hence thesis;

      end;

      now

        let a,b be Element of B1();

        reconsider x1 = a, y1 = b as Object of B1();

        reconsider x2 = x1, y2 = y1 as Object of B2() by A7;

        reconsider a9 = a, b9 = b as Object of A() by A5;



         A8: <^x2, y2^> c= <^a9, b9^> by ALTCAT_2: 31;



         A9: <^x2, y2^> c= <^x1, y1^>

        proof

          let f be object;

          assume

           A10: f in <^x2, y2^>;

          then

          reconsider f as Morphism of a9, b9 by A8;

          Q[a9, b9, f] by A4, A8, A10;

          hence thesis by A2, A8, A10;

        end;



         A11: <^x1, y1^> c= <^a9, b9^> by ALTCAT_2: 31;

         <^x1, y1^> c= <^x2, y2^>

        proof

          let f be object;

          assume

           A12: f in <^x1, y1^>;

          then

          reconsider f as Morphism of a9, b9 by A11;

          Q[a9, b9, f] by A2, A11, A12;

          hence thesis by A4, A11, A12;

        end;

        hence (the Arrows of B1() . (a,b)) = (the Arrows of B2() . (a,b)) by A9;

      end;

      hence thesis by A7, ALTCAT_1: 7, ALTCAT_2: 26;

    end;

    theorem :: YELLOW20:26



     Th26: for A be non empty AltCatStr, B be non empty SubCatStr of A holds B is full iff for a1,a2 be Object of A, b1,b2 be Object of B st b1 = a1 & b2 = a2 holds <^b1, b2^> = <^a1, a2^>

    proof

      let A be non empty AltCatStr, B be non empty SubCatStr of A;

      thus B is full implies for a1,a2 be Object of A, b1,b2 be Object of B st b1 = a1 & b2 = a2 holds <^b1, b2^> = <^a1, a2^> by ALTCAT_2: 28;



       A1: the carrier of B c= the carrier of A by ALTCAT_2:def 11;



       A2: ( dom the Arrows of B) = [:the carrier of B, the carrier of B:] by PARTFUN1:def 2;

      assume

       A3: for a1,a2 be Object of A, b1,b2 be Object of B st b1 = a1 & b2 = a2 holds <^b1, b2^> = <^a1, a2^>;

       A4:

      now

        let x be object;

        assume x in ( dom the Arrows of B);

        then

        consider b1,b2 be object such that

         A5: b1 in the carrier of B & b2 in the carrier of B and

         A6: x = [b1, b2] by ZFMISC_1:def 2;

        reconsider b1, b2 as Object of B by A5;

        reconsider a1 = b1, a2 = b2 as Object of A by A1;



        thus (the Arrows of B . x) = <^b1, b2^> by A6

        .= <^a1, a2^> by A3

        .= (the Arrows of A . x) by A6;

      end;



       A7: ( dom the Arrows of A) = [:the carrier of A, the carrier of A:] by PARTFUN1:def 2;

      ( [:the carrier of A, the carrier of A:] /\ [:the carrier of B, the carrier of B:]) = [:the carrier of B, the carrier of B:] by A1, XBOOLE_1: 28, ZFMISC_1: 96;

      hence the Arrows of B = (the Arrows of A || the carrier of B) by A7, A2, A4, FUNCT_1: 46;

    end;

    scheme :: YELLOW20:sch2

    FullSubcategoryEx { A() -> category , P[ set] } :

ex B be strict full non empty subcategory of A() st for a be Object of A() holds a is Object of B iff P[a]

      provided

       A1: ex a be Object of A() st P[a];

      defpred Q[ set, set, set] means not contradiction;



       A2: for a,b,c be Object of A() st P[a] & P[b] & P[c] & <^a, b^> <> {} & <^b, c^> <> {} holds for f be Morphism of a, b, g be Morphism of b, c st Q[a, b, f] & Q[b, c, g] holds Q[a, c, (g * f)];



       A3: for a be Object of A() st P[a] holds Q[a, a, ( idm a)];



       A4: ex a be Object of A() st P[a] by A1;

      consider B be strict non empty subcategory of A() such that

       A5: for a be Object of A() holds a is Object of B iff P[a] and

       A6: for a,b be Object of A(), a9,b9 be Object of B st a9 = a & b9 = b & <^a, b^> <> {} holds for f be Morphism of a, b holds f in <^a9, b9^> iff Q[a, b, f] from YELLOW18:sch 7( A4, A2, A3);

      now

        let a1,a2 be Object of A(), b1,b2 be Object of B;

        assume

         A7: b1 = a1 & b2 = a2;



         A8: <^a1, a2^> c= <^b1, b2^> by A6, A7;

         <^b1, b2^> c= <^a1, a2^> by A7, ALTCAT_2: 31;

        hence <^b1, b2^> = <^a1, a2^> by A8;

      end;

      then B is full by Th26;

      hence thesis by A5;

    end;

    scheme :: YELLOW20:sch3

    FullSubcategoryUniq { A() -> category , B1,B2() -> full non empty subcategory of A() , P[ set] } :

the AltCatStr of B1() = the AltCatStr of B2()

      provided

       A1: for a be Object of A() holds a is Object of B1() iff P[a]

       and

       A2: for a be Object of A() holds a is Object of B2() iff P[a];



       A3: for a be Object of A() holds a is Object of B2() iff P[a] by A2;

      defpred Q[ set, set, set] means not contradiction;

       A4:

      now

        let a,b be Object of A(), a9,b9 be Object of B1();

        assume a9 = a & b9 = b;

        then <^a9, b9^> = <^a, b^> by Th26;

        hence <^a, b^> <> {} implies for f be Morphism of a, b holds f in <^a9, b9^> iff Q[a, b, f];

      end;

       A5:

      now

        let a,b be Object of A(), a9,b9 be Object of B2();

        assume a9 = a & b9 = b;

        then <^a9, b9^> = <^a, b^> by Th26;

        hence <^a, b^> <> {} implies for f be Morphism of a, b holds f in <^a9, b9^> iff Q[a, b, f];

      end;



       A6: for a be Object of A() holds a is Object of B1() iff P[a] by A1;

      thus thesis from SubcategoryUniq( A6, A4, A3, A5);

    end;

    begin

    registration

      let f be Function-yielding Function;

      let x,y be set;

      cluster (f . (x,y)) -> Relation-like Function-like;

      coherence ;

    end

    theorem :: YELLOW20:27



     Th27: for A be category, C be non empty subcategory of A holds for a,b be Object of C st <^a, b^> <> {} holds for f be Morphism of a, b holds (( incl C) . f) = f

    proof

      let A be category, C be non empty subcategory of A;

      let a,b be Object of C such that

       A1: <^a, b^> <> {} ;

      let f be Morphism of a, b;



       A2: the MorphMap of ( incl C) = ( id the Arrows of C) & [a, b] in [:the carrier of C, the carrier of C:] by FUNCTOR0:def 28, ZFMISC_1:def 2;

       <^(( incl C) . a), (( incl C) . b)^> <> {} by A1, FUNCTOR0: 28, XBOOLE_1: 3;



      hence (( incl C) . f) = (( Morph-Map (( incl C),a,b)) . f) by A1, FUNCTOR0:def 15

      .= (( id (the Arrows of C . (a,b))) . f) by A2, MSUALG_3:def 1

      .= f;

    end;

    registration

      let A be category;

      let C be non empty subcategory of A;

      cluster ( incl C) -> id-preserving comp-preserving;

      coherence

      proof

        thus ( incl C) is id-preserving

        proof

          let a be Object of C;



           A1: (( incl C) . a) = a by FUNCTOR0: 27;



          thus (( Morph-Map (( incl C),a,a)) . ( idm a)) = (( incl C) . ( idm a)) by FUNCTOR0:def 15

          .= ( idm a) by Th27

          .= ( idm (( incl C) . a)) by A1, ALTCAT_2: 34;

        end;

        let o1,o2,o3 be Object of C such that

         A2: <^o1, o2^> <> {} & <^o2, o3^> <> {} ;

        let f be Morphism of o1, o2, g be Morphism of o2, o3;

         <^o1, o3^> <> {} by A2, ALTCAT_1:def 2;

        then

         A3: (( incl C) . o3) = o3 & (( incl C) . (g * f)) = (g * f) by Th27, FUNCTOR0: 27;



         A4: (( incl C) . o1) = o1 & (( incl C) . o2) = o2 by FUNCTOR0: 27;

        (( incl C) . g) = g & (( incl C) . f) = f by A2, Th27;

        hence thesis by A2, A4, A3, ALTCAT_2: 32;

      end;

    end

    registration

      let A be category;

      let C be non empty subcategory of A;

      cluster ( incl C) -> Covariant;

      coherence ;

    end

    definition

      let A be category;

      let C be non empty subcategory of A;

      :: original: incl

      redefine

      func incl C -> strict covariant Functor of C, A ;

      coherence by FUNCTOR0:def 25;

    end

    definition

      let A,B be category;

      let C be non empty subcategory of A;

      let F be covariant Functor of A, B;

      :: original: |

      redefine

      func F | C -> strict covariant Functor of C, B ;

      coherence

      proof

        (F | C) = (F * ( incl C));

        hence thesis;

      end;

    end

    definition

      let A,B be category;

      let C be non empty subcategory of A;

      let F be contravariant Functor of A, B;

      :: original: |

      redefine

      func F | C -> strict contravariant Functor of C, B ;

      coherence

      proof

        (F | C) = (F * ( incl C));

        hence thesis;

      end;

    end

    theorem :: YELLOW20:28



     Th28: for A,B be category, C be non empty subcategory of A holds for F be FunctorStr over A, B holds for a be Object of A, c be Object of C st c = a holds ((F | C) . c) = (F . a)

    proof

      let A,B be category, C be non empty subcategory of A;

      let F be FunctorStr over A, B;

      let b be Object of A;

      let a be Object of C;

      assume a = b;

      then (( incl C) . a) = b by FUNCTOR0: 27;

      hence thesis by FUNCTOR0: 33;

    end;

    theorem :: YELLOW20:29



     Th29: for A,B be category, C be non empty subcategory of A holds for F be covariant Functor of A, B holds for a,b be Object of A, c,d be Object of C st c = a & d = b & <^c, d^> <> {} holds for f be Morphism of a, b holds for g be Morphism of c, d st g = f holds ((F | C) . g) = (F . f)

    proof

      let A,B be category, C be non empty subcategory of A;

      let F be covariant Functor of A, B;

      let a,b be Object of A;

      let c,d be Object of C;

      assume that

       A1: c = a & d = b and

       A2: <^c, d^> <> {} ;

      let f be Morphism of a, b;

      let g be Morphism of c, d;

      assume g = f;

      then

       A3: (( incl C) . g) = f by A2, Th27;

      (( incl C) . c) = a & (( incl C) . d) = b by A1, FUNCTOR0: 27;

      hence thesis by A2, A3, FUNCTOR3: 6;

    end;

    theorem :: YELLOW20:30



     Th30: for A,B be category, C be non empty subcategory of A holds for F be contravariant Functor of A, B holds for a,b be Object of A, c,d be Object of C st c = a & d = b & <^c, d^> <> {} holds for f be Morphism of a, b holds for g be Morphism of c, d st g = f holds ((F | C) . g) = (F . f)

    proof

      let A,B be category, C be non empty subcategory of A;

      let F be contravariant Functor of A, B;

      let a,b be Object of A;

      let c,d be Object of C;

      assume that

       A1: c = a & d = b and

       A2: <^c, d^> <> {} ;

      let f be Morphism of a, b;

      let g be Morphism of c, d;

      assume g = f;

      then

       A3: (( incl C) . g) = f by A2, Th27;

      (( incl C) . c) = a & (( incl C) . d) = b by A1, FUNCTOR0: 27;

      hence thesis by A2, A3, FUNCTOR3: 8;

    end;

    theorem :: YELLOW20:31



     Th31: for A,B be non empty AltGraph holds for F be BimapStr over A, B st F is Covariant one-to-one holds for a,b be Object of A st (F . a) = (F . b) holds a = b

    proof

      let A,B be non empty AltGraph;

      let F be BimapStr over A, B;

      given f be Function of the carrier of A, the carrier of B such that

       A1: the ObjectMap of F = [:f, f:];

      assume the ObjectMap of F is one-to-one;

      then

       A2: f is one-to-one by A1, FUNCTOR0: 7;

      let a,b be Object of A such that

       A3: (F . a) = (F . b);



       A4: ( [(f . a), (f . a)] `1 ) = (f . a) & ( [(f . b), (f . b)] `1 ) = (f . b);

      (the ObjectMap of F . (a,a)) = [(f . a), (f . a)] & (the ObjectMap of F . (b,b)) = [(f . b), (f . b)] by A1, FUNCT_3: 75;

      hence thesis by A2, A3, A4, FUNCT_2: 19;

    end;

    theorem :: YELLOW20:32



     Th32: for A,B be non empty reflexive AltGraph holds for F be feasible Covariant FunctorStr over A, B st F is faithful holds for a,b be Object of A st <^a, b^> <> {} holds for f,g be Morphism of a, b st (F . f) = (F . g) holds f = g

    proof

      let A,B be non empty reflexive AltGraph;

      let F be feasible Covariant FunctorStr over A, B such that

       A1: for i be set, f be Function st i in ( dom the MorphMap of F) & (the MorphMap of F . i) = f holds f is one-to-one;

      let a,b be Object of A such that

       A2: <^a, b^> <> {} ;

      let f,g be Morphism of a, b;

      ( dom the MorphMap of F) = [:the carrier of A, the carrier of A:] & [a, b] in [:the carrier of A, the carrier of A:] by PARTFUN1:def 2, ZFMISC_1:def 2;

      then

       A3: ( Morph-Map (F,a,b)) is one-to-one by A1;



       A4: <^(F . a), (F . b)^> <> {} by A2, FUNCTOR0:def 18;

      then (F . f) = (( Morph-Map (F,a,b)) . f) & (F . g) = (( Morph-Map (F,a,b)) . g) by A2, FUNCTOR0:def 15;

      hence thesis by A2, A4, A3, FUNCT_2: 19;

    end;

    theorem :: YELLOW20:33



     Th33: for A,B be non empty AltGraph holds for F be Covariant FunctorStr over A, B st F is surjective holds for a,b be Object of B st <^a, b^> <> {} holds for f be Morphism of a, b holds ex c,d be Object of A, g be Morphism of c, d st a = (F . c) & b = (F . d) & <^c, d^> <> {} & f = (F . g)

    proof

      let A,B be non empty AltGraph;

      let F be Covariant FunctorStr over A, B;

      given f be ManySortedFunction of the Arrows of A, (the Arrows of B * the ObjectMap of F) such that

       A1: f = the MorphMap of F & f is "onto";

      assume

       A2: ( rng the ObjectMap of F) = [:the carrier of B, the carrier of B:];

      let a,b be Object of B such that

       A3: <^a, b^> <> {} ;

      the ObjectMap of F is Covariant by FUNCTOR0:def 12;

      then

      consider g be Function of the carrier of A, the carrier of B such that

       A4: the ObjectMap of F = [:g, g:];

      let f be Morphism of a, b;

      ( dom the ObjectMap of F) = [:the carrier of A, the carrier of A:] & [a, b] in ( rng the ObjectMap of F) by A2, FUNCT_2:def 1, ZFMISC_1:def 2;

      then

      consider x be object such that

       A5: x in [:the carrier of A, the carrier of A:] and

       A6: [a, b] = (the ObjectMap of F . x) by FUNCT_1:def 3;

      consider c,d be object such that

       A7: c in the carrier of A & d in the carrier of A and

       A8: [c, d] = x by A5, ZFMISC_1:def 2;

      reconsider c, d as Object of A by A7;

      (the ObjectMap of F . (d,d)) = [(g . d), (g . d)] by A4, FUNCT_3: 75;

      then

       A9: (F . d) = (g . d);

      (the ObjectMap of F . (c,c)) = [(g . c), (g . c)] by A4, FUNCT_3: 75;

      then (F . c) = (g . c);

      then

       A10: (the ObjectMap of F . (c,d)) = [(F . c), (F . d)] by A4, A9, FUNCT_3: 75;

      ( rng ( Morph-Map (F,c,d))) = ((the Arrows of B * the ObjectMap of F) . [c, d]) by A1, A5, A8

      .= <^a, b^> by A5, A6, A8, FUNCT_2: 15;

      then

      consider g be object such that

       A11: g in ( dom ( Morph-Map (F,c,d))) and

       A12: f = (( Morph-Map (F,c,d)) . g) by A3, FUNCT_1:def 3;

      take c, d;

      reconsider g as Morphism of c, d by A11;

      take g;

      thus a = (F . c) & b = (F . d) & <^c, d^> <> {} by A6, A8, A10, A11, XTUPLE_0: 1;

      thus thesis by A3, A6, A8, A10, A11, A12, FUNCTOR0:def 15;

    end;

    theorem :: YELLOW20:34



     Th34: for A,B be non empty AltGraph holds for F be BimapStr over A, B st F is Contravariant one-to-one holds for a,b be Object of A st (F . a) = (F . b) holds a = b

    proof

      let A,B be non empty AltGraph;

      let F be BimapStr over A, B;

      given f be Function of the carrier of A, the carrier of B such that

       A1: the ObjectMap of F = ( ~ [:f, f:]);

      assume the ObjectMap of F is one-to-one;

      then [:f, f:] is one-to-one by A1, FUNCTOR0: 9;

      then

       A2: f is one-to-one by FUNCTOR0: 7;

      let a,b be Object of A such that

       A3: (F . a) = (F . b);



       A4: ( dom the ObjectMap of F) = [:the carrier of A, the carrier of A:] by FUNCT_2:def 1;

       [b, b] in [:the carrier of A, the carrier of A:] by ZFMISC_1:def 2;

      then (the ObjectMap of F . (b,b)) = ( [:f, f:] . (b,b)) by A1, A4, FUNCT_4: 43;

      then

       A5: (the ObjectMap of F . (b,b)) = [(f . b), (f . b)] by FUNCT_3: 75;

       [a, a] in [:the carrier of A, the carrier of A:] by ZFMISC_1:def 2;

      then (the ObjectMap of F . (a,a)) = ( [:f, f:] . (a,a)) by A1, A4, FUNCT_4: 43;

      then

       A6: (the ObjectMap of F . (a,a)) = [(f . a), (f . a)] by FUNCT_3: 75;

      ( [(f . a), (f . a)] `1 ) = (f . a) & ( [(f . b), (f . b)] `1 ) = (f . b);

      hence thesis by A2, A3, A6, A5, FUNCT_2: 19;

    end;

    theorem :: YELLOW20:35



     Th35: for A,B be non empty reflexive AltGraph holds for F be feasible Contravariant FunctorStr over A, B st F is faithful holds for a,b be Object of A st <^a, b^> <> {} holds for f,g be Morphism of a, b st (F . f) = (F . g) holds f = g

    proof

      let A,B be non empty reflexive AltGraph;

      let F be feasible Contravariant FunctorStr over A, B such that

       A1: for i be set, f be Function st i in ( dom the MorphMap of F) & (the MorphMap of F . i) = f holds f is one-to-one;

      let a,b be Object of A such that

       A2: <^a, b^> <> {} ;

      let f,g be Morphism of a, b;

      ( dom the MorphMap of F) = [:the carrier of A, the carrier of A:] & [a, b] in [:the carrier of A, the carrier of A:] by PARTFUN1:def 2, ZFMISC_1:def 2;

      then

       A3: ( Morph-Map (F,a,b)) is one-to-one by A1;



       A4: <^(F . b), (F . a)^> <> {} by A2, FUNCTOR0:def 19;

      then (F . f) = (( Morph-Map (F,a,b)) . f) & (F . g) = (( Morph-Map (F,a,b)) . g) by A2, FUNCTOR0:def 16;

      hence thesis by A2, A4, A3, FUNCT_2: 19;

    end;

    theorem :: YELLOW20:36



     Th36: for A,B be non empty AltGraph holds for F be Contravariant FunctorStr over A, B st F is surjective holds for a,b be Object of B st <^a, b^> <> {} holds for f be Morphism of a, b holds ex c,d be Object of A, g be Morphism of c, d st b = (F . c) & a = (F . d) & <^c, d^> <> {} & f = (F . g)

    proof

      let A,B be non empty AltGraph;

      let F be Contravariant FunctorStr over A, B;

      given f be ManySortedFunction of the Arrows of A, (the Arrows of B * the ObjectMap of F) such that

       A1: f = the MorphMap of F & f is "onto";

      assume

       A2: ( rng the ObjectMap of F) = [:the carrier of B, the carrier of B:];

      let a,b be Object of B such that

       A3: <^a, b^> <> {} ;

      let f be Morphism of a, b;

      ( dom the ObjectMap of F) = [:the carrier of A, the carrier of A:] & [a, b] in ( rng the ObjectMap of F) by A2, FUNCT_2:def 1, ZFMISC_1:def 2;

      then

      consider x be object such that

       A4: x in [:the carrier of A, the carrier of A:] and

       A5: [a, b] = (the ObjectMap of F . x) by FUNCT_1:def 3;



       A6: ( dom the ObjectMap of F) = [:the carrier of A, the carrier of A:] by FUNCT_2:def 1;

      the ObjectMap of F is Contravariant by FUNCTOR0:def 13;

      then

      consider g be Function of the carrier of A, the carrier of B such that

       A7: the ObjectMap of F = ( ~ [:g, g:]);

      consider d,c be object such that

       A8: d in the carrier of A & c in the carrier of A and

       A9: [d, c] = x by A4, ZFMISC_1:def 2;

      reconsider c, d as Object of A by A8;

       [c, c] in [:the carrier of A, the carrier of A:] by ZFMISC_1:def 2;

      then (the ObjectMap of F . (c,c)) = ( [:g, g:] . (c,c)) by A7, A6, FUNCT_4: 43;

      then (the ObjectMap of F . (c,c)) = [(g . c), (g . c)] by FUNCT_3: 75;

      then

       A10: (F . c) = (g . c);

       [d, d] in [:the carrier of A, the carrier of A:] by ZFMISC_1:def 2;

      then (the ObjectMap of F . (d,d)) = ( [:g, g:] . (d,d)) by A7, A6, FUNCT_4: 43;

      then (the ObjectMap of F . (d,d)) = [(g . d), (g . d)] by FUNCT_3: 75;

      then

       A11: (F . d) = (g . d);

       [d, c] in [:the carrier of A, the carrier of A:] by ZFMISC_1:def 2;



      then

       A12: (the ObjectMap of F . (d,c)) = ( [:g, g:] . (c,d)) by A7, A6, FUNCT_4: 43

      .= [(F . c), (F . d)] by A10, A11, FUNCT_3: 75;

      ( rng ( Morph-Map (F,d,c))) = ((the Arrows of B * the ObjectMap of F) . [d, c]) by A1, A4, A9

      .= <^a, b^> by A4, A5, A9, FUNCT_2: 15;

      then

      consider g be object such that

       A13: g in ( dom ( Morph-Map (F,d,c))) and

       A14: f = (( Morph-Map (F,d,c)) . g) by A3, FUNCT_1:def 3;

      take d, c;

      reconsider g as Morphism of d, c by A13;

      take g;

      thus b = (F . d) & a = (F . c) & <^d, c^> <> {} by A5, A9, A12, A13, XTUPLE_0: 1;

      thus thesis by A3, A5, A9, A12, A13, A14, FUNCTOR0:def 16;

    end;

    begin

    definition

      let A,B be category;

      let F be FunctorStr over A, B;

      let A9,B9 be category;

      :: YELLOW20:def4

      pred A9,B9 are_isomorphic_under F means A9 is subcategory of A & B9 is subcategory of B & ex G be covariant Functor of A9, B9 st G is bijective & (for a9 be Object of A9, a be Object of A st a9 = a holds (G . a9) = (F . a)) & for b9,c9 be Object of A9, b,c be Object of A st <^b9, c9^> <> {} & b9 = b & c9 = c holds for f9 be Morphism of b9, c9, f be Morphism of b, c st f9 = f holds (G . f9) = (( Morph-Map (F,b,c)) . f);

      :: YELLOW20:def5

      pred A9,B9 are_anti-isomorphic_under F means A9 is subcategory of A & B9 is subcategory of B & ex G be contravariant Functor of A9, B9 st G is bijective & (for a9 be Object of A9, a be Object of A st a9 = a holds (G . a9) = (F . a)) & for b9,c9 be Object of A9, b,c be Object of A st <^b9, c9^> <> {} & b9 = b & c9 = c holds for f9 be Morphism of b9, c9, f be Morphism of b, c st f9 = f holds (G . f9) = (( Morph-Map (F,b,c)) . f);

    end

    theorem :: YELLOW20:37

    for A,B,A1,B1 be category, F be FunctorStr over A, B st (A1,B1) are_isomorphic_under F holds (A1,B1) are_isomorphic ;

    theorem :: YELLOW20:38

    for A,B,A1,B1 be category, F be FunctorStr over A, B st (A1,B1) are_anti-isomorphic_under F holds (A1,B1) are_anti-isomorphic ;

    theorem :: YELLOW20:39

    for A,B be category, F be covariant Functor of A, B st (A,B) are_isomorphic_under F holds F is bijective

    proof

      let A,B be category, F be covariant Functor of A, B such that A is subcategory of A and B is subcategory of B;

      given G be covariant Functor of A, B such that

       A1: G is bijective and

       A2: for a9 be Object of A, a be Object of A st a9 = a holds (G . a9) = (F . a) and

       A3: for b9,c9 be Object of A, b,c be Object of A st <^b9, c9^> <> {} & b9 = b & c9 = c holds for f9 be Morphism of b9, c9, f be Morphism of b, c st f9 = f holds (G . f9) = (( Morph-Map (F,b,c)) . f);

      G is injective surjective by A1;

      then

       A4: G is one-to-one faithful full onto;

       A5:

      now

        let a,b be Object of A such that

         A6: <^a, b^> <> {} ;

        let f be Morphism of a, b;

         <^(F . a), (F . b)^> <> {} by A6, FUNCTOR0:def 18;



        hence (F . f) = (( Morph-Map (F,a,b)) . f) by A6, FUNCTOR0:def 15

        .= (G . f) by A3, A6;

      end;

      for a be Object of A holds (F . a) = (G . a) by A2;

      then the FunctorStr of F = the FunctorStr of G by A5, YELLOW18: 1;

      hence the ObjectMap of F is one-to-one & the MorphMap of F is "1-1" & (ex f be ManySortedFunction of the Arrows of A, (the Arrows of B * the ObjectMap of F) st f = the MorphMap of F & f is "onto") & the ObjectMap of F is onto by A4;

    end;

    theorem :: YELLOW20:40

    for A,B be category, F be contravariant Functor of A, B st (A,B) are_anti-isomorphic_under F holds F is bijective

    proof

      let A,B be category, F be contravariant Functor of A, B such that A is subcategory of A and B is subcategory of B;

      given G be contravariant Functor of A, B such that

       A1: G is bijective and

       A2: for a9 be Object of A, a be Object of A st a9 = a holds (G . a9) = (F . a) and

       A3: for b9,c9 be Object of A, b,c be Object of A st <^b9, c9^> <> {} & b9 = b & c9 = c holds for f9 be Morphism of b9, c9, f be Morphism of b, c st f9 = f holds (G . f9) = (( Morph-Map (F,b,c)) . f);

      G is injective surjective by A1;

      then

       A4: G is one-to-one faithful full onto;

       A5:

      now

        let a,b be Object of A such that

         A6: <^a, b^> <> {} ;

        let f be Morphism of a, b;

         <^(F . b), (F . a)^> <> {} by A6, FUNCTOR0:def 19;



        hence (F . f) = (( Morph-Map (F,a,b)) . f) by A6, FUNCTOR0:def 16

        .= (G . f) by A3, A6;

      end;

      for a be Object of A holds (F . a) = (G . a) by A2;

      then the FunctorStr of F = the FunctorStr of G by A5, YELLOW18: 2;

      hence the ObjectMap of F is one-to-one & the MorphMap of F is "1-1" & (ex f be ManySortedFunction of the Arrows of A, (the Arrows of B * the ObjectMap of F) st f = the MorphMap of F & f is "onto") & the ObjectMap of F is onto by A4;

    end;

    theorem :: YELLOW20:41

    for A,B be category, F be covariant Functor of A, B st F is bijective holds (A,B) are_isomorphic_under F

    proof

      let A,B be category, F be covariant Functor of A, B such that

       A1: F is bijective;

      the Arrows of A = the Arrows of A & the Arrows of B = the Arrows of B;

      hence A is subcategory of A & B is subcategory of B by ALTCAT_2: 20, ALTCAT_4: 35;

      take F;

      thus F is bijective & for a9 be Object of A, a be Object of A st a9 = a holds (F . a9) = (F . a) by A1;

      let b9,c9 be Object of A, b,c be Object of A;

      assume

       A2: <^b9, c9^> <> {} & b9 = b & c9 = c;

      then <^(F . b), (F . c)^> <> {} by FUNCTOR0:def 18;

      hence thesis by A2, FUNCTOR0:def 15;

    end;

    theorem :: YELLOW20:42

    for A,B be category, F be contravariant Functor of A, B st F is bijective holds (A,B) are_anti-isomorphic_under F

    proof

      let A,B be category, F be contravariant Functor of A, B such that

       A1: F is bijective;

      the Arrows of A = the Arrows of A & the Arrows of B = the Arrows of B;

      hence A is subcategory of A & B is subcategory of B by ALTCAT_2: 20, ALTCAT_4: 35;

      take F;

      thus F is bijective & for a9 be Object of A, a be Object of A st a9 = a holds (F . a9) = (F . a) by A1;

      let b9,c9 be Object of A, b,c be Object of A;

      assume

       A2: <^b9, c9^> <> {} & b9 = b & c9 = c;

      then <^(F . c), (F . b)^> <> {} by FUNCTOR0:def 19;

      hence thesis by A2, FUNCTOR0:def 16;

    end;

    theorem :: YELLOW20:43

    for A be category, B be non empty subcategory of A holds (B,B) are_isomorphic_under ( id A)

    proof

      let A be category, B be non empty subcategory of A;

      set F = ( id A);

      thus B is subcategory of A & B is subcategory of A;

      take G = ( id B);

      thus G is bijective;

      hereby

        let a be Object of B, a1 be Object of A;

        assume a = a1;



        hence (G . a) = a1 by FUNCTOR0: 29

        .= (F . a1) by FUNCTOR0: 29;

      end;

      let b,c be Object of B, b1,c1 be Object of A such that

       A1: <^b, c^> <> {} and

       A2: b = b1 & c = c1;

      let f be Morphism of b, c, f1 be Morphism of b1, c1 such that

       A3: f = f1;



       A4: <^b, c^> c= <^b1, c1^> & f in <^b, c^> by A1, A2, ALTCAT_2: 31;



       A5: (F . b1) = b1 & (F . c1) = c1 by FUNCTOR0: 29;



      thus (G . f) = f by A1, FUNCTOR0: 31

      .= (F . f1) by A3, A4, FUNCTOR0: 31

      .= (( Morph-Map (F,b1,c1)) . f1) by A4, A5, FUNCTOR0:def 15;

    end;

    theorem :: YELLOW20:44



     Th44: for f,g be Function st f c= g holds ( ~ f) c= ( ~ g)

    proof

      let f,g be Function such that

       A1: f c= g;

      let x,y be object;

      assume

       A2: [x, y] in ( ~ f);

      then x in ( dom ( ~ f)) by XTUPLE_0:def 12;

      then

      consider z2,z1 be object such that

       A3: x = [z1, z2] and

       A4: [z2, z1] in ( dom f) by FUNCT_4:def 2;

      y = (( ~ f) . (z1,z2)) by A2, A3, FUNCT_1: 1

      .= (f . (z2,z1)) by A4, FUNCT_4:def 2;

      then

       A5: [ [z2, z1], y] in f by A4, FUNCT_1: 1;

      then

       A6: [z2, z1] in ( dom g) by A1, FUNCT_1: 1;

      y = (g . (z2,z1)) by A1, A5, FUNCT_1: 1;

      then

       A7: y = (( ~ g) . (z1,z2)) by A6, FUNCT_4:def 2;

      x in ( dom ( ~ g)) by A3, A6, FUNCT_4:def 2;

      hence thesis by A3, A7, FUNCT_1: 1;

    end;

    theorem :: YELLOW20:45

    for f,g be Function st ( dom f) is Relation & ( ~ f) c= ( ~ g) holds f c= g

    proof

      let f,g be Function;

      assume ( dom f) is Relation;

      then

      reconsider R = ( dom f) as Relation;

      R c= [:( dom R), ( rng R):] by RELAT_1: 7;

      then

       A1: ( ~ ( ~ f)) = f by FUNCT_4: 52;

      assume ( ~ f) c= ( ~ g);

      then ( ~ ( ~ g)) c= g & f c= ( ~ ( ~ g)) by A1, Th44, FUNCT_4: 51;

      hence thesis;

    end;

    theorem :: YELLOW20:46



     Th46: for I,J be set holds for A be ManySortedSet of [:I, I:], B be ManySortedSet of [:J, J:] st A cc= B holds ( ~ A) cc= ( ~ B)

    proof

      let I,J be set;

      let A be ManySortedSet of [:I, I:], B be ManySortedSet of [:J, J:] such that

       A1: [:I, I:] c= [:J, J:] and

       A2: for x st x in [:I, I:] holds (A . x) c= (B . x);

      thus [:I, I:] c= [:J, J:] by A1;

      let x;

      assume x in [:I, I:];

      then

      consider x1,x2 be object such that

       A3: x1 in I & x2 in I and

       A4: x = [x1, x2] by ZFMISC_1:def 2;



       A5: [x2, x1] in [:I, I:] by A3, ZFMISC_1:def 2;

      ( dom A) = [:I, I:] by PARTFUN1:def 2;

      then

       A6: (( ~ A) . (x1,x2)) = (A . (x2,x1)) by A5, FUNCT_4:def 2;

      ( dom B) = [:J, J:] by PARTFUN1:def 2;

      then (( ~ B) . (x1,x2)) = (B . (x2,x1)) by A1, A5, FUNCT_4:def 2;

      hence thesis by A2, A4, A5, A6;

    end;

    theorem :: YELLOW20:47



     Th47: for A be transitive non empty AltCatStr holds for B be transitive non empty SubCatStr of A holds (B opp ) is SubCatStr of (A opp )

    proof

      let A be transitive non empty AltCatStr;

      let B be transitive non empty SubCatStr of A;



       A1: (B,(B opp )) are_opposite by YELLOW18:def 4;

      then

       A2: the carrier of (B opp ) = the carrier of B by YELLOW18:def 3;



       A3: the Arrows of (B opp ) = ( ~ the Arrows of B) by A1, YELLOW18:def 3;



       A4: (A,(A opp )) are_opposite by YELLOW18:def 4;

      then

       A5: the carrier of (A opp ) = the carrier of A by YELLOW18:def 3;

      hence the carrier of (B opp ) c= the carrier of (A opp ) by A2, ALTCAT_2:def 11;

      the Arrows of B cc= the Arrows of A & the Arrows of (A opp ) = ( ~ the Arrows of A) by A4, ALTCAT_2:def 11, YELLOW18:def 3;

      hence the Arrows of (B opp ) cc= the Arrows of (A opp ) by A3, Th46;



       A6: the carrier of B c= the carrier of A by ALTCAT_2:def 11;

      hence [:the carrier of (B opp ), the carrier of (B opp ), the carrier of (B opp ):] c= [:the carrier of (A opp ), the carrier of (A opp ), the carrier of (A opp ):] by A5, A2, MCART_1: 73;

      let x;

      assume x in [:the carrier of (B opp ), the carrier of (B opp ), the carrier of (B opp ):];

      then

      consider x1,x2,x3 be object such that

       A7: x1 in the carrier of B & x2 in the carrier of B & x3 in the carrier of B and

       A8: x = [x1, x2, x3] by A2, MCART_1: 68;

      reconsider a = x1, b = x2, c = x3 as Object of B by A7;

      reconsider a1 = a, b1 = b, c1 = c as Object of A by A6;

      reconsider a19 = a1, b19 = b1, c19 = c1 as Object of (A opp ) by A4, YELLOW18:def 3;



       A9: the Comp of B cc= the Comp of A & (the Comp of B . (c,b,a)) = (the Comp of B . [c, b, a]) by ALTCAT_2:def 11, MULTOP_1:def 1;



       A10: (the Comp of A . (c1,b1,a1)) = (the Comp of A . [c1, b1, a1]) by MULTOP_1:def 1;

       [x3, x2, x1] in [:the carrier of B, the carrier of B, the carrier of B:] by A7, MCART_1: 69;

      then

       A11: (the Comp of B . (c,b,a)) c= (the Comp of A . (c1,b1,a1)) by A9, A10;

      reconsider a9 = a, b9 = b, c9 = c as Object of (B opp ) by A1, YELLOW18:def 3;



       A12: (the Comp of (B opp ) . (a9,b9,c9)) = (the Comp of (B opp ) . x) & (the Comp of (A opp ) . (a19,b19,c19)) = (the Comp of (A opp ) . x) by A8, MULTOP_1:def 1;



       A13: (the Comp of (A opp ) . (a19,b19,c19)) = ( ~ (the Comp of A . (c1,b1,a1))) by A4, YELLOW18:def 3;

      (the Comp of (B opp ) . (a9,b9,c9)) = ( ~ (the Comp of B . (c,b,a))) by A1, YELLOW18:def 3;

      hence thesis by A13, A12, A11, Th44;

    end;

    theorem :: YELLOW20:48



     Th48: for A be category, B be non empty subcategory of A holds (B opp ) is subcategory of (A opp )

    proof

      let A be category, B be non empty subcategory of A;

      reconsider BB = (B opp ) as transitive non empty SubCatStr of (A opp ) by Th47;



       A1: ((A opp ),A) are_opposite by YELLOW18:def 4;



       A2: (BB,B) are_opposite by YELLOW18:def 4;

      BB is id-inheriting

      proof

        per cases ;

          case BB is non empty;

          let o be Object of BB, o9 be Object of (A opp );

          reconsider a9 = o9 as Object of A by A1, YELLOW18:def 3;

          reconsider a = o as Object of B by A2, YELLOW18:def 3;

          assume o = o9;

          then ( idm a9) in <^a, a^> by ALTCAT_2:def 14;

          then ( idm o9) in <^a, a^> by A1, YELLOW18: 10;

          hence thesis by A2, YELLOW18: 7;

        end;

          case BB is empty;

        end;

      end;

      hence thesis;

    end;

    theorem :: YELLOW20:49

    for A be category, B be non empty subcategory of A holds (B,(B opp )) are_anti-isomorphic_under ( dualizing-func (A,(A opp )))

    proof

      let A be category, B be non empty subcategory of A;

      set F = ( dualizing-func (A,(A opp )));



       A1: (B,(B opp )) are_opposite by YELLOW18:def 4;

      thus B is subcategory of A & (B opp ) is subcategory of (A opp ) by Th48;

      take G = ( dualizing-func (B,(B opp )));

      thus G is bijective;



       A2: (A,(A opp )) are_opposite by YELLOW18:def 4;

      hereby

        let a be Object of B, a1 be Object of A;

        assume a = a1;



        hence (G . a) = a1 by A1, YELLOW18:def 5

        .= (F . a1) by A2, YELLOW18:def 5;

      end;

      let b,c be Object of B, b1,c1 be Object of A such that

       A3: <^b, c^> <> {} and

       A4: b = b1 & c = c1;

      let f be Morphism of b, c, f1 be Morphism of b1, c1 such that

       A5: f = f1;



       A6: <^b, c^> c= <^b1, c1^> & f in <^b, c^> by A3, A4, ALTCAT_2: 31;

      then

       A7: <^(F . c1), (F . b1)^> <> {} by FUNCTOR0:def 19;



      thus (G . f) = f by A1, A3, YELLOW18:def 5

      .= (F . f1) by A2, A5, A6, YELLOW18:def 5

      .= (( Morph-Map (F,b1,c1)) . f1) by A6, A7, FUNCTOR0:def 16;

    end;

    theorem :: YELLOW20:50

    for A1,A2 be category, F be covariant Functor of A1, A2 st F is bijective holds for B1 be non empty subcategory of A1 holds for B2 be non empty subcategory of A2 st (B1,B2) are_isomorphic_under F holds (B2,B1) are_isomorphic_under (F " )

    proof

      let A1,A2 be category, F be covariant Functor of A1, A2 such that

       A1: F is bijective;

      F is surjective by A1;

      then F is onto;

      then

       A2: F is coreflexive by FUNCTOR0: 46;

      ex H be Functor of A2, A1 st H = (F " ) & H is bijective covariant by A1, FUNCTOR0: 48;

      then

      reconsider F9 = (F " ) as covariant Functor of A2, A1;

      let B1 be non empty subcategory of A1;

      let B2 be non empty subcategory of A2 such that B1 is subcategory of A1 and B2 is subcategory of A2;

      given G be covariant Functor of B1, B2 such that

       A3: G is bijective and

       A4: for a be Object of B1, a1 be Object of A1 st a = a1 holds (G . a) = (F . a1) and

       A5: for b,c be Object of B1, b1,c1 be Object of A1 st <^b, c^> <> {} & b = b1 & c = c1 holds for f be Morphism of b, c, f1 be Morphism of b1, c1 st f = f1 holds (G . f) = (( Morph-Map (F,b1,c1)) . f1);

      G is surjective by A3;

      then G is onto;

      then

       A6: G is coreflexive by FUNCTOR0: 46;

      thus B2 is subcategory of A2 & B1 is subcategory of A1;

      consider H be Functor of B2, B1 such that

       A7: H = (G " ) and

       A8: H is bijective covariant by A3, FUNCTOR0: 48;

      reconsider H as covariant Functor of B2, B1 by A8;

      take H;

      thus H is bijective by A8;



       A9: the carrier of B1 c= the carrier of A1 by ALTCAT_2:def 11;

      now

        let a be Object of B2, a1 be Object of A2;

        reconsider Ha = (H . a) as Object of A1 by A9;

        (G . (H . a)) = (F . Ha) by A4;

        then

         A11: (F . Ha) = a by A3, A7, A6, Th1;

        assume a = a1;

        hence (H . a) = ((F " ) . a1) by A1, A2, A11, Th1;

      end;

      let b,c be Object of B2, b1,c1 be Object of A2 such that

       A12: <^b, c^> <> {} and

       A13: b = b1 & c = c1;

      let f be Morphism of b, c, f1 be Morphism of b1, c1 such that

       A14: f = f1;



       A15: <^b, c^> c= <^b1, c1^> & f in <^b, c^> by A12, A13, ALTCAT_2: 31;



       A16: (G . (H . b)) = b & (G . (H . c)) = c by A3, A7, A6, Th1;



       A17: <^(H . b), (H . c)^> <> {} by A12, FUNCTOR0:def 18;

      then

       A18: (H . f) in <^(H . b), (H . c)^>;



       A19: (F . ((F " ) . b1)) = b1 & (F . ((F " ) . c1)) = c1 by A1, A2, Th1;



       A20: (H . b) = ((F " ) . b1) & (H . c) = ((F " ) . c1) by A10, A13;

      then

       A21: <^(H . b), (H . c)^> c= <^((F " ) . b1), ((F " ) . c1)^> by ALTCAT_2: 31;

      then

      reconsider Hf = (H . f) as Morphism of ((F " ) . b1), ((F " ) . c1) by A18;

      (G . (H . f)) = (( Morph-Map (F,((F " ) . b1),((F " ) . c1))) . Hf) by A5, A20, A17

      .= (F . Hf) by A21, A18, A15, A19, FUNCTOR0:def 15;

      then (F . Hf) = f by A3, A7, A17, A16, Th2;



      hence (H . f) = (F9 . f1) by A1, A14, A21, A18, A19, Th2

      .= (( Morph-Map ((F " ),b1,c1)) . f1) by A21, A18, A15, FUNCTOR0:def 15;

    end;

    theorem :: YELLOW20:51

    for A1,A2 be category, F be contravariant Functor of A1, A2 st F is bijective holds for B1 be non empty subcategory of A1 holds for B2 be non empty subcategory of A2 st (B1,B2) are_anti-isomorphic_under F holds (B2,B1) are_anti-isomorphic_under (F " )

    proof

      let A1,A2 be category, F be contravariant Functor of A1, A2 such that

       A1: F is bijective;

      F is surjective by A1;

      then F is onto;

      then

       A2: F is coreflexive by FUNCTOR0: 47;

      ex H be Functor of A2, A1 st H = (F " ) & H is bijective contravariant by A1, FUNCTOR0: 49;

      then

      reconsider F9 = (F " ) as contravariant Functor of A2, A1;

      let B1 be non empty subcategory of A1;

      let B2 be non empty subcategory of A2 such that B1 is subcategory of A1 and B2 is subcategory of A2;

      given G be contravariant Functor of B1, B2 such that

       A3: G is bijective and

       A4: for a be Object of B1, a1 be Object of A1 st a = a1 holds (G . a) = (F . a1) and

       A5: for b,c be Object of B1, b1,c1 be Object of A1 st <^b, c^> <> {} & b = b1 & c = c1 holds for f be Morphism of b, c, f1 be Morphism of b1, c1 st f = f1 holds (G . f) = (( Morph-Map (F,b1,c1)) . f1);

      G is surjective by A3;

      then G is onto;

      then

       A6: G is coreflexive by FUNCTOR0: 47;

      thus B2 is subcategory of A2 & B1 is subcategory of A1;

      consider H be Functor of B2, B1 such that

       A7: H = (G " ) and

       A8: H is bijective contravariant by A3, FUNCTOR0: 49;

      reconsider H as contravariant Functor of B2, B1 by A8;

      take H;

      thus H is bijective by A8;



       A9: the carrier of B1 c= the carrier of A1 by ALTCAT_2:def 11;

      now

        let a be Object of B2, a1 be Object of A2;

        reconsider Ha = (H . a) as Object of A1 by A9;

        (G . (H . a)) = (F . Ha) by A4;

        then

         A11: (F . Ha) = a by A3, A7, A6, Th1;

        assume a = a1;

        hence (H . a) = ((F " ) . a1) by A1, A2, A11, Th1;

      end;

      let b,c be Object of B2, b1,c1 be Object of A2 such that

       A12: <^b, c^> <> {} and

       A13: b = b1 & c = c1;

      let f be Morphism of b, c, f1 be Morphism of b1, c1 such that

       A14: f = f1;



       A15: <^b, c^> c= <^b1, c1^> & f in <^b, c^> by A12, A13, ALTCAT_2: 31;



       A16: (G . (H . b)) = b & (G . (H . c)) = c by A3, A7, A6, Th1;



       A17: <^(H . c), (H . b)^> <> {} by A12, FUNCTOR0:def 19;

      then

       A18: (H . f) in <^(H . c), (H . b)^>;



       A19: (F . ((F " ) . b1)) = b1 & (F . ((F " ) . c1)) = c1 by A1, A2, Th1;



       A20: (H . b) = ((F " ) . b1) & (H . c) = ((F " ) . c1) by A10, A13;

      then

       A21: <^(H . c), (H . b)^> c= <^((F " ) . c1), ((F " ) . b1)^> by ALTCAT_2: 31;

      then

      reconsider Hf = (H . f) as Morphism of ((F " ) . c1), ((F " ) . b1) by A18;

      (G . (H . f)) = (( Morph-Map (F,((F " ) . c1),((F " ) . b1))) . Hf) by A5, A20, A17

      .= (F . Hf) by A21, A18, A15, A19, FUNCTOR0:def 16;

      then (F . Hf) = f by A3, A7, A17, A16, Th3;



      hence (H . f) = (F9 . f1) by A1, A14, A21, A18, A19, Th3

      .= (( Morph-Map ((F " ),b1,c1)) . f1) by A21, A18, A15, FUNCTOR0:def 16;

    end;

    theorem :: YELLOW20:52

    for A1,A2,A3 be category holds for F be covariant Functor of A1, A2 holds for G be covariant Functor of A2, A3 holds for B1 be non empty subcategory of A1 holds for B2 be non empty subcategory of A2 holds for B3 be non empty subcategory of A3 st (B1,B2) are_isomorphic_under F & (B2,B3) are_isomorphic_under G holds (B1,B3) are_isomorphic_under (G * F)

    proof

      let A1,A2,A3 be category;

      let F be covariant Functor of A1, A2;

      let G be covariant Functor of A2, A3;

      let B1 be non empty subcategory of A1;

      let B2 be non empty subcategory of A2;

      let B3 be non empty subcategory of A3;

      assume that B1 is subcategory of A1 and B2 is subcategory of A2;

      given F1 be covariant Functor of B1, B2 such that

       A1: F1 is bijective and

       A2: for a be Object of B1, a1 be Object of A1 st a = a1 holds (F1 . a) = (F . a1) and

       A3: for b,c be Object of B1, b1,c1 be Object of A1 st <^b, c^> <> {} & b = b1 & c = c1 holds for f be Morphism of b, c, f1 be Morphism of b1, c1 st f = f1 holds (F1 . f) = (( Morph-Map (F,b1,c1)) . f1);

      assume that B2 is subcategory of A2 and B3 is subcategory of A3;

      given G1 be covariant Functor of B2, B3 such that

       A4: G1 is bijective and

       A5: for a be Object of B2, a1 be Object of A2 st a = a1 holds (G1 . a) = (G . a1) and

       A6: for b,c be Object of B2, b1,c1 be Object of A2 st <^b, c^> <> {} & b = b1 & c = c1 holds for f be Morphism of b, c, f1 be Morphism of b1, c1 st f = f1 holds (G1 . f) = (( Morph-Map (G,b1,c1)) . f1);

      thus B1 is subcategory of A1 & B3 is subcategory of A3;

      take (G1 * F1);

      thus (G1 * F1) is bijective by A1, A4, FUNCTOR1: 12;

      hereby

        let a be Object of B1, b be Object of A1;

        assume a = b;

        then (G1 . (F1 . a)) = (G . (F . b)) by A2, A5;



        hence ((G1 * F1) . a) = (G . (F . b)) by FUNCTOR0: 33

        .= ((G * F) . b) by FUNCTOR0: 33;

      end;

      let b,c be Object of B1, b1,c1 be Object of A1 such that

       A7: <^b, c^> <> {} and

       A8: b = b1 & c = c1;



       A9: ((G * F) . b1) = (G . (F . b1)) & ((G * F) . c1) = (G . (F . c1)) by FUNCTOR0: 33;

      let f be Morphism of b, c, f1 be Morphism of b1, c1;



       A10: f in <^b, c^> & <^b, c^> c= <^b1, c1^> by A7, A8, ALTCAT_2: 31;

      then

       A11: <^((G * F) . b1), ((G * F) . c1)^> <> {} by FUNCTOR0:def 18;



       A12: <^(F1 . b), (F1 . c)^> <> {} by A7, FUNCTOR0:def 18;

      then

       A13: (F1 . f) in <^(F1 . b), (F1 . c)^>;



       A14: (F1 . b) = (F . b1) & (F1 . c) = (F . c1) by A2, A8;

      then

       A15: <^(F1 . b), (F1 . c)^> c= <^(F . b1), (F . c1)^> by ALTCAT_2: 31;

      assume f = f1;



      then (F1 . f) = (( Morph-Map (F,b1,c1)) . f1) by A3, A7, A8

      .= (F . f1) by A10, A13, A15, FUNCTOR0:def 15;

      then (G1 . (F1 . f)) = (( Morph-Map (G,(F . b1),(F . c1))) . (F . f1)) by A6, A12, A14;



      hence ((G1 * F1) . f) = (( Morph-Map (G,(F . b1),(F . c1))) . (F . f1)) by A7, FUNCTOR3: 6

      .= (G . (F . f1)) by A13, A15, A11, A9, FUNCTOR0:def 15

      .= ((G * F) . f1) by A10, FUNCTOR3: 6

      .= (( Morph-Map ((G * F),b1,c1)) . f1) by A10, A11, FUNCTOR0:def 15;

    end;

    theorem :: YELLOW20:53

    for A1,A2,A3 be category holds for F be contravariant Functor of A1, A2 holds for G be covariant Functor of A2, A3 holds for B1 be non empty subcategory of A1 holds for B2 be non empty subcategory of A2 holds for B3 be non empty subcategory of A3 st (B1,B2) are_anti-isomorphic_under F & (B2,B3) are_isomorphic_under G holds (B1,B3) are_anti-isomorphic_under (G * F)

    proof

      let A1,A2,A3 be category;

      let F be contravariant Functor of A1, A2;

      let G be covariant Functor of A2, A3;

      let B1 be non empty subcategory of A1;

      let B2 be non empty subcategory of A2;

      let B3 be non empty subcategory of A3;

      assume that B1 is subcategory of A1 and B2 is subcategory of A2;

      given F1 be contravariant Functor of B1, B2 such that

       A1: F1 is bijective and

       A2: for a be Object of B1, a1 be Object of A1 st a = a1 holds (F1 . a) = (F . a1) and

       A3: for b,c be Object of B1, b1,c1 be Object of A1 st <^b, c^> <> {} & b = b1 & c = c1 holds for f be Morphism of b, c, f1 be Morphism of b1, c1 st f = f1 holds (F1 . f) = (( Morph-Map (F,b1,c1)) . f1);

      assume that B2 is subcategory of A2 and B3 is subcategory of A3;

      given G1 be covariant Functor of B2, B3 such that

       A4: G1 is bijective and

       A5: for a be Object of B2, a1 be Object of A2 st a = a1 holds (G1 . a) = (G . a1) and

       A6: for b,c be Object of B2, b1,c1 be Object of A2 st <^b, c^> <> {} & b = b1 & c = c1 holds for f be Morphism of b, c, f1 be Morphism of b1, c1 st f = f1 holds (G1 . f) = (( Morph-Map (G,b1,c1)) . f1);

      thus B1 is subcategory of A1 & B3 is subcategory of A3;

      take (G1 * F1);

      thus (G1 * F1) is bijective by A1, A4, FUNCTOR1: 12;

      hereby

        let a be Object of B1, b be Object of A1;

        assume a = b;

        then (G1 . (F1 . a)) = (G . (F . b)) by A2, A5;



        hence ((G1 * F1) . a) = (G . (F . b)) by FUNCTOR0: 33

        .= ((G * F) . b) by FUNCTOR0: 33;

      end;

      let b,c be Object of B1, b1,c1 be Object of A1 such that

       A7: <^b, c^> <> {} and

       A8: b = b1 & c = c1;



       A9: ((G * F) . b1) = (G . (F . b1)) & ((G * F) . c1) = (G . (F . c1)) by FUNCTOR0: 33;

      let f be Morphism of b, c, f1 be Morphism of b1, c1;



       A10: f in <^b, c^> & <^b, c^> c= <^b1, c1^> by A7, A8, ALTCAT_2: 31;

      then

       A11: <^((G * F) . c1), ((G * F) . b1)^> <> {} by FUNCTOR0:def 19;



       A12: <^(F1 . c), (F1 . b)^> <> {} by A7, FUNCTOR0:def 19;

      then

       A13: (F1 . f) in <^(F1 . c), (F1 . b)^>;



       A14: (F1 . b) = (F . b1) & (F1 . c) = (F . c1) by A2, A8;

      then

       A15: <^(F1 . c), (F1 . b)^> c= <^(F . c1), (F . b1)^> by ALTCAT_2: 31;

      assume f = f1;



      then (F1 . f) = (( Morph-Map (F,b1,c1)) . f1) by A3, A7, A8

      .= (F . f1) by A10, A13, A15, FUNCTOR0:def 16;

      then (G1 . (F1 . f)) = (( Morph-Map (G,(F . c1),(F . b1))) . (F . f1)) by A6, A12, A14;



      hence ((G1 * F1) . f) = (( Morph-Map (G,(F . c1),(F . b1))) . (F . f1)) by A7, FUNCTOR3: 9

      .= (G . (F . f1)) by A13, A15, A11, A9, FUNCTOR0:def 15

      .= ((G * F) . f1) by A10, FUNCTOR3: 9

      .= (( Morph-Map ((G * F),b1,c1)) . f1) by A10, A11, FUNCTOR0:def 16;

    end;

    theorem :: YELLOW20:54

    for A1,A2,A3 be category holds for F be covariant Functor of A1, A2 holds for G be contravariant Functor of A2, A3 holds for B1 be non empty subcategory of A1 holds for B2 be non empty subcategory of A2 holds for B3 be non empty subcategory of A3 st (B1,B2) are_isomorphic_under F & (B2,B3) are_anti-isomorphic_under G holds (B1,B3) are_anti-isomorphic_under (G * F)

    proof

      let A1,A2,A3 be category;

      let F be covariant Functor of A1, A2;

      let G be contravariant Functor of A2, A3;

      let B1 be non empty subcategory of A1;

      let B2 be non empty subcategory of A2;

      let B3 be non empty subcategory of A3;

      assume that B1 is subcategory of A1 and B2 is subcategory of A2;

      given F1 be covariant Functor of B1, B2 such that

       A1: F1 is bijective and

       A2: for a be Object of B1, a1 be Object of A1 st a = a1 holds (F1 . a) = (F . a1) and

       A3: for b,c be Object of B1, b1,c1 be Object of A1 st <^b, c^> <> {} & b = b1 & c = c1 holds for f be Morphism of b, c, f1 be Morphism of b1, c1 st f = f1 holds (F1 . f) = (( Morph-Map (F,b1,c1)) . f1);

      assume that B2 is subcategory of A2 and B3 is subcategory of A3;

      given G1 be contravariant Functor of B2, B3 such that

       A4: G1 is bijective and

       A5: for a be Object of B2, a1 be Object of A2 st a = a1 holds (G1 . a) = (G . a1) and

       A6: for b,c be Object of B2, b1,c1 be Object of A2 st <^b, c^> <> {} & b = b1 & c = c1 holds for f be Morphism of b, c, f1 be Morphism of b1, c1 st f = f1 holds (G1 . f) = (( Morph-Map (G,b1,c1)) . f1);

      thus B1 is subcategory of A1 & B3 is subcategory of A3;

      take (G1 * F1);

      thus (G1 * F1) is bijective by A1, A4, FUNCTOR1: 12;

      hereby

        let a be Object of B1, b be Object of A1;

        assume a = b;

        then (G1 . (F1 . a)) = (G . (F . b)) by A2, A5;



        hence ((G1 * F1) . a) = (G . (F . b)) by FUNCTOR0: 33

        .= ((G * F) . b) by FUNCTOR0: 33;

      end;

      let b,c be Object of B1, b1,c1 be Object of A1 such that

       A7: <^b, c^> <> {} and

       A8: b = b1 & c = c1;



       A9: ((G * F) . b1) = (G . (F . b1)) & ((G * F) . c1) = (G . (F . c1)) by FUNCTOR0: 33;

      let f be Morphism of b, c, f1 be Morphism of b1, c1;



       A10: f in <^b, c^> & <^b, c^> c= <^b1, c1^> by A7, A8, ALTCAT_2: 31;

      then

       A11: <^((G * F) . c1), ((G * F) . b1)^> <> {} by FUNCTOR0:def 19;



       A12: <^(F1 . b), (F1 . c)^> <> {} by A7, FUNCTOR0:def 18;

      then

       A13: (F1 . f) in <^(F1 . b), (F1 . c)^>;



       A14: (F1 . b) = (F . b1) & (F1 . c) = (F . c1) by A2, A8;

      then

       A15: <^(F1 . b), (F1 . c)^> c= <^(F . b1), (F . c1)^> by ALTCAT_2: 31;

      assume f = f1;



      then (F1 . f) = (( Morph-Map (F,b1,c1)) . f1) by A3, A7, A8

      .= (F . f1) by A10, A13, A15, FUNCTOR0:def 15;

      then (G1 . (F1 . f)) = (( Morph-Map (G,(F . b1),(F . c1))) . (F . f1)) by A6, A12, A14;



      hence ((G1 * F1) . f) = (( Morph-Map (G,(F . b1),(F . c1))) . (F . f1)) by A7, FUNCTOR3: 8

      .= (G . (F . f1)) by A13, A15, A11, A9, FUNCTOR0:def 16

      .= ((G * F) . f1) by A10, FUNCTOR3: 8

      .= (( Morph-Map ((G * F),b1,c1)) . f1) by A10, A11, FUNCTOR0:def 16;

    end;

    theorem :: YELLOW20:55

    for A1,A2,A3 be category holds for F be contravariant Functor of A1, A2 holds for G be contravariant Functor of A2, A3 holds for B1 be non empty subcategory of A1 holds for B2 be non empty subcategory of A2 holds for B3 be non empty subcategory of A3 st (B1,B2) are_anti-isomorphic_under F & (B2,B3) are_anti-isomorphic_under G holds (B1,B3) are_isomorphic_under (G * F)

    proof

      let A1,A2,A3 be category;

      let F be contravariant Functor of A1, A2;

      let G be contravariant Functor of A2, A3;

      let B1 be non empty subcategory of A1;

      let B2 be non empty subcategory of A2;

      let B3 be non empty subcategory of A3;

      assume that B1 is subcategory of A1 and B2 is subcategory of A2;

      given F1 be contravariant Functor of B1, B2 such that

       A1: F1 is bijective and

       A2: for a be Object of B1, a1 be Object of A1 st a = a1 holds (F1 . a) = (F . a1) and

       A3: for b,c be Object of B1, b1,c1 be Object of A1 st <^b, c^> <> {} & b = b1 & c = c1 holds for f be Morphism of b, c, f1 be Morphism of b1, c1 st f = f1 holds (F1 . f) = (( Morph-Map (F,b1,c1)) . f1);

      assume that B2 is subcategory of A2 and B3 is subcategory of A3;

      given G1 be contravariant Functor of B2, B3 such that

       A4: G1 is bijective and

       A5: for a be Object of B2, a1 be Object of A2 st a = a1 holds (G1 . a) = (G . a1) and

       A6: for b,c be Object of B2, b1,c1 be Object of A2 st <^b, c^> <> {} & b = b1 & c = c1 holds for f be Morphism of b, c, f1 be Morphism of b1, c1 st f = f1 holds (G1 . f) = (( Morph-Map (G,b1,c1)) . f1);

      thus B1 is subcategory of A1 & B3 is subcategory of A3;

      take (G1 * F1);

      thus (G1 * F1) is bijective by A1, A4, FUNCTOR1: 12;

      hereby

        let a be Object of B1, b be Object of A1;

        assume a = b;

        then (G1 . (F1 . a)) = (G . (F . b)) by A2, A5;



        hence ((G1 * F1) . a) = (G . (F . b)) by FUNCTOR0: 33

        .= ((G * F) . b) by FUNCTOR0: 33;

      end;

      let b,c be Object of B1, b1,c1 be Object of A1 such that

       A7: <^b, c^> <> {} and

       A8: b = b1 & c = c1;



       A9: ((G * F) . b1) = (G . (F . b1)) & ((G * F) . c1) = (G . (F . c1)) by FUNCTOR0: 33;

      let f be Morphism of b, c, f1 be Morphism of b1, c1;



       A10: f in <^b, c^> & <^b, c^> c= <^b1, c1^> by A7, A8, ALTCAT_2: 31;

      then

       A11: <^((G * F) . b1), ((G * F) . c1)^> <> {} by FUNCTOR0:def 18;



       A12: <^(F1 . c), (F1 . b)^> <> {} by A7, FUNCTOR0:def 19;

      then

       A13: (F1 . f) in <^(F1 . c), (F1 . b)^>;



       A14: (F1 . b) = (F . b1) & (F1 . c) = (F . c1) by A2, A8;

      then

       A15: <^(F1 . c), (F1 . b)^> c= <^(F . c1), (F . b1)^> by ALTCAT_2: 31;

      assume f = f1;



      then (F1 . f) = (( Morph-Map (F,b1,c1)) . f1) by A3, A7, A8

      .= (F . f1) by A10, A13, A15, FUNCTOR0:def 16;

      then (G1 . (F1 . f)) = (( Morph-Map (G,(F . c1),(F . b1))) . (F . f1)) by A6, A12, A14;



      hence ((G1 * F1) . f) = (( Morph-Map (G,(F . c1),(F . b1))) . (F . f1)) by A7, FUNCTOR3: 7

      .= (G . (F . f1)) by A13, A15, A11, A9, FUNCTOR0:def 16

      .= ((G * F) . f1) by A10, FUNCTOR3: 7

      .= (( Morph-Map ((G * F),b1,c1)) . f1) by A10, A11, FUNCTOR0:def 15;

    end;

    theorem :: YELLOW20:56

    for A1,A2 be non empty category, F be covariant Functor of A1, A2, B1 be non empty subcategory of A1, B2 be non empty subcategory of A2 st F is bijective & (for a be Object of A1 holds a is Object of B1 iff (F . a) is Object of B2) & (for a,b be Object of A1 st <^a, b^> <> {} holds for a1,b1 be Object of B1 st a1 = a & b1 = b holds for a2,b2 be Object of B2 st a2 = (F . a) & b2 = (F . b) holds for f be Morphism of a, b holds f in <^a1, b1^> iff (F . f) in <^a2, b2^>) holds (B1,B2) are_isomorphic_under F

    proof

      let A1,A2 be non empty category, F be covariant Functor of A1, A2, B1 be non empty subcategory of A1, B2 be non empty subcategory of A2;

      assume that

       A1: F is bijective and

       A2: for a be Object of A1 holds a is Object of B1 iff (F . a) is Object of B2 and

       A3: for a,b be Object of A1 st <^a, b^> <> {} holds for a1,b1 be Object of B1 st a1 = a & b1 = b holds for a2,b2 be Object of B2 st a2 = (F . a) & b2 = (F . b) holds for f be Morphism of a, b holds f in <^a1, b1^> iff (F . f) in <^a2, b2^>;

      thus (B1,B2) are_isomorphic_under F

      proof

        deffunc F( Object of B1, Object of B1, Morphism of $1, $2) = ((F | B1) . $3);

        deffunc O( Object of B1) = ((F | B1) . $1);



         A4: F is injective surjective by A1;



         A5: for a,b be Object of B2 st <^a, b^> <> {} holds for f be Morphism of a, b holds ex c,d be Object of B1, g be Morphism of c, d st a = O(c) & b = O(d) & <^c, d^> <> {} & f = F(c,d,g)

        proof



           A6: the carrier of B2 c= the carrier of A2 by ALTCAT_2:def 11;

          let a,b be Object of B2 such that

           A7: <^a, b^> <> {} ;

          reconsider a1 = a, b1 = b as Object of A2 by A6;

          let f be Morphism of a, b;



           A8: <^a, b^> c= <^a1, b1^> & f in <^a, b^> by A7, ALTCAT_2: 31;

          then

          reconsider f1 = f as Morphism of a1, b1;

          consider c1,d1 be Object of A1, g1 be Morphism of c1, d1 such that

           A9: a1 = (F . c1) & b1 = (F . d1) and

           A10: <^c1, d1^> <> {} and

           A11: f1 = (F . g1) by A4, A8, Th33;

          reconsider c = c1, d = d1 as Object of B1 by A2, A9;

          reconsider g = g1 as Morphism of c, d by A3, A7, A9, A10, A11;

          take c, d, g;

          g1 in <^c, d^> by A3, A7, A9, A10, A11;

          hence thesis by A9, A11, Th28, Th29;

        end;



         A12: the carrier of B1 c= the carrier of A1 by ALTCAT_2:def 11;

         A13:

        now

          let a be Object of B1;

          reconsider b = a as Object of A1 by A12;

          ((F | B1) . a) = (F . b) by Th28;

          hence O(a) is Object of B2 by A2;

        end;

         A14:

        now

          let a,b be Object of B1 such that

           A15: <^a, b^> <> {} ;

          let f be Morphism of a, b;

          reconsider c = a, d = b as Object of A1 by A12;



           A16: <^a, b^> c= <^c, d^> & f in <^a, b^> by A15, ALTCAT_2: 31;

          then

          reconsider g = f as Morphism of c, d;

          reconsider a9 = ((F | B1) . a), b9 = ((F | B1) . b) as Object of B2 by A13;



           A17: ((F | B1) . a) = (F . c) & ((F | B1) . b) = (F . d) by Th28;

          ((F | B1) . f) = (F . g) by A15, Th29;

          then ((F | B1) . f) in <^a9, b9^> by A3, A16, A17;

          hence F(a,b,f) in (the Arrows of B2 . ( O(a), O(b)));

        end;

        thus B1 is subcategory of A1 & B2 is subcategory of A2;



         A18: F is one-to-one faithful surjective by A4;

         A19:

        now

          let a,b be Object of B1 such that

           A20: <^a, b^> <> {} ;

          reconsider a1 = a, b1 = b as Object of A1 by A12;

          let f,g be Morphism of a, b;



           A21: <^a, b^> c= <^a1, b1^> & f in <^a, b^> by A20, ALTCAT_2: 31;

          reconsider f1 = f, g1 = g as Morphism of a1, b1 by A21;

          assume F(a,b,f) = F(a,b,g);



          then (F . f1) = ((F | B1) . g) by A20, Th29

          .= (F . g1) by A20, Th29;

          hence f = g by A18, A21, Th32;

        end;

         A22:

        now

          let a,b,c be Object of B1 such that

           A23: <^a, b^> <> {} and

           A24: <^b, c^> <> {} ;

          let f be Morphism of a, b, g be Morphism of b, c;

          reconsider a1 = a, b1 = b, c1 = c as Object of A1 by A12;

          let a9,b9,c9 be Object of B2 such that

           A25: a9 = O(a) and

           A26: b9 = O(b) and

           A27: c9 = O(c);

          let f9 be Morphism of a9, b9, g9 be Morphism of b9, c9 such that

           A28: f9 = F(a,b,f) and

           A29: g9 = F(b,c,g);



           A30: b9 = (F . b1) by A26, Th28;



           A31: <^b, c^> c= <^b1, c1^> & g in <^b, c^> by A24, ALTCAT_2: 31;

          then

          reconsider g1 = g as Morphism of b1, c1;



           A32: c9 = (F . c1) by A27, Th28;



           A33: <^a, b^> c= <^a1, b1^> & f in <^a, b^> by A23, ALTCAT_2: 31;

          then

          reconsider f1 = f as Morphism of a1, b1;



           A34: a9 = (F . a1) by A25, Th28;



           A35: g9 = (F . g1) by A24, A29, Th29;

          then

           A36: g9 in <^b9, c9^> by A3, A31, A30, A32;



           A37: f9 = (F . f1) by A23, A28, Th29;

          then

           A38: f9 in <^a9, b9^> by A3, A33, A34, A30;

           <^a, c^> <> {} & (g * f) = (g1 * f1) by A23, A24, ALTCAT_1:def 2, ALTCAT_2: 32;

          then ((F | B1) . (g * f)) = (F . (g1 * f1)) by Th29;



          hence F(a,c,*) = ((F . g1) * (F . f1)) by A33, A31, FUNCTOR0:def 23

          .= (g9 * f9) by A34, A30, A32, A37, A35, A38, A36, ALTCAT_2: 32;

        end;

         A39:

        now

          let a be Object of B1, a9 be Object of B2 such that

           A40: a9 = O(a);

          reconsider a1 = a as Object of A1 by A12;



          thus F(a,a,idm) = (F . ( idm a1)) by Th29, ALTCAT_2: 34

          .= ( idm (F . a1)) by FUNCTOR2: 1

          .= ( idm a9) by A40, Th28, ALTCAT_2: 34;

        end;

        consider G be covariant strict Functor of B1, B2 such that

         A41: for a be Object of B1 holds (G . a) = O(a) and

         A42: for a,b be Object of B1 st <^a, b^> <> {} holds for f be Morphism of a, b holds (G . f) = F(a,b,f) from YELLOW18:sch 8( A13, A14, A22, A39);

        take G;

         A43:

        now

          let a,b be Object of B1;

          reconsider a1 = a, b1 = b as Object of A1 by A12;

          assume O(a) = O(b);



          then (F . a1) = ((F | B1) . b) by Th28

          .= (F . b1) by Th28;

          hence a = b by A18, Th31;

        end;

        thus G is bijective from YELLOW18:sch 10( A41, A42, A43, A19, A5);

        hereby

          let a be Object of B1, a1 be Object of A1 such that

           A44: a = a1;



          thus (G . a) = ((F | B1) . a) by A41

          .= (F . a1) by A44, Th28;

        end;

        let b,c be Object of B1, b1,c1 be Object of A1 such that

         A45: <^b, c^> <> {} and

         A46: b1 = b & c1 = c;

        let f be Morphism of b, c, f1 be Morphism of b1, c1 such that

         A47: f = f1;



         A48: <^b, c^> c= <^b1, c1^> & f in <^b, c^> by A45, A46, ALTCAT_2: 31;

        then

         A49: <^(F . b1), (F . c1)^> <> {} by FUNCTOR0:def 18;



        thus (G . f) = ((F | B1) . f) by A42, A45

        .= (F . f1) by A45, A46, A47, Th29

        .= (( Morph-Map (F,b1,c1)) . f1) by A48, A49, FUNCTOR0:def 15;

      end;

    end;

    theorem :: YELLOW20:57

    for A1,A2 be non empty category, F be contravariant Functor of A1, A2, B1 be non empty subcategory of A1, B2 be non empty subcategory of A2 st F is bijective & (for a be Object of A1 holds a is Object of B1 iff (F . a) is Object of B2) & (for a,b be Object of A1 st <^a, b^> <> {} holds for a1,b1 be Object of B1 st a1 = a & b1 = b holds for a2,b2 be Object of B2 st a2 = (F . a) & b2 = (F . b) holds for f be Morphism of a, b holds f in <^a1, b1^> iff (F . f) in <^b2, a2^>) holds (B1,B2) are_anti-isomorphic_under F

    proof

      let A1,A2 be non empty category, F be contravariant Functor of A1, A2, B1 be non empty subcategory of A1, B2 be non empty subcategory of A2;

      assume that

       A1: F is bijective and

       A2: for a be Object of A1 holds a is Object of B1 iff (F . a) is Object of B2 and

       A3: for a,b be Object of A1 st <^a, b^> <> {} holds for a1,b1 be Object of B1 st a1 = a & b1 = b holds for a2,b2 be Object of B2 st a2 = (F . a) & b2 = (F . b) holds for f be Morphism of a, b holds f in <^a1, b1^> iff (F . f) in <^b2, a2^>;

      thus (B1,B2) are_anti-isomorphic_under F

      proof

        deffunc F( Object of B1, Object of B1, Morphism of $1, $2) = ((F | B1) . $3);

        deffunc O( Object of B1) = ((F | B1) . $1);



         A4: F is injective surjective by A1;



         A5: for a,b be Object of B2 st <^a, b^> <> {} holds for f be Morphism of a, b holds ex c,d be Object of B1, g be Morphism of c, d st b = O(c) & a = O(d) & <^c, d^> <> {} & f = F(c,d,g)

        proof



           A6: the carrier of B2 c= the carrier of A2 by ALTCAT_2:def 11;

          let a,b be Object of B2 such that

           A7: <^a, b^> <> {} ;

          reconsider a1 = a, b1 = b as Object of A2 by A6;

          let f be Morphism of a, b;



           A8: <^a, b^> c= <^a1, b1^> & f in <^a, b^> by A7, ALTCAT_2: 31;

          then

          reconsider f1 = f as Morphism of a1, b1;

          consider c1,d1 be Object of A1, g1 be Morphism of c1, d1 such that

           A9: b1 = (F . c1) & a1 = (F . d1) and

           A10: <^c1, d1^> <> {} and

           A11: f1 = (F . g1) by A4, A8, Th36;

          reconsider c = c1, d = d1 as Object of B1 by A2, A9;

          reconsider g = g1 as Morphism of c, d by A3, A7, A9, A10, A11;

          take c, d, g;

          g1 in <^c, d^> by A3, A7, A9, A10, A11;

          hence thesis by A9, A11, Th28, Th30;

        end;



         A12: the carrier of B1 c= the carrier of A1 by ALTCAT_2:def 11;

         A13:

        now

          let a be Object of B1;

          reconsider b = a as Object of A1 by A12;

          ((F | B1) . a) = (F . b) by Th28;

          hence O(a) is Object of B2 by A2;

        end;

         A14:

        now

          let a,b be Object of B1 such that

           A15: <^a, b^> <> {} ;

          let f be Morphism of a, b;

          reconsider c = a, d = b as Object of A1 by A12;



           A16: <^a, b^> c= <^c, d^> & f in <^a, b^> by A15, ALTCAT_2: 31;

          then

          reconsider g = f as Morphism of c, d;

          reconsider a9 = ((F | B1) . a), b9 = ((F | B1) . b) as Object of B2 by A13;



           A17: ((F | B1) . a) = (F . c) & ((F | B1) . b) = (F . d) by Th28;

          ((F | B1) . f) = (F . g) by A15, Th30;

          then ((F | B1) . f) in <^b9, a9^> by A3, A16, A17;

          hence F(a,b,f) in (the Arrows of B2 . ( O(b), O(a)));

        end;

        thus B1 is subcategory of A1 & B2 is subcategory of A2;



         A18: F is one-to-one faithful surjective by A4;

         A19:

        now

          let a,b be Object of B1 such that

           A20: <^a, b^> <> {} ;

          reconsider a1 = a, b1 = b as Object of A1 by A12;

          let f,g be Morphism of a, b;



           A21: <^a, b^> c= <^a1, b1^> & f in <^a, b^> by A20, ALTCAT_2: 31;

          reconsider f1 = f, g1 = g as Morphism of a1, b1 by A21;

          assume F(a,b,f) = F(a,b,g);



          then (F . f1) = ((F | B1) . g) by A20, Th30

          .= (F . g1) by A20, Th30;

          hence f = g by A18, A21, Th35;

        end;

         A22:

        now

          let a,b,c be Object of B1 such that

           A23: <^a, b^> <> {} and

           A24: <^b, c^> <> {} ;

          let f be Morphism of a, b, g be Morphism of b, c;

          reconsider a1 = a, b1 = b, c1 = c as Object of A1 by A12;

          let a9,b9,c9 be Object of B2 such that

           A25: a9 = O(a) and

           A26: b9 = O(b) and

           A27: c9 = O(c);

          let f9 be Morphism of b9, a9, g9 be Morphism of c9, b9 such that

           A28: f9 = F(a,b,f) and

           A29: g9 = F(b,c,g);



           A30: b9 = (F . b1) by A26, Th28;



           A31: <^b, c^> c= <^b1, c1^> & g in <^b, c^> by A24, ALTCAT_2: 31;

          then

          reconsider g1 = g as Morphism of b1, c1;



           A32: c9 = (F . c1) by A27, Th28;



           A33: <^a, b^> c= <^a1, b1^> & f in <^a, b^> by A23, ALTCAT_2: 31;

          then

          reconsider f1 = f as Morphism of a1, b1;



           A34: a9 = (F . a1) by A25, Th28;



           A35: g9 = (F . g1) by A24, A29, Th30;

          then

           A36: g9 in <^c9, b9^> by A3, A31, A30, A32;



           A37: f9 = (F . f1) by A23, A28, Th30;

          then

           A38: f9 in <^b9, a9^> by A3, A33, A34, A30;

           <^a, c^> <> {} & (g * f) = (g1 * f1) by A23, A24, ALTCAT_1:def 2, ALTCAT_2: 32;

          then ((F | B1) . (g * f)) = (F . (g1 * f1)) by Th30;



          hence F(a,c,*) = ((F . f1) * (F . g1)) by A33, A31, FUNCTOR0:def 24

          .= (f9 * g9) by A34, A30, A32, A37, A35, A38, A36, ALTCAT_2: 32;

        end;

         A39:

        now

          let a be Object of B1, a9 be Object of B2 such that

           A40: a9 = O(a);

          reconsider a1 = a as Object of A1 by A12;



          thus F(a,a,idm) = (F . ( idm a1)) by Th30, ALTCAT_2: 34

          .= ( idm (F . a1)) by ALTCAT_4: 13

          .= ( idm a9) by A40, Th28, ALTCAT_2: 34;

        end;

        consider G be contravariant strict Functor of B1, B2 such that

         A41: for a be Object of B1 holds (G . a) = O(a) and

         A42: for a,b be Object of B1 st <^a, b^> <> {} holds for f be Morphism of a, b holds (G . f) = F(a,b,f) from YELLOW18:sch 9( A13, A14, A22, A39);

        take G;

         A43:

        now

          let a,b be Object of B1;

          reconsider a1 = a, b1 = b as Object of A1 by A12;

          assume O(a) = O(b);



          then (F . a1) = ((F | B1) . b) by Th28

          .= (F . b1) by Th28;

          hence a = b by A18, Th34;

        end;

        thus G is bijective from YELLOW18:sch 12( A41, A42, A43, A19, A5);

        hereby

          let a be Object of B1, a1 be Object of A1 such that

           A44: a = a1;



          thus (G . a) = ((F | B1) . a) by A41

          .= (F . a1) by A44, Th28;

        end;

        let b,c be Object of B1, b1,c1 be Object of A1;

        assume that

         A45: <^b, c^> <> {} and

         A46: b = b1 & c = c1;

        let f be Morphism of b, c, f1 be Morphism of b1, c1 such that

         A47: f = f1;



         A48: <^b, c^> c= <^b1, c1^> & f in <^b, c^> by A45, A46, ALTCAT_2: 31;

        then

         A49: <^(F . c1), (F . b1)^> <> {} by FUNCTOR0:def 19;



        thus (G . f) = ((F | B1) . f) by A42, A45

        .= (F . f1) by A45, A46, A47, Th30

        .= (( Morph-Map (F,b1,c1)) . f1) by A48, A49, FUNCTOR0:def 16;

      end;

    end;