ens_1.miz



    begin

    reserve V for non empty set,

A,B,A9,B9 for Element of V;

    definition

      let V;

      :: ENS_1:def1

      func Funcs (V) -> set equals ( union the set of all ( Funcs (A,B)));

      coherence ;

    end

    registration

      let V;

      cluster ( Funcs V) -> functional non empty;

      coherence

      proof

        set F = the set of all ( Funcs (A,B));

        set A = the Element of V;

        ( id A) in ( Funcs (A,A)) & ( Funcs (A,A)) in F by FUNCT_2: 9;

        then

        reconsider UF = ( union F) as non empty set by TARSKI:def 4;

        now

          let f be set;

          assume f in UF;

          then

          consider C be set such that

           A1: f in C and

           A2: C in F by TARSKI:def 4;

          ex A, B st C = ( Funcs (A,B)) by A2;

          hence f is Function by A1;

        end;

        hence thesis;

      end;

    end

    theorem :: ENS_1:1

    

     Th1: for f be set holds f in ( Funcs V) iff ex A, B st (B = {} implies A = {} ) & f is Function of A, B

    proof

      let f be set;

      set F = the set of all ( Funcs (A,B));

      thus f in ( Funcs V) implies ex A, B st (B = {} implies A = {} ) & f is Function of A, B

      proof

        assume f in ( Funcs V);

        then

        consider C be set such that

         A1: f in C and

         A2: C in F by TARSKI:def 4;

        consider A, B such that

         A3: C = ( Funcs (A,B)) by A2;

        take A, B;

        thus thesis by A1, A3, FUNCT_2: 66;

      end;

      given A, B such that

       A4: (B = {} implies A = {} ) & f is Function of A, B;

      

       A5: ( Funcs (A,B)) in F;

      f in ( Funcs (A,B)) by A4, FUNCT_2: 8;

      hence thesis by A5, TARSKI:def 4;

    end;

    theorem :: ENS_1:2

    ( Funcs (A,B)) c= ( Funcs V)

    proof

      let x be object;

      assume

       A1: x in ( Funcs (A,B));

      then

       A2: x is Function of A, B by FUNCT_2: 66;

      B = {} implies A = {} by A1;

      hence thesis by A2, Th1;

    end;

    theorem :: ENS_1:3

    

     Th3: for W be non empty Subset of V holds ( Funcs W) c= ( Funcs V)

    proof

      let W be non empty Subset of V;

      let f be object;

      assume f in ( Funcs W);

      then ex A,B be Element of W st (B = {} implies A = {} ) & f is Function of A, B by Th1;

      hence thesis by Th1;

    end;

    reserve f,f9 for Element of ( Funcs V);

    definition

      let V;

      :: ENS_1:def2

      func Maps (V) -> set equals { [ [A, B], f] : (B = {} implies A = {} ) & f is Function of A, B };

      coherence ;

    end

    registration

      let V;

      cluster ( Maps V) -> non empty;

      coherence

      proof

        set FV = { [ [A, B], f] : (B = {} implies A = {} ) & f is Function of A, B };

        set A = the Element of V;

        now

          set f = ( id A);

          take m = [ [A, A], f];

          

           A1: A = {} implies A = {} ;

          f in ( Funcs V) by Th1;

          hence m in FV by A1;

        end;

        hence thesis;

      end;

    end

    reserve m,m1,m2,m3,m9 for Element of ( Maps V);

    theorem :: ENS_1:4

    

     Th4: ex f, A, B st m = [ [A, B], f] & (B = {} implies A = {} ) & f is Function of A, B

    proof

      m in { [ [A, B], f] : (B = {} implies A = {} ) & f is Function of A, B };

      then ex A, B, f st m = [ [A, B], f] & (B = {} implies A = {} ) & f is Function of A, B;

      hence thesis;

    end;

    theorem :: ENS_1:5

    

     Th5: for f be Function of A, B st B = {} implies A = {} holds [ [A, B], f] in ( Maps V)

    proof

      let f be Function of A, B;

      assume

       A1: B = {} implies A = {} ;

      then f in ( Funcs V) by Th1;

      hence thesis by A1;

    end;

    theorem :: ENS_1:6

    ( Maps V) c= [: [:V, V:], ( Funcs V):]

    proof

      let m be object;

      assume m in ( Maps V);

      then ex A, B, f st m = [ [A, B], f] & (B = {} implies A = {} ) & f is Function of A, B;

      hence thesis;

    end;

    theorem :: ENS_1:7

    

     Th7: for W be non empty Subset of V holds ( Maps W) c= ( Maps V)

    proof

      let W be non empty Subset of V;

      let x be object;

      assume x in ( Maps W);

      then

      consider A,B be Element of W, f be Element of ( Funcs W) such that

       A1: x = [ [A, B], f] & (B = {} implies A = {} ) & f is Function of A, B;

      ( Funcs W) c= ( Funcs V) & f in ( Funcs W) by Th3;

      hence thesis by A1;

    end;

    

     Lm1: for x1,y1,x2,y2,x3,y3 be set st [ [x1, x2], x3] = [ [y1, y2], y3] holds x1 = y1 & x2 = y2

    proof

      let x1,y1,x2,y2,x3,y3 be set;

      assume [ [x1, x2], x3] = [ [y1, y2], y3];

      then [x1, x2] = [y1, y2] by XTUPLE_0: 1;

      hence thesis by XTUPLE_0: 1;

    end;

    registration

      let V be non empty set, m be Element of ( Maps V);

      cluster (m `2 ) -> Function-like Relation-like;

      coherence

      proof

        ex f be Element of ( Funcs V), A,B be Element of V st m = [ [A, B], f] & (B = {} implies A = {} ) & f is Function of A, B by Th4;

        hence thesis;

      end;

    end

    definition

      let V, m;

      :: ENS_1:def3

      func dom m -> Element of V equals ((m `1 ) `1 );

      coherence

      proof

        consider f, A, B such that

         A1: m = [ [A, B], f] and B = {} implies A = {} and f is Function of A, B by Th4;

         [A, B] = (m `1 ) by A1;

        hence thesis;

      end;

      :: ENS_1:def4

      func cod m -> Element of V equals ((m `1 ) `2 );

      coherence

      proof

        consider f, A, B such that

         A2: m = [ [A, B], f] and B = {} implies A = {} and f is Function of A, B by Th4;

         [A, B] = (m `1 ) by A2;

        hence thesis;

      end;

    end

    theorem :: ENS_1:8

    

     Th8: m = [ [( dom m), ( cod m)], (m `2 )]

    proof

      consider f, A, B such that

       A1: m = [ [A, B], f] & (B = {} implies A = {} ) & f is Function of A, B by Th4;

      thus thesis by A1;

    end;

    

     Lm2: (m `2 ) = (m9 `2 ) & ( dom m) = ( dom m9) & ( cod m) = ( cod m9) implies m = m9

    proof

      m = [ [( dom m), ( cod m)], (m `2 )] by Th8;

      hence thesis by Th8;

    end;

    theorem :: ENS_1:9

    

     Th9: (( cod m) <> {} or ( dom m) = {} ) & (m `2 ) is Function of ( dom m), ( cod m)

    proof

      consider f, A, B such that

       A1: m = [ [A, B], f] and

       A2: (B = {} implies A = {} ) & f is Function of A, B by Th4;

      thus thesis by A1, A2;

    end;

    

     Lm3: ( dom (m `2 )) = ( dom m) & ( rng (m `2 )) c= ( cod m)

    proof

      

       A1: (m `2 ) is Function of ( dom m), ( cod m) by Th9;

      ( cod m) <> {} or ( dom m) = {} by Th9;

      hence thesis by A1, FUNCT_2:def 1, RELAT_1:def 19;

    end;

    theorem :: ENS_1:10

    

     Th10: for f be Function, A,B be set st [ [A, B], f] in ( Maps V) holds (B = {} implies A = {} ) & f is Function of A, B

    proof

      let f be Function, A,B be set;

      assume [ [A, B], f] in ( Maps V);

      then

      consider f9, A9, B9 such that

       A1: [ [A, B], f] = [ [A9, B9], f9] and

       A2: (B9 = {} implies A9 = {} ) & f9 is Function of A9, B9 by Th4;

      f = f9 & A = A9 by A1, Lm1, XTUPLE_0: 1;

      hence thesis by A1, A2, Lm1;

    end;

    definition

      let V, A;

      :: ENS_1:def5

      func id$ A -> Element of ( Maps V) equals [ [A, A], ( id A)];

      coherence by Th5;

    end

    theorem :: ENS_1:11

    (( id$ A) `2 ) = ( id A) & ( dom ( id$ A)) = A & ( cod ( id$ A)) = A;

    definition

      let V, m1, m2;

      assume

       A1: ( cod m1) = ( dom m2);

      :: ENS_1:def6

      func m2 * m1 -> Element of ( Maps V) equals

      : Def6: [ [( dom m1), ( cod m2)], ((m2 `2 ) * (m1 `2 ))];

      coherence

      proof

        

         A2: ( cod m2) <> {} or ( dom m2) = {} by Th9;

        

         A3: ( cod m1) <> {} or ( dom m1) = {} by Th9;

        (m1 `2 ) is Function of ( dom m1), ( cod m1) & (m2 `2 ) is Function of ( dom m2), ( cod m2) by Th9;

        then ((m2 `2 ) * (m1 `2 )) is Function of ( dom m1), ( cod m2) by A1, A3, FUNCT_2: 13;

        hence thesis by A1, A3, A2, Th5;

      end;

    end

    theorem :: ENS_1:12

    

     Th12: ( dom m2) = ( cod m1) implies ((m2 * m1) `2 ) = ((m2 `2 ) * (m1 `2 )) & ( dom (m2 * m1)) = ( dom m1) & ( cod (m2 * m1)) = ( cod m2)

    proof

      assume ( dom m2) = ( cod m1);

      

      then [ [( dom m1), ( cod m2)], ((m2 `2 ) * (m1 `2 ))] = (m2 * m1) by Def6

      .= [ [( dom (m2 * m1)), ( cod (m2 * m1))], ((m2 * m1) `2 )] by Th8;

      hence thesis by Lm1, XTUPLE_0: 1;

    end;

    theorem :: ENS_1:13

    

     Th13: ( dom m2) = ( cod m1) & ( dom m3) = ( cod m2) implies (m3 * (m2 * m1)) = ((m3 * m2) * m1)

    proof

      assume that

       A1: ( dom m2) = ( cod m1) and

       A2: ( dom m3) = ( cod m2);

      

       A3: ( cod (m2 * m1)) = ( cod m2) by A1, Th12;

      ((m2 * m1) `2 ) = ((m2 `2 ) * (m1 `2 )) by A1, Th12;

      then

       A4: ((m3 * (m2 * m1)) `2 ) = ((m3 `2 ) * ((m2 `2 ) * (m1 `2 ))) by A2, A3, Th12;

      

       A5: ( dom (m3 * m2)) = ( dom m2) by A2, Th12;

      then

       A6: ( dom ((m3 * m2) * m1)) = ( dom m1) by A1, Th12;

      ( dom (m2 * m1)) = ( dom m1) by A1, Th12;

      then

       A7: ( dom (m3 * (m2 * m1))) = ( dom m1) by A2, A3, Th12;

      ( cod (m3 * m2)) = ( cod m3) by A2, Th12;

      then

       A8: ( cod ((m3 * m2) * m1)) = ( cod m3) by A1, A5, Th12;

      ((m3 * m2) `2 ) = ((m3 `2 ) * (m2 `2 )) by A2, Th12;

      then

       A9: (((m3 * m2) * m1) `2 ) = (((m3 `2 ) * (m2 `2 )) * (m1 `2 )) by A1, A5, Th12;

      ( cod (m3 * (m2 * m1))) = ( cod m3) by A2, A3, Th12;

      hence thesis by A4, A7, A9, A6, A8, Lm2, RELAT_1: 36;

    end;

    theorem :: ENS_1:14

    

     Th14: (m * ( id$ ( dom m))) = m & (( id$ ( cod m)) * m) = m

    proof

      set i1 = ( id$ ( dom m)), i2 = ( id$ ( cod m));

      

       A1: (m `2 ) is Function of ( dom m), ( cod m) by Th9;

      then

       A2: ( rng (m `2 )) c= ( cod m) by RELAT_1:def 19;

      ( cod m) <> {} or ( dom m) = {} by Th9;

      then

       A3: ( dom (m `2 )) = ( dom m) by A1, FUNCT_2:def 1;

      

       A4: ( cod i1) = ( dom m);

      then

       A5: ( cod (m * i1)) = ( cod m) by Th12;

      ((m * i1) `2 ) = ((m `2 ) * (i1 `2 )) & ( dom (m * i1)) = ( dom i1) by A4, Th12;

      hence (m * i1) = m by A3, A5, Lm2, RELAT_1: 52;

      

       A6: ( dom i2) = ( cod m);

      then

       A7: ( cod (i2 * m)) = ( cod i2) by Th12;

      ((i2 * m) `2 ) = ((i2 `2 ) * (m `2 )) & ( dom (i2 * m)) = ( dom m) by A6, Th12;

      hence thesis by A2, A7, Lm2, RELAT_1: 53;

    end;

    definition

      let V, A, B;

      :: ENS_1:def7

      func Maps (A,B) -> set equals { [ [A, B], f] where f be Element of ( Funcs V) : [ [A, B], f] in ( Maps V) };

      correctness ;

    end

    theorem :: ENS_1:15

    

     Th15: for f be Function of A, B st B = {} implies A = {} holds [ [A, B], f] in ( Maps (A,B))

    proof

      let f be Function of A, B;

      assume B = {} implies A = {} ;

      then f in ( Funcs V) & [ [A, B], f] in ( Maps V) by Th1, Th5;

      hence thesis;

    end;

    theorem :: ENS_1:16

    

     Th16: m in ( Maps (A,B)) implies m = [ [A, B], (m `2 )]

    proof

      assume m in ( Maps (A,B));

      then

       A1: ex f be Element of ( Funcs V) st m = [ [A, B], f] & [ [A, B], f] in ( Maps V);

      thus thesis by A1;

    end;

    theorem :: ENS_1:17

    

     Th17: ( Maps (A,B)) c= ( Maps V)

    proof

      let z be object;

      assume z in ( Maps (A,B));

      then ex f be Element of ( Funcs V) st z = [ [A, B], f] & [ [A, B], f] in ( Maps V);

      hence thesis;

    end;

    

     Lm4: for f be Function st [ [A, B], f] in ( Maps (A,B)) holds (B = {} implies A = {} ) & f is Function of A, B

    proof

      

       A1: ( Maps (A,B)) c= ( Maps V) by Th17;

      let f be Function;

      assume [ [A, B], f] in ( Maps (A,B));

      hence thesis by A1, Th10;

    end;

    theorem :: ENS_1:18

    ( Maps V) = ( union the set of all ( Maps (A,B)))

    proof

      set M = the set of all ( Maps (A,B));

      now

        let z be object;

        thus z in ( Maps V) implies z in ( union M)

        proof

          assume z in ( Maps V);

          then

          consider f be Element of ( Funcs V), A,B be Element of V such that

           A1: z = [ [A, B], f] & (B = {} implies A = {} ) & f is Function of A, B by Th4;

          

           A2: ( Maps (A,B)) in M;

          z in ( Maps (A,B)) by A1, Th15;

          hence thesis by A2, TARSKI:def 4;

        end;

        assume z in ( union M);

        then

        consider C be set such that

         A3: z in C and

         A4: C in M by TARSKI:def 4;

        consider A, B such that

         A5: C = ( Maps (A,B)) by A4;

        ex f be Element of ( Funcs V) st z = [ [A, B], f] & [ [A, B], f] in ( Maps V) by A3, A5;

        hence z in ( Maps V);

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: ENS_1:19

    

     Th19: m in ( Maps (A,B)) iff ( dom m) = A & ( cod m) = B

    proof

      

       A1: (m `2 ) is Function of ( dom m), ( cod m) by Th9;

      thus m in ( Maps (A,B)) implies ( dom m) = A & ( cod m) = B

      proof

        assume m in ( Maps (A,B));

        then

         A2: m = [ [A, B], (m `2 )] by Th16;

        thus thesis by A2;

      end;

      ( cod m) <> {} or ( dom m) = {} by Th9;

      then [ [( dom m), ( cod m)], (m `2 )] in ( Maps (( dom m),( cod m))) by A1, Th15;

      hence thesis by Th8;

    end;

    theorem :: ENS_1:20

    

     Th20: m in ( Maps (A,B)) implies (m `2 ) in ( Funcs (A,B))

    proof

      assume

       A1: m in ( Maps (A,B));

      then

       A2: m = [ [A, B], (m `2 )] by Th16;

      then

       A3: (m `2 ) is Function of A, B by A1, Lm4;

      B = {} implies A = {} by A1, A2, Lm4;

      hence thesis by A3, FUNCT_2: 8;

    end;

    

     Lm5: for W be non empty Subset of V, A,B be Element of W, A9,B9 be Element of V st A = A9 & B = B9 holds ( Maps (A,B)) = ( Maps (A9,B9))

    proof

      let W be non empty Subset of V;

      let A,B be Element of W, A9,B9 be Element of V such that

       A1: A = A9 & B = B9;

      now

        let x be object;

        thus x in ( Maps (A,B)) implies x in ( Maps (A9,B9))

        proof

          

           A2: ( Maps W) c= ( Maps V) by Th7;

          assume

           A3: x in ( Maps (A,B));

          

           A4: ( Maps (A,B)) c= ( Maps W) by Th17;

          then

          reconsider m = x as Element of ( Maps W) by A3;

          x in ( Maps W) by A3, A4;

          then

          reconsider m9 = x as Element of ( Maps V) by A2;

          

           A5: ( dom m) = ( dom m9) & ( cod m) = ( cod m9);

          m = [ [A, B], (m `2 )] by A3, Th16;

          then ( dom m) = A & ( cod m) = B;

          hence thesis by A1, A5, Th19;

        end;

        assume

         A6: x in ( Maps (A9,B9));

        ( Maps (A9,B9)) c= ( Maps V) by Th17;

        then

        reconsider m9 = x as Element of ( Maps V) by A6;

        

         A7: m9 = [ [A9, B9], (m9 `2 )] by A6, Th16;

        then

         A8: (m9 `2 ) is Function of A9, B9 by A6, Lm4;

        B9 = {} implies A9 = {} by A6, A7, Lm4;

        hence x in ( Maps (A,B)) by A1, A7, A8, Th15;

      end;

      hence thesis by TARSKI: 2;

    end;

    definition

      let V, m;

      :: ENS_1:def8

      attr m is surjective means ( rng (m `2 )) = ( cod m);

    end

    begin

    definition

      let V;

      :: ENS_1:def9

      func fDom V -> Function of ( Maps V), V means

      : Def9: for m holds (it . m) = ( dom m);

      existence

      proof

        deffunc F( Element of ( Maps V)) = ( dom $1);

        ex F be Function of ( Maps V), V st for m holds (F . m) = F(m) from FUNCT_2:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        let h1,h2 be Function of ( Maps V), V such that

         A1: for m holds (h1 . m) = ( dom m) and

         A2: for m holds (h2 . m) = ( dom m);

        now

          let m;

          

          thus (h1 . m) = ( dom m) by A1

          .= (h2 . m) by A2;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      :: ENS_1:def10

      func fCod V -> Function of ( Maps V), V means

      : Def10: for m holds (it . m) = ( cod m);

      existence

      proof

        deffunc F( Element of ( Maps V)) = ( cod $1);

        ex F be Function of ( Maps V), V st for m holds (F . m) = F(m) from FUNCT_2:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        let h1,h2 be Function of ( Maps V), V such that

         A3: for m holds (h1 . m) = ( cod m) and

         A4: for m holds (h2 . m) = ( cod m);

        now

          let m;

          

          thus (h1 . m) = ( cod m) by A3

          .= (h2 . m) by A4;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      :: ENS_1:def11

      func fComp V -> PartFunc of [:( Maps V), ( Maps V):], ( Maps V) means

      : Def11: (for m2, m1 holds [m2, m1] in ( dom it ) iff ( dom m2) = ( cod m1)) & for m2, m1 st ( dom m2) = ( cod m1) holds (it . [m2, m1]) = (m2 * m1);

      existence

      proof

        defpred P[ object, object, object] means for m2, m1 st m2 = $1 & m1 = $2 holds ( dom m2) = ( cod m1) & $3 = (m2 * m1);

        

         A5: for x,y,z1,z2 be object st x in ( Maps V) & y in ( Maps V) & P[x, y, z1] & P[x, y, z2] holds z1 = z2

        proof

          let x,y,z1,z2 be object;

          assume x in ( Maps V) & y in ( Maps V);

          then

          reconsider m2 = x, m1 = y as Element of ( Maps V);

          assume that

           A6: P[x, y, z1] and

           A7: P[x, y, z2];

          z1 = (m2 * m1) by A6;

          hence thesis by A7;

        end;

        

         A8: for x,y,z be object st x in ( Maps V) & y in ( Maps V) & P[x, y, z] holds z in ( Maps V)

        proof

          let x,y,z be object;

          assume x in ( Maps V) & y in ( Maps V);

          then

          reconsider m2 = x, m1 = y as Element of ( Maps V);

          assume P[x, y, z];

          then z = (m2 * m1);

          hence thesis;

        end;

        consider h be PartFunc of [:( Maps V), ( Maps V):], ( Maps V) such that

         A9: for x,y be object holds [x, y] in ( dom h) iff x in ( Maps V) & y in ( Maps V) & ex z be object st P[x, y, z] and

         A10: for x,y be object st [x, y] in ( dom h) holds P[x, y, (h . (x,y))] from BINOP_1:sch 5( A8, A5);

        take h;

        thus

         A11: for m2, m1 holds [m2, m1] in ( dom h) iff ( dom m2) = ( cod m1)

        proof

          let m2, m1;

          thus [m2, m1] in ( dom h) implies ( dom m2) = ( cod m1)

          proof

            assume [m2, m1] in ( dom h);

            then ex z be object st P[m2, m1, z] by A9;

            hence thesis;

          end;

          assume ( dom m2) = ( cod m1);

          then P[m2, m1, (m2 * m1)];

          hence thesis by A9;

        end;

        let m2, m1;

        assume ( dom m2) = ( cod m1);

        then [m2, m1] in ( dom h) by A11;

        then P[m2, m1, (h . (m2,m1))] by A10;

        hence thesis;

      end;

      uniqueness

      proof

        let h1,h2 be PartFunc of [:( Maps V), ( Maps V):], ( Maps V) such that

         A12: for m2, m1 holds [m2, m1] in ( dom h1) iff ( dom m2) = ( cod m1) and

         A13: for m2, m1 st ( dom m2) = ( cod m1) holds (h1 . [m2, m1]) = (m2 * m1) and

         A14: for m2, m1 holds [m2, m1] in ( dom h2) iff ( dom m2) = ( cod m1) and

         A15: for m2, m1 st ( dom m2) = ( cod m1) holds (h2 . [m2, m1]) = (m2 * m1);

        

         A16: ( dom h2) c= [:( Maps V), ( Maps V):] by RELAT_1:def 18;

        

         A17: ( dom h1) c= [:( Maps V), ( Maps V):] by RELAT_1:def 18;

        

         A18: ( dom h1) = ( dom h2)

        proof

          let x,y be object;

          thus [x, y] in ( dom h1) implies [x, y] in ( dom h2)

          proof

            assume

             A19: [x, y] in ( dom h1);

            then

            reconsider m2 = x, m1 = y as Element of ( Maps V) by A17, ZFMISC_1: 87;

            ( dom m2) = ( cod m1) by A12, A19;

            hence thesis by A14;

          end;

          assume

           A20: [x, y] in ( dom h2);

          then

          reconsider m2 = x, m1 = y as Element of ( Maps V) by A16, ZFMISC_1: 87;

          ( dom m2) = ( cod m1) by A14, A20;

          hence thesis by A12;

        end;

        now

          let m be Element of [:( Maps V), ( Maps V):];

          consider m2, m1 such that

           A21: m = [m2, m1] by DOMAIN_1: 1;

          assume m in ( dom h1);

          then

           A22: ( dom m2) = ( cod m1) by A12, A21;

          then (h1 . [m2, m1]) = (m2 * m1) by A13;

          hence (h1 . m) = (h2 . m) by A15, A21, A22;

        end;

        hence thesis by A18, PARTFUN1: 5;

      end;

    end

    definition

      ::$Canceled

      let V;

      :: ENS_1:def13

      func Ens (V) -> non empty non void strict CatStr equals CatStr (# V, ( Maps V), ( fDom V), ( fCod V), ( fComp V) #);

      coherence ;

    end

    registration

      let V;

      cluster ( Ens V) -> Category-like reflexive transitive associative with_identities;

      coherence

      proof

        set M = ( Maps V), d = ( fDom V), c = ( fCod V), p = ( fComp V);

        reconsider C = CatStr (# V, M, d, c, p #) as non empty non void CatStr;

        

         A1: C is Category-like

        proof

          let ff,gg be Morphism of C;

          reconsider f = ff, g = gg as Element of M;

          (d . g) = ( dom g) & (c . f) = ( cod f) by Def9, Def10;

          hence thesis by Def11;

        end;

        

         A2: C is transitive

        proof

          let ff,gg be Morphism of C such that

           A3: ( dom gg) = ( cod ff);

           [gg, ff] in ( dom the Comp of C) by A3, A1;

          then

           A4: (the Comp of C . (gg,ff)) = (gg (*) ff) by CAT_1:def 1;

          reconsider f = ff, g = gg as Element of M;

          

           A5: (d . g) = ( dom g) & (c . f) = ( cod f) by Def9, Def10;

          then

           A6: (p . [g, f]) = (g * f) by A3, Def11;

          

           A7: (d . f) = ( dom f) & (c . g) = ( cod g) by Def9, Def10;

          ( dom (g * f)) = ( dom f) & ( cod (g * f)) = ( cod g) by A3, A5, Th12;

          hence thesis by A6, A7, Def9, Def10, A4;

        end;

        

         A8: C is associative

        proof

          let ff,gg,hh be Morphism of C such that

           A9: ( dom hh) = ( cod gg) and

           A10: ( dom gg) = ( cod ff);

          reconsider f = ff, g = gg, h = hh as Element of M;

          

           A11: ( dom h) = (d . h) & ( cod g) = (c . g) by Def9, Def10;

          then

           A12: ( dom (h * g)) = ( dom g) by A9, Th12;

          

           A13: ( dom g) = (d . g) & ( cod f) = (c . f) by Def9, Def10;

          then

           A14: ( cod (g * f)) = ( dom h) by A9, A10, A11, Th12;

           [hh, gg] in ( dom the Comp of C) by A9, A1;

          then

           A15: (hh (*) gg) = (the Comp of C . (hh,gg)) by CAT_1:def 1;

          ( dom (hh (*) gg)) = ( dom gg) by A2, A9;

          then

           A16: [(hh (*) gg), ff] in ( dom the Comp of C) by A1, A10;

           [gg, ff] in ( dom the Comp of C) by A10, A1;

          then

           A17: (gg (*) ff) = (the Comp of C . (gg,ff)) by CAT_1:def 1;

          ( cod (gg (*) ff)) = ( cod gg) by A2, A10;

          then [hh, (gg (*) ff)] in ( dom the Comp of C) by A1, A9;

          

          hence (hh (*) (gg (*) ff)) = (the Comp of C . (hh,(the Comp of C . (gg,ff)))) by A17, CAT_1:def 1

          .= (p . [h, (g * f)]) by A10, A13, Def11

          .= (h * (g * f)) by A14, Def11

          .= ((h * g) * f) by A9, A10, A11, A13, Th13

          .= (p . [(h * g), f]) by A10, A13, A12, Def11

          .= (the Comp of C . ((the Comp of C . (hh,gg)),ff)) by A9, A11, Def11

          .= ((hh (*) gg) (*) ff) by A16, A15, CAT_1:def 1;

        end;

        

         A18: C is reflexive

        proof

          let a be Element of C;

          reconsider aa = a as Element of V;

          reconsider ii = ( id$ aa) as Morphism of C;

          

           A19: ( cod ii) = ( cod ( id$ aa)) by Def10

          .= a;

          ( dom ii) = ( dom ( id$ aa)) by Def9

          .= a;

          then ii in ( Hom (a,a)) by A19;

          hence ( Hom (a,a)) <> {} ;

        end;

        C is with_identities

        proof

          let a be Element of C;

          reconsider aa = a as Element of V;

          reconsider ii = ( id$ aa) as Morphism of C;

          

           A20: ( cod ii) = ( cod ( id$ aa)) by Def10

          .= a;

          

           A21: ( dom ii) = ( dom ( id$ aa)) by Def9

          .= a;

          then

          reconsider ii as Morphism of a, a by A20, CAT_1: 4;

          take ii;

          let b be Element of C;

          thus ( Hom (a,b)) <> {} implies for g be Morphism of a, b holds (g (*) ii) = g

          proof

            assume

             A22: ( Hom (a,b)) <> {} ;

            let g be Morphism of a, b;

            reconsider gg = g as Element of ( Maps V);

            

             A23: ( dom gg) = ( dom g) by Def9

            .= aa by A22, CAT_1: 5;

            then

             A24: ( cod ( id$ aa)) = ( dom gg);

            ( dom g) = a by A22, CAT_1: 5;

            then [g, ii] in ( dom p) by A20, A1;

            

            hence (g (*) ii) = (p . (g,ii)) by CAT_1:def 1

            .= (gg * ( id$ aa)) by A24, Def11

            .= g by A23, Th14;

          end;

          assume

           A25: ( Hom (b,a)) <> {} ;

          let g be Morphism of b, a;

          reconsider gg = g as Element of ( Maps V);

          

           A26: ( cod gg) = ( cod g) by Def10

          .= aa by A25, CAT_1: 5;

          then

           A27: ( dom ( id$ aa)) = ( cod gg);

          ( cod g) = a by A25, CAT_1: 5;

          then [ii, g] in ( dom p) by A21, A1;

          

          hence (ii (*) g) = (p . (ii,g)) by CAT_1:def 1

          .= (( id$ aa) * gg) by A27, Def11

          .= g by A26, Th14;

        end;

        hence thesis by A1, A2, A8, A18;

      end;

    end

    reserve a,b for Object of ( Ens V);

    ::$Canceled

    theorem :: ENS_1:22

    A is Object of ( Ens V);

    definition

      let V, A;

      :: ENS_1:def14

      func @ A -> Object of ( Ens V) equals A;

      coherence ;

    end

    theorem :: ENS_1:23

    a is Element of V;

    definition

      let V, a;

      :: ENS_1:def15

      func @ a -> Element of V equals a;

      coherence ;

    end

    reserve f,g,f1,f2 for Morphism of ( Ens V);

    theorem :: ENS_1:24

    m is Morphism of ( Ens V);

    definition

      let V, m;

      :: ENS_1:def16

      func @ m -> Morphism of ( Ens V) equals m;

      coherence ;

    end

    theorem :: ENS_1:25

    f is Element of ( Maps V);

    definition

      let V, f;

      :: ENS_1:def17

      func @ f -> Element of ( Maps V) equals f;

      coherence ;

    end

    theorem :: ENS_1:26

    ( dom f) = ( dom ( @ f)) & ( cod f) = ( cod ( @ f)) by Def9, Def10;

    theorem :: ENS_1:27

    

     Th26: ( Hom (a,b)) = ( Maps (( @ a),( @ b)))

    proof

      now

        let x be object;

        thus x in ( Hom (a,b)) implies x in ( Maps (( @ a),( @ b)))

        proof

          assume

           A1: x in ( Hom (a,b));

          then

          reconsider f = x as Morphism of ( Ens V);

          ( cod f) = b by A1, CAT_1: 1;

          then

           A2: ( cod ( @ f)) = ( @ b) by Def10;

          ( dom f) = a by A1, CAT_1: 1;

          then ( dom ( @ f)) = ( @ a) by Def9;

          hence thesis by A2, Th19;

        end;

        assume

         A3: x in ( Maps (( @ a),( @ b)));

        ( Maps (( @ a),( @ b))) c= ( Maps V) by Th17;

        then

        reconsider m = x as Element of ( Maps V) by A3;

        ( cod m) = ( @ b) by A3, Th19;

        then

         A4: ( cod ( @ m)) = b by Def10;

        ( dom m) = ( @ a) by A3, Th19;

        then ( dom ( @ m)) = a by Def9;

        hence x in ( Hom (a,b)) by A4;

      end;

      hence thesis by TARSKI: 2;

    end;

    

     Lm6: ( Hom (a,b)) <> {} implies ( Funcs (( @ a),( @ b))) <> {}

    proof

      set m = the Element of ( Maps (( @ a),( @ b)));

      assume ( Hom (a,b)) <> {} ;

      then

       A1: ( Maps (( @ a),( @ b))) <> {} by Th26;

      reconsider m as Element of ( Maps V) by A1, Th17, TARSKI:def 3;

      (m `2 ) in ( Funcs (( @ a),( @ b))) by A1, Th20;

      hence thesis;

    end;

    theorem :: ENS_1:28

    

     Th27: ( dom g) = ( cod f) implies (g (*) f) = (( @ g) * ( @ f))

    proof

      assume

       A1: ( dom g) = ( cod f);

      then ( dom ( @ g)) = ( cod f) by Def9;

      then

       A2: ( dom ( @ g)) = ( cod ( @ f)) by Def10;

      

      thus (g (*) f) = (the Comp of ( Ens V) . (( @ g),f)) by A1, CAT_1: 16

      .= (( @ g) * ( @ f)) by A2, Def11;

    end;

    theorem :: ENS_1:29

    

     Th28: ( id a) = ( id$ ( @ a))

    proof

      reconsider aa = a as Element of V;

      reconsider ii = ( id$ aa) as Morphism of ( Ens V);

      

       A1: ( cod ii) = ( cod ( id$ aa)) by Def10

      .= a;

      

       A2: ( dom ii) = ( dom ( id$ aa)) by Def9

      .= a;

      then

      reconsider ii as Morphism of a, a by A1, CAT_1: 4;

      for b be Object of ( Ens V) holds (( Hom (a,b)) <> {} implies for f be Morphism of a, b holds (f (*) ii) = f) & (( Hom (b,a)) <> {} implies for f be Morphism of b, a holds (ii (*) f) = f)

      proof

        let b be Element of ( Ens V);

        set p = the Comp of ( Ens V);

        thus ( Hom (a,b)) <> {} implies for g be Morphism of a, b holds (g (*) ii) = g

        proof

          assume

           A3: ( Hom (a,b)) <> {} ;

          let g be Morphism of a, b;

          reconsider gg = g as Element of ( Maps V);

          

           A4: ( dom gg) = ( dom g) by Def9

          .= aa by A3, CAT_1: 5;

          then

           A5: ( cod ( id$ aa)) = ( dom gg);

          ( dom g) = a by A3, CAT_1: 5;

          then [g, ii] in ( dom p) by A1, CAT_1:def 6;

          

          hence (g (*) ii) = (p . (g,ii)) by CAT_1:def 1

          .= (gg * ( id$ aa)) by A5, Def11

          .= g by A4, Th14;

        end;

        assume

         A6: ( Hom (b,a)) <> {} ;

        let g be Morphism of b, a;

        reconsider gg = g as Element of ( Maps V);

        

         A7: ( cod gg) = ( cod g) by Def10

        .= aa by A6, CAT_1: 5;

        then

         A8: ( dom ( id$ aa)) = ( cod gg);

        ( cod g) = a by A6, CAT_1: 5;

        then [ii, g] in ( dom p) by A2, CAT_1:def 6;

        

        hence (ii (*) g) = (p . (ii,g)) by CAT_1:def 1

        .= (( id$ aa) * gg) by A8, Def11

        .= g by A7, Th14;

      end;

      hence thesis by CAT_1:def 12;

    end;

    theorem :: ENS_1:30

    a = {} implies a is initial

    proof

      assume

       A1: a = {} ;

      let b;

      ( Maps (( @ a),( @ b))) <> {} by A1, Th15;

      hence

       A2: ( Hom (a,b)) <> {} by Th26;

      set m = [ [( @ a), ( @ b)], {} ];

       {} is Function of ( @ a), ( @ b) by A1, RELSET_1: 12;

      then m in ( Maps (( @ a),( @ b))) by A1, Th15;

      then m in ( Hom (a,b)) by Th26;

      then

      reconsider f = m as Morphism of a, b by CAT_1:def 5;

      take f;

      let g be Morphism of a, b;

      reconsider m9 = g as Element of ( Maps V);

      g in ( Hom (a,b)) by A2, CAT_1:def 5;

      then

       A3: g in ( Maps (( @ a),( @ b))) by Th26;

      then

       A4: m9 = [ [( @ a), ( @ b)], (m9 `2 )] by Th16;

      then (m9 `2 ) is Function of ( @ a), ( @ b) by A3, Lm4;

      hence thesis by A1, A4;

    end;

    theorem :: ENS_1:31

    

     Th30: {} in V & a is initial implies a = {}

    proof

      assume {} in V;

      then

      reconsider B = {} as Element of V;

      set b = ( @ B);

      assume a is initial;

      then ( Hom (a,b)) <> {} ;

      then ( Funcs (( @ a),( @ b))) <> {} by Lm6;

      hence thesis;

    end;

    theorem :: ENS_1:32

    for W be Universe, a be Object of ( Ens W) st a is initial holds a = {} by Th30, CLASSES2: 56;

    theorem :: ENS_1:33

    (ex x be set st a = {x}) implies a is terminal

    proof

      given x be set such that

       A1: a = {x};

      let b;

      set h = the Function of ( @ b), ( @ a);

      set m = [ [( @ b), ( @ a)], h];

      

       A2: m in ( Maps (( @ b),( @ a))) by A1, Th15;

      hence

       A3: ( Hom (b,a)) <> {} by Th26;

      m in ( Hom (b,a)) by A2, Th26;

      then

      reconsider f = m as Morphism of b, a by CAT_1:def 5;

      take f;

      let g be Morphism of b, a;

      reconsider m9 = g as Element of ( Maps V);

      g in ( Hom (b,a)) by A3, CAT_1:def 5;

      then

       A4: g in ( Maps (( @ b),( @ a))) by Th26;

      then

       A5: m9 = [ [( @ b), ( @ a)], (m9 `2 )] by Th16;

      then (m9 `2 ) is Function of ( @ b), ( @ a) by A4, Lm4;

      hence thesis by A1, A5, FUNCT_2: 51;

    end;

    theorem :: ENS_1:34

    

     Th33: V <> { {} } & a is terminal implies ex x be set st a = {x}

    proof

      assume that

       A1: V <> { {} } and

       A2: a is terminal;

      set x = the Element of ( @ a);

       A3:

      now

        assume

         A4: ( @ a) = {} ;

        now

          consider C be object such that

           A5: C in V and

           A6: C <> {} by A1, ZFMISC_1: 35;

          reconsider C as Element of V by A5;

          set b = ( @ C);

          ( Hom (b,a)) <> {} by A2;

          then ( Funcs (( @ b),( @ a))) <> {} by Lm6;

          hence contradiction by A4, A6;

        end;

        hence contradiction;

      end;

      now

        assume a <> {x};

        then

        consider y be object such that

         A7: y in ( @ a) and

         A8: y <> x by A3, ZFMISC_1: 35;

        reconsider fy = (( @ a) --> y) as Function of ( @ a), ( @ a) by A7, FUNCOP_1: 45;

        reconsider fx = (( @ a) --> x) as Function of ( @ a), ( @ a) by A7, FUNCOP_1: 45;

        (fx . y) = x by A7, FUNCOP_1: 7;

        then

         A9: fx <> fy by A7, A8, FUNCOP_1: 7;

        

         A10: [ [( @ a), ( @ a)], fx] in ( Maps (( @ a),( @ a))) by Th15;

        

         A11: [ [( @ a), ( @ a)], fy] in ( Maps (( @ a),( @ a))) by Th15;

        ( Maps (( @ a),( @ a))) c= ( Maps V) by Th17;

        then

        reconsider m1 = [ [( @ a), ( @ a)], fx], m2 = [ [( @ a), ( @ a)], fy] as Element of ( Maps V) by A10, A11;

        

         A12: m2 in ( Hom (a,a)) by A11, Th26;

        m1 in ( Hom (a,a)) by A10, Th26;

        then

        reconsider f = ( @ m1), g = ( @ m2) as Morphism of a, a by A12, CAT_1:def 5;

        consider h be Morphism of a, a such that

         A13: for h9 be Morphism of a, a holds h = h9 by A2;

        f = h by A13

        .= g by A13;

        hence contradiction by A9, XTUPLE_0: 1;

      end;

      hence thesis;

    end;

    theorem :: ENS_1:35

    for W be Universe, a be Object of ( Ens W) st a is terminal holds ex x be set st a = {x}

    proof

      let W be Universe, a be Object of ( Ens W);

      now

        

         A1: { {} } in W by CLASSES2: 56, CLASSES2: 57;

        assume W = { {} };

        hence contradiction by A1;

      end;

      hence thesis by Th33;

    end;

    theorem :: ENS_1:36

    for a,b be Object of ( Ens V), f be Morphism of a, b st ( Hom (a,b)) <> {} holds f is monic iff (( @ f) `2 ) is one-to-one

    proof

      let a,b be Object of ( Ens V), f be Morphism of a, b such that

       A1: ( Hom (a,b)) <> {} ;

      set m = ( @ f);

      

       A2: ( dom m) = ( dom f) by Def9;

      then

       A3: ( dom (m `2 )) = ( dom f) by Lm3;

      thus f is monic implies (( @ f) `2 ) is one-to-one

      proof

        set A = ( dom (( @ f) `2 ));

        assume

         A4: f is monic;

        let x1,x2 be object such that

         A5: x1 in A and

         A6: x2 in A and

         A7: ((( @ f) `2 ) . x1) = ((( @ f) `2 ) . x2);

        

         A8: A = ( dom ( @ f)) by Lm3;

        then

        reconsider A as Element of V;

        

         A9: ( dom f) = A by A8, Def9;

        reconsider fx1 = (A --> x1), fx2 = (A --> x2) as Function of A, A by A5, A6, FUNCOP_1: 45;

        reconsider m1 = [ [A, A], fx1], m2 = [ [A, A], fx2] as Element of ( Maps V) by Th5;

        set f1 = ( @ m1), f2 = ( @ m2);

        set h1 = ((( @ f) `2 ) * (( @ f1) `2 )), h2 = ((( @ f) `2 ) * (( @ f2) `2 ));

        set ff1 = (( @ f) * ( @ f1)), ff2 = (( @ f) * ( @ f2));

        

         A10: ( cod m2) = A;

        then

         A11: (ff2 `2 ) = h2 & ( dom ff2) = ( dom ( @ f2)) by A8, Th12;

        ( cod ff2) = ( cod ( @ f)) by A8, A10, Th12;

        then

         A12: ff2 = [ [( dom ( @ f2)), ( cod ( @ f))], h2] by A11, Th8;

        ( dom ( @ f2)) = A;

        then

         A13: ( dom f2) = A by Def9;

        ( cod ( @ f2)) = A;

        then

         A14: ( cod f2) = A by Def10;

        then

         A15: (f (*) f2) = ff2 by A9, Th27;

        

         A16: ( cod m1) = A;

        then

         A17: (ff1 `2 ) = h1 & ( dom ff1) = ( dom ( @ f1)) by A8, Th12;

        now

          thus

           A18: ( dom h1) = A & ( dom h2) = A by A17, A11, Lm3;

          let x be object;

          assume

           A19: x in A;

          ((( @ f1) `2 ) . x) = x1 by A19, FUNCOP_1: 7;

          then

           A20: (h1 . x) = ((( @ f) `2 ) . x1) by A18, A19, FUNCT_1: 12;

          ((( @ f2) `2 ) . x) = x2 by A19, FUNCOP_1: 7;

          hence (h1 . x) = (h2 . x) by A7, A18, A19, A20, FUNCT_1: 12;

        end;

        then

         A21: h1 = h2;

        ( cod ff1) = ( cod ( @ f)) by A8, A16, Th12;

        then

         A22: ff1 = [ [( dom ( @ f1)), ( cod ( @ f))], h1] by A17, Th8;

        ( dom ( @ f1)) = A;

        then

         A23: ( dom f1) = A by Def9;

        ( cod ( @ f1)) = A;

        then

         A24: ( cod f1) = A by Def10;

        reconsider A as Object of ( Ens V);

        

         A25: ( dom f) = a by A1, CAT_1: 5;

        then

         A26: f1 in ( Hom (A,a)) & f2 in ( Hom (A,a)) by A23, A9, A24, A13, A14;

        then

        reconsider f1, f2 as Morphism of A, a by CAT_1:def 5;

        

         A27: (f * f1) = (f (*) f1) by A1, A26, CAT_1:def 13

        .= (f (*) f2) by A22, A12, A21, A15, A24, A9, Th27

        .= (f * f2) by A1, A26, CAT_1:def 13;

        ( Hom (A,a)) <> {} by A25, A9;

        then f1 = f2 by A4, A27;

        then fx1 = fx2 by XTUPLE_0: 1;

        

        hence x1 = (fx2 . x1) by A5, FUNCOP_1: 7

        .= x2 by A5, FUNCOP_1: 7;

      end;

      assume

       A28: (m `2 ) is one-to-one;

      thus ( Hom (a,b)) <> {} by A1;

      let c be Object of ( Ens V) such that

       A29: ( Hom (c,a)) <> {} ;

      let f1,f2 be Morphism of c, a;

      

       A30: ( dom f1) = c by A29, CAT_1: 5

      .= ( dom f2) by A29, CAT_1: 5;

      

       A31: ( cod f1) = a by A29, CAT_1: 5

      .= ( dom f) by A1, CAT_1: 5;

      

       A32: ( cod f2) = a by A29, CAT_1: 5

      .= ( dom f) by A1, CAT_1: 5;

      assume

       A33: (f * f1) = (f * f2);

      set m1 = ( @ f1), m2 = ( @ f2);

      

       A34: (m * m1) = (f (*) f1) by A31, Th27

      .= (f * f1) by A29, A1, CAT_1:def 13;

      

       A35: (m * m2) = (f (*) f2) by A32, Th27

      .= (f * f2) by A29, A1, CAT_1:def 13;

      

       A36: m1 = [ [( dom m1), ( cod m1)], (m1 `2 )] by Th8;

      

       A37: ( dom m2) = ( dom f2) by Def9;

      then

       A38: ( dom (m2 `2 )) = ( dom f2) by Lm3;

      

       A39: ( cod m1) = ( cod f1) by Def10;

      then

       A40: ( rng (m1 `2 )) c= ( cod f1) by Lm3;

      

       A41: ( cod m2) = ( cod f2) by Def10;

      then

       A42: ( rng (m2 `2 )) c= ( cod f2) by Lm3;

      

       A43: (m * m2) = [ [( dom m2), ( cod m)], ((m `2 ) * (m2 `2 ))] by A32, A41, A2, Def6;

      (m * m1) = [ [( dom m1), ( cod m)], ((m `2 ) * (m1 `2 ))] by A31, A39, A2, Def6;

      then

       A44: ((m `2 ) * (m1 `2 )) = ((m `2 ) * (m2 `2 )) by A35, A33, A34, A43, XTUPLE_0: 1;

      

       A45: ( dom m1) = ( dom f1) by Def9;

      then ( dom (m1 `2 )) = ( dom f1) by Lm3;

      then (m1 `2 ) = (m2 `2 ) by A28, A30, A31, A32, A38, A3, A40, A42, A44, FUNCT_1: 27;

      hence thesis by A30, A31, A32, A45, A37, A39, A41, A36, Th8;

    end;

    theorem :: ENS_1:37

    

     Th36: for a,b be Object of ( Ens V), f be Morphism of a, b st ( Hom (a,b)) <> {} holds f is epi & (ex A st ex x1,x2 be set st x1 in A & x2 in A & x1 <> x2) implies ( @ f) is surjective

    proof

      let a,b be Object of ( Ens V), f be Morphism of a, b such that

       A1: ( Hom (a,b)) <> {} ;

      assume

       A2: f is epi;

      given B be Element of V, x1,x2 be set such that

       A3: x1 in B and

       A4: x2 in B and

       A5: x1 <> x2;

      

       A6: ( cod ( @ f)) c= ( rng (( @ f) `2 ))

      proof

        set A = ( cod ( @ f));

        reconsider g1 = (A --> x1) as Function of A, B by A3, FUNCOP_1: 45;

        let x be object;

        assume that

         A7: x in A and

         A8: not x in ( rng (( @ f) `2 ));

        set h = ( {x} --> x2), g2 = (g1 +* h);

        

         A9: ( dom h) = {x} by FUNCOP_1: 13;

        

         A10: ( rng h) = {x2} by FUNCOP_1: 8;

        ( rng g1) = {x1} by A7, FUNCOP_1: 8;

        then ( rng g2) c= ( {x1} \/ {x2}) by A10, FUNCT_4: 17;

        then

         A11: ( rng g2) c= {x1, x2} by ENUMSET1: 1;

         {x1, x2} c= B by A3, A4, ZFMISC_1: 32;

        then

         A12: ( rng g2) c= B by A11;

        ( dom g1) = A by FUNCOP_1: 13;

        

        then ( dom g2) = (A \/ {x}) by A9, FUNCT_4:def 1

        .= A by A7, ZFMISC_1: 40;

        then

        reconsider g2 as Function of A, B by A3, A12, FUNCT_2:def 1, RELSET_1: 4;

        

         A13: ( cod f) = A by Def10;

        

         A14: x in {x} by TARSKI:def 1;

        then (h . x) = x2 by FUNCOP_1: 7;

        then

         A15: (g2 . x) = x2 by A14, A9, FUNCT_4: 13;

        

         A16: (g1 . x) = x1 by A7, FUNCOP_1: 7;

        reconsider m1 = [ [A, B], g1], m2 = [ [A, B], g2] as Element of ( Maps V) by A3, Th5;

        set f1 = ( @ m1), f2 = ( @ m2);

        set h1 = ((( @ f1) `2 ) * (( @ f) `2 )), h2 = ((( @ f2) `2 ) * (( @ f) `2 ));

        set f1f = (( @ f1) * ( @ f)), f2f = (( @ f2) * ( @ f));

        

         A17: ( dom m1) = A;

        then

         A18: (f1f `2 ) = h1 & ( dom f1f) = ( dom ( @ f)) by Th12;

        

         A19: ( dom m2) = A;

        then

         A20: (f2f `2 ) = h2 & ( dom f2f) = ( dom ( @ f)) by Th12;

        ( cod ( @ f2)) = B;

        then

         A21: ( cod f2) = B by Def10;

        ( dom ( @ f2)) = A;

        then

         A22: ( dom f2) = A by Def9;

        then

         A23: (f2 (*) f) = f2f by A13, Th27;

        now

          thus

           A24: ( dom h1) = ( dom ( @ f)) & ( dom h2) = ( dom ( @ f)) by A18, A20, Lm3;

          let z be object;

          set y = ((( @ f) `2 ) . z);

          assume

           A25: z in ( dom ( @ f));

          then z in ( dom (( @ f) `2 )) by Lm3;

          then y in ( rng (( @ f) `2 )) by FUNCT_1:def 3;

          then

           A26: not y in {x} by A8, TARSKI:def 1;

          (h1 . z) = (g1 . y) & (h2 . z) = (g2 . y) by A24, A25, FUNCT_1: 12;

          hence (h1 . z) = (h2 . z) by A9, A26, FUNCT_4: 11;

        end;

        then

         A27: h1 = h2;

        ( cod f1f) = ( cod ( @ f1)) by A17, Th12;

        then

         A28: f1f = [ [( dom ( @ f)), ( cod ( @ f1))], h1] by A18, Th8;

        ( cod f2f) = ( cod ( @ f2)) by A19, Th12;

        then

         A29: f2f = [ [( dom ( @ f)), ( cod ( @ f2))], h2] by A20, Th8;

        

         A30: f1f = f2f by A28, A29, A27;

        ( cod ( @ f1)) = B;

        then

         A31: ( cod f1) = B by Def10;

        ( dom ( @ f1)) = A;

        then

         A32: ( dom f1) = A by Def9;

        reconsider B as Object of ( Ens V);

        

         A33: ( cod f) = b by A1, CAT_1: 5;

        then

         A34: f1 in ( Hom (b,B)) by A13, A31, A32;

        then

        reconsider f1 as Morphism of b, B by CAT_1:def 5;

        f2 in ( Hom (b,B)) by A13, A21, A22, A33;

        then

        reconsider f2 as Morphism of b, B by CAT_1:def 5;

        (f1 * f) = (f1 (*) f) by A1, A34, CAT_1:def 13

        .= (f2 (*) f) by A30, A23, A32, A13, Th27

        .= (f2 * f) by A1, A34, CAT_1:def 13;

        then f1 = f2 by A2, A34;

        hence contradiction by A5, A16, A15, XTUPLE_0: 1;

      end;

      ( rng (( @ f) `2 )) c= ( cod ( @ f)) by Lm3;

      hence ( rng (( @ f) `2 )) = ( cod ( @ f)) by A6, XBOOLE_0:def 10;

    end;

    theorem :: ENS_1:38

    for a,b be Object of ( Ens V) st ( Hom (a,b)) <> {} holds for f be Morphism of a, b st ( @ f) is surjective holds f is epi

    proof

      let a,b be Object of ( Ens V) such that

       A1: ( Hom (a,b)) <> {} ;

      let f be Morphism of a, b;

      set m = ( @ f);

      assume

       A2: ( rng (m `2 )) = ( cod m);

      thus ( Hom (a,b)) <> {} by A1;

      let c be Object of ( Ens V) such that

       A3: ( Hom (b,c)) <> {} ;

      let f1,f2 be Morphism of b, c;

      

       A4: ( dom f1) = b by A3, CAT_1: 5

      .= ( cod f) by A1, CAT_1: 5;

      

       A5: ( dom f2) = b by A3, CAT_1: 5

      .= ( cod f) by A1, CAT_1: 5;

      

       A6: ( cod f1) = c by A3, CAT_1: 5

      .= ( cod f2) by A3, CAT_1: 5;

      assume

       A7: (f1 * f) = (f2 * f);

      set m1 = ( @ f1), m2 = ( @ f2);

      

       A8: (m1 * m) = (f1 (*) f) by A4, Th27

      .= (f1 * f) by A1, A3, CAT_1:def 13;

      

       A9: (m2 * m) = (f2 (*) f) by A5, Th27

      .= (f2 * f) by A1, A3, CAT_1:def 13;

      

       A10: m1 = [ [( dom m1), ( cod m1)], (m1 `2 )] by Th8;

      

       A11: ( cod m1) = ( cod f1) & ( cod m2) = ( cod f2) by Def10;

      

       A12: ( dom m2) = ( dom f2) by Def9;

      then

       A13: ( dom (m2 `2 )) = ( dom f2) by Lm3;

      

       A14: ( cod m) = ( cod f) by Def10;

      then

       A15: (m2 * m) = [ [( dom m), ( cod m2)], ((m2 `2 ) * (m `2 ))] by A5, A12, Def6;

      

       A16: ( dom m1) = ( dom f1) by Def9;

      then (m1 * m) = [ [( dom m), ( cod m1)], ((m1 `2 ) * (m `2 ))] by A4, A14, Def6;

      then

       A17: ((m1 `2 ) * (m `2 )) = ((m2 `2 ) * (m `2 )) by A7, A8, A15, A9, XTUPLE_0: 1;

      ( dom (m1 `2 )) = ( dom f1) by A16, Lm3;

      then (m1 `2 ) = (m2 `2 ) by A2, A4, A5, A14, A17, A13, FUNCT_1: 86;

      hence thesis by A4, A5, A6, A16, A12, A11, A10, Th8;

    end;

    theorem :: ENS_1:39

    for W be Universe, a,b be Object of ( Ens W) st ( Hom (a,b)) <> {} holds for f be Morphism of a, b st f is epi holds ( @ f) is surjective

    proof

      let W be Universe, a,b be Object of ( Ens W) such that ( Hom (a,b)) <> {} ;

      let f be Morphism of a, b;

       {} in W & { {} } in W by CLASSES2: 56, CLASSES2: 57;

      then

       A1: { {} , { {} }} in W by CLASSES2: 58;

       {} in { {} , { {} }} & { {} } in { {} , { {} }} by TARSKI:def 2;

      hence thesis by A1, Th36;

    end;

    

     Lm7: for W be non empty Subset of V holds ( Ens W) is Subcategory of ( Ens V)

    proof

      let W be non empty Subset of V;

      

       A1: for a,b be Object of ( Ens W), a9,b9 be Object of ( Ens V) st a = a9 & b = b9 holds ( Hom (a,b)) = ( Hom (a9,b9))

      proof

        let a,b be Object of ( Ens W), a9,b9 be Object of ( Ens V);

        assume

         A2: a = a9 & b = b9;

        ( Hom (a,b)) = ( Maps (( @ a),( @ b))) & ( Hom (a9,b9)) = ( Maps (( @ a9),( @ b9))) by Th26;

        hence thesis by A2, Lm5;

      end;

      set w = the Comp of ( Ens W), v = the Comp of ( Ens V);

      thus the carrier of ( Ens W) c= the carrier of ( Ens V);

      thus for a,b be Object of ( Ens W), a9,b9 be Object of ( Ens V) st a = a9 & b = b9 holds ( Hom (a,b)) c= ( Hom (a9,b9)) by A1;

      now

        

         A3: ( dom w) c= [:( Maps W), ( Maps W):] by RELAT_1:def 18;

        thus

         A4: ( dom w) c= ( dom v)

        proof

          let x,y be object;

          assume

           A5: [x, y] in ( dom w);

          then

          consider m2,m1 be Element of ( Maps W) such that

           A6: [x, y] = [m2, m1] by A3, DOMAIN_1: 1;

          reconsider m19 = m1, m29 = m2 as Element of ( Maps V) by Th7, TARSKI:def 3;

          

           A7: ( dom m29) = ( dom m2) & ( cod m19) = ( cod m1);

          ( dom m2) = ( cod m1) by A5, A6, Def11;

          hence thesis by A6, A7, Def11;

        end;

        let x be object;

        assume

         A8: x in ( dom w);

        then

        consider m2,m1 be Element of ( Maps W) such that

         A9: x = [m2, m1] by A3, DOMAIN_1: 1;

        reconsider m19 = m1, m29 = m2 as Element of ( Maps V) by Th7, TARSKI:def 3;

        

         A10: ( dom m29) = ( cod m19) by A4, A8, A9, Def11;

        

         A11: ( dom m2) = ( cod m1) by A8, A9, Def11;

        then

         A12: (m2 * m1) = [ [( dom m1), ( cod m2)], ((m2 `2 ) * (m1 `2 ))] by Def6;

        ( dom m1) = ( dom m19) & ( cod m2) = ( cod m29);

        then (m29 * m19) = [ [( dom m1), ( cod m2)], ((m2 `2 ) * (m1 `2 ))] by A10, Def6;

        

        hence (w . x) = (m29 * m19) by A9, A11, A12, Def11

        .= (v . x) by A9, A10, Def11;

      end;

      hence the Comp of ( Ens W) c= the Comp of ( Ens V) by GRFUNC_1: 2;

      let a be Object of ( Ens W), a9 be Object of ( Ens V);

      

       A13: ( id$ ( @ a)) = [ [( @ a), ( @ a)], ( id ( @ a))];

      assume a = a9;

      

      hence ( id a) = ( id$ ( @ a9)) by A13, Th28

      .= ( id a9) by Th28;

    end;

    theorem :: ENS_1:40

    for W be non empty Subset of V holds ( Ens W) is full Subcategory of ( Ens V)

    proof

      let W be non empty Subset of V;

      reconsider E = ( Ens W) as Subcategory of ( Ens V) by Lm7;

      for a,b be Object of E, a9,b9 be Object of ( Ens V) st a = a9 & b = b9 holds ( Hom (a,b)) = ( Hom (a9,b9))

      proof

        let a,b be Object of E, a9,b9 be Object of ( Ens V);

        assume

         A1: a = a9 & b = b9;

        reconsider aa = a, bb = b as Element of ( Ens W);

        ( Hom (aa,bb)) = ( Maps (( @ aa),( @ bb))) & ( Hom (a9,b9)) = ( Maps (( @ a9),( @ b9))) by Th26;

        hence thesis by A1, Lm5;

      end;

      hence thesis by CAT_2:def 6;

    end;

    begin

    reserve C for Category,

a,b,a9,b9,c for Object of C,

f,g,h,f9,g9 for Morphism of C;

    definition

      let C;

      :: ENS_1:def18

      func Hom (C) -> set equals the set of all ( Hom (a,b));

      coherence ;

    end

    registration

      let C;

      cluster ( Hom C) -> non empty;

      coherence

      proof

        set a = the Object of C;

        ( Hom (a,a)) in the set of all ( Hom (a9,b9));

        hence thesis;

      end;

    end

    theorem :: ENS_1:41

    ( Hom (a,b)) in ( Hom C);

    theorem :: ENS_1:42

    (( Hom (a,( cod f))) = {} implies ( Hom (a,( dom f))) = {} ) & (( Hom (( dom f),a)) = {} implies ( Hom (( cod f),a)) = {} )

    proof

      ( Hom (( dom f),( cod f))) <> {} by CAT_1: 2;

      hence thesis by CAT_1: 24;

    end;

    definition

      let C, a, f;

      :: ENS_1:def19

      func hom (a,f) -> Function of ( Hom (a,( dom f))), ( Hom (a,( cod f))) means

      : Def18: for g st g in ( Hom (a,( dom f))) holds (it . g) = (f (*) g);

      existence

      proof

        defpred P[ object, object] means for g st g = $1 holds $2 = (f (*) g);

        set X = ( Hom (a,( dom f))), Y = ( Hom (a,( cod f)));

        

         A1: for x be object st x in X holds ex y be object st y in Y & P[x, y]

        proof

          let x be object;

          assume

           A2: x in X;

          then

          reconsider g = x as Morphism of a, ( dom f) by CAT_1:def 5;

          take (f (*) g);

          ( Hom (( dom f),( cod f))) <> {} & f is Morphism of ( dom f), ( cod f) by CAT_1: 1, CAT_1: 4;

          hence thesis by A2, CAT_1: 23;

        end;

        consider h be Function such that

         A3: ( dom h) = X & ( rng h) c= Y and

         A4: for x be object st x in X holds P[x, (h . x)] from FUNCT_1:sch 6( A1);

        ( Hom (( dom f),( cod f))) <> {} by CAT_1: 2;

        then Y = {} implies X = {} by CAT_1: 24;

        then

        reconsider h as Function of X, Y by A3, FUNCT_2:def 1, RELSET_1: 4;

        take h;

        thus thesis by A4;

      end;

      uniqueness

      proof

        set X = ( Hom (a,( dom f))), Y = ( Hom (a,( cod f)));

        let h1,h2 be Function of X, Y such that

         A5: for g st g in X holds (h1 . g) = (f (*) g) and

         A6: for g st g in X holds (h2 . g) = (f (*) g);

        now

          let x be object;

          assume

           A7: x in X;

          then

          reconsider g = x as Morphism of C;

          

          thus (h1 . x) = (f (*) g) by A5, A7

          .= (h2 . x) by A6, A7;

        end;

        hence thesis by FUNCT_2: 12;

      end;

      :: ENS_1:def20

      func hom (f,a) -> Function of ( Hom (( cod f),a)), ( Hom (( dom f),a)) means

      : Def19: for g st g in ( Hom (( cod f),a)) holds (it . g) = (g (*) f);

      existence

      proof

        defpred P[ object, object] means for g st g = $1 holds $2 = (g (*) f);

        set X = ( Hom (( cod f),a)), Y = ( Hom (( dom f),a));

        

         A8: for x be object st x in X holds ex y be object st y in Y & P[x, y]

        proof

          let x be object;

          assume

           A9: x in X;

          then

          reconsider g = x as Morphism of ( cod f), a by CAT_1:def 5;

          take (g (*) f);

          ( Hom (( dom f),( cod f))) <> {} & f is Morphism of ( dom f), ( cod f) by CAT_1: 2, CAT_1: 4;

          hence thesis by A9, CAT_1: 23;

        end;

        consider h be Function such that

         A10: ( dom h) = X & ( rng h) c= Y and

         A11: for x be object st x in X holds P[x, (h . x)] from FUNCT_1:sch 6( A8);

        ( Hom (( dom f),( cod f))) <> {} by CAT_1: 2;

        then Y = {} implies X = {} by CAT_1: 24;

        then

        reconsider h as Function of X, Y by A10, FUNCT_2:def 1, RELSET_1: 4;

        take h;

        thus thesis by A11;

      end;

      uniqueness

      proof

        set X = ( Hom (( cod f),a)), Y = ( Hom (( dom f),a));

        let h1,h2 be Function of X, Y such that

         A12: for g st g in X holds (h1 . g) = (g (*) f) and

         A13: for g st g in X holds (h2 . g) = (g (*) f);

        now

          let x be object;

          assume

           A14: x in X;

          then

          reconsider g = x as Morphism of C;

          

          thus (h1 . x) = (g (*) f) by A12, A14

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

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: ENS_1:43

    

     Th42: ( hom (a,( id c))) = ( id ( Hom (a,c)))

    proof

      set A = ( Hom (a,c));

      now

        A = {} implies A = {} ;

        hence ( dom ( hom (a,( id c)))) = A by FUNCT_2:def 1;

        let x be object;

        assume

         A1: x in A;

        then

        reconsider g = x as Morphism of C;

        

         A2: ( cod g) = c by A1, CAT_1: 1;

        

        thus (( hom (a,( id c))) . x) = (( id c) (*) g) by A1, Def18

        .= x by A2, CAT_1: 21;

      end;

      hence thesis by FUNCT_1: 17;

    end;

    theorem :: ENS_1:44

    

     Th43: ( hom (( id c),a)) = ( id ( Hom (c,a)))

    proof

      set A = ( Hom (c,a));

      now

        A = {} implies A = {} ;

        hence ( dom ( hom (( id c),a))) = A by FUNCT_2:def 1;

        let x be object;

        assume

         A1: x in A;

        then

        reconsider g = x as Morphism of C;

        

         A2: ( dom g) = c by A1, CAT_1: 1;

        

        thus (( hom (( id c),a)) . x) = (g (*) ( id c)) by A1, Def19

        .= x by A2, CAT_1: 22;

      end;

      hence thesis by FUNCT_1: 17;

    end;

    theorem :: ENS_1:45

    

     Th44: ( dom g) = ( cod f) implies ( hom (a,(g (*) f))) = (( hom (a,g)) * ( hom (a,f)))

    proof

      assume

       A1: ( dom g) = ( cod f);

      then

       A2: ( dom (g (*) f)) = ( dom f) by CAT_1: 17;

      

       A3: ( cod (g (*) f)) = ( cod g) by A1, CAT_1: 17;

      now

        set h = ( hom (a,(g (*) f))), h2 = ( hom (a,g)), h1 = ( hom (a,f));

        

         A4: ( Hom (( dom f),( cod f))) <> {} by CAT_1: 2;

        then

         A5: ( Hom (a,( cod f))) = {} implies ( Hom (a,( dom f))) = {} by CAT_1: 24;

        ( Hom (( dom g),( cod g))) <> {} by CAT_1: 2;

        then

         A6: ( Hom (a,( cod g))) = {} implies ( Hom (a,( dom g))) = {} by CAT_1: 24;

        hence ( dom h) = ( Hom (a,( dom f))) by A1, A2, A3, A5, FUNCT_2:def 1;

        thus

         A7: ( dom (h2 * h1)) = ( Hom (a,( dom f))) by A1, A5, A6, FUNCT_2:def 1;

        let x be object;

        assume

         A8: x in ( Hom (a,( dom f)));

        then

        reconsider f9 = x as Morphism of C;

        

         A9: ( cod f9) = ( dom f) by A8, CAT_1: 1;

        

         A10: (h1 . x) in ( Hom (a,( dom g))) by A1, A4, A8, CAT_1: 24, FUNCT_2: 5;

        then

        reconsider g9 = (h1 . x) as Morphism of C;

        

        thus (h . x) = ((g (*) f) (*) f9) by A2, A8, Def18

        .= (g (*) (f (*) f9)) by A1, A9, CAT_1: 18

        .= (g (*) g9) by A8, Def18

        .= (h2 . g9) by A10, Def18

        .= ((h2 * h1) . x) by A7, A8, FUNCT_1: 12;

      end;

      hence thesis;

    end;

    theorem :: ENS_1:46

    

     Th45: ( dom g) = ( cod f) implies ( hom ((g (*) f),a)) = (( hom (f,a)) * ( hom (g,a)))

    proof

      assume

       A1: ( dom g) = ( cod f);

      then

       A2: ( cod (g (*) f)) = ( cod g) by CAT_1: 17;

      

       A3: ( dom (g (*) f)) = ( dom f) by A1, CAT_1: 17;

      now

        set h = ( hom ((g (*) f),a)), h2 = ( hom (g,a)), h1 = ( hom (f,a));

        

         A4: ( Hom (( dom g),( cod g))) <> {} by CAT_1: 2;

        then

         A5: ( Hom (( dom g),a)) = {} implies ( Hom (( cod g),a)) = {} by CAT_1: 24;

        ( Hom (( dom f),( cod f))) <> {} by CAT_1: 2;

        then

         A6: ( Hom (( dom f),a)) = {} implies ( Hom (( cod f),a)) = {} by CAT_1: 24;

        hence ( dom h) = ( Hom (( cod g),a)) by A1, A3, A2, A5, FUNCT_2:def 1;

        thus

         A7: ( dom (h1 * h2)) = ( Hom (( cod g),a)) by A1, A6, A5, FUNCT_2:def 1;

        let x be object;

        assume

         A8: x in ( Hom (( cod g),a));

        then

        reconsider f9 = x as Morphism of C;

        

         A9: ( dom f9) = ( cod g) by A8, CAT_1: 1;

        

         A10: (h2 . x) in ( Hom (( cod f),a)) by A1, A4, A8, CAT_1: 24, FUNCT_2: 5;

        then

        reconsider g9 = (h2 . x) as Morphism of C;

        

        thus (h . x) = (f9 (*) (g (*) f)) by A2, A8, Def19

        .= ((f9 (*) g) (*) f) by A1, A9, CAT_1: 18

        .= (g9 (*) f) by A8, Def19

        .= (h1 . g9) by A10, Def19

        .= ((h1 * h2) . x) by A7, A8, FUNCT_1: 12;

      end;

      hence thesis;

    end;

    theorem :: ENS_1:47

    

     Th46: [ [( Hom (a,( dom f))), ( Hom (a,( cod f)))], ( hom (a,f))] is Element of ( Maps ( Hom C))

    proof

      ( Hom (( dom f),( cod f))) <> {} by CAT_1: 2;

      then

       A1: ( Hom (a,( cod f))) = {} implies ( Hom (a,( dom f))) = {} by CAT_1: 24;

      ( Hom (a,( dom f))) in ( Hom C) & ( Hom (a,( cod f))) in ( Hom C);

      hence thesis by A1, Th5;

    end;

    theorem :: ENS_1:48

    

     Th47: [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))] is Element of ( Maps ( Hom C))

    proof

      ( Hom (( dom f),( cod f))) <> {} by CAT_1: 2;

      then

       A1: ( Hom (( dom f),a)) = {} implies ( Hom (( cod f),a)) = {} by CAT_1: 24;

      ( Hom (( dom f),a)) in ( Hom C) & ( Hom (( cod f),a)) in ( Hom C);

      hence thesis by A1, Th5;

    end;

    definition

      let C, a;

      :: ENS_1:def21

      func hom?- (a) -> Function of the carrier' of C, ( Maps ( Hom C)) means

      : Def20: for f holds (it . f) = [ [( Hom (a,( dom f))), ( Hom (a,( cod f)))], ( hom (a,f))];

      existence

      proof

        defpred P[ object, object] means for f st f = $1 holds $2 = [ [( Hom (a,( dom f))), ( Hom (a,( cod f)))], ( hom (a,f))];

        set X = the carrier' of C, Y = ( Maps ( Hom C));

        

         A1: for x be object st x in X holds ex y be object st y in Y & P[x, y]

        proof

          let x be object;

          assume x in X;

          then

          reconsider f = x as Morphism of C;

          take y = [ [( Hom (a,( dom f))), ( Hom (a,( cod f)))], ( hom (a,f))];

          y is Element of Y by Th46;

          hence thesis;

        end;

        consider h be Function such that

         A2: ( dom h) = X & ( rng h) c= Y and

         A3: for x be object st x in X holds P[x, (h . x)] from FUNCT_1:sch 6( A1);

        reconsider h as Function of X, Y by A2, FUNCT_2:def 1, RELSET_1: 4;

        take h;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let h1,h2 be Function of the carrier' of C, ( Maps ( Hom C)) such that

         A4: for f holds (h1 . f) = [ [( Hom (a,( dom f))), ( Hom (a,( cod f)))], ( hom (a,f))] and

         A5: for f holds (h2 . f) = [ [( Hom (a,( dom f))), ( Hom (a,( cod f)))], ( hom (a,f))];

        now

          let f;

          

          thus (h1 . f) = [ [( Hom (a,( dom f))), ( Hom (a,( cod f)))], ( hom (a,f))] by A4

          .= (h2 . f) by A5;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      :: ENS_1:def22

      func hom-? (a) -> Function of the carrier' of C, ( Maps ( Hom C)) means

      : Def21: for f holds (it . f) = [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))];

      existence

      proof

        defpred P[ object, object] means for f st f = $1 holds $2 = [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))];

        set X = the carrier' of C, Y = ( Maps ( Hom C));

        

         A6: for x be object st x in X holds ex y be object st y in Y & P[x, y]

        proof

          let x be object;

          assume x in X;

          then

          reconsider f = x as Morphism of C;

          take y = [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))];

          y is Element of Y by Th47;

          hence thesis;

        end;

        consider h be Function such that

         A7: ( dom h) = X & ( rng h) c= Y and

         A8: for x be object st x in X holds P[x, (h . x)] from FUNCT_1:sch 6( A6);

        reconsider h as Function of X, Y by A7, FUNCT_2:def 1, RELSET_1: 4;

        take h;

        thus thesis by A8;

      end;

      uniqueness

      proof

        let h1,h2 be Function of the carrier' of C, ( Maps ( Hom C)) such that

         A9: for f holds (h1 . f) = [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))] and

         A10: for f holds (h2 . f) = [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))];

        now

          let f;

          

          thus (h1 . f) = [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))] by A9

          .= (h2 . f) by A10;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    

     Lm8: for T be Function of the carrier' of C, ( Maps ( Hom C)) st ( Hom C) c= V holds T is Function of the carrier' of C, the carrier' of ( Ens V)

    proof

      let T be Function of the carrier' of C, ( Maps ( Hom C));

      assume ( Hom C) c= V;

      then ( Maps ( Hom C)) c= ( Maps V) by Th7;

      hence thesis by FUNCT_2: 7;

    end;

    

     Lm9: ( Hom C) c= V implies for d be Object of ( Ens V) st d = ( Hom (a,c)) holds (( hom?- a) . ( id c)) = ( id d)

    proof

      

       A1: ( Hom (a,c)) in ( Hom C);

      assume ( Hom C) c= V;

      then

      reconsider A = ( Hom (a,c)) as Element of V by A1;

      

       A2: ( hom (a,( id c))) = ( id A) by Th42;

      let d be Object of ( Ens V);

      assume d = ( Hom (a,c));

      

      hence (( hom?- a) . ( id c)) = ( id$ ( @ d)) by A2, Def20

      .= ( id d) by Th28;

    end;

    

     Lm10: ( Hom C) c= V implies for d be Object of ( Ens V) st d = ( Hom (c,a)) holds (( hom-? a) . ( id c)) = ( id d)

    proof

      

       A1: ( Hom (c,a)) in ( Hom C);

      assume ( Hom C) c= V;

      then

      reconsider A = ( Hom (c,a)) as Element of V by A1;

      

       A2: ( hom (( id c),a)) = ( id A) by Th43;

      let d be Object of ( Ens V);

      assume d = ( Hom (c,a));

      

      hence (( hom-? a) . ( id c)) = ( id$ ( @ d)) by A2, Def21

      .= ( id d) by Th28;

    end;

    theorem :: ENS_1:49

    

     Th48: ( Hom C) c= V implies ( hom?- a) is Functor of C, ( Ens V)

    proof

      assume

       A1: ( Hom C) c= V;

      then

      reconsider T = ( hom?- a) as Function of the carrier' of C, the carrier' of ( Ens V) by Lm8;

      now

        thus for c be Object of C holds ex d be Object of ( Ens V) st (T . ( id c)) = ( id d)

        proof

          let c be Object of C;

          ( Hom (a,c)) in ( Hom C);

          then

          reconsider A = ( Hom (a,c)) as Element of V by A1;

          take d = ( @ A);

          thus thesis by A1, Lm9;

        end;

        thus for f be Morphism of C holds (T . ( id ( dom f))) = ( id ( dom (T . f))) & (T . ( id ( cod f))) = ( id ( cod (T . f)))

        proof

          let f be Morphism of C;

          set b = ( dom f), c = ( cod f);

          set g = (T . f);

          ( Hom (a,b)) in ( Hom C) & ( Hom (a,c)) in ( Hom C);

          then

          reconsider A = ( Hom (a,b)), B = ( Hom (a,c)) as Element of V by A1;

          

           A2: [ [( Hom (a,b)), ( Hom (a,c))], ( hom (a,f))] = ( @ g) by Def20

          .= [ [( dom ( @ g)), ( cod ( @ g))], (( @ g) `2 )] by Th8

          .= [ [( dom g), ( cod ( @ g))], (( @ g) `2 )] by Def9

          .= [ [( dom g), ( cod g)], (( @ g) `2 )] by Def10;

          

          thus (T . ( id b)) = ( id ( @ A)) by A1, Lm9

          .= ( id ( dom (T . f))) by A2, Lm1;

          

          thus (T . ( id c)) = ( id ( @ B)) by A1, Lm9

          .= ( id ( cod (T . f))) by A2, Lm1;

        end;

        let f,g be Morphism of C such that

         A3: ( dom g) = ( cod f);

        

         A4: [ [( Hom (a,( dom g))), ( Hom (a,( cod g)))], ( hom (a,g))] = ( @ (T . g)) by Def20

        .= [ [( dom ( @ (T . g))), ( cod ( @ (T . g)))], (( @ (T . g)) `2 )] by Th8

        .= [ [( dom (T . g)), ( cod ( @ (T . g)))], (( @ (T . g)) `2 )] by Def9

        .= [ [( dom (T . g)), ( cod (T . g))], (( @ (T . g)) `2 )] by Def10;

        then

         A5: (( @ (T . g)) `2 ) = ( hom (a,g)) by XTUPLE_0: 1;

        ( cod (T . g)) = ( Hom (a,( cod g))) by A4, Lm1;

        then

         A6: ( cod ( @ (T . g))) = ( Hom (a,( cod g))) by Def10;

        

         A7: ( dom (T . g)) = ( Hom (a,( dom g))) by A4, Lm1;

        then

         A8: ( dom ( @ (T . g))) = ( Hom (a,( dom g))) by Def9;

        

         A9: [ [( Hom (a,( dom f))), ( Hom (a,( cod f)))], ( hom (a,f))] = ( @ (T . f)) by Def20

        .= [ [( dom ( @ (T . f))), ( cod ( @ (T . f)))], (( @ (T . f)) `2 )] by Th8

        .= [ [( dom (T . f)), ( cod ( @ (T . f)))], (( @ (T . f)) `2 )] by Def9

        .= [ [( dom (T . f)), ( cod (T . f))], (( @ (T . f)) `2 )] by Def10;

        then

         A10: (( @ (T . f)) `2 ) = ( hom (a,f)) by XTUPLE_0: 1;

        ( dom (T . f)) = ( Hom (a,( dom f))) by A9, Lm1;

        then

         A11: ( dom ( @ (T . f))) = ( Hom (a,( dom f))) by Def9;

        

         A12: ( cod (T . f)) = ( Hom (a,( cod f))) by A9, Lm1;

        then

         A13: ( cod ( @ (T . f))) = ( Hom (a,( cod f))) by Def10;

        ( dom (g (*) f)) = ( dom f) & ( cod (g (*) f)) = ( cod g) by A3, CAT_1: 17;

        

        hence (T . (g (*) f)) = [ [( Hom (a,( dom f))), ( Hom (a,( cod g)))], ( hom (a,(g (*) f)))] by Def20

        .= [ [( Hom (a,( dom f))), ( Hom (a,( cod g)))], (( hom (a,g)) * ( hom (a,f)))] by A3, Th44

        .= (( @ (T . g)) * ( @ (T . f))) by A3, A10, A11, A13, A5, A8, A6, Def6

        .= ((T . g) (*) (T . f)) by A3, A12, A7, Th27;

      end;

      hence thesis by CAT_1: 61;

    end;

    theorem :: ENS_1:50

    

     Th49: ( Hom C) c= V implies ( hom-? a) is Contravariant_Functor of C, ( Ens V)

    proof

      assume

       A1: ( Hom C) c= V;

      then

      reconsider T = ( hom-? a) as Function of the carrier' of C, the carrier' of ( Ens V) by Lm8;

      now

        thus for c be Object of C holds ex d be Object of ( Ens V) st (T . ( id c)) = ( id d)

        proof

          let c be Object of C;

          ( Hom (c,a)) in ( Hom C);

          then

          reconsider A = ( Hom (c,a)) as Element of V by A1;

          take d = ( @ A);

          thus thesis by A1, Lm10;

        end;

        thus for f be Morphism of C holds (T . ( id ( dom f))) = ( id ( cod (T . f))) & (T . ( id ( cod f))) = ( id ( dom (T . f)))

        proof

          let f be Morphism of C;

          set b = ( cod f), c = ( dom f);

          set g = (T . f);

          ( Hom (b,a)) in ( Hom C) & ( Hom (c,a)) in ( Hom C);

          then

          reconsider A = ( Hom (b,a)), B = ( Hom (c,a)) as Element of V by A1;

          

           A2: [ [( Hom (b,a)), ( Hom (c,a))], ( hom (f,a))] = ( @ g) by Def21

          .= [ [( dom ( @ g)), ( cod ( @ g))], (( @ g) `2 )] by Th8

          .= [ [( dom g), ( cod ( @ g))], (( @ g) `2 )] by Def9

          .= [ [( dom g), ( cod g)], (( @ g) `2 )] by Def10;

          

          thus (T . ( id c)) = ( id ( @ B)) by A1, Lm10

          .= ( id ( cod (T . f))) by A2, Lm1;

          

          thus (T . ( id b)) = ( id ( @ A)) by A1, Lm10

          .= ( id ( dom (T . f))) by A2, Lm1;

        end;

        let f,g be Morphism of C such that

         A3: ( dom g) = ( cod f);

        

         A4: [ [( Hom (( cod g),a)), ( Hom (( dom g),a))], ( hom (g,a))] = ( @ (T . g)) by Def21

        .= [ [( dom ( @ (T . g))), ( cod ( @ (T . g)))], (( @ (T . g)) `2 )] by Th8

        .= [ [( dom (T . g)), ( cod ( @ (T . g)))], (( @ (T . g)) `2 )] by Def9

        .= [ [( dom (T . g)), ( cod (T . g))], (( @ (T . g)) `2 )] by Def10;

        then

         A5: (( @ (T . g)) `2 ) = ( hom (g,a)) by XTUPLE_0: 1;

        ( dom (T . g)) = ( Hom (( cod g),a)) by A4, Lm1;

        then

         A6: ( dom ( @ (T . g))) = ( Hom (( cod g),a)) by Def9;

        

         A7: ( cod (T . g)) = ( Hom (( dom g),a)) by A4, Lm1;

        then

         A8: ( cod ( @ (T . g))) = ( Hom (( dom g),a)) by Def10;

        

         A9: [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))] = ( @ (T . f)) by Def21

        .= [ [( dom ( @ (T . f))), ( cod ( @ (T . f)))], (( @ (T . f)) `2 )] by Th8

        .= [ [( dom (T . f)), ( cod ( @ (T . f)))], (( @ (T . f)) `2 )] by Def9

        .= [ [( dom (T . f)), ( cod (T . f))], (( @ (T . f)) `2 )] by Def10;

        then

         A10: (( @ (T . f)) `2 ) = ( hom (f,a)) by XTUPLE_0: 1;

        ( cod (T . f)) = ( Hom (( dom f),a)) by A9, Lm1;

        then

         A11: ( cod ( @ (T . f))) = ( Hom (( dom f),a)) by Def10;

        

         A12: ( dom (T . f)) = ( Hom (( cod f),a)) by A9, Lm1;

        then

         A13: ( dom ( @ (T . f))) = ( Hom (( cod f),a)) by Def9;

        ( dom (g (*) f)) = ( dom f) & ( cod (g (*) f)) = ( cod g) by A3, CAT_1: 17;

        

        hence (T . (g (*) f)) = [ [( Hom (( cod g),a)), ( Hom (( dom f),a))], ( hom ((g (*) f),a))] by Def21

        .= [ [( Hom (( cod g),a)), ( Hom (( dom f),a))], (( hom (f,a)) * ( hom (g,a)))] by A3, Th45

        .= (( @ (T . f)) * ( @ (T . g))) by A3, A10, A13, A11, A5, A6, A8, Def6

        .= ((T . f) (*) (T . g)) by A3, A12, A7, Th27;

      end;

      hence thesis by OPPCAT_1:def 9;

    end;

    theorem :: ENS_1:51

    

     Th50: ( Hom (( dom f),( cod f9))) = {} implies ( Hom (( cod f),( dom f9))) = {}

    proof

      assume that

       A1: ( Hom (( dom f),( cod f9))) = {} and

       A2: ( Hom (( cod f),( dom f9))) <> {} ;

      

       A3: ( Hom (( dom f9),( cod f9))) <> {} by CAT_1: 2;

      ( Hom (( dom f),( cod f))) <> {} by CAT_1: 2;

      then ( Hom (( dom f),( dom f9))) <> {} by A2, CAT_1: 24;

      hence contradiction by A1, A3, CAT_1: 24;

    end;

    definition

      let C, f, g;

      :: ENS_1:def23

      func hom (f,g) -> Function of ( Hom (( cod f),( dom g))), ( Hom (( dom f),( cod g))) means

      : Def22: for h st h in ( Hom (( cod f),( dom g))) holds (it . h) = ((g (*) h) (*) f);

      existence

      proof

        defpred P[ object, object] means for h st h = $1 holds $2 = ((g (*) h) (*) f);

        set X = ( Hom (( cod f),( dom g))), Y = ( Hom (( dom f),( cod g)));

        

         A1: for x be object st x in X holds ex y be object st y in Y & P[x, y]

        proof

          let x be object;

          

           A2: ( Hom (( dom f),( cod f))) <> {} & f is Morphism of ( dom f), ( cod f) by CAT_1: 2, CAT_1: 4;

          assume

           A3: x in X;

          then

          reconsider h = x as Morphism of ( cod f), ( dom g) by CAT_1:def 5;

          take ((g (*) h) (*) f);

          ( Hom (( dom g),( cod g))) <> {} & g is Morphism of ( dom g), ( cod g) by CAT_1: 2, CAT_1: 4;

          then

           A4: (g (*) h) in ( Hom (( cod f),( cod g))) by A3, CAT_1: 23;

          then (g (*) h) is Morphism of ( cod f), ( cod g) by CAT_1:def 5;

          hence thesis by A4, A2, CAT_1: 23;

        end;

        consider h be Function such that

         A5: ( dom h) = X & ( rng h) c= Y and

         A6: for x be object st x in X holds P[x, (h . x)] from FUNCT_1:sch 6( A1);

        Y = {} implies X = {} by Th50;

        then

        reconsider h as Function of X, Y by A5, FUNCT_2:def 1, RELSET_1: 4;

        take h;

        thus thesis by A6;

      end;

      uniqueness

      proof

        set X = ( Hom (( cod f),( dom g))), Y = ( Hom (( dom f),( cod g)));

        let h1,h2 be Function of X, Y such that

         A7: for h st h in X holds (h1 . h) = ((g (*) h) (*) f) and

         A8: for h st h in X holds (h2 . h) = ((g (*) h) (*) f);

        now

          let x be object;

          assume

           A9: x in X;

          then

          reconsider h = x as Morphism of C;

          

          thus (h1 . x) = ((g (*) h) (*) f) by A7, A9

          .= (h2 . x) by A8, A9;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: ENS_1:52

    

     Th51: [ [( Hom (( cod f),( dom g))), ( Hom (( dom f),( cod g)))], ( hom (f,g))] is Element of ( Maps ( Hom C))

    proof

      

       A1: ( Hom (( dom f),( cod g))) in ( Hom C) & ( Hom (( cod f),( dom g))) in ( Hom C);

      ( Hom (( dom f),( cod g))) = {} implies ( Hom (( cod f),( dom g))) = {} by Th50;

      hence thesis by A1, Th5;

    end;

    theorem :: ENS_1:53

    

     Th52: ( hom (( id a),f)) = ( hom (a,f)) & ( hom (f,( id a))) = ( hom (f,a))

    proof

      

       A1: ( cod ( id a)) = a;

      now

        ( Hom (( dom f),( cod f))) <> {} by CAT_1: 2;

        then ( Hom (a,( cod f))) = {} implies ( Hom (a,( dom f))) = {} by CAT_1: 24;

        hence ( dom ( hom (( id a),f))) = ( Hom (a,( dom f))) & ( dom ( hom (a,f))) = ( Hom (a,( dom f))) by FUNCT_2:def 1;

        let x be object;

        assume

         A2: x in ( Hom (a,( dom f)));

        then

        reconsider g = x as Morphism of C;

        

         A3: ( dom g) = a by A2, CAT_1: 1;

        

         A4: ( cod g) = ( dom f) by A2, CAT_1: 1;

        

        thus (( hom (( id a),f)) . x) = ((f (*) g) (*) ( id a)) by A2, Def22

        .= (f (*) (g (*) ( id a))) by A1, A3, A4, CAT_1: 18

        .= (f (*) g) by A3, CAT_1: 22

        .= (( hom (a,f)) . x) by A2, Def18;

      end;

      hence ( hom (( id a),f)) = ( hom (a,f));

      now

        ( Hom (( dom f),( cod f))) <> {} by CAT_1: 2;

        then ( Hom (( dom f),a)) = {} implies ( Hom (( cod f),a)) = {} by CAT_1: 24;

        hence ( dom ( hom (f,( id a)))) = ( Hom (( cod f),a)) & ( dom ( hom (f,a))) = ( Hom (( cod f),a)) by FUNCT_2:def 1;

        let x be object;

        assume

         A5: x in ( Hom (( cod f),a));

        then

        reconsider g = x as Morphism of C;

        

         A6: ( cod g) = a by A5, CAT_1: 1;

        

        thus (( hom (f,( id a))) . x) = ((( id a) (*) g) (*) f) by A5, Def22

        .= (g (*) f) by A6, CAT_1: 21

        .= (( hom (f,a)) . x) by A5, Def19;

      end;

      hence thesis;

    end;

    theorem :: ENS_1:54

    

     Th53: ( hom (( id a),( id b))) = ( id ( Hom (a,b)))

    proof

      

      thus ( hom (( id a),( id b))) = ( hom (a,( id b))) by Th52

      .= ( id ( Hom (a,b))) by Th42;

    end;

    theorem :: ENS_1:55

    ( hom (f,g)) = (( hom (( dom f),g)) * ( hom (f,( dom g))))

    proof

      now

        

         A1: ( Hom (( dom f),( cod g))) = {} implies ( Hom (( cod f),( dom g))) = {} by Th50;

        hence ( dom ( hom (f,g))) = ( Hom (( cod f),( dom g))) by FUNCT_2:def 1;

        ( Hom (( dom f),( cod f))) <> {} by CAT_1: 2;

        then ( Hom (( dom f),( dom g))) = {} implies ( Hom (( cod f),( dom g))) = {} by CAT_1: 24;

        hence

         A2: ( dom (( hom (( dom f),g)) * ( hom (f,( dom g))))) = ( Hom (( cod f),( dom g))) by A1, FUNCT_2:def 1;

        let x be object;

        assume

         A3: x in ( Hom (( cod f),( dom g)));

        then

        reconsider h = x as Morphism of C;

        

         A4: ( dom h) = ( cod f) by A3, CAT_1: 1;

        then

         A5: ( dom (h (*) f)) = ( dom f) by CAT_1: 17;

        

         A6: ( cod h) = ( dom g) by A3, CAT_1: 1;

        then ( cod (h (*) f)) = ( dom g) by A4, CAT_1: 17;

        then

         A7: (h (*) f) in ( Hom (( dom f),( dom g))) by A5;

        

        thus (( hom (f,g)) . x) = ((g (*) h) (*) f) by A3, Def22

        .= (g (*) (h (*) f)) by A4, A6, CAT_1: 18

        .= (( hom (( dom f),g)) . (h (*) f)) by A7, Def18

        .= (( hom (( dom f),g)) . (( hom (f,( dom g))) . h)) by A3, Def19

        .= ((( hom (( dom f),g)) * ( hom (f,( dom g)))) . x) by A2, A3, FUNCT_1: 12;

      end;

      hence thesis;

    end;

    theorem :: ENS_1:56

    

     Th55: ( cod g) = ( dom f) & ( dom g9) = ( cod f9) implies ( hom ((f (*) g),(g9 (*) f9))) = (( hom (g,g9)) * ( hom (f,f9)))

    proof

      assume that

       A1: ( cod g) = ( dom f) and

       A2: ( dom g9) = ( cod f9);

      

       A3: ( dom (g9 (*) f9)) = ( dom f9) by A2, CAT_1: 17;

      

       A4: ( cod (f (*) g)) = ( cod f) by A1, CAT_1: 17;

      

       A5: ( cod (g9 (*) f9)) = ( cod g9) & ( dom (f (*) g)) = ( dom g) by A1, A2, CAT_1: 17;

      now

        set h = ( hom ((f (*) g),(g9 (*) f9))), h2 = ( hom (g,g9)), h1 = ( hom (f,f9));

        

         A6: ( Hom (( dom f),( cod f9))) = {} implies ( Hom (( cod f),( dom f9))) = {} by Th50;

        

         A7: ( Hom (( dom g),( cod g9))) = {} implies ( Hom (( cod g),( dom g9))) = {} by Th50;

        hence ( dom h) = ( Hom (( cod f),( dom f9))) by A1, A2, A3, A5, A4, A6, FUNCT_2:def 1;

        thus

         A8: ( dom (h2 * h1)) = ( Hom (( cod f),( dom f9))) by A1, A2, A7, A6, FUNCT_2:def 1;

        let x be object;

        assume

         A9: x in ( Hom (( cod f),( dom f9)));

        then

        reconsider k = x as Morphism of C;

        

         A10: (h1 . x) in ( Hom (( cod g),( dom g9))) by A1, A2, A9, Th50, FUNCT_2: 5;

        then

        reconsider l = (h1 . x) as Morphism of C;

        

         A11: ( dom k) = ( cod f) by A9, CAT_1: 1;

        then

         A12: ( cod (k (*) (f (*) g))) = ( cod k) by A4, CAT_1: 17;

        

         A13: ( cod k) = ( dom f9) by A9, CAT_1: 1;

        then

         A14: ( dom (f9 (*) k)) = ( dom k) by CAT_1: 17;

        then

         A15: ( dom ((f9 (*) k) (*) f)) = ( dom f) by A11, CAT_1: 17;

        ( cod (f9 (*) k)) = ( cod f9) by A13, CAT_1: 17;

        then

         A16: ( cod ((f9 (*) k) (*) f)) = ( cod f9) by A11, A14, CAT_1: 17;

        

        thus (h . x) = (((g9 (*) f9) (*) k) (*) (f (*) g)) by A3, A4, A9, Def22

        .= ((g9 (*) f9) (*) (k (*) (f (*) g))) by A3, A4, A13, A11, CAT_1: 18

        .= (g9 (*) (f9 (*) (k (*) (f (*) g)))) by A2, A13, A12, CAT_1: 18

        .= (g9 (*) ((f9 (*) k) (*) (f (*) g))) by A4, A13, A11, CAT_1: 18

        .= (g9 (*) (((f9 (*) k) (*) f) (*) g)) by A1, A11, A14, CAT_1: 18

        .= ((g9 (*) ((f9 (*) k) (*) f)) (*) g) by A1, A2, A15, A16, CAT_1: 18

        .= ((g9 (*) l) (*) g) by A9, Def22

        .= (h2 . l) by A10, Def22

        .= ((h2 * h1) . x) by A8, A9, FUNCT_1: 12;

      end;

      hence thesis;

    end;

    definition

      let C;

      :: ENS_1:def24

      func hom?? (C) -> Function of the carrier' of [:C, C:], ( Maps ( Hom C)) means

      : Def23: for f, g holds (it . [f, g]) = [ [( Hom (( cod f),( dom g))), ( Hom (( dom f),( cod g)))], ( hom (f,g))];

      existence

      proof

        defpred P[ object, object] means for f, g st $1 = [f, g] holds $2 = [ [( Hom (( cod f),( dom g))), ( Hom (( dom f),( cod g)))], ( hom (f,g))];

        set X = the carrier' of [:C, C:], Y = ( Maps ( Hom C));

        

         A1: for x be object st x in X holds ex y be object st y in Y & P[x, y]

        proof

          let x be object;

          assume x in X;

          then

          consider f, g such that

           A2: x = [f, g] by DOMAIN_1: 1;

          take y = [ [( Hom (( cod f),( dom g))), ( Hom (( dom f),( cod g)))], ( hom (f,g))];

          y is Element of Y by Th51;

          hence y in Y;

          let f9, g9;

          assume x = [f9, g9];

          then f9 = f & g9 = g by A2, XTUPLE_0: 1;

          hence thesis;

        end;

        consider h be Function such that

         A3: ( dom h) = X & ( rng h) c= Y and

         A4: for x be object st x in X holds P[x, (h . x)] from FUNCT_1:sch 6( A1);

        reconsider h as Function of X, Y by A3, FUNCT_2:def 1, RELSET_1: 4;

        take h;

        thus thesis by A4;

      end;

      uniqueness

      proof

        let h1,h2 be Function of the carrier' of [:C, C:], ( Maps ( Hom C)) such that

         A5: for f, g holds (h1 . [f, g]) = [ [( Hom (( cod f),( dom g))), ( Hom (( dom f),( cod g)))], ( hom (f,g))] and

         A6: for f, g holds (h2 . [f, g]) = [ [( Hom (( cod f),( dom g))), ( Hom (( dom f),( cod g)))], ( hom (f,g))];

        now

          thus the carrier' of [:C, C:] = [:the carrier' of C, the carrier' of C:];

          let f, g;

          

          thus (h1 . (f,g)) = [ [( Hom (( cod f),( dom g))), ( Hom (( dom f),( cod g)))], ( hom (f,g))] by A5

          .= (h2 . (f,g)) by A6;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    theorem :: ENS_1:57

    

     Th56: ( hom?- a) = (( curry ( hom?? C)) . ( id a)) & ( hom-? a) = (( curry' ( hom?? C)) . ( id a))

    proof

      reconsider T = ( hom?? C) as Function of [:the carrier' of C, the carrier' of C:], ( Maps ( Hom C));

      now

        let f;

        

        thus ((( curry T) . ( id a)) . f) = (T . (( id a),f)) by FUNCT_5: 69

        .= [ [( Hom (( cod ( id a)),( dom f))), ( Hom (( dom ( id a)),( cod f)))], ( hom (( id a),f))] by Def23

        .= [ [( Hom (( cod ( id a)),( dom f))), ( Hom (( dom ( id a)),( cod f)))], ( hom (a,f))] by Th52

        .= [ [( Hom (a,( dom f))), ( Hom (( dom ( id a)),( cod f)))], ( hom (a,f))]

        .= [ [( Hom (a,( dom f))), ( Hom (a,( cod f)))], ( hom (a,f))]

        .= (( hom?- a) . f) by Def20;

      end;

      hence ( hom?- a) = (( curry ( hom?? C)) . ( id a)) by FUNCT_2: 63;

      now

        let f;

        

        thus ((( curry' T) . ( id a)) . f) = (T . (f,( id a))) by FUNCT_5: 70

        .= [ [( Hom (( cod f),( dom ( id a)))), ( Hom (( dom f),( cod ( id a))))], ( hom (f,( id a)))] by Def23

        .= [ [( Hom (( cod f),( dom ( id a)))), ( Hom (( dom f),( cod ( id a))))], ( hom (f,a))] by Th52

        .= [ [( Hom (( cod f),a)), ( Hom (( dom f),( cod ( id a))))], ( hom (f,a))]

        .= [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))]

        .= (( hom-? a) . f) by Def21;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    

     Lm11: ( Hom C) c= V implies for d be Object of ( Ens V) st d = ( Hom (a,b)) holds (( hom?? C) . [( id a), ( id b)]) = ( id d)

    proof

      

       A1: ( Hom (a,b)) in ( Hom C);

      assume ( Hom C) c= V;

      then

      reconsider A = ( Hom (a,b)) as Element of V by A1;

      

       A2: ( hom (( id a),( id b))) = ( id A) by Th53;

      let d be Object of ( Ens V);

      assume d = ( Hom (a,b));

      

      hence (( hom?? C) . [( id a), ( id b)]) = ( id$ ( @ d)) by A2, Def23

      .= ( id d) by Th28;

    end;

    theorem :: ENS_1:58

    

     Th57: ( Hom C) c= V implies ( hom?? C) is Functor of [:(C opp ), C:], ( Ens V)

    proof

      assume

       A1: ( Hom C) c= V;

      then (C opp ) = CatStr (# the carrier of C, the carrier' of C, the Target of C, the Source of C, ( ~ the Comp of C) #) & ( Maps ( Hom C)) c= ( Maps V) by Th7;

      then

      reconsider T = ( hom?? C) as Function of the carrier' of [:(C opp ), C:], the carrier' of ( Ens V) by FUNCT_2: 7;

      now

        thus for c be Object of [:(C opp ), C:] holds ex d be Object of ( Ens V) st (T . ( id c)) = ( id d)

        proof

          let c be Object of [:(C opp ), C:];

          consider a be Object of (C opp ), b such that

           A2: c = [a, b] by DOMAIN_1: 1;

          ( Hom (( opp a),b)) in ( Hom C);

          then

          reconsider A = ( Hom (( opp a),b)) as Element of V by A1;

          take d = ( @ A);

          

           A3: ( id ( opp a)) = ( id a) by OPPCAT_1: 72;

          ( id c) = [( id ( opp a)), ( id b)] by A3, A2, CAT_2: 31;

          hence thesis by A1, Lm11;

        end;

        thus for fg be Morphism of [:(C opp ), C:] holds (T . ( id ( dom fg))) = ( id ( dom (T . fg))) & (T . ( id ( cod fg))) = ( id ( cod (T . fg)))

        proof

          let fg be Morphism of [:(C opp ), C:];

          consider f be Morphism of (C opp ), g such that

           A4: fg = [f, g] by DOMAIN_1: 1;

          ( Hom (( cod ( opp f)),( dom g))) in ( Hom C) & ( Hom (( dom ( opp f)),( cod g))) in ( Hom C);

          then

          reconsider A = ( Hom (( cod ( opp f)),( dom g))), B = ( Hom (( dom ( opp f)),( cod g))) as Element of V by A1;

          set h = (T . fg);

          

           A5: ( id ( opp ( dom f))) = ( id ( dom f)) by OPPCAT_1: 72;

          

           A6: ( id ( opp ( cod f))) = ( id ( cod f)) by OPPCAT_1: 72;

          

           A7: [ [( Hom (( cod ( opp f)),( dom g))), ( Hom (( dom ( opp f)),( cod g)))], ( hom (( opp f),g))] = ( @ h) by A4, Def23

          .= [ [( dom ( @ h)), ( cod ( @ h))], (( @ h) `2 )] by Th8

          .= [ [( dom h), ( cod ( @ h))], (( @ h) `2 )] by Def9

          .= [ [( dom h), ( cod h)], (( @ h) `2 )] by Def10;

          

          thus (T . ( id ( dom fg))) = (T . ( id [( dom f), ( dom g)])) by A4, CAT_2: 28

          .= (T . [( id ( dom f)), ( id ( dom g))]) by CAT_2: 31

          .= ( id ( @ A)) by A1, Lm11, A5

          .= ( id ( dom (T . fg))) by A7, Lm1;

          

          thus (T . ( id ( cod fg))) = (T . ( id [( cod f), ( cod g)])) by A4, CAT_2: 28

          .= (T . [( id ( cod f)), ( id ( cod g))]) by CAT_2: 31

          .= ( id ( @ B)) by A1, Lm11, A6

          .= ( id ( cod (T . fg))) by A7, Lm1;

        end;

        let ff,gg be Morphism of [:(C opp ), C:] such that

         A8: ( dom gg) = ( cod ff);

        consider g be Morphism of (C opp ), g9 such that

         A9: gg = [g, g9] by DOMAIN_1: 1;

        

         A10: [ [( Hom (( cod ( opp g)),( dom g9))), ( Hom (( dom ( opp g)),( cod g9)))], ( hom (( opp g),g9))] = ( @ (T . gg)) by A9, Def23

        .= [ [( dom ( @ (T . gg))), ( cod ( @ (T . gg)))], (( @ (T . gg)) `2 )] by Th8

        .= [ [( dom (T . gg)), ( cod ( @ (T . gg)))], (( @ (T . gg)) `2 )] by Def9

        .= [ [( dom (T . gg)), ( cod (T . gg))], (( @ (T . gg)) `2 )] by Def10;

        then

         A11: (( @ (T . gg)) `2 ) = ( hom (( opp g),g9)) by XTUPLE_0: 1;

        ( cod (T . gg)) = ( Hom (( dom ( opp g)),( cod g9))) by A10, Lm1;

        then

         A12: ( cod ( @ (T . gg))) = ( Hom (( dom ( opp g)),( cod g9))) by Def10;

        

         A13: ( dom (T . gg)) = ( Hom (( cod ( opp g)),( dom g9))) by A10, Lm1;

        then

         A14: ( dom ( @ (T . gg))) = ( Hom (( cod ( opp g)),( dom g9))) by Def9;

        consider f be Morphism of (C opp ), f9 such that

         A15: ff = [f, f9] by DOMAIN_1: 1;

        

         A16: [ [( Hom (( cod ( opp f)),( dom f9))), ( Hom (( dom ( opp f)),( cod f9)))], ( hom (( opp f),f9))] = ( @ (T . ff)) by A15, Def23

        .= [ [( dom ( @ (T . ff))), ( cod ( @ (T . ff)))], (( @ (T . ff)) `2 )] by Th8

        .= [ [( dom (T . ff)), ( cod ( @ (T . ff)))], (( @ (T . ff)) `2 )] by Def9

        .= [ [( dom (T . ff)), ( cod (T . ff))], (( @ (T . ff)) `2 )] by Def10;

        then

         A17: (( @ (T . ff)) `2 ) = ( hom (( opp f),f9)) by XTUPLE_0: 1;

        ( dom (T . ff)) = ( Hom (( cod ( opp f)),( dom f9))) by A16, Lm1;

        then

         A18: ( dom ( @ (T . ff))) = ( Hom (( cod ( opp f)),( dom f9))) by Def9;

        

         A19: ( cod (T . ff)) = ( Hom (( dom ( opp f)),( cod f9))) by A16, Lm1;

        then

         A20: ( cod ( @ (T . ff))) = ( Hom (( dom ( opp f)),( cod f9))) by Def10;

        

         A21: ( cod ff) = [( cod f), ( cod f9)] by A15, CAT_2: 28;

        

         A22: ( dom gg) = [( dom g), ( dom g9)] by A9, CAT_2: 28;

        then

         A23: ( cod ( opp g)) = ( dom ( opp f)) by A8, A21, XTUPLE_0: 1;

        then

         A24: ( dom (( opp f) (*) ( opp g))) = ( dom ( opp g)) & ( cod (( opp f) (*) ( opp g))) = ( cod ( opp f)) by CAT_1: 17;

        

         A25: ( dom g) = ( cod f) by A8, A22, A21, XTUPLE_0: 1;

        

         A26: ( dom g9) = ( cod f9) by A8, A22, A21, XTUPLE_0: 1;

        then

         A27: ( dom (g9 (*) f9)) = ( dom f9) & ( cod (g9 (*) f9)) = ( cod g9) by CAT_1: 17;

        

        thus (T . (gg (*) ff)) = (T . [( opp (g (*) f)), (g9 (*) f9)]) by A8, A15, A9, CAT_2: 30

        .= (T . [(( opp f) (*) ( opp g)), (g9 (*) f9)]) by A25, OPPCAT_1: 18

        .= [ [( Hom (( cod (( opp f) (*) ( opp g))),( dom (g9 (*) f9)))), ( Hom (( dom (( opp f) (*) ( opp g))),( cod (g9 (*) f9))))], ( hom ((( opp f) (*) ( opp g)),(g9 (*) f9)))] by Def23

        .= [ [( Hom (( cod ( opp f)),( dom f9))), ( Hom (( dom ( opp g)),( cod g9)))], (( hom (( opp g),g9)) * ( hom (( opp f),f9)))] by A23, A26, A27, A24, Th55

        .= (( @ (T . gg)) * ( @ (T . ff))) by A17, A18, A20, A11, A14, A12, A23, A26, Def6

        .= ((T . gg) (*) (T . ff)) by A19, A13, A23, A26, Th27;

      end;

      hence thesis by CAT_1: 61;

    end;

    definition

      let V, C, a;

      assume

       A1: ( Hom C) c= V;

      :: ENS_1:def25

      func hom?- (V,a) -> Functor of C, ( Ens V) equals

      : Def24: ( hom?- a);

      coherence by A1, Th48;

      :: ENS_1:def26

      func hom-? (V,a) -> Contravariant_Functor of C, ( Ens V) equals

      : Def25: ( hom-? a);

      coherence by A1, Th49;

    end

    definition

      let V, C;

      assume

       A1: ( Hom C) c= V;

      :: ENS_1:def27

      func hom?? (V,C) -> Functor of [:(C opp ), C:], ( Ens V) equals

      : Def26: ( hom?? C);

      coherence by A1, Th57;

    end

    theorem :: ENS_1:59

    ( Hom C) c= V implies (( hom?- (V,a)) . f) = [ [( Hom (a,( dom f))), ( Hom (a,( cod f)))], ( hom (a,f))]

    proof

      assume ( Hom C) c= V;

      

      hence (( hom?- (V,a)) . f) = (( hom?- a) . f) by Def24

      .= [ [( Hom (a,( dom f))), ( Hom (a,( cod f)))], ( hom (a,f))] by Def20;

    end;

    theorem :: ENS_1:60

    ( Hom C) c= V implies (( Obj ( hom?- (V,a))) . b) = ( Hom (a,b))

    proof

      assume

       A1: ( Hom C) c= V;

      ( Hom (a,b)) in ( Hom C);

      then

      reconsider A = ( Hom (a,b)) as Element of V by A1;

      set d = ( @ A);

      (( hom?- (V,a)) . ( id b)) = (( hom?- a) . ( id b)) by A1, Def24

      .= ( id d) by A1, Lm9;

      hence thesis by CAT_1: 67;

    end;

    theorem :: ENS_1:61

    ( Hom C) c= V implies (( hom-? (V,a)) . f) = [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))]

    proof

      assume ( Hom C) c= V;

      

      hence (( hom-? (V,a)) . f) = (( hom-? a) . f) by Def25

      .= [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))] by Def21;

    end;

    theorem :: ENS_1:62

    ( Hom C) c= V implies (( Obj ( hom-? (V,a))) . b) = ( Hom (b,a))

    proof

      assume

       A1: ( Hom C) c= V;

      ( Hom (b,a)) in ( Hom C);

      then

      reconsider A = ( Hom (b,a)) as Element of V by A1;

      set d = ( @ A);

      (( hom-? (V,a)) . ( id b)) = (( hom-? a) . ( id b)) by A1, Def25

      .= ( id d) by A1, Lm10;

      hence thesis by OPPCAT_1: 30;

    end;

    theorem :: ENS_1:63

    ( Hom C) c= V implies (( hom?? (V,C)) . [(f opp ), g]) = [ [( Hom (( cod f),( dom g))), ( Hom (( dom f),( cod g)))], ( hom (f,g))]

    proof

      assume

       A1: ( Hom C) c= V;

      

      thus (( hom?? (V,C)) . [(f opp ), g]) = (( hom?? C) . [f, g]) by A1, Def26

      .= [ [( Hom (( cod f),( dom g))), ( Hom (( dom f),( cod g)))], ( hom (f,g))] by Def23;

    end;

    theorem :: ENS_1:64

    ( Hom C) c= V implies (( Obj ( hom?? (V,C))) . [(a opp ), b]) = ( Hom (a,b))

    proof

      assume

       A1: ( Hom C) c= V;

      ( Hom (a,b)) in ( Hom C);

      then

      reconsider A = ( Hom (a,b)) as Element of V by A1;

      

       A2: ( id (a opp )) = ( id a) by OPPCAT_1: 71;

      set d = ( @ A);

      (( hom?? (V,C)) . ( id [(a opp ), b])) = (( hom?? (V,C)) . [( id (a opp )), ( id b)]) by CAT_2: 31

      .= (( hom?? C) . [( id a), ( id b)]) by A1, Def26, A2

      .= ( id d) by A1, Lm11;

      hence thesis by CAT_1: 67;

    end;

    theorem :: ENS_1:65

    ( Hom C) c= V implies (( hom?? (V,C)) ?- (a opp )) = ( hom?- (V,a))

    proof

      assume

       A1: ( Hom C) c= V;

      

       A2: ( id (a opp )) = ( id a) by OPPCAT_1: 71;

      

      thus (( hom?? (V,C)) ?- (a opp )) = (( curry ( hom?? C)) . ( id a)) by A1, Def26, A2

      .= ( hom?- a) by Th56

      .= ( hom?- (V,a)) by A1, Def24;

    end;

    theorem :: ENS_1:66

    ( Hom C) c= V implies (( hom?? (V,C)) -? a) = ( hom-? (V,a))

    proof

      assume

       A1: ( Hom C) c= V;

      

      hence (( hom?? (V,C)) -? a) = (( curry' ( hom?? C)) . ( id a)) by Def26

      .= ( hom-? a) by Th56

      .= ( hom-? (V,a)) by A1, Def25;

    end;