altcat_6.miz

    begin

    reserve I for set,

E for non empty set;

    set C = ( EnsCat { {} });



     Lm1: the carrier of C = { 0 } by ALTCAT_1:def 14;



     Lm2: ( Funcs ( {} , {} )) = { {} } by FUNCT_5: 57;

     Lm3:

    now

      let o1,o be Object of C;



       A1: o1 = {} & o = {} by Lm1, TARSKI:def 1;

       <^o1, o^> = ( Funcs (o1,o)) by ALTCAT_1:def 14;

      hence {} is Morphism of o1, o & {} in <^o1, o^> by A1, Lm1, Lm2;

    end;

     Lm4:

    now

      let o1,o be Object of C;

      let m1 be Morphism of o1, o;



       A1: o = {} & o1 = {} by Lm1, TARSKI:def 1;

       <^o1, o^> = ( Funcs (o1,o)) by ALTCAT_1:def 14;

      hence m1 = {} by A1, Lm2, TARSKI:def 1;

    end;

     Lm5:

    now

      let o1,o be Object of C;

      o = {} & o1 = {} by Lm1, TARSKI:def 1;

      hence o1 = o;

    end;

     Lm6:

    now

      let o1,o be Object of C;

      let m1,m be Morphism of o1, o;



      thus m1 = {} by Lm4

      .= m by Lm4;

    end;

    registration

      let I be non empty set;

      let A be ManySortedSet of I;

      let i be Element of I;

      cluster ( coprod (i,A)) -> Relation-like Function-like;

      coherence

      proof

        set f = ( coprod (i,A));

        thus f is Relation-like

        proof

          let x be object;

          assume x in f;

          then ex a be set st a in (A . i) & x = [a, i] by MSAFREE:def 2;

          hence thesis;

        end;

        let x,y1,y2 be object;

        assume [x, y1] in f;

        then

         A1: ex a be set st a in (A . i) & [x, y1] = [a, i] by MSAFREE:def 2;

        assume [x, y2] in f;

        then ex b be set st b in (A . i) & [x, y2] = [b, i] by MSAFREE:def 2;

        then y1 = i & y2 = i by A1, XTUPLE_0: 1;

        hence thesis;

      end;

    end

    definition

      let C be non empty AltCatStr;

      let o be Object of C;

      let I be set;

      let f be ObjectsFamily of I, C;

      :: ALTCAT_6:def1

      mode MorphismsFamily of f,o -> ManySortedSet of I means

      : Def1: for i be object st i in I holds ex o1 be Object of C st o1 = (f . i) & (it . i) is Morphism of o1, o;

      existence

      proof

        defpred P[ object, object] means ex o1 be Object of C st o1 = (f . $1) & $2 is Morphism of o1, o;



         A1: for i be object st i in I holds ex j be object st P[i, j]

        proof

          let i be object;

          assume i in I;

          then

          reconsider o1 = (f . i) as Object of C by FUNCT_2: 5;

          take the Morphism of o1, o;

          thus thesis;

        end;

        ex f be ManySortedSet of I st for i be object st i in I holds P[i, (f . i)] from PBOOLE:sch 3( A1);

        hence thesis;

      end;

    end

    definition

      let C be non empty AltCatStr;

      let o be Object of C;

      let I be non empty set;

      let f be ObjectsFamily of I, C;

      :: original: MorphismsFamily

      redefine

      :: ALTCAT_6:def2

      mode MorphismsFamily of f,o means

      : Def2: for i be Element of I holds (it . i) is Morphism of (f . i), o;

      compatibility

      proof

        let F be ManySortedSet of I;

        hereby

          assume

           A1: F is MorphismsFamily of f, o;

          let i be Element of I;

          ex o1 be Object of C st o1 = (f . i) & (F . i) is Morphism of o1, o by A1, Def1;

          hence (F . i) is Morphism of (f . i), o;

        end;

        assume

         A2: for i be Element of I holds (F . i) is Morphism of (f . i), o;

        let i be object;

        assume i in I;

        then

        reconsider j = i as Element of I;

        take (f . j);

        thus thesis by A2;

      end;

    end

    definition

      let C be non empty AltCatStr;

      let o be Object of C;

      let I be non empty set;

      let f be ObjectsFamily of I, C;

      let M be MorphismsFamily of f, o;

      let i be Element of I;

      :: original: .

      redefine

      func M . i -> Morphism of (f . i), o ;

      coherence by Def2;

    end

    registration

      let C be functional non empty AltCatStr;

      let o be Object of C;

      let I be set;

      let f be ObjectsFamily of I, C;

      cluster -> Function-yielding for MorphismsFamily of f, o;

      coherence

      proof

        let F be MorphismsFamily of f, o;

        let i be object;

        assume i in ( dom F);

        then ex o1 be Object of C st o1 = (f . i) & (F . i) is Morphism of o1, o by Def1;

        hence thesis;

      end;

    end

    theorem :: ALTCAT_6:1



     Th1: for C be non empty AltCatStr, o be Object of C holds for f be ObjectsFamily of {} , C holds {} is MorphismsFamily of f, o

    proof

      let C be non empty AltCatStr, o be Object of C, f be ObjectsFamily of {} , C;

      reconsider A = {} as {} -defined Relation;

      A is total;

      then

      reconsider A = {} as ManySortedSet of {} ;

      A is MorphismsFamily of f, o

      proof

        let i be object;

        thus thesis;

      end;

      hence thesis;

    end;

    definition

      let C be non empty AltCatStr;

      let I be set;

      let A be ObjectsFamily of I, C;

      let B be Object of C;

      let P be MorphismsFamily of A, B;

      :: ALTCAT_6:def3

      attr P is feasible means for i be set st i in I holds ex o be Object of C st o = (A . i) & (P . i) in <^o, B^>;

    end

    definition

      let C be non empty AltCatStr;

      let I be non empty set;

      let A be ObjectsFamily of I, C;

      let B be Object of C;

      let P be MorphismsFamily of A, B;

      :: original: feasible

      redefine

      :: ALTCAT_6:def4

      attr P is feasible means

      : Def4: for i be Element of I holds (P . i) in <^(A . i), B^>;

      compatibility

      proof

        thus P is feasible implies for i be Element of I holds (P . i) in <^(A . i), B^>

        proof

          assume

           A1: P is feasible;

          let i be Element of I;

          ex o be Object of C st o = (A . i) & (P . i) in <^o, B^> by A1;

          hence thesis;

        end;

        assume

         A2: for i be Element of I holds (P . i) in <^(A . i), B^>;

        let i be set;

        assume i in I;

        then

        reconsider i as Element of I;

        reconsider A as ObjectsFamily of I, C;

        take (A . i);

        thus thesis by A2;

      end;

    end

    definition

      let C be category;

      let I be set;

      let A be ObjectsFamily of I, C;

      let B be Object of C;

      let P be MorphismsFamily of A, B;

      :: ALTCAT_6:def5

      attr P is coprojection-morphisms means for X be Object of C, F be MorphismsFamily of A, X st F is feasible holds ex f be Morphism of B, X st f in <^B, X^> & (for i be set st i in I holds ex si be Object of C, Pi be Morphism of si, B st si = (A . i) & Pi = (P . i) & (F . i) = (f * Pi)) & for f1 be Morphism of B, X st for i be set st i in I holds ex si be Object of C, Pi be Morphism of si, B st si = (A . i) & Pi = (P . i) & (F . i) = (f1 * Pi) holds f = f1;

    end

    definition

      let C be category;

      let I be non empty set;

      let A be ObjectsFamily of I, C;

      let B be Object of C;

      let P be MorphismsFamily of A, B;

      :: original: coprojection-morphisms

      redefine

      :: ALTCAT_6:def6

      attr P is coprojection-morphisms means for X be Object of C, F be MorphismsFamily of A, X st F is feasible holds ex f be Morphism of B, X st f in <^B, X^> & (for i be Element of I holds (F . i) = (f * (P . i))) & for f1 be Morphism of B, X st for i be Element of I holds (F . i) = (f1 * (P . i)) holds f = f1;

      correctness

      proof

        thus P is coprojection-morphisms implies for Y be Object of C, F be MorphismsFamily of A, Y st F is feasible holds ex f be Morphism of B, Y st f in <^B, Y^> & (for i be Element of I holds (F . i) = (f * (P . i))) & for f1 be Morphism of B, Y st for i be Element of I holds (F . i) = (f1 * (P . i)) holds f = f1

        proof

          assume

           A1: P is coprojection-morphisms;

          let Y be Object of C, F be MorphismsFamily of A, Y;

          assume

           A2: F is feasible;

          consider f be Morphism of B, Y such that

           A3: f in <^B, Y^> and

           A4: for i be set st i in I holds ex si be Object of C, Pi be Morphism of si, B st si = (A . i) & Pi = (P . i) & (F . i) = (f * Pi) and

           A5: for f1 be Morphism of B, Y st for i be set st i in I holds ex si be Object of C, Pi be Morphism of si, B st si = (A . i) & Pi = (P . i) & (F . i) = (f1 * Pi) holds f = f1 by A2, A1;

          take f;

          thus f in <^B, Y^> by A3;

          hereby

            let i be Element of I;

            ex si be Object of C, Pi be Morphism of si, B st si = (A . i) & Pi = (P . i) & (F . i) = (f * Pi) by A4;

            hence (F . i) = (f * (P . i));

          end;

          let f1 be Morphism of B, Y such that

           A6: for i be Element of I holds (F . i) = (f1 * (P . i));

          for i be set st i in I holds ex si be Object of C, Pi be Morphism of si, B st si = (A . i) & Pi = (P . i) & (F . i) = (f1 * Pi)

          proof

            let i be set;

            assume i in I;

            then

            reconsider i as Element of I;

            reconsider si = (A . i) as Object of C;

            reconsider Pi = (P . i) as Morphism of si, B;

            take si, Pi;

            thus thesis by A6;

          end;

          hence thesis by A5;

        end;

        assume

         A7: for Y be Object of C, F be MorphismsFamily of A, Y st F is feasible holds ex f be Morphism of B, Y st f in <^B, Y^> & (for i be Element of I holds (F . i) = (f * (P . i))) & for f1 be Morphism of B, Y st for i be Element of I holds (F . i) = (f1 * (P . i)) holds f = f1;

        let Y be Object of C, F be MorphismsFamily of A, Y;

        assume F is feasible;

        then

        consider f be Morphism of B, Y such that

         A8: f in <^B, Y^> and

         A9: for i be Element of I holds (F . i) = (f * (P . i)) and

         A10: for f1 be Morphism of B, Y st for i be Element of I holds (F . i) = (f1 * (P . i)) holds f = f1 by A7;

        take f;

        thus f in <^B, Y^> by A8;

        thus for i be set st i in I holds ex si be Object of C, Pi be Morphism of si, B st si = (A . i) & Pi = (P . i) & (F . i) = (f * Pi)

        proof

          let i be set;

          assume i in I;

          then

          reconsider j = i as Element of I;

          take (A . j), (P . j);

          thus thesis by A9;

        end;

        let f1 be Morphism of B, Y such that

         A11: for i be set st i in I holds ex si be Object of C, Pi be Morphism of si, B st si = (A . i) & Pi = (P . i) & (F . i) = (f1 * Pi);

        now

          let i be Element of I;

          ex si be Object of C, Pi be Morphism of si, B st si = (A . i) & Pi = (P . i) & (F . i) = (f1 * Pi) by A11;

          hence (F . i) = (f1 * (P . i));

        end;

        hence thesis by A10;

      end;

    end

    registration

      let C be category, A be ObjectsFamily of {} , C;

      let B be Object of C;

      cluster -> feasible for MorphismsFamily of A, B;

      coherence ;

    end

    theorem :: ALTCAT_6:2



     Th2: for C be category, A be ObjectsFamily of {} , C holds for B be Object of C st B is initial holds ex P be MorphismsFamily of A, B st P is empty coprojection-morphisms

    proof

      let C be category;

      let A be ObjectsFamily of {} , C;

      let B be Object of C;

      assume

       A1: B is initial;

      reconsider P = {} as MorphismsFamily of A, B by Th1;

      take P;

      thus P is empty;

      let X be Object of C, F be MorphismsFamily of A, X;

      assume F is feasible;

      consider f be Morphism of B, X such that

       A2: f in <^B, X^> & for M1 be Morphism of B, X st M1 in <^B, X^> holds f = M1 by A1, ALTCAT_3: 25;

      take f;

      thus thesis by A2;

    end;

    theorem :: ALTCAT_6:3



     Th3: for A be ObjectsFamily of I, ( EnsCat { {} }), o be Object of ( EnsCat { {} }) holds (I --> {} ) is MorphismsFamily of A, o

    proof

      let A be ObjectsFamily of I, C;

      let o be Object of C;

      let i be object such that

       A1: i in I;

      reconsider I as non empty set by A1;

      reconsider j = i as Element of I by A1;

      reconsider A1 = A as ObjectsFamily of I, C;

      reconsider o1 = (A1 . j) as Object of C;

      take o1;

      thus o1 = (A . i);

      thus thesis by Lm3;

    end;

    theorem :: ALTCAT_6:4



     Th4: for A be ObjectsFamily of I, ( EnsCat { {} }), o be Object of ( EnsCat { {} }), P be MorphismsFamily of A, o st P = (I --> {} ) holds P is feasible coprojection-morphisms

    proof

      let A be ObjectsFamily of I, ( EnsCat { {} });

      let o be Object of ( EnsCat { {} });

      let P be MorphismsFamily of A, o;

      assume

       A1: P = (I --> {} );

      thus P is feasible

      proof

        let i be set;

        assume

         A2: i in I;

        then

        reconsider I as non empty set;

        reconsider i as Element of I by A2;

        reconsider A as ObjectsFamily of I, C;

        (P . i) = {} by A1;

        then (P . i) in <^(A . i), o^> by Lm3;

        hence thesis;

      end;

      let Y be Object of C, F be MorphismsFamily of A, Y;

      assume F is feasible;

      reconsider f = {} as Morphism of o, Y by Lm3;

      take f;

      thus f in <^o, Y^> by Lm3;

      thus for i be set st i in I holds ex si be Object of C, Pi be Morphism of si, o st si = (A . i) & Pi = (P . i) & (F . i) = (f * Pi)

      proof

        let i be set;

        assume

         A3: i in I;

        then

        reconsider I as non empty set;

        reconsider j = i as Element of I by A3;

        reconsider M = {} as Morphism of o, o by Lm3;

        reconsider A1 = A as ObjectsFamily of I, C;

        reconsider F1 = F as MorphismsFamily of A1, Y;

        take o, M;

        (A1 . j) = {} by Lm1, TARSKI:def 1;

        hence o = (A . i) by Lm5;

        thus M = (P . i) by A1;

        (F1 . j) is Morphism of o, Y & (f * M) is Morphism of o, Y by Lm5;

        hence thesis by Lm6;

      end;

      thus thesis by Lm4;

    end;

    definition

      let C be category;

      :: ALTCAT_6:def7

      attr C is with_coproducts means

      : Def7: for I be set, A be ObjectsFamily of I, C holds ex B be Object of C, P be MorphismsFamily of A, B st P is feasible coprojection-morphisms;

    end

    registration

      cluster ( EnsCat { {} }) -> with_coproducts;

      coherence

      proof

        let I be set, A be ObjectsFamily of I, C;

        reconsider o = {} as Object of C by Lm1, TARSKI:def 1;

        reconsider P = (I --> {} ) as MorphismsFamily of A, o by Th3;

        take o, P;

        thus thesis by Th4;

      end;

    end

    registration

      cluster with_products with_coproducts strict for category;

      existence

      proof

        take ( EnsCat { {} });

        thus thesis;

      end;

    end

    definition

      let C be category;

      let I be set, A be ObjectsFamily of I, C;

      let B be Object of C;

      :: ALTCAT_6:def8

      attr B is A -CatCoproduct-like means ex P be MorphismsFamily of A, B st P is feasible coprojection-morphisms;

    end

    registration

      let C be with_coproducts category;

      let I be set, A be ObjectsFamily of I, C;

      cluster A -CatCoproduct-like for Object of C;

      existence

      proof

        consider B be Object of C, P be MorphismsFamily of A, B such that

         A1: P is feasible coprojection-morphisms by Def7;

        take B, P;

        thus thesis by A1;

      end;

    end

    registration

      let C be category;

      let A be ObjectsFamily of {} , C;

      cluster A -CatCoproduct-like -> initial for Object of C;

      coherence

      proof

        let B be Object of C such that

         A1: B is A -CatCoproduct-like;

        for X be Object of C holds ex M be Morphism of B, X st M in <^B, X^> & for M1 be Morphism of B, X st M1 in <^B, X^> holds M = M1

        proof

          let X be Object of C;

          consider P be MorphismsFamily of A, B such that

           A2: P is feasible coprojection-morphisms by A1;

          set F = the MorphismsFamily of A, X;

          consider f be Morphism of B, X such that

           A3: f in <^B, X^> and for i be set st i in {} holds ex si be Object of C, Pi be Morphism of si, B st si = (A . i) & Pi = (P . i) & (F . i) = (f * Pi) and

           A4: for f1 be Morphism of B, X st for i be set st i in {} holds ex si be Object of C, Pi be Morphism of si, B st si = (A . i) & Pi = (P . i) & (F . i) = (f1 * Pi) holds f = f1 by A2;

          take f;

          thus f in <^B, X^> by A3;

          let M be Morphism of B, X;

          for i be set st i in {} holds ex si be Object of C, Pi be Morphism of si, B st si = (A . i) & Pi = (P . i) & (F . i) = (M * Pi);

          hence thesis by A4;

        end;

        hence thesis by ALTCAT_3: 25;

      end;

    end

    theorem :: ALTCAT_6:5

    for C be category, A be ObjectsFamily of {} , C holds for B be Object of C st B is initial holds B is A -CatCoproduct-like

    proof

      let C be category;

      let A be ObjectsFamily of {} , C;

      let B be Object of C;

      assume B is initial;

      then ex P be MorphismsFamily of A, B st P is empty coprojection-morphisms by Th2;

      hence thesis;

    end;

    theorem :: ALTCAT_6:6

    for C be category, A be ObjectsFamily of I, C, C1,C2 be Object of C st C1 is A -CatCoproduct-like & C2 is A -CatCoproduct-like holds (C1,C2) are_iso

    proof

      let C be category;

      let A be ObjectsFamily of I, C;

      let C1,C2 be Object of C;

      assume that

       A1: C1 is A -CatCoproduct-like and

       A2: C2 is A -CatCoproduct-like;

      per cases ;

        suppose I is empty;

        hence thesis by A1, A2, ALTCAT_3: 26;

      end;

        suppose I is non empty;

        then

        reconsider I as non empty set;

        reconsider A as ObjectsFamily of I, C;

        consider P1 be MorphismsFamily of A, C1 such that

         A3: P1 is feasible and

         A4: P1 is coprojection-morphisms by A1;

        consider P2 be MorphismsFamily of A, C2 such that

         A5: P2 is feasible and

         A6: P2 is coprojection-morphisms by A2;

        consider f1 be Morphism of C1, C2 such that

         A7: f1 in <^C1, C2^> and

         A8: for i be Element of I holds (P2 . i) = (f1 * (P1 . i)) and for fa be Morphism of C1, C2 st for i be Element of I holds (P2 . i) = (fa * (P1 . i)) holds f1 = fa by A4, A5;

        consider g1 be Morphism of C1, C1 such that g1 in <^C1, C1^> and for i be Element of I holds (P1 . i) = (g1 * (P1 . i)) and

         A9: for fa be Morphism of C1, C1 st for i be Element of I holds (P1 . i) = (fa * (P1 . i)) holds g1 = fa by A3, A4;

        consider f2 be Morphism of C2, C1 such that

         A10: f2 in <^C2, C1^> and

         A11: for i be Element of I holds (P1 . i) = (f2 * (P2 . i)) and for fa be Morphism of C2, C1 st for i be Element of I holds (P1 . i) = (fa * (P2 . i)) holds f2 = fa by A3, A6;

        consider g2 be Morphism of C2, C2 such that g2 in <^C2, C2^> and for i be Element of I holds (P2 . i) = (g2 * (P2 . i)) and

         A12: for fa be Morphism of C2, C2 st for i be Element of I holds (P2 . i) = (fa * (P2 . i)) holds fa = g2 by A5, A6;

        thus <^C1, C2^> <> {} & <^C2, C1^> <> {} by A7, A10;

        take f1;



         A13: f1 is retraction

        proof

          take f2;

          now

            let i be Element of I;

            (P2 . i) in <^(A . i), C2^> by A5;

            hence (P2 . i) = (( idm C2) * (P2 . i)) by ALTCAT_1: 20;

          end;

          then

           A14: g2 = ( idm C2) by A12;

          now

            let i be Element of I;

            (P2 . i) in <^(A . i), C2^> by A5;



            hence ((f1 * f2) * (P2 . i)) = (f1 * (f2 * (P2 . i))) by A7, A10, ALTCAT_1: 21

            .= (f1 * (P1 . i)) by A11

            .= (P2 . i) by A8;

          end;

          hence (f1 * f2) = ( idm C2) by A14, A12;

        end;

        f1 is coretraction

        proof

          take f2;

          now

            let i be Element of I;

            (P1 . i) in <^(A . i), C1^> by A3;

            hence (P1 . i) = (( idm C1) * (P1 . i)) by ALTCAT_1: 20;

          end;

          then

           A15: g1 = ( idm C1) by A9;

          now

            let i be Element of I;

            (P1 . i) in <^(A . i), C1^> by A3;



            hence ((f2 * f1) * (P1 . i)) = (f2 * (f1 * (P1 . i))) by A7, A10, ALTCAT_1: 21

            .= (f2 * (P2 . i)) by A8

            .= (P1 . i) by A11;

          end;

          hence (f2 * f1) = ( idm C1) by A15, A9;

        end;

        hence thesis by A7, A10, A13, ALTCAT_3: 6;

      end;

    end;

    reserve A for ObjectsFamily of I, ( EnsCat E);

    definition

      let I, E, A;

      assume

       A1: ( Union ( coprod A)) in E;

      :: ALTCAT_6:def9

      func EnsCatCoproductObj A -> Object of ( EnsCat E) equals

      : Def9: ( Union ( coprod A));

      coherence by A1, ALTCAT_1:def 14;

    end

    definition

      let I, E, A;

      :: ALTCAT_6:def10

      func Coprod (A) -> ManySortedSet of I means

      : Def10: for i be object st i in I holds ex F be Function of (A . i), ( Union ( coprod A)) st (it . i) = F & for x be object st x in (A . i) holds (F . x) = [x, i];

      existence

      proof

        defpred P[ object, object] means ex F be Function of (A . $1), ( Union ( coprod A)) st $2 = F & for x be object st x in (A . $1) holds (F . x) = [x, $1];



         A1: for i be object st i in I holds ex j be object st P[i, j]

        proof

          let i be object such that

           A2: i in I;

          defpred R[ object, object] means $2 = [$1, i];



           A3: for x be object st x in (A . i) holds ex y be object st y in ( Union ( coprod A)) & R[x, y]

          proof

            let x be object such that

             A4: x in (A . i);

            take y = [x, i];

            set Z = ( coprod (i,A));



             A5: y in Z by A2, A4, MSAFREE:def 2;



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

            (( coprod A) . i) = Z by A2, MSAFREE:def 3;

            then Z in ( rng ( coprod A)) by A2, A6, FUNCT_1: 3;

            hence y in ( Union ( coprod A)) by A5, TARSKI:def 4;

            thus R[x, y];

          end;

          ex F be Function of (A . i), ( Union ( coprod A)) st for x be object st x in (A . i) holds R[x, (F . x)] from FUNCT_2:sch 1( A3);

          hence thesis;

        end;

        ex f be ManySortedSet of I st for i be object st i in I holds P[i, (f . i)] from PBOOLE:sch 3( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let X,Y be ManySortedSet of I such that

         A7: for i be object st i in I holds ex F be Function of (A . i), ( Union ( coprod A)) st (X . i) = F & for x be object st x in (A . i) holds (F . x) = [x, i] and

         A8: for i be object st i in I holds ex F be Function of (A . i), ( Union ( coprod A)) st (Y . i) = F & for x be object st x in (A . i) holds (F . x) = [x, i];

        let i be object such that

         A9: i in I;

        consider F be Function of (A . i), ( Union ( coprod A)) such that

         A10: (X . i) = F and

         A11: for x be object st x in (A . i) holds (F . x) = [x, i] by A7, A9;

        consider G be Function of (A . i), ( Union ( coprod A)) such that

         A12: (Y . i) = G and

         A13: for x be object st x in (A . i) holds (G . x) = [x, i] by A8, A9;

        per cases ;

          suppose (A . i) is empty;

          then G = {} & F = {} ;

          hence thesis by A10, A12;

        end;

          suppose

           A14: (A . i) is non empty;

          F = G

          proof

            let x be Element of (A . i);



            thus (F . x) = [x, i] by A11, A14

            .= (G . x) by A13, A14;

          end;

          hence thesis by A10, A12;

        end;

      end;

    end

    registration

      let I, E, A;

      cluster ( Coprod A) -> Function-yielding;

      coherence

      proof

        let i be object;

        assume i in ( dom ( Coprod A));

        then ex F be Function of (A . i), ( Union ( coprod A)) st (( Coprod A) . i) = F & for x be object st x in (A . i) holds (F . x) = [x, i] by Def10;

        hence thesis;

      end;

    end

    definition

      let I, E, A;

      assume

       A1: ( Union ( coprod A)) in E;

      :: ALTCAT_6:def11

      func EnsCatCoproduct A -> MorphismsFamily of A, ( EnsCatCoproductObj A) equals

      : Def11: ( Coprod A);

      coherence

      proof

        set P = ( Coprod A);

        set B = ( EnsCatCoproductObj A);



         A2: B = ( Union ( coprod A)) by A1, Def9;

        let i be object such that

         A3: i in I;

        consider F be Function of (A . i), ( Union ( coprod A)) such that

         A4: (P . i) = F and for x be object st x in (A . i) holds (F . x) = [x, i] by A3, Def10;

        reconsider J = I as non empty set by A3;

        reconsider j = i as Element of J by A3;

        reconsider A1 = A as ObjectsFamily of J, ( EnsCat E);



         A5: <^(A1 . j), B^> = ( Funcs ((A1 . j),B)) by ALTCAT_1:def 14;

        take o1 = (A1 . j);

        thus o1 = (A . i);

        per cases ;

          suppose B <> {} ;

          hence thesis by A2, A4, A5, FUNCT_2: 8;

        end;

          suppose

           A6: B = {} ;

          then

           A7: (P . i) = {} by A4, A2;

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

          then

           A8: (( coprod A) . i) in ( rng ( coprod A)) by A3, FUNCT_1: 3;

          ( rng ( coprod A)) = {} or ( rng ( coprod A)) = { {} } by A2, A6, SCMYCIEL: 18;

          then (( coprod A) . i) = {} by A8, TARSKI:def 1;

          then (A . i) = {} by A3, MSAFREE: 2;

          hence thesis by A5, A7, A6, TARSKI:def 1, FUNCT_2: 127;

        end;

      end;

    end

    theorem :: ALTCAT_6:7



     Th7: ( Union ( coprod A)) = {} implies ( Coprod A) is empty-yielding

    proof

      assume

       A1: ( Union ( coprod A)) = {} ;

      let i be object;

      assume i in I;

      then ex F be Function of (A . i), ( Union ( coprod A)) st (( Coprod A) . i) = F & for x be object st x in (A . i) holds (F . x) = [x, i] by Def10;

      hence thesis by A1;

    end;

    theorem :: ALTCAT_6:8



     Th8: ( Union ( coprod A)) = {} implies A is empty-yielding

    proof

      assume

       A1: ( Union ( coprod A)) = {} ;

      let i be object;

      assume i in I;

      then

      consider F be Function of (A . i), ( Union ( coprod A)) such that (( Coprod A) . i) = F and

       A2: for x be object st x in (A . i) holds (F . x) = [x, i] by Def10;

      assume (A . i) is non empty;

      then

      consider x be object such that

       A3: x in (A . i) by XBOOLE_0: 7;

      (F . x) = [x, i] by A2, A3;

      hence thesis by A1;

    end;

    theorem :: ALTCAT_6:9

    ( Union ( coprod A)) in E & ( Union ( coprod A)) = {} implies ( EnsCatCoproduct A) = (I --> {} )

    proof

      assume that

       A1: ( Union ( coprod A)) in E and

       A2: ( Union ( coprod A)) = {} ;

      let i be object;

      assume i in I;



       A4: ( Coprod A) is empty-yielding by A2, Th7;



      thus (( EnsCatCoproduct A) . i) = (( Coprod A) . i) by A1, Def11

      .= {} by A4

      .= ((I --> {} ) . i);

    end;

    theorem :: ALTCAT_6:10



     Th10: ( Union ( coprod A)) in E implies ( EnsCatCoproduct A) is feasible coprojection-morphisms

    proof

      set B = ( EnsCatCoproductObj A);

      set P = ( EnsCatCoproduct A);

      assume

       A1: ( Union ( coprod A)) in E;

      then

       A2: B = ( Union ( coprod A)) by Def9;



       A3: P = ( Coprod A) by A1, Def11;

      per cases ;

        suppose

         A4: ( Union ( coprod A)) <> {} ;

        then

         A5: B <> {} by A1, Def9;

        thus

         A6: P is feasible

        proof

          let i be set;

          assume

           A7: i in I;

          then

          reconsider I as non empty set;

          reconsider i as Element of I by A7;

          reconsider A as ObjectsFamily of I, ( EnsCat E);

          reconsider P as MorphismsFamily of A, B;

          take (A . i);



           A8: <^(A . i), B^> = ( Funcs ((A . i),B)) by ALTCAT_1:def 14;

          ( Funcs ((A . i),B)) <> {} by A5;

          then (P . i) in <^(A . i), B^> by A8;

          hence thesis;

        end;

        let X be Object of ( EnsCat E), F be MorphismsFamily of A, X;

        assume

         A9: F is feasible;



         A10: <^B, X^> = ( Funcs (B,X)) by ALTCAT_1:def 14;

        defpred P[ object, object] means ($1 `2 ) in I & ($1 `1 ) in (A . ($1 `2 )) & $2 = ((F . ($1 `2 )) . ($1 `1 )) & for j be object st j in I & $1 = [($1 `1 ), j] holds ((F . j) . ($1 `1 )) = $2;



         A11: for b be object st b in B holds ex u be object st P[b, u]

        proof

          let b be object;

          assume b in B;

          then

          consider Z be set such that

           A12: b in Z and

           A13: Z in ( rng ( coprod A)) by A2, TARSKI:def 4;

          consider i be object such that

           A14: i in ( dom ( coprod A)) and

           A15: (( coprod A) . i) = Z by A13, FUNCT_1:def 3;

          (( coprod A) . i) = ( coprod (i,A)) by A14, MSAFREE:def 3;

          then

          consider x be set such that

           A16: x in (A . i) and

           A17: b = [x, i] by A12, A14, A15, MSAFREE:def 2;

          take ((F . i) . x);

          thus (b `2 ) in I & (b `1 ) in (A . (b `2 )) & ((F . (b `2 )) . (b `1 )) = ((F . i) . x) by A14, A16, A17;

          let j be object such that j in I and

           A18: b = [(b `1 ), j];

          thus thesis by A17, A18, XTUPLE_0: 1;

        end;

        consider ff be Function such that

         A19: ( dom ff) = B and

         A20: for x be object st x in B holds P[x, (ff . x)] from CLASSES1:sch 1( A11);



         A21: ( rng ff) c= X

        proof

          let y be object;

          assume y in ( rng ff);

          then

          consider x be object such that

           A22: x in ( dom ff) and

           A23: (ff . x) = y by FUNCT_1:def 3;

          set i = (x `2 );



           A24: i in I by A19, A20, A22;



           A25: (x `1 ) in (A . i) by A19, A20, A22;



           A26: (ff . x) = ((F . i) . (x `1 )) by A19, A20, A22;

          consider o1 be Object of ( EnsCat E) such that

           A27: o1 = (A . i) and (F . i) is Morphism of o1, X by A24, Def1;



           A28: <^o1, X^> = ( Funcs (o1,X)) by ALTCAT_1:def 14;

          then

           A29: X <> {} by A24, A25, A27, A9, Def4;

          (F . i) is Function of o1, X by A9, A24, A27, A28, Def4, FUNCT_2: 66;

          hence thesis by A23, A25, A26, A27, A29, FUNCT_2: 5;

        end;

        then

        reconsider ff as Morphism of B, X by A10, A19, FUNCT_2:def 2;

        take ff;

        thus

         A30: ff in <^B, X^> by A10, A21, A19, FUNCT_2:def 2;

        thus for i be set st i in I holds ex si be Object of ( EnsCat E), Pi be Morphism of si, B st si = (A . i) & Pi = (P . i) & (F . i) = (ff * Pi)

        proof

          let i be set;

          assume

           A31: i in I;

          then

          reconsider I as non empty set;

          reconsider j = i as Element of I by A31;

          reconsider A1 = A as ObjectsFamily of I, ( EnsCat E);

          reconsider P1 = P as MorphismsFamily of A1, B;

          reconsider F1 = F as MorphismsFamily of A1, X;

          take (A1 . j), (P1 . j);

          thus (A1 . j) = (A . i) & (P1 . j) = (P . i);

          reconsider p = (P1 . j) as Function;



           A32: <^(A1 . j), B^> = ( Funcs ((A1 . j),B)) by ALTCAT_1:def 14;



           A33: <^(A1 . j), B^> <> {} by A6, Def4;



           A34: <^(A1 . j), X^> = ( Funcs ((A1 . j),X)) by ALTCAT_1:def 14;

           <^(A1 . j), X^> <> {} by A9, Def4;

          then

           A35: (ff * (P1 . j)) = (ff * p) by A30, A33, ALTCAT_1: 16;



           A36: (F1 . j) in ( Funcs ((A1 . j),X)) by A34, A9, Def4;

          then

           A37: ( dom (F1 . j)) = (A1 . j) by FUNCT_2: 92;



           A38: ( dom (ff * (P1 . j))) = (A1 . j) by A34, A36, FUNCT_2: 92;



           A39: ( dom (P1 . j)) = (A1 . j) by A32, A33, FUNCT_2: 92;

          now

            let x be object;

            assume

             A40: x in ( dom (F1 . j));

            p is Function of (A1 . j), B by A32, A6, Def4, FUNCT_2: 66;

            then

             A41: (p . x) in B by A5, A37, A40, FUNCT_2: 5;

            set x1 = ((p . x) `1 );

            ex C be Function of (A . j), ( Union ( coprod A)) st (P . i) = C & for x be object st x in (A . i) holds (C . x) = [x, i] by A3, Def10;

            then

             A42: (p . x) = [x, j] by A37, A40;

            then (ff . (p . x)) = ((F . j) . x1) by A41, A20;

            hence ((ff * p) . x) = ((F1 . j) . x) by A42, A37, A40, A39, FUNCT_1: 13;

          end;

          hence (F . i) = (ff * (P1 . j)) by A35, A38, A36, FUNCT_1: 2, FUNCT_2: 92;

        end;

        let f1 be Morphism of B, X such that

         A43: for i be set st i in I holds ex si be Object of ( EnsCat E), Pi be Morphism of si, B st si = (A . i) & Pi = (P . i) & (F . i) = (f1 * Pi);

        per cases ;

          suppose X = {} ;

          then f1 = {} & ff = {} by A5, A10, SUBSET_1:def 1;

          hence ff = f1;

        end;

          suppose

           A44: X <> {} ;

          f1 is Function of B, X by A10, A30, FUNCT_2: 66;

          then

           A45: ( dom f1) = B by A44, FUNCT_2:def 1;

          now

            let x be object;

            assume

             A46: x in ( dom ff);

            set a = (x `1 );

            set i = (x `2 );



             A47: i in I by A19, A20, A46;

            then

            consider C be Function of (A . i), ( Union ( coprod A)) such that

             A48: (P . i) = C and

             A49: for x be object st x in (A . i) holds (C . x) = [x, i] by A3, Def10;

            consider si be Object of ( EnsCat E), Pi be Morphism of si, B such that si = (A . i) and

             A50: Pi = (P . i) and

             A51: (F . i) = (f1 * Pi) by A43, A47;



             A52: a in (A . i) by A19, A20, A46;

            then

             A53: a in ( dom Pi) by A48, A50, A4, FUNCT_2:def 1;



             A54: <^si, B^> = ( Funcs (si,B)) by ALTCAT_1:def 14;

             <^si, X^> = ( Funcs (si,X)) by ALTCAT_1:def 14;

            then

             A55: (f1 * Pi) = (f1 qua Function * Pi) by A2, A4, A44, A54, A10, ALTCAT_1: 16;



             A56: ex y,z be object st x = [y, z] by A2, A19, A46, CARD_3: 21;

            (C . a) = [a, i] by A49, A52;



            hence (f1 . x) = ((F . i) . a) by A48, A50, A56, A51, A53, A55, FUNCT_1: 13

            .= (ff . x) by A19, A20, A46;

          end;

          hence thesis by A19, A45, FUNCT_1: 2;

        end;

      end;

        suppose

         A57: ( Union ( coprod A)) = {} ;

        thus P is feasible

        proof

          let i be set such that

           A58: i in I;

          reconsider I as non empty set by A58;

          reconsider i as Element of I by A58;

          reconsider A as ObjectsFamily of I, ( EnsCat E);

          take (A . i);



           A59: ( Coprod A) is empty-yielding by A57, Th7;

          A is empty-yielding by A57, Th8;

          then

           A60: (A . i) = {} ;



           A61: <^(A . i), B^> = { {} } by A2, A57, A60, Lm2, ALTCAT_1:def 14;

          (P . i) = {} by A3, A59;

          hence thesis by A61, TARSKI:def 1;

        end;

        let X be Object of ( EnsCat E), F be MorphismsFamily of A, X;

        assume F is feasible;



         A62: <^B, X^> = ( Funcs (B,X)) by ALTCAT_1:def 14

        .= { {} } by A2, A57, FUNCT_5: 57;

        then

        reconsider f = {} as Morphism of B, X by TARSKI:def 1;

        take f;

        thus f in <^B, X^> by A62;

        thus for i be set st i in I holds ex si be Object of ( EnsCat E), Pi be Morphism of si, B st si = (A . i) & Pi = (P . i) & (F . i) = (f * Pi)

        proof

          let i be set such that

           A63: i in I;

          reconsider J = I as non empty set by A63;

          reconsider j = i as Element of J by A63;

          reconsider A1 = A as ObjectsFamily of J, ( EnsCat E);

          reconsider P1 = P as MorphismsFamily of A1, B;

          reconsider si = (A1 . j) as Object of ( EnsCat E);

          reconsider Pi = (P1 . j) as Morphism of si, B;

          reconsider F1 = F as MorphismsFamily of A1, X;

          reconsider F2 = (F1 . j) as Morphism of si, X;

          take si, Pi;

          thus si = (A . i) & Pi = (P . i);



           A64: A is empty-yielding by A57, Th8;

          then

           A65: si = {} ;

          then

           A66: <^si, B^> = { {} } by A2, A57, Lm2, ALTCAT_1:def 14;



           A67: <^si, X^> <> {} by A62, A64, A2, A57;



           A68: ( Funcs (si,X)) = { {} } by A65, FUNCT_5: 57;



           A69: <^si, X^> = ( Funcs (si,X)) by ALTCAT_1:def 14;



          thus (F . i) = F2

          .= {} by A68, A69, TARSKI:def 1

          .= (f qua Function * Pi)

          .= (f * Pi) by A62, A66, A67, ALTCAT_1: 16;

        end;

        thus thesis by A62, TARSKI:def 1;

      end;

    end;

    theorem :: ALTCAT_6:11

    ( Union ( coprod A)) in E implies ( EnsCatCoproductObj A) is A -CatCoproduct-like

    proof

      assume

       A1: ( Union ( coprod A)) in E;

      take ( EnsCatCoproduct A);

      thus thesis by A1, Th10;

    end;

    theorem :: ALTCAT_6:12

    (for I, A holds ( Union ( coprod A)) in E) implies ( EnsCat E) is with_coproducts

    proof

      assume

       A1: for I, A holds ( Union ( coprod A)) in E;

      let I, A;

      take ( EnsCatCoproductObj A), ( EnsCatCoproduct A);

      ( Union ( coprod A)) in E by A1;

      hence thesis by Th10;

    end;