yoneda_1.miz



    begin

    reserve y for set;

    reserve A for Category,

a,o for Object of A;

    reserve f for Morphism of A;

    definition

      let A;

      :: YONEDA_1:def1

      func EnsHom (A) -> Category equals ( Ens ( Hom A));

      correctness ;

    end

    theorem :: YONEDA_1:1

    

     Th1: for f,g be Function, m1,m2 be Morphism of ( EnsHom A) st ( cod m1) = ( dom m2) & [ [( dom m1), ( cod m1)], f] = m1 & [ [( dom m2), ( cod m2)], g] = m2 holds [ [( dom m1), ( cod m2)], (g * f)] = (m2 (*) m1)

    proof

      let f,g be Function;

      let m1,m2 be Morphism of ( EnsHom A) such that

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

       A2: [ [( dom m1), ( cod m1)], f] = m1 and

       A3: [ [( dom m2), ( cod m2)], g] = m2;

      

       A4: ( EnsHom A) = CatStr (# ( Hom A), ( Maps ( Hom A)), ( fDom ( Hom A)), ( fCod ( Hom A)), ( fComp ( Hom A)) #) by ENS_1:def 13;

      then

      reconsider m19 = m1 as Element of ( Maps ( Hom A));

      reconsider m29 = m2 as Element of ( Maps ( Hom A)) by A4;

      

       A5: ( cod m19) = ((m1 `1 ) `2 ) by ENS_1:def 4

      .= ( [( dom m1), ( cod m1)] `2 ) by A2

      .= ( dom m2) by A1

      .= ( [( dom m2), ( cod m2)] `1 )

      .= ((m2 `1 ) `1 ) by A3

      .= ( dom m29) by ENS_1:def 3;

      

       A6: (m19 `2 ) = f by A2;

      

       A7: (m29 `2 ) = g by A3;

      

       A8: ( cod m2) = ( [( dom m2), ( cod m2)] `2 )

      .= ((m2 `1 ) `2 ) by A3

      .= ( cod m29) by ENS_1:def 4;

      

       A9: ( dom m19) = ((m1 `1 ) `1 ) by ENS_1:def 3

      .= ( [( dom m1), ( cod m1)] `1 ) by A2

      .= ( dom m1);

       [m2, m1] in ( dom the Comp of ( EnsHom A)) by A1, CAT_1: 15;

      

      then (m2 (*) m1) = (( fComp ( Hom A)) . (m29,m19)) by A4, CAT_1:def 1

      .= (m29 * m19) by A5, ENS_1:def 11

      .= [ [( dom m1), ( cod m2)], (g * f)] by A5, A9, A8, A7, A6, ENS_1:def 6;

      hence thesis;

    end;

    definition

      let A, a;

      :: YONEDA_1:def2

      func <|a,?> -> Functor of A, ( EnsHom A) equals ( hom?- a);

      coherence by ENS_1: 49;

    end

    theorem :: YONEDA_1:2

    

     Th2: for f be Morphism of A holds <|( cod f),?> is_naturally_transformable_to <|( dom f),?>

    proof

      let f;

      set F1 = <|( cod f),?>, F2 = <|( dom f),?>;

      set B = ( EnsHom A);

      deffunc F( Element of A) = [ [( Hom (( cod f),$1)), ( Hom (( dom f),$1))], ( hom (f,$1))];

      

       A1: for a be Object of A holds [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))] in ( Hom ((F1 . a),(F2 . a)))

      proof

        let a be Object of A;

        

         A2: ( EnsHom A) = CatStr (# ( Hom A), ( Maps ( Hom A)), ( fDom ( Hom A)), ( fCod ( Hom A)), ( fComp ( Hom A)) #) by ENS_1:def 13;

        then

        reconsider m = [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))] as Morphism of ( EnsHom A) by ENS_1: 48;

        reconsider m9 = m as Element of ( Maps ( Hom A)) by ENS_1: 48;

        

         A3: ( cod m) = (( fCod ( Hom A)) . m) by A2

        .= ( cod m9) by ENS_1:def 10

        .= ((m `1 ) `2 ) by ENS_1:def 4

        .= ( [( Hom (( cod f),a)), ( Hom (( dom f),a))] `2 )

        .= ( Hom (( dom f),a))

        .= (( Obj ( hom?- (( Hom A),( dom f)))) . a) by ENS_1: 60

        .= (( hom?- (( Hom A),( dom f))) . a)

        .= (F2 . a) by ENS_1:def 25;

        ( dom m) = (( fDom ( Hom A)) . m) by A2

        .= ( dom m9) by ENS_1:def 9

        .= ((m `1 ) `1 ) by ENS_1:def 3

        .= ( [( Hom (( cod f),a)), ( Hom (( dom f),a))] `1 )

        .= ( Hom (( cod f),a))

        .= (( Obj ( hom?- (( Hom A),( cod f)))) . a) by ENS_1: 60

        .= (( hom?- (( Hom A),( cod f))) . a)

        .= (F1 . a) by ENS_1:def 25;

        hence thesis by A3;

      end;

      

       A4: for a be Element of A holds F(a) in the carrier' of B

      proof

        let a;

         [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))] in ( Hom ((F1 . a),(F2 . a))) by A1;

        hence thesis;

      end;

      consider t be Function of the carrier of A, the carrier' of B such that

       A5: for o be Element of A holds (t . o) = F(o) from FUNCT_2:sch 8( A4);

      

       A6: for a be Object of A holds (t . a) is Morphism of (F1 . a), (F2 . a)

      proof

        let a;

         [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))] in ( Hom ((F1 . a),(F2 . a))) by A1;

        then [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))] is Morphism of (F1 . a), (F2 . a) by CAT_1:def 5;

        hence thesis by A5;

      end;

      for a be Object of A holds ( Hom ((F1 . a),(F2 . a))) <> {} by A1;

      then

       A7: F1 is_transformable_to F2 by NATTRA_1:def 2;

      then

      reconsider t as transformation of F1, F2 by A6, NATTRA_1:def 3;

      for a,b be Object of A st ( Hom (a,b)) <> {} holds for g be Morphism of a, b holds ((t . b) * (F1 /. g)) = ((F2 /. g) * (t . a))

      proof

        let a,b be Object of A such that

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

        

         A9: ( Hom ((F1 . a),(F1 . b))) <> {} by A8, CAT_1: 84;

        let g be Morphism of a, b;

        

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

        

         A11: ( rng ( hom (( cod f),g))) c= ( dom ( hom (f,b)))

        proof

          

           A12: ( cod g) = b by A8, CAT_1: 5;

          per cases ;

            suppose

             A13: ( Hom (( dom f),b)) = {} ;

            ( Hom (( cod f),b)) = {} by A13, ENS_1: 42;

            hence thesis by A12;

          end;

            suppose

             A14: ( Hom (( dom f),b)) <> {} ;

            ( cod g) = b by A8, CAT_1: 5;

            then

             A15: ( rng ( hom (( cod f),g))) c= ( Hom (( cod f),( cod g))) & ( Hom (( cod f),( cod g))) = ( dom ( hom (f,b))) by A14, FUNCT_2:def 1, RELAT_1:def 19;

            let e be object;

            assume e in ( rng ( hom (( cod f),g)));

            hence thesis by A15;

          end;

        end;

        

         A16: ( rng ( hom (f,a))) c= ( dom ( hom (( dom f),g)))

        proof

          

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

          per cases ;

            suppose

             A18: ( Hom (( dom f),( cod g))) = {} ;

            ( Hom (( dom f),( dom g))) = {} by A18, ENS_1: 42;

            hence thesis by A17;

          end;

            suppose

             A19: ( Hom (( dom f),( cod g))) <> {} ;

            let e be object;

            assume

             A20: e in ( rng ( hom (f,a)));

            ( rng ( hom (f,a))) c= ( Hom (( dom f),a)) & ( Hom (( dom f),a)) = ( dom ( hom (( dom f),g))) by A17, A19, FUNCT_2:def 1, RELAT_1:def 19;

            hence thesis by A20;

          end;

        end;

        

         A21: ( dom (( hom (f,b)) * ( hom (( cod f),g)))) = ( dom (( hom (( dom f),g)) * ( hom (f,a))))

        proof

          per cases ;

            suppose

             A22: ( Hom (( cod f),( dom g))) = {} ;

            ( dom (( hom (f,b)) * ( hom (( cod f),g)))) = ( dom ( hom (( cod f),g))) by A11, RELAT_1: 27

            .= ( Hom (( cod f),( dom g))) by A22

            .= ( dom ( hom (f,a))) by A10, A22

            .= ( dom (( hom (( dom f),g)) * ( hom (f,a)))) by A16, RELAT_1: 27;

            hence thesis;

          end;

            suppose

             A23: ( Hom (( cod f),( dom g))) <> {} ;

            then

             A24: ( Hom (( cod f),( cod g))) <> {} by ENS_1: 42;

            

             A25: ( Hom (( dom f),a)) <> {} by A10, A23, ENS_1: 42;

            ( dom (( hom (f,b)) * ( hom (( cod f),g)))) = ( dom ( hom (( cod f),g))) by A11, RELAT_1: 27

            .= ( Hom (( cod f),( dom g))) by A24, FUNCT_2:def 1

            .= ( Hom (( cod f),a)) by A8, CAT_1: 5

            .= ( dom ( hom (f,a))) by A25, FUNCT_2:def 1

            .= ( dom (( hom (( dom f),g)) * ( hom (f,a)))) by A16, RELAT_1: 27;

            hence thesis;

          end;

        end;

        

         A26: for x be object st x in ( dom (( hom (f,b)) * ( hom (( cod f),g)))) holds ((( hom (f,b)) * ( hom (( cod f),g))) . x) = ((( hom (( dom f),g)) * ( hom (f,a))) . x)

        proof

          let x be object such that

           A27: x in ( dom (( hom (f,b)) * ( hom (( cod f),g))));

          per cases ;

            suppose

             A28: ( Hom (( cod f),( dom g))) <> {} ;

            

             A29: x in ( dom ( hom (( cod f),g))) by A27, FUNCT_1: 11;

            ( Hom (( cod f),( cod g))) <> {} by A28, ENS_1: 42;

            then

             A30: x in ( Hom (( cod f),( dom g))) by A29, FUNCT_2:def 1;

            then

            reconsider x as Morphism of A;

            

             A31: ( dom g) = ( cod x) & ( dom x) = ( cod f) by A30, CAT_1: 1;

            

             A32: ( dom g) = ( cod x) by A30, CAT_1: 1;

            

            then

             A33: ( cod (g (*) x)) = ( cod g) by CAT_1: 17

            .= b by A8, CAT_1: 5;

            

             A34: (( hom (f,a)) . x) = (x (*) f) by A10, A30, ENS_1:def 20;

            then

            reconsider h = (( hom (f,a)) . x) as Morphism of A;

            

             A35: ( dom x) = ( cod f) by A30, CAT_1: 1;

            then

             A36: ( dom (x (*) f)) = ( dom f) by CAT_1: 17;

            ( dom (g (*) x)) = ( dom x) by A32, CAT_1: 17

            .= ( cod f) by A30, CAT_1: 1;

            then

             A37: (g (*) x) in ( Hom (( cod f),b)) by A33;

            ( cod (x (*) f)) = ( cod x) by A35, CAT_1: 17

            .= ( dom g) by A30, CAT_1: 1;

            then

             A38: (( hom (f,a)) . x) in ( Hom (( dom f),( dom g))) by A34, A36;

            ((( hom (f,b)) * ( hom (( cod f),g))) . x) = (( hom (f,b)) . (( hom (( cod f),g)) . x)) by A27, FUNCT_1: 12

            .= (( hom (f,b)) . (g (*) x)) by A30, ENS_1:def 19

            .= ((g (*) x) (*) f) by A37, ENS_1:def 20

            .= (g (*) (x (*) f)) by A31, CAT_1: 18

            .= (g (*) h) by A10, A30, ENS_1:def 20

            .= (( hom (( dom f),g)) . (( hom (f,a)) . x)) by A38, ENS_1:def 19

            .= ((( hom (( dom f),g)) * ( hom (f,a))) . x) by A21, A27, FUNCT_1: 12;

            hence thesis;

          end;

            suppose

             A39: ( Hom (( cod f),( dom g))) = {} ;

            x in ( dom ( hom (( cod f),g))) by A27, FUNCT_1: 11;

            hence thesis by A39;

          end;

        end;

        

         A40: ( Hom ((F2 . a),(F2 . b))) <> {} by A8, CAT_1: 84;

        

         A41: ( cod g) = b by A8, CAT_1: 5;

        reconsider f4 = (t . a) as Morphism of ( EnsHom A);

        

         A42: (t . a) = (t qua Function of the carrier of A, the carrier' of B . a) by A7, NATTRA_1:def 5

        .= [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))] by A5;

        then

        reconsider f49 = f4 as Element of ( Maps ( Hom A)) by ENS_1: 48;

        

         A43: ( Hom ((F1 . a),(F2 . a))) <> {} by A1;

        reconsider f1 = (t . b) as Morphism of ( EnsHom A);

        

         A44: (t . b) = (t qua Function of the carrier of A, the carrier' of B . b) by A7, NATTRA_1:def 5

        .= [ [( Hom (( cod f),b)), ( Hom (( dom f),b))], ( hom (f,b))] by A5;

        then

        reconsider f19 = f1 as Element of ( Maps ( Hom A)) by ENS_1: 48;

        

         A45: ( EnsHom A) = CatStr (# ( Hom A), ( Maps ( Hom A)), ( fDom ( Hom A)), ( fCod ( Hom A)), ( fComp ( Hom A)) #) by ENS_1:def 13;

        

        then

         A46: ( cod f1) = (( fCod ( Hom A)) . f1)

        .= ( cod f19) by ENS_1:def 10

        .= ((f1 `1 ) `2 ) by ENS_1:def 4

        .= ( [( Hom (( cod f),b)), ( Hom (( dom f),b))] `2 ) by A44

        .= ( Hom (( dom f),b));

        

         A47: ( dom f4) = (( fDom ( Hom A)) . f4) by A45

        .= ( dom f49) by ENS_1:def 9

        .= ((f4 `1 ) `1 ) by ENS_1:def 3

        .= ( [( Hom (( cod f),a)), ( Hom (( dom f),a))] `1 ) by A42

        .= ( Hom (( cod f),a));

        

         A48: ( cod f4) = (( fCod ( Hom A)) . f4) by A45

        .= ( cod f49) by ENS_1:def 10

        .= ((f4 `1 ) `2 ) by ENS_1:def 4

        .= ( [( Hom (( cod f),a)), ( Hom (( dom f),a))] `2 ) by A42

        .= ( Hom (( dom f),a));

        reconsider f2 = (F1 /. g) as Morphism of ( EnsHom A);

        

         A49: f2 = (( hom?- ( cod f)) . g) by A8, CAT_3:def 10

        .= [ [( Hom (( cod f),( dom g))), ( Hom (( cod f),( cod g)))], ( hom (( cod f),g))] by ENS_1:def 21;

        then

        reconsider f29 = f2 as Element of ( Maps ( Hom A)) by ENS_1: 47;

        

         A50: ( dom f2) = (( fDom ( Hom A)) . f2) by A45

        .= ( dom f29) by ENS_1:def 9

        .= ((f2 `1 ) `1 ) by ENS_1:def 3

        .= ( [( Hom (( cod f),( dom g))), ( Hom (( cod f),( cod g)))] `1 ) by A49

        .= ( Hom (( cod f),( dom g)));

        

         A51: ( cod f2) = (( fCod ( Hom A)) . f2) by A45

        .= ( cod f29) by ENS_1:def 10

        .= ((f2 `1 ) `2 ) by ENS_1:def 4

        .= ( [( Hom (( cod f),( dom g))), ( Hom (( cod f),( cod g)))] `2 ) by A49

        .= ( Hom (( cod f),( cod g)));

        

         A52: ( dom f1) = (( fDom ( Hom A)) . f1) by A45

        .= ( dom f19) by ENS_1:def 9

        .= ((f1 `1 ) `1 ) by ENS_1:def 3

        .= ( [( Hom (( cod f),b)), ( Hom (( dom f),b))] `1 ) by A44

        .= ( Hom (( cod f),b));

        then

         A53: ( cod f2) = ( dom f1) by A8, A51, CAT_1: 5;

        reconsider f3 = (F2 /. g) as Morphism of ( EnsHom A);

        

         A54: f3 = (( hom?- ( dom f)) . g) by A8, CAT_3:def 10

        .= [ [( Hom (( dom f),( dom g))), ( Hom (( dom f),( cod g)))], ( hom (( dom f),g))] by ENS_1:def 21;

        then

        reconsider f39 = f3 as Element of ( Maps ( Hom A)) by ENS_1: 47;

        

         A55: ( cod f3) = (( fCod ( Hom A)) . f3) by A45

        .= ( cod f39) by ENS_1:def 10

        .= ((f3 `1 ) `2 ) by ENS_1:def 4

        .= ( [( Hom (( dom f),( dom g))), ( Hom (( dom f),( cod g)))] `2 ) by A54

        .= ( Hom (( dom f),( cod g)));

        

         A56: ( dom f3) = (( fDom ( Hom A)) . f3) by A45

        .= ( dom f39) by ENS_1:def 9

        .= ((f3 `1 ) `1 ) by ENS_1:def 3

        .= ( [( Hom (( dom f),( dom g))), ( Hom (( dom f),( cod g)))] `1 ) by A54

        .= ( Hom (( dom f),( dom g)));

        then

         A57: ( cod f4) = ( dom f3) by A8, A48, CAT_1: 5;

        ( Hom ((F1 . b),(F2 . b))) <> {} by A1;

        

        then ((t . b) * (F1 /. g)) = (f1 (*) f2) by A9, CAT_1:def 13

        .= [ [( Hom (( cod f),( dom g))), ( Hom (( dom f),b))], (( hom (f,b)) * ( hom (( cod f),g)))] by A44, A52, A46, A49, A50, A51, A53, Th1

        .= [ [( Hom (( cod f),a)), ( Hom (( dom f),( cod g)))], (( hom (( dom f),g)) * ( hom (f,a)))] by A10, A41, A21, A26, FUNCT_1: 2

        .= (f3 (*) f4) by A54, A56, A55, A42, A47, A48, A57, Th1

        .= ((F2 /. g) * (t . a)) by A40, A43, CAT_1:def 13;

        hence thesis;

      end;

      hence thesis by A7, NATTRA_1:def 7;

    end;

    definition

      let A, f;

      :: YONEDA_1:def3

      func <|f,?> -> natural_transformation of <|( cod f),?>, <|( dom f),?> means

      : Def3: for o be Object of A holds (it . o) = [ [( Hom (( cod f),o)), ( Hom (( dom f),o))], ( hom (f,( id o)))];

      existence

      proof

        set B = ( EnsHom A);

        deffunc F( Element of A) = [ [( Hom (( cod f),$1)), ( Hom (( dom f),$1))], ( hom (f,( id $1)))];

        set F1 = <|( cod f),?>, F2 = <|( dom f),?>;

        

         A1: for o be Object of A holds [ [( Hom (( cod f),o)), ( Hom (( dom f),o))], ( hom (f,( id o)))] in ( Hom ((F1 . o),(F2 . o)))

        proof

          let o be Object of A;

          

           A2: ( EnsHom A) = CatStr (# ( Hom A), ( Maps ( Hom A)), ( fDom ( Hom A)), ( fCod ( Hom A)), ( fComp ( Hom A)) #) by ENS_1:def 13;

          

           A3: ( hom (f,( id o))) = ( hom (f,o)) by ENS_1: 53;

          then

          reconsider m = [ [( Hom (( cod f),o)), ( Hom (( dom f),o))], ( hom (f,( id o)))] as Morphism of ( EnsHom A) by A2, ENS_1: 48;

          reconsider m9 = m as Element of ( Maps ( Hom A)) by A3, ENS_1: 48;

          

           A4: ( cod m) = (( fCod ( Hom A)) . m) by A2

          .= ( cod m9) by ENS_1:def 10

          .= ((m `1 ) `2 ) by ENS_1:def 4

          .= ( [( Hom (( cod f),o)), ( Hom (( dom f),o))] `2 )

          .= ( Hom (( dom f),o))

          .= (( Obj ( hom?- (( Hom A),( dom f)))) . o) by ENS_1: 60

          .= (( hom?- (( Hom A),( dom f))) . o)

          .= (F2 . o) by ENS_1:def 25;

          ( dom m) = (( fDom ( Hom A)) . m) by A2

          .= ( dom m9) by ENS_1:def 9

          .= ((m `1 ) `1 ) by ENS_1:def 3

          .= ( [( Hom (( cod f),o)), ( Hom (( dom f),o))] `1 )

          .= ( Hom (( cod f),o))

          .= (( Obj ( hom?- (( Hom A),( cod f)))) . o) by ENS_1: 60

          .= (( hom?- (( Hom A),( cod f))) . o)

          .= (F1 . o) by ENS_1:def 25;

          hence thesis by A4;

        end;

        

         A5: for o be Element of A holds F(o) in the carrier' of ( EnsHom A)

        proof

          let o;

           [ [( Hom (( cod f),o)), ( Hom (( dom f),o))], ( hom (f,( id o)))] in ( Hom ((F1 . o),(F2 . o))) by A1;

          hence thesis;

        end;

        consider t be Function of the carrier of A, the carrier' of ( EnsHom A) such that

         A6: for o be Element of A holds (t . o) = F(o) from FUNCT_2:sch 8( A5);

        

         A7: for o be Object of A holds (t . o) is Morphism of (F1 . o), (F2 . o)

        proof

          let o;

           [ [( Hom (( cod f),o)), ( Hom (( dom f),o))], ( hom (f,( id o)))] in ( Hom ((F1 . o),(F2 . o))) by A1;

          then [ [( Hom (( cod f),o)), ( Hom (( dom f),o))], ( hom (f,( id o)))] is Morphism of (F1 . o), (F2 . o) by CAT_1:def 5;

          hence thesis by A6;

        end;

        for o be Object of A holds ( Hom ((F1 . o),(F2 . o))) <> {} by A1;

        then

         A8: F1 is_transformable_to F2 by NATTRA_1:def 2;

        then

        reconsider t as transformation of F1, F2 by A7, NATTRA_1:def 3;

        

         A9: for a,b be Object of A st ( Hom (a,b)) <> {} holds for g be Morphism of a, b holds ((t . b) * (F1 /. g)) = ((F2 /. g) * (t . a))

        proof

          let a,b be Object of A such that

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

          

           A11: ( Hom ((F1 . a),(F1 . b))) <> {} by A10, CAT_1: 84;

          let g be Morphism of a, b;

          

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

          

           A13: ( rng ( hom (( cod f),g))) c= ( dom ( hom (f,b)))

          proof

            

             A14: ( cod g) = b by A10, CAT_1: 5;

            per cases ;

              suppose

               A15: ( Hom (( dom f),b)) = {} ;

              ( Hom (( cod f),b)) = {} by A15, ENS_1: 42;

              hence thesis by A14;

            end;

              suppose

               A16: ( Hom (( dom f),b)) <> {} ;

              ( cod g) = b by A10, CAT_1: 5;

              then

               A17: ( rng ( hom (( cod f),g))) c= ( Hom (( cod f),( cod g))) & ( Hom (( cod f),( cod g))) = ( dom ( hom (f,b))) by A16, FUNCT_2:def 1, RELAT_1:def 19;

              let e be object;

              assume e in ( rng ( hom (( cod f),g)));

              hence thesis by A17;

            end;

          end;

          

           A18: ( rng ( hom (f,a))) c= ( dom ( hom (( dom f),g)))

          proof

            

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

            per cases ;

              suppose

               A20: ( Hom (( dom f),( cod g))) = {} ;

              ( Hom (( dom f),( dom g))) = {} by A20, ENS_1: 42;

              hence thesis by A19;

            end;

              suppose

               A21: ( Hom (( dom f),( cod g))) <> {} ;

              let e be object;

              assume

               A22: e in ( rng ( hom (f,a)));

              ( rng ( hom (f,a))) c= ( Hom (( dom f),a)) & ( Hom (( dom f),a)) = ( dom ( hom (( dom f),g))) by A19, A21, FUNCT_2:def 1, RELAT_1:def 19;

              hence thesis by A22;

            end;

          end;

          

           A23: ( dom (( hom (f,b)) * ( hom (( cod f),g)))) = ( dom (( hom (( dom f),g)) * ( hom (f,a))))

          proof

            per cases ;

              suppose

               A24: ( Hom (( cod f),( dom g))) = {} ;

              ( dom (( hom (f,b)) * ( hom (( cod f),g)))) = ( dom ( hom (( cod f),g))) by A13, RELAT_1: 27

              .= ( Hom (( cod f),a)) by A12, A24

              .= ( dom ( hom (f,a))) by A12, A24

              .= ( dom (( hom (( dom f),g)) * ( hom (f,a)))) by A18, RELAT_1: 27;

              hence thesis;

            end;

              suppose

               A25: ( Hom (( cod f),( dom g))) <> {} ;

              then

               A26: ( Hom (( cod f),( cod g))) <> {} by ENS_1: 42;

              

               A27: ( Hom (( dom f),a)) <> {} by A12, A25, ENS_1: 42;

              ( dom (( hom (f,b)) * ( hom (( cod f),g)))) = ( dom ( hom (( cod f),g))) by A13, RELAT_1: 27

              .= ( Hom (( cod f),a)) by A12, A26, FUNCT_2:def 1

              .= ( dom ( hom (f,a))) by A27, FUNCT_2:def 1

              .= ( dom (( hom (( dom f),g)) * ( hom (f,a)))) by A18, RELAT_1: 27;

              hence thesis;

            end;

          end;

          

           A28: for x be object st x in ( dom (( hom (f,b)) * ( hom (( cod f),g)))) holds ((( hom (f,b)) * ( hom (( cod f),g))) . x) = ((( hom (( dom f),g)) * ( hom (f,a))) . x)

          proof

            let x be object such that

             A29: x in ( dom (( hom (f,b)) * ( hom (( cod f),g))));

            per cases ;

              suppose

               A30: ( Hom (( cod f),( dom g))) <> {} ;

              

               A31: x in ( dom ( hom (( cod f),g))) by A29, FUNCT_1: 11;

              ( Hom (( cod f),( cod g))) <> {} by A30, ENS_1: 42;

              then

               A32: x in ( Hom (( cod f),( dom g))) by A31, FUNCT_2:def 1;

              then

              reconsider x as Morphism of A;

              

               A33: ( dom g) = ( cod x) by A32, CAT_1: 1;

              ( cod g) = b by A10, CAT_1: 5;

              then

               A34: ( cod (g (*) x)) = b by A33, CAT_1: 17;

              ( dom (g (*) x)) = ( dom x) by A33, CAT_1: 17

              .= ( cod f) by A32, CAT_1: 1;

              then

               A35: (g (*) x) in ( Hom (( cod f),b)) by A34;

              

               A36: ( dom x) = ( cod f) by A32, CAT_1: 1;

              then

               A37: ( dom (x (*) f)) = ( dom f) by CAT_1: 17;

              

               A38: (( hom (f,a)) . x) = (x (*) f) by A12, A32, ENS_1:def 20;

              then

              reconsider h = (( hom (f,a)) . x) as Morphism of A;

              

               A39: ( dom g) = ( cod x) & ( dom x) = ( cod f) by A32, CAT_1: 1;

              ( cod (x (*) f)) = ( cod x) by A36, CAT_1: 17

              .= ( dom g) by A32, CAT_1: 1;

              then

               A40: (( hom (f,a)) . x) in ( Hom (( dom f),( dom g))) by A38, A37;

              ((( hom (f,b)) * ( hom (( cod f),g))) . x) = (( hom (f,b)) . (( hom (( cod f),g)) . x)) by A29, FUNCT_1: 12

              .= (( hom (f,b)) . (g (*) x)) by A32, ENS_1:def 19

              .= ((g (*) x) (*) f) by A35, ENS_1:def 20

              .= (g (*) (x (*) f)) by A39, CAT_1: 18

              .= (g (*) h) by A12, A32, ENS_1:def 20

              .= (( hom (( dom f),g)) . (( hom (f,a)) . x)) by A40, ENS_1:def 19

              .= ((( hom (( dom f),g)) * ( hom (f,a))) . x) by A23, A29, FUNCT_1: 12;

              hence thesis;

            end;

              suppose

               A41: ( Hom (( cod f),( dom g))) = {} ;

              x in ( dom ( hom (( cod f),g))) by A29, FUNCT_1: 11;

              hence thesis by A41;

            end;

          end;

          

           A42: ( Hom ((F2 . a),(F2 . b))) <> {} by A10, CAT_1: 84;

          

           A43: ( cod g) = b by A10, CAT_1: 5;

          reconsider f4 = (t . a) as Morphism of ( EnsHom A);

          

           A44: (t . a) = (t qua Function of the carrier of A, the carrier' of B . a) by A8, NATTRA_1:def 5

          .= [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,( id a)))] by A6

          .= [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))] by ENS_1: 53;

          then

          reconsider f49 = f4 as Element of ( Maps ( Hom A)) by ENS_1: 48;

          

           A45: ( Hom ((F1 . a),(F2 . a))) <> {} by A1;

          reconsider f1 = (t . b) as Morphism of ( EnsHom A);

          

           A46: (t . b) = (t qua Function of the carrier of A, the carrier' of B . b) by A8, NATTRA_1:def 5

          .= [ [( Hom (( cod f),b)), ( Hom (( dom f),b))], ( hom (f,( id b)))] by A6

          .= [ [( Hom (( cod f),b)), ( Hom (( dom f),b))], ( hom (f,b))] by ENS_1: 53;

          then

          reconsider f19 = f1 as Element of ( Maps ( Hom A)) by ENS_1: 48;

          

           A47: ( EnsHom A) = CatStr (# ( Hom A), ( Maps ( Hom A)), ( fDom ( Hom A)), ( fCod ( Hom A)), ( fComp ( Hom A)) #) by ENS_1:def 13;

          

          then

           A48: ( cod f1) = (( fCod ( Hom A)) . f1)

          .= ( cod f19) by ENS_1:def 10

          .= ((f1 `1 ) `2 ) by ENS_1:def 4

          .= ( [( Hom (( cod f),b)), ( Hom (( dom f),b))] `2 ) by A46

          .= ( Hom (( dom f),b));

          

           A49: ( dom f4) = (( fDom ( Hom A)) . f4) by A47

          .= ( dom f49) by ENS_1:def 9

          .= ((f4 `1 ) `1 ) by ENS_1:def 3

          .= ( [( Hom (( cod f),a)), ( Hom (( dom f),a))] `1 ) by A44

          .= ( Hom (( cod f),a));

          

           A50: ( cod f4) = (( fCod ( Hom A)) . f4) by A47

          .= ( cod f49) by ENS_1:def 10

          .= ((f4 `1 ) `2 ) by ENS_1:def 4

          .= ( [( Hom (( cod f),a)), ( Hom (( dom f),a))] `2 ) by A44

          .= ( Hom (( dom f),a));

          reconsider f2 = (F1 /. g) as Morphism of ( EnsHom A);

          

           A51: f2 = (( hom?- ( cod f)) . g) by A10, CAT_3:def 10

          .= [ [( Hom (( cod f),( dom g))), ( Hom (( cod f),( cod g)))], ( hom (( cod f),g))] by ENS_1:def 21;

          then

          reconsider f29 = f2 as Element of ( Maps ( Hom A)) by ENS_1: 47;

          

           A52: ( dom f2) = (( fDom ( Hom A)) . f2) by A47

          .= ( dom f29) by ENS_1:def 9

          .= ((f2 `1 ) `1 ) by ENS_1:def 3

          .= ( [( Hom (( cod f),( dom g))), ( Hom (( cod f),( cod g)))] `1 ) by A51

          .= ( Hom (( cod f),( dom g)));

          

           A53: ( cod f2) = (( fCod ( Hom A)) . f2) by A47

          .= ( cod f29) by ENS_1:def 10

          .= ((f2 `1 ) `2 ) by ENS_1:def 4

          .= ( [( Hom (( cod f),( dom g))), ( Hom (( cod f),( cod g)))] `2 ) by A51

          .= ( Hom (( cod f),( cod g)));

          

           A54: ( dom f1) = (( fDom ( Hom A)) . f1) by A47

          .= ( dom f19) by ENS_1:def 9

          .= ((f1 `1 ) `1 ) by ENS_1:def 3

          .= ( [( Hom (( cod f),b)), ( Hom (( dom f),b))] `1 ) by A46

          .= ( Hom (( cod f),b));

          then

           A55: ( cod f2) = ( dom f1) by A10, A53, CAT_1: 5;

          reconsider f3 = (F2 /. g) as Morphism of ( EnsHom A);

          

           A56: f3 = (( hom?- ( dom f)) . g) by A10, CAT_3:def 10

          .= [ [( Hom (( dom f),( dom g))), ( Hom (( dom f),( cod g)))], ( hom (( dom f),g))] by ENS_1:def 21;

          then

          reconsider f39 = f3 as Element of ( Maps ( Hom A)) by ENS_1: 47;

          

           A57: ( cod f3) = (( fCod ( Hom A)) . f3) by A47

          .= ( cod f39) by ENS_1:def 10

          .= ((f3 `1 ) `2 ) by ENS_1:def 4

          .= ( [( Hom (( dom f),( dom g))), ( Hom (( dom f),( cod g)))] `2 ) by A56

          .= ( Hom (( dom f),( cod g)));

          

           A58: ( dom f3) = (( fDom ( Hom A)) . f3) by A47

          .= ( dom f39) by ENS_1:def 9

          .= ((f3 `1 ) `1 ) by ENS_1:def 3

          .= ( [( Hom (( dom f),( dom g))), ( Hom (( dom f),( cod g)))] `1 ) by A56

          .= ( Hom (( dom f),( dom g)));

          then

           A59: ( cod f4) = ( dom f3) by A10, A50, CAT_1: 5;

          ( Hom ((F1 . b),(F2 . b))) <> {} by A1;

          

          then ((t . b) * (F1 /. g)) = (f1 (*) f2) by A11, CAT_1:def 13

          .= [ [( Hom (( cod f),( dom g))), ( Hom (( dom f),b))], (( hom (f,b)) * ( hom (( cod f),g)))] by A46, A54, A48, A51, A52, A53, A55, Th1

          .= [ [( Hom (( cod f),a)), ( Hom (( dom f),( cod g)))], (( hom (( dom f),g)) * ( hom (f,a)))] by A12, A43, A23, A28, FUNCT_1: 2

          .= (f3 (*) f4) by A56, A58, A57, A44, A49, A50, A59, Th1

          .= ((F2 /. g) * (t . a)) by A42, A45, CAT_1:def 13;

          hence thesis;

        end;

        F1 is_naturally_transformable_to F2 by Th2;

        then

        reconsider t as natural_transformation of F1, F2 by A9, NATTRA_1:def 8;

        for o be Element of A holds (t . o) = [ [( Hom (( cod f),o)), ( Hom (( dom f),o))], ( hom (f,( id o)))]

        proof

          let o;

          (t . o) = (t qua Function . o) by A8, NATTRA_1:def 5

          .= [ [( Hom (( cod f),o)), ( Hom (( dom f),o))], ( hom (f,( id o)))] by A6;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        for a be Object of A holds [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))] in ( Hom (( <|( cod f),?> . a),( <|( dom f),?> . a)))

        proof

          let a be Object of A;

          

           A60: ( EnsHom A) = CatStr (# ( Hom A), ( Maps ( Hom A)), ( fDom ( Hom A)), ( fCod ( Hom A)), ( fComp ( Hom A)) #) by ENS_1:def 13;

          then

          reconsider m = [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))] as Morphism of ( EnsHom A) by ENS_1: 48;

          reconsider m9 = m as Element of ( Maps ( Hom A)) by ENS_1: 48;

          

           A61: ( cod m) = (( fCod ( Hom A)) . m) by A60

          .= ( cod m9) by ENS_1:def 10

          .= ((m `1 ) `2 ) by ENS_1:def 4

          .= ( [( Hom (( cod f),a)), ( Hom (( dom f),a))] `2 )

          .= ( Hom (( dom f),a))

          .= (( Obj ( hom?- (( Hom A),( dom f)))) . a) by ENS_1: 60

          .= (( hom?- (( Hom A),( dom f))) . a)

          .= ( <|( dom f),?> . a) by ENS_1:def 25;

          ( dom m) = (( fDom ( Hom A)) . m) by A60

          .= ( dom m9) by ENS_1:def 9

          .= ((m `1 ) `1 ) by ENS_1:def 3

          .= ( [( Hom (( cod f),a)), ( Hom (( dom f),a))] `1 )

          .= ( Hom (( cod f),a))

          .= (( Obj ( hom?- (( Hom A),( cod f)))) . a) by ENS_1: 60

          .= (( hom?- (( Hom A),( cod f))) . a)

          .= ( <|( cod f),?> . a) by ENS_1:def 25;

          hence thesis by A61;

        end;

        then for a be Object of A holds ( Hom (( <|( cod f),?> . a),( <|( dom f),?> . a))) <> {} ;

        then

         A62: <|( cod f),?> is_transformable_to <|( dom f),?> by NATTRA_1:def 2;

        let h1,h2 be natural_transformation of <|( cod f),?>, <|( dom f),?> such that

         A63: for o be Object of A holds (h1 . o) = [ [( Hom (( cod f),o)), ( Hom (( dom f),o))], ( hom (f,( id o)))] and

         A64: for o be Object of A holds (h2 . o) = [ [( Hom (( cod f),o)), ( Hom (( dom f),o))], ( hom (f,( id o)))];

        now

          let o;

          

          thus (h1 . o) = [ [( Hom (( cod f),o)), ( Hom (( dom f),o))], ( hom (f,( id o)))] by A63

          .= (h2 . o) by A64;

        end;

        hence thesis by A62, NATTRA_1: 19;

      end;

    end

    theorem :: YONEDA_1:3

    

     Th3: for f be Element of the carrier' of A holds [ [ <|( cod f),?>, <|( dom f),?>], <|f,?>] is Element of the carrier' of ( Functors (A,( EnsHom A)))

    proof

      let f be Element of the carrier' of A;

       <|( cod f),?> is_naturally_transformable_to <|( dom f),?> by Th2;

      then [ [ <|( cod f),?>, <|( dom f),?>], <|f,?>] in ( NatTrans (A,( EnsHom A))) by NATTRA_1:def 16;

      hence thesis by NATTRA_1:def 17;

    end;

    definition

      let A;

      :: YONEDA_1:def4

      func Yoneda (A) -> Contravariant_Functor of A, ( Functors (A,( EnsHom A))) means

      : Def4: for f be Morphism of A holds (it . f) = [ [ <|( cod f),?>, <|( dom f),?>], <|f,?>];

      existence

      proof

        deffunc F( Element of the carrier' of A) = [ [ <|( cod $1),?>, <|( dom $1),?>], <|$1,?>];

        

         A1: for f be Element of the carrier' of A holds F(f) in the carrier' of ( Functors (A,( EnsHom A)))

        proof

          let f;

           [ [ <|( cod f),?>, <|( dom f),?>], <|f,?>] is Morphism of ( Functors (A,( EnsHom A))) by Th3;

          hence thesis;

        end;

        consider F be Function of the carrier' of A, the carrier' of ( Functors (A,( EnsHom A))) such that

         A2: for f be Element of the carrier' of A holds (F . f) = F(f) from FUNCT_2:sch 8( A1);

        

         A3: for f,g be Morphism of A st ( dom g) = ( cod f) holds (F . (g (*) f)) = ((F . f) (*) (F . g))

        proof

          let f,g be Morphism of A;

          reconsider t1 = <|g,?> as natural_transformation of <|( cod g),?>, <|( dom g),?>;

          assume

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

          then

          reconsider t = <|f,?> as natural_transformation of <|( dom g),?>, <|( dom f),?>;

          

           A5: (F . g) = [ [ <|( cod g),?>, <|( dom g),?>], t1] by A2;

          

           A6: ( dom (g (*) f)) = ( dom f) by A4, CAT_1: 17;

          then

          reconsider tt = (t `*` t1) as natural_transformation of <|( cod (g (*) f)),?>, <|( dom (g (*) f)),?> by A4, CAT_1: 17;

          

           A7: ( cod (g (*) f)) = ( cod g) by A4, CAT_1: 17;

          for o be Object of A holds ( <|(g (*) f),?> . o) = (tt . o)

          proof

            set F1 = <|( cod f),?>, F2 = <|( dom f),?>;

            let o be Object of A;

            reconsider f1 = (t . o) as Morphism of ( EnsHom A);

            reconsider f2 = (t1 . o) as Morphism of ( EnsHom A);

            

             A8: f2 = [ [( Hom (( cod g),o)), ( Hom (( dom g),o))], ( hom (g,( id o)))] by Def3;

            for a be Object of A holds [ [( Hom (( cod g),a)), ( Hom (( dom g),a))], ( hom (g,a))] in ( Hom (( <|( cod g),?> . a),( <|( dom g),?> . a)))

            proof

              let a be Object of A;

              

               A9: ( EnsHom A) = CatStr (# ( Hom A), ( Maps ( Hom A)), ( fDom ( Hom A)), ( fCod ( Hom A)), ( fComp ( Hom A)) #) by ENS_1:def 13;

              then

              reconsider m = [ [( Hom (( cod g),a)), ( Hom (( dom g),a))], ( hom (g,a))] as Morphism of ( EnsHom A) by ENS_1: 48;

              reconsider m9 = m as Element of ( Maps ( Hom A)) by ENS_1: 48;

              

               A10: ( cod m) = (( fCod ( Hom A)) . m) by A9

              .= ( cod m9) by ENS_1:def 10

              .= ((m `1 ) `2 ) by ENS_1:def 4

              .= ( [( Hom (( cod g),a)), ( Hom (( dom g),a))] `2 )

              .= ( Hom (( dom g),a))

              .= (( Obj ( hom?- (( Hom A),( dom g)))) . a) by ENS_1: 60

              .= (( hom?- (( Hom A),( dom g))) . a)

              .= ( <|( dom g),?> . a) by ENS_1:def 25;

              ( dom m) = (( fDom ( Hom A)) . m) by A9

              .= ( dom m9) by ENS_1:def 9

              .= ((m `1 ) `1 ) by ENS_1:def 3

              .= ( [( Hom (( cod g),a)), ( Hom (( dom g),a))] `1 )

              .= ( Hom (( cod g),a))

              .= (( Obj ( hom?- (( Hom A),( cod g)))) . a) by ENS_1: 60

              .= (( hom?- (( Hom A),( cod g))) . a)

              .= ( <|( cod g),?> . a) by ENS_1:def 25;

              hence thesis by A10;

            end;

            then

             A11: ( Hom (( <|( cod g),?> . o),( <|( dom g),?> . o))) <> {} ;

            for a be Object of A holds [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))] in ( Hom ((F1 . a),(F2 . a)))

            proof

              let a be Object of A;

              

               A12: ( EnsHom A) = CatStr (# ( Hom A), ( Maps ( Hom A)), ( fDom ( Hom A)), ( fCod ( Hom A)), ( fComp ( Hom A)) #) by ENS_1:def 13;

              then

              reconsider m = [ [( Hom (( cod f),a)), ( Hom (( dom f),a))], ( hom (f,a))] as Morphism of ( EnsHom A) by ENS_1: 48;

              reconsider m9 = m as Element of ( Maps ( Hom A)) by ENS_1: 48;

              

               A13: ( cod m) = (( fCod ( Hom A)) . m) by A12

              .= ( cod m9) by ENS_1:def 10

              .= ((m `1 ) `2 ) by ENS_1:def 4

              .= ( [( Hom (( cod f),a)), ( Hom (( dom f),a))] `2 )

              .= ( Hom (( dom f),a))

              .= (( Obj ( hom?- (( Hom A),( dom f)))) . a) by ENS_1: 60

              .= (( hom?- (( Hom A),( dom f))) . a)

              .= (F2 . a) by ENS_1:def 25;

              ( dom m) = (( fDom ( Hom A)) . m) by A12

              .= ( dom m9) by ENS_1:def 9

              .= ((m `1 ) `1 ) by ENS_1:def 3

              .= ( [( Hom (( cod f),a)), ( Hom (( dom f),a))] `1 )

              .= ( Hom (( cod f),a))

              .= (( Obj ( hom?- (( Hom A),( cod f)))) . a) by ENS_1: 60

              .= (( hom?- (( Hom A),( cod f))) . a)

              .= (F1 . a) by ENS_1:def 25;

              hence thesis by A13;

            end;

            then

             A14: ( Hom ((F1 . o),(F2 . o))) <> {} ;

            

             A15: ( <|(g (*) f),?> . o) = [ [( Hom (( cod g),o)), ( Hom (( dom (g (*) f)),o))], ( hom ((g (*) f),( id o)))] by A7, Def3

            .= [ [( Hom (( cod g),o)), ( Hom (( dom f),o))], ( hom ((g (*) f),o))] by A6, ENS_1: 53;

            

             A16: (t . o) = [ [( Hom (( cod f),o)), ( Hom (( dom f),o))], ( hom (f,( id o)))] by A4, Def3;

            

             A17: ( EnsHom A) = CatStr (# ( Hom A), ( Maps ( Hom A)), ( fDom ( Hom A)), ( fCod ( Hom A)), ( fComp ( Hom A)) #) by ENS_1:def 13;

            then

            reconsider f19 = f1 as Element of ( Maps ( Hom A));

            reconsider f29 = f2 as Element of ( Maps ( Hom A)) by A17;

            

             A18: ( cod f2) = (( fCod ( Hom A)) . f2) by A17

            .= ( cod f29) by ENS_1:def 10

            .= ((f2 `1 ) `2 ) by ENS_1:def 4

            .= ( [( Hom (( cod g),o)), ( Hom (( dom g),o))] `2 ) by A8

            .= ( Hom (( dom g),o));

            

             A19: ( cod f1) = (( fCod ( Hom A)) . f1) by A17

            .= ( cod f19) by ENS_1:def 10

            .= ((f1 `1 ) `2 ) by ENS_1:def 4

            .= ( [( Hom (( cod f),o)), ( Hom (( dom f),o))] `2 ) by A16

            .= ( Hom (( dom f),o));

            

             A20: ( dom f1) = (( fDom ( Hom A)) . f1) by A17

            .= ( dom f19) by ENS_1:def 9

            .= ((f1 `1 ) `1 ) by ENS_1:def 3

            .= ( [( Hom (( cod f),o)), ( Hom (( dom f),o))] `1 ) by A16

            .= ( Hom (( cod f),o));

            

             A21: ( dom f2) = (( fDom ( Hom A)) . f2) by A17

            .= ( dom f29) by ENS_1:def 9

            .= ((f2 `1 ) `1 ) by ENS_1:def 3

            .= ( [( Hom (( cod g),o)), ( Hom (( dom g),o))] `1 ) by A8

            .= ( Hom (( cod g),o));

             <|( dom g),?> is_naturally_transformable_to <|( dom f),?> & <|( cod g),?> is_naturally_transformable_to <|( dom g),?> by A4, Th2;

            

            then (tt . o) = ((t . o) * (t1 . o)) by A6, A7, NATTRA_1: 25

            .= (f1 (*) f2) by A4, A14, A11, CAT_1:def 13

            .= [ [( Hom (( cod g),o)), ( Hom (( dom f),o))], (( hom (f,( id o))) * ( hom (g,( id o))))] by A4, A16, A8, A20, A18, A21, A19, Th1

            .= [ [( Hom (( cod g),o)), ( Hom (( dom f),o))], (( hom (f,o)) * ( hom (g,( id o))))] by ENS_1: 53

            .= [ [( Hom (( cod g),o)), ( Hom (( dom f),o))], (( hom (f,o)) * ( hom (g,o)))] by ENS_1: 53

            .= [ [( Hom (( cod g),o)), ( Hom (( dom f),o))], ( hom ((g (*) f),o))] by A4, ENS_1: 46;

            hence thesis by A15;

          end;

          then

           A22: <|(g (*) f),?> = tt by Th2, ISOCAT_1: 26;

          

           A23: (F . f) = [ [ <|( dom g),?>, <|( dom f),?>], t] by A2, A4;

          then

           A24: [(F . f), (F . g)] in ( dom the Comp of ( Functors (A,( EnsHom A)))) by A5, NATTRA_1: 35;

          then

          consider F9,F19,F29 be Functor of A, ( EnsHom A), t9 be natural_transformation of F9, F19, t19 be natural_transformation of F19, F29 such that

           A25: (F . g) = [ [F9, F19], t9] and

           A26: (F . f) = [ [F19, F29], t19] and

           A27: (the Comp of ( Functors (A,( EnsHom A))) . ((F . f),(F . g))) = [ [F9, F29], (t19 `*` t9)] by NATTRA_1:def 17;

          

           A28: <|f,?> = t19 by A23, A26, XTUPLE_0: 1;

           [F19, F29] = [ <|( dom g),?>, <|( dom f),?>] by A23, A26, XTUPLE_0: 1;

          then

           A29: <|( dom f),?> = F29 by XTUPLE_0: 1;

           [F9, F19] = [ <|( cod g),?>, <|( dom g),?>] by A5, A25, XTUPLE_0: 1;

          then

           A30: <|( cod g),?> = F9 & <|( dom g),?> = F19 by XTUPLE_0: 1;

           <|g,?> = t9 by A5, A25, XTUPLE_0: 1;

          then ((F . f) (*) (F . g)) = [ [ <|( cod g),?>, <|( dom f),?>], (t `*` t1)] by A24, A27, A28, A30, A29, CAT_1:def 1;

          hence thesis by A2, A6, A7, A22;

        end;

        

         A31: for f be Morphism of A holds (F . ( id ( dom f))) = ( id ( cod (F . f))) & (F . ( id ( cod f))) = ( id ( dom (F . f)))

        proof

          let f;

          set g = (F . f);

          set X = ( dom <|( id ( dom f)),?>);

          

           A32: ( dom <|( id ( dom f)),?>) = the carrier of A by FUNCT_2:def 1

          .= ( dom ( id <|( dom f),?>)) by FUNCT_2:def 1;

          

           A33: (F . ( id ( dom f))) = [ [ <|( cod ( id ( dom f))),?>, <|( dom ( id ( dom f))),?>], <|( id ( dom f)),?>] by A2

          .= [ [ <|( dom f),?>, <|( dom ( id ( dom f))),?>], <|( id ( dom f)),?>]

          .= [ [ <|( dom f),?>, <|( dom f),?>], <|( id ( dom f)),?>];

          

           A34: g = [ [ <|( cod f),?>, <|( dom f),?>], <|f,?>] by A2;

          then ( cod g) = <|( dom f),?> by NATTRA_1: 33;

          then

           A35: [ [ <|( dom f),?>, <|( dom f),?>], ( id <|( dom f),?>)] = ( id ( cod (F . f))) by NATTRA_1:def 17;

          

           A36: for y be object st y in X holds ( <|( id ( dom f)),?> . y) = (( id <|( dom f),?>) . y)

          proof

            let y be object;

            assume y in X;

            then

            reconsider z = y as Object of A by FUNCT_2:def 1;

            reconsider zz = ( id z) as Morphism of z, z;

            

             A37: ( Hom (z,z)) <> {} ;

            ( <|( id ( dom f)),?> . z) = [ [( Hom (( cod ( id ( dom f))),z)), ( Hom (( dom ( id ( dom f))),z))], ( hom (( id ( dom f)),( id z)))] by Def3

            .= [ [( Hom (( dom f),z)), ( Hom (( dom ( id ( dom f))),z))], ( hom (( id ( dom f)),( id z)))]

            .= [ [( Hom (( dom f),z)), ( Hom (( dom f),z))], ( hom (( id ( dom f)),( id z)))]

            .= [ [( Hom (( dom f),z)), ( Hom (( dom f),z))], ( hom (( dom f),( id z)))] by ENS_1: 53

            .= [ [( Hom (( dom f),z)), ( Hom (( dom f),( cod ( id z))))], ( hom (( dom f),( id z)))]

            .= [ [( Hom (( dom f),( dom ( id z)))), ( Hom (( dom f),( cod ( id z))))], ( hom (( dom f),( id z)))]

            .= ( <|( dom f),?> qua Function . ( id z)) by ENS_1:def 21

            .= ( <|( dom f),?> /. zz) by A37, CAT_3:def 10

            .= ( id ( <|( dom f),?> . z)) by NATTRA_1: 15

            .= (( id <|( dom f),?>) . z) by NATTRA_1: 20

            .= (( id <|( dom f),?>) qua Function . z) by NATTRA_1:def 5;

            hence thesis by NATTRA_1:def 5;

          end;

          set X = ( dom <|( id ( cod f)),?>);

          

           A38: for y be object st y in X holds ( <|( id ( cod f)),?> . y) = (( id <|( cod f),?>) . y)

          proof

            let y be object;

            assume y in X;

            then

            reconsider z = y as Object of A by FUNCT_2:def 1;

            

             A39: ( Hom (z,z)) <> {} ;

            ( <|( id ( cod f)),?> . z) = [ [( Hom (( cod ( id ( cod f))),z)), ( Hom (( dom ( id ( cod f))),z))], ( hom (( id ( cod f)),( id z)))] by Def3

            .= [ [( Hom (( cod f),z)), ( Hom (( dom ( id ( cod f))),z))], ( hom (( id ( cod f)),( id z)))]

            .= [ [( Hom (( cod f),z)), ( Hom (( cod f),z))], ( hom (( id ( cod f)),( id z)))]

            .= [ [( Hom (( cod f),z)), ( Hom (( cod f),z))], ( hom (( cod f),( id z)))] by ENS_1: 53

            .= [ [( Hom (( cod f),z)), ( Hom (( cod f),( cod ( id z))))], ( hom (( cod f),( id z)))]

            .= [ [( Hom (( cod f),( dom ( id z)))), ( Hom (( cod f),( cod ( id z))))], ( hom (( cod f),( id z)))]

            .= ( <|( cod f),?> qua Function . ( id z)) by ENS_1:def 21

            .= ( <|( cod f),?> /. ( id z)) by A39, CAT_3:def 10

            .= ( id ( <|( cod f),?> . z)) by NATTRA_1: 15

            .= (( id <|( cod f),?>) . z) by NATTRA_1: 20

            .= (( id <|( cod f),?>) qua Function . z) by NATTRA_1:def 5;

            hence thesis by NATTRA_1:def 5;

          end;

          ( dom <|( id ( cod f)),?>) = the carrier of A by FUNCT_2:def 1

          .= ( dom ( id <|( cod f),?>)) by FUNCT_2:def 1;

          then

           A40: <|( id ( cod f)),?> = ( id <|( cod f),?>) by A38, FUNCT_1: 2;

          

           A41: (F . ( id ( cod f))) = [ [ <|( cod ( id ( cod f))),?>, <|( dom ( id ( cod f))),?>], <|( id ( cod f)),?>] by A2

          .= [ [ <|( cod f),?>, <|( dom ( id ( cod f))),?>], <|( id ( cod f)),?>]

          .= [ [ <|( cod f),?>, <|( cod f),?>], <|( id ( cod f)),?>];

          ( dom g) = <|( cod f),?> by A34, NATTRA_1: 33;

          hence thesis by A33, A35, A32, A36, A41, A40, FUNCT_1: 2, NATTRA_1:def 17;

        end;

        for c be Object of A holds ex d be Object of ( Functors (A,( EnsHom A))) st (F . ( id c)) = ( id d)

        proof

          let c be Object of A;

          set X = ( dom <|( id c),?>);

           <|c,?> in ( Funct (A,( EnsHom A))) by CAT_2:def 2;

          then

          reconsider d = <|c,?> as Object of ( Functors (A,( EnsHom A))) by NATTRA_1:def 17;

          take d;

          

           A42: for y be object st y in X holds ( <|( id c),?> . y) = (( id <|c,?>) . y)

          proof

            let y be object;

            assume y in X;

            then

            reconsider z = y as Object of A by FUNCT_2:def 1;

            reconsider zz = ( id z) as Morphism of z, z;

            

             A43: ( Hom (z,z)) <> {} ;

            ( <|( id c),?> . z) = [ [( Hom (( cod ( id c)),z)), ( Hom (( dom ( id c)),z))], ( hom (( id c),( id z)))] by Def3

            .= [ [( Hom (c,z)), ( Hom (( dom ( id c)),z))], ( hom (( id c),( id z)))]

            .= [ [( Hom (c,z)), ( Hom (c,z))], ( hom (( id c),( id z)))]

            .= [ [( Hom (c,z)), ( Hom (c,z))], ( hom (c,( id z)))] by ENS_1: 53

            .= [ [( Hom (c,z)), ( Hom (c,( cod ( id z))))], ( hom (c,( id z)))]

            .= [ [( Hom (c,( dom ( id z)))), ( Hom (c,( cod ( id z))))], ( hom (c,( id z)))]

            .= ( <|c,?> qua Function . ( id z)) by ENS_1:def 21

            .= ( <|c,?> /. zz) by A43, CAT_3:def 10

            .= ( id ( <|c,?> . z)) by NATTRA_1: 15

            .= (( id <|c,?>) . z) by NATTRA_1: 20

            .= (( id <|c,?>) qua Function . z) by NATTRA_1:def 5;

            hence thesis by NATTRA_1:def 5;

          end;

          ( dom <|( id c),?>) = the carrier of A by FUNCT_2:def 1

          .= ( dom ( id <|c,?>)) by FUNCT_2:def 1;

          then

           A44: <|( id c),?> = ( id <|c,?>) by A42, FUNCT_1: 2;

          (F . ( id c)) = [ [ <|( cod ( id c)),?>, <|( dom ( id c)),?>], <|( id c),?>] by A2

          .= [ [ <|c,?>, <|( dom ( id c)),?>], <|( id c),?>]

          .= [ [ <|c,?>, <|c,?>], ( id <|c,?>)] by A44

          .= ( id d) by NATTRA_1:def 17;

          hence thesis;

        end;

        then

        reconsider F as Contravariant_Functor of A, ( Functors (A,( EnsHom A))) by A31, A3, OPPCAT_1:def 9;

        for f be Element of the carrier' of A holds (F . f) = [ [ <|( cod f),?>, <|( dom f),?>], <|f,?>] by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let h1,h2 be Contravariant_Functor of A, ( Functors (A,( EnsHom A))) such that

         A45: for f holds (h1 . f) = [ [ <|( cod f),?>, <|( dom f),?>], <|f,?>] and

         A46: for f holds (h2 . f) = [ [ <|( cod f),?>, <|( dom f),?>], <|f,?>];

        now

          let f;

          

          thus (h1 . f) = [ [ <|( cod f),?>, <|( dom f),?>], <|f,?>] by A45

          .= (h2 . f) by A46;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let A,B be Category;

      let F be Contravariant_Functor of A, B;

      let c be Object of A;

      :: YONEDA_1:def5

      func F . c -> Object of B equals (( Obj F) . c);

      correctness ;

    end

    theorem :: YONEDA_1:4

    for F be Functor of A, ( Functors (A,( EnsHom A))) st ( Obj F) is one-to-one & F is faithful holds F is one-to-one

    proof

      let F be Functor of A, ( Functors (A,( EnsHom A)));

      assume

       A1: ( Obj F) is one-to-one;

      assume

       A2: F is faithful;

      for x1,x2 be object st x1 in ( dom F) & x2 in ( dom F) & (F . x1) = (F . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume that

         A3: x1 in ( dom F) & x2 in ( dom F) and

         A4: (F . x1) = (F . x2);

        reconsider m1 = x1, m2 = x2 as Morphism of A by A3, FUNCT_2:def 1;

        set o1 = ( dom m1), o2 = ( cod m1);

        set o3 = ( dom m2), o4 = ( cod m2);

        reconsider m19 = m1 as Morphism of o1, o2 by CAT_1: 4;

        reconsider m29 = m2 as Morphism of o3, o4 by CAT_1: 4;

        

         A5: ( Hom (o1,o2)) <> {} by CAT_1: 2;

        then

         A6: ( Hom ((F . o1),(F . o2))) <> {} by CAT_1: 84;

        

         A7: ( Hom (o3,o4)) <> {} by CAT_1: 2;

        then

         A8: ( Hom ((F . o3),(F . o4))) <> {} by CAT_1: 84;

        

         A9: (F /. m19) = (F . m2) by A4, A5, CAT_3:def 10

        .= (F /. m29) by A7, CAT_3:def 10;

        (( Obj F) . o1) = (F . o1)

        .= ( dom (F /. m29)) by A9, A6, CAT_1: 5

        .= (( Obj F) . o3) by A8, CAT_1: 5;

        then

         A10: m2 is Morphism of ( dom m2), ( cod m2) & o1 = o3 by A1, CAT_1: 4, FUNCT_2: 19;

        (( Obj F) . o2) = (F . o2)

        .= ( cod (F /. m29)) by A9, A6, CAT_1: 5

        .= (( Obj F) . o4) by A8, CAT_1: 5;

        then m1 is Morphism of ( dom m1), ( cod m1) & m2 is Morphism of o1, o2 by A1, A10, CAT_1: 4, FUNCT_2: 19;

        hence thesis by A2, A4, A5;

      end;

      hence thesis by FUNCT_1:def 4;

    end;

    definition

      let C,D be Category;

      let T be Contravariant_Functor of C, D;

      :: YONEDA_1:def6

      attr T is faithful means for c,c9 be Object of C st ( Hom (c,c9)) <> {} holds for f1,f2 be Morphism of c, c9 holds (T . f1) = (T . f2) implies f1 = f2;

    end

    theorem :: YONEDA_1:5

    

     Th5: for F be Contravariant_Functor of A, ( Functors (A,( EnsHom A))) st ( Obj F) is one-to-one & F is faithful holds F is one-to-one

    proof

      let F be Contravariant_Functor of A, ( Functors (A,( EnsHom A)));

      assume

       A1: ( Obj F) is one-to-one;

      assume

       A2: F is faithful;

      for x1,x2 be object st x1 in ( dom F) & x2 in ( dom F) & (F . x1) = (F . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume that

         A3: x1 in ( dom F) & x2 in ( dom F) and

         A4: (F . x1) = (F . x2);

        reconsider m1 = x1, m2 = x2 as Morphism of A by A3, FUNCT_2:def 1;

        set o1 = ( dom m1), o2 = ( cod m1);

        set o3 = ( dom m2), o4 = ( cod m2);

        reconsider m29 = m2 as Morphism of o3, o4 by CAT_1: 4;

        (( Obj F) . o1) = ( cod (F . m29)) by A4, OPPCAT_1: 32

        .= (( Obj F) . o3) by OPPCAT_1: 32;

        then

         A5: m2 is Morphism of ( dom m2), ( cod m2) & o1 = o3 by A1, CAT_1: 4, FUNCT_2: 19;

        

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

        (( Obj F) . o2) = ( dom (F . m29)) by A4, OPPCAT_1: 32

        .= (( Obj F) . o4) by OPPCAT_1: 32;

        then m2 is Morphism of o1, o2 by A1, A5, FUNCT_2: 19;

        hence thesis by A2, A4, A6;

      end;

      hence thesis by FUNCT_1:def 4;

    end;

    registration

      let A;

      cluster ( Yoneda A) -> faithful;

      coherence

      proof

        set F = ( Yoneda A);

        for o1,o2 be Object of A st ( Hom (o1,o2)) <> {} holds for x1,x2 be Morphism of o1, o2 holds (F . x1) = (F . x2) implies x1 = x2

        proof

          let o1,o2 be Object of A;

          assume

           A1: ( Hom (o1,o2)) <> {} ;

          let x1,x2 be Morphism of o1, o2;

          

           A2: x2 in ( Hom (o1,o2)) by A1, CAT_1:def 5;

          assume (F . x1) = (F . x2);

          then [ [ <|( cod x1),?>, <|( dom x1),?>], <|x1,?>] = (F . x2) by Def4;

          then [ [ <|( cod x1),?>, <|( dom x1),?>], <|x1,?>] = [ [ <|( cod x2),?>, <|( dom x2),?>], <|x2,?>] by Def4;

          then [ <|( cod x1),?>, <|( dom x1),?>, <|x1,?>] = [ [ <|( cod x2),?>, <|( dom x2),?>], <|x2,?>];

          then [ <|( cod x1),?>, <|( dom x1),?>, <|x1,?>] = [ <|( cod x2),?>, <|( dom x2),?>, <|x2,?>];

          then

           A3: <|x1,?> = <|x2,?> by XTUPLE_0: 3;

          

           A4: x1 in ( Hom (o1,o2)) by A1, CAT_1:def 5;

          

          then

           A5: ( dom x1) = o1 by CAT_1: 1

          .= ( dom x2) by A2, CAT_1: 1;

          ( cod x1) = o2 by A4, CAT_1: 1

          .= ( cod x2) by A2, CAT_1: 1;

          then [ [( Hom (( cod x1),o2)), ( Hom (( dom x1),o2))], ( hom (x1,( id o2)))] = ( <|x2,?> . o2) by A5, A3, Def3;

          then [ [( Hom (( cod x1),o2)), ( Hom (( dom x1),o2))], ( hom (x1,( id o2)))] = [ [( Hom (( cod x2),o2)), ( Hom (( dom x2),o2))], ( hom (x2,( id o2)))] by Def3;

          then [ [( Hom (o2,o2)), ( Hom (( dom x1),o2))], ( hom (x1,( id o2)))] = [ [( Hom (( cod x2),o2)), ( Hom (( dom x2),o2))], ( hom (x2,( id o2)))] by A4, CAT_1: 1;

          then [ [( Hom (o2,o2)), ( Hom (o1,o2))], ( hom (x1,( id o2)))] = [ [( Hom (( cod x2),o2)), ( Hom (( dom x2),o2))], ( hom (x2,( id o2)))] by A4, CAT_1: 1;

          then [ [( Hom (o2,o2)), ( Hom (o1,o2))], ( hom (x1,( id o2)))] = [ [( Hom (o2,o2)), ( Hom (( dom x2),o2))], ( hom (x2,( id o2)))] by A2, CAT_1: 1;

          then [ [( Hom (o2,o2)), ( Hom (o1,o2))], ( hom (x1,( id o2)))] = [ [( Hom (o2,o2)), ( Hom (o1,o2))], ( hom (x2,( id o2)))] by A2, CAT_1: 1;

          then [ [( Hom (o2,o2)), ( Hom (o1,o2))], ( hom (x1,( id o2)))] = [( Hom (o2,o2)), ( Hom (o1,o2)), ( hom (x2,( id o2)))];

          then

           A6: [( Hom (o2,o2)), ( Hom (o1,o2)), ( hom (x1,( id o2)))] = [( Hom (o2,o2)), ( Hom (o1,o2)), ( hom (x2,( id o2)))];

          reconsider dd = ( id o2) as Morphism of A;

          

           A7: ( Hom (o2,o2)) <> {} ;

          then

           A8: (( id o2) (*) dd) = (( id o2) * ( id o2)) by CAT_1:def 13;

          ( id o2) in ( Hom (o2,o2)) by CAT_1: 27;

          then ( id o2) in ( Hom (( cod x2),o2)) by A2, CAT_1: 1;

          then ( id o2) in ( Hom (( cod x2),( dom ( id o2))));

          

          then

           A9: (( hom (x2,( id o2))) . dd) = ((( id o2) * ( id o2)) (*) x2 qua Morphism of A) by A8, ENS_1:def 23

          .= (( id o2) (*) x2 qua Morphism of A)

          .= (( id o2) * x2) by A1, A7, CAT_1:def 13

          .= x2 by A1, CAT_1: 28;

          ( id o2) in ( Hom (o2,o2)) by CAT_1: 27;

          then ( id o2) in ( Hom (( cod x1),o2)) by A4, CAT_1: 1;

          then ( id o2) in ( Hom (( cod x1),( dom ( id o2))));

          

          then (( hom (x1,( id o2))) . dd) = ((( id o2) * ( id o2)) (*) x1 qua Morphism of A) by A8, ENS_1:def 23

          .= (( id o2) (*) x1 qua Morphism of A)

          .= (( id o2) * x1) by A1, A7, CAT_1:def 13

          .= x1 by A1, CAT_1: 28;

          hence thesis by A9, A6, XTUPLE_0: 3;

        end;

        hence thesis;

      end;

    end

    registration

      let A;

      cluster ( Yoneda A) -> one-to-one;

      coherence

      proof

        set F = ( Yoneda A);

        for x1,x2 be object st x1 in ( dom ( Obj F)) & x2 in ( dom ( Obj F)) & (( Obj F) . x1) = (( Obj F) . x2) holds x1 = x2

        proof

          let x1,x2 be object;

          assume that

           A1: x1 in ( dom ( Obj F)) & x2 in ( dom ( Obj F)) and

           A2: (( Obj F) . x1) = (( Obj F) . x2);

          reconsider c = x1, c1 = x2 as Object of A by A1, FUNCT_2:def 1;

          reconsider f = ( id c1) as Morphism of c1, c1;

           <|c1,?> in ( Funct (A,( EnsHom A))) by CAT_2:def 2;

          then

          reconsider d1 = <|c1,?> as Object of ( Functors (A,( EnsHom A))) by NATTRA_1:def 17;

           <|c,?> in ( Funct (A,( EnsHom A))) by CAT_2:def 2;

          then

          reconsider d = <|c,?> as Object of ( Functors (A,( EnsHom A))) by NATTRA_1:def 17;

          (F . ( id c1)) = ( id d1)

          proof

            set X = ( dom <|( id c1),?>);

            

             A3: for y be object st y in X holds ( <|( id c1),?> . y) = (( id <|c1,?>) . y)

            proof

              let y be object;

              assume y in X;

              then

              reconsider z = y as Object of A by FUNCT_2:def 1;

              reconsider zz = ( id z) as Morphism of z, z;

              

               A4: ( Hom (z,z)) <> {} ;

              ( <|( id c1),?> . z) = [ [( Hom (( cod ( id c1)),z)), ( Hom (( dom ( id c1)),z))], ( hom (( id c1),( id z)))] by Def3

              .= [ [( Hom (c1,z)), ( Hom (( dom ( id c1)),z))], ( hom (( id c1),( id z)))]

              .= [ [( Hom (c1,z)), ( Hom (c1,z))], ( hom (( id c1),( id z)))]

              .= [ [( Hom (c1,z)), ( Hom (c1,z))], ( hom (c1,( id z)))] by ENS_1: 53

              .= [ [( Hom (c1,z)), ( Hom (c1,( cod ( id z))))], ( hom (c1,( id z)))]

              .= [ [( Hom (c1,( dom ( id z)))), ( Hom (c1,( cod ( id z))))], ( hom (c1,( id z)))]

              .= ( <|c1,?> qua Function . ( id z)) by ENS_1:def 21

              .= ( <|c1,?> /. zz) by A4, CAT_3:def 10

              .= ( id ( <|c1,?> . z)) by NATTRA_1: 15

              .= (( id <|c1,?>) . z) by NATTRA_1: 20

              .= (( id <|c1,?>) qua Function . z) by NATTRA_1:def 5;

              hence thesis by NATTRA_1:def 5;

            end;

            ( dom <|( id c1),?>) = the carrier of A by FUNCT_2:def 1

            .= ( dom ( id <|c1,?>)) by FUNCT_2:def 1;

            then

             A5: <|( id c1),?> = ( id <|c1,?>) by A3, FUNCT_1: 2;

            (F . ( id c1)) = [ [ <|( cod ( id c1)),?>, <|( dom ( id c1)),?>], <|( id c1),?>] by Def4

            .= [ [ <|c1,?>, <|( dom ( id c1)),?>], <|( id c1),?>]

            .= [ [ <|c1,?>, <|c1,?>], ( id <|c1,?>)] by A5

            .= ( id d1) by NATTRA_1:def 17;

            hence thesis;

          end;

          then

           A6: (( Obj F) . c1) = d1 by OPPCAT_1: 30;

          (F . ( id c)) = ( id d)

          proof

            set X = ( dom <|( id c),?>);

            

             A7: for y be object st y in X holds ( <|( id c),?> . y) = (( id <|c,?>) . y)

            proof

              let y be object;

              assume y in X;

              then

              reconsider z = y as Object of A by FUNCT_2:def 1;

              reconsider zz = ( id z) as Morphism of z, z;

              

               A8: ( Hom (z,z)) <> {} ;

              ( <|( id c),?> . z) = [ [( Hom (( cod ( id c)),z)), ( Hom (( dom ( id c)),z))], ( hom (( id c),( id z)))] by Def3

              .= [ [( Hom (c,z)), ( Hom (( dom ( id c)),z))], ( hom (( id c),( id z)))]

              .= [ [( Hom (c,z)), ( Hom (c,z))], ( hom (( id c),( id z)))]

              .= [ [( Hom (c,z)), ( Hom (c,z))], ( hom (c,( id z)))] by ENS_1: 53

              .= [ [( Hom (c,z)), ( Hom (c,( cod ( id z))))], ( hom (c,( id z)))]

              .= [ [( Hom (c,( dom ( id z)))), ( Hom (c,( cod ( id z))))], ( hom (c,( id z)))]

              .= ( <|c,?> qua Function . ( id z)) by ENS_1:def 21

              .= ( <|c,?> /. zz) by A8, CAT_3:def 10

              .= ( id ( <|c,?> . z)) by NATTRA_1: 15

              .= (( id <|c,?>) . z) by NATTRA_1: 20

              .= (( id <|c,?>) qua Function . z) by NATTRA_1:def 5;

              hence thesis by NATTRA_1:def 5;

            end;

            ( dom <|( id c),?>) = the carrier of A by FUNCT_2:def 1

            .= ( dom ( id <|c,?>)) by FUNCT_2:def 1;

            then

             A9: <|( id c),?> = ( id <|c,?>) by A7, FUNCT_1: 2;

            (F . ( id c)) = [ [ <|( cod ( id c)),?>, <|( dom ( id c)),?>], <|( id c),?>] by Def4

            .= [ [ <|c,?>, <|( dom ( id c)),?>], <|( id c),?>]

            .= [ [ <|c,?>, <|c,?>], ( id <|c,?>)] by A9

            .= ( id d) by NATTRA_1:def 17;

            hence thesis;

          end;

          then (( Obj F) . c) = d by OPPCAT_1: 30;

          then [ [( Hom (c,( dom f))), ( Hom (c,( cod f)))], ( hom (c,f))] = (( hom?- c1) . f) by A2, A6, ENS_1:def 21;

          then [ [( Hom (c,( dom f))), ( Hom (c,( cod f)))], ( hom (c,f))] = [ [( Hom (c1,( dom f))), ( Hom (c1,( cod f)))], ( hom (c1,f))] by ENS_1:def 21;

          then [( Hom (c,( dom f))), ( Hom (c,( cod f))), ( hom (c,f))] = [ [( Hom (c1,( dom f))), ( Hom (c1,( cod f)))], ( hom (c1,f))];

          then [( Hom (c,( dom f))), ( Hom (c,( cod f))), ( hom (c,f))] = [( Hom (c1,( dom f))), ( Hom (c1,( cod f))), ( hom (c1,f))];

          then ( Hom (c,( dom f))) = ( Hom (c1,( dom f))) by XTUPLE_0: 3;

          then ( Hom (c,( dom f))) = ( Hom (c1,c1));

          then

           A10: ( Hom (c,c1)) = ( Hom (c1,c1));

          ( id c1) in ( Hom (c1,c1)) by CAT_1: 27;

          then

          reconsider h = ( id c1) as Morphism of c, c1 by A10, CAT_1:def 5;

          ( dom h) = c by A10, CAT_1: 5;

          hence thesis;

        end;

        then ( Obj F) is one-to-one by FUNCT_1:def 4;

        hence thesis by Th5;

      end;

    end

    definition

      let C,D be Category;

      let T be Contravariant_Functor of C, D;

      :: YONEDA_1:def7

      attr T is full means for c,c9 be Object of C st ( Hom ((T . c9),(T . c))) <> {} holds for g be Morphism of (T . c9), (T . c) holds ( Hom (c,c9)) <> {} & ex f be Morphism of c, c9 st g = (T . f);

    end

    registration

      let A;

      ::$Notion-Name

      cluster ( Yoneda A) -> full;

      coherence

      proof

        set F = ( Yoneda A);

        for c,c9 be Object of A st ( Hom ((F . c9),(F . c))) <> {} holds for g be Morphism of (F . c9), (F . c) holds ( Hom (c,c9)) <> {} & ex f be Morphism of c, c9 st g = (F . f)

        proof

          let c,c9 be Object of A;

          assume

           A1: ( Hom ((F . c9),(F . c))) <> {} ;

          

           A2: ( <|c9,?> . c9) = (( hom?- (( Hom A),c9)) . c9) by ENS_1:def 25

          .= (( Obj ( hom?- (( Hom A),c9))) . c9)

          .= ( Hom (c9,c9)) by ENS_1: 60;

          let g be Morphism of (F . c9), (F . c);

          g in the carrier' of ( Functors (A,( EnsHom A)));

          then g in ( NatTrans (A,( EnsHom A))) by NATTRA_1:def 17;

          then

          consider F1,F2 be Functor of A, ( EnsHom A), t be natural_transformation of F1, F2 such that

           A3: g = [ [F1, F2], t] and

           A4: F1 is_naturally_transformable_to F2 by NATTRA_1:def 16;

          

           A5: ( dom g) = F1 by A3, NATTRA_1: 33;

           <|c9,?> in ( Funct (A,( EnsHom A))) by CAT_2:def 2;

          then

          reconsider d1 = <|c9,?> as Object of ( Functors (A,( EnsHom A))) by NATTRA_1:def 17;

           <|c,?> in ( Funct (A,( EnsHom A))) by CAT_2:def 2;

          then

          reconsider d = <|c,?> as Object of ( Functors (A,( EnsHom A))) by NATTRA_1:def 17;

          

           A6: (F . ( id c)) = ( id d)

          proof

            set X = ( dom <|( id c),?>);

            

             A7: for y be object st y in X holds ( <|( id c),?> . y) = (( id <|c,?>) . y)

            proof

              let y be object;

              assume y in X;

              then

              reconsider z = y as Object of A by FUNCT_2:def 1;

              reconsider zz = ( id z) as Morphism of z, z;

              

               A8: ( Hom (z,z)) <> {} ;

              ( <|( id c),?> . z) = [ [( Hom (( cod ( id c)),z)), ( Hom (( dom ( id c)),z))], ( hom (( id c),( id z)))] by Def3

              .= [ [( Hom (c,z)), ( Hom (( dom ( id c)),z))], ( hom (( id c),( id z)))]

              .= [ [( Hom (c,z)), ( Hom (c,z))], ( hom (( id c),( id z)))]

              .= [ [( Hom (c,z)), ( Hom (c,z))], ( hom (c,( id z)))] by ENS_1: 53

              .= [ [( Hom (c,z)), ( Hom (c,( cod ( id z))))], ( hom (c,( id z)))]

              .= [ [( Hom (c,( dom ( id z)))), ( Hom (c,( cod ( id z))))], ( hom (c,( id z)))]

              .= ( <|c,?> qua Function . ( id z)) by ENS_1:def 21

              .= ( <|c,?> /. zz) by A8, CAT_3:def 10

              .= ( id ( <|c,?> . z)) by NATTRA_1: 15

              .= (( id <|c,?>) . z) by NATTRA_1: 20

              .= (( id <|c,?>) qua Function . z) by NATTRA_1:def 5;

              hence thesis by NATTRA_1:def 5;

            end;

            ( dom <|( id c),?>) = the carrier of A by FUNCT_2:def 1

            .= ( dom ( id <|c,?>)) by FUNCT_2:def 1;

            then

             A9: <|( id c),?> = ( id <|c,?>) by A7, FUNCT_1: 2;

            (F . ( id c)) = [ [ <|( cod ( id c)),?>, <|( dom ( id c)),?>], <|( id c),?>] by Def4

            .= [ [ <|c,?>, <|( dom ( id c)),?>], <|( id c),?>]

            .= [ [ <|c,?>, <|c,?>], ( id <|c,?>)] by A9

            .= ( id d) by NATTRA_1:def 17;

            hence thesis;

          end;

          then

           A10: (F . c) = d by OPPCAT_1: 30;

          

           A11: (F . ( id c9)) = ( id d1)

          proof

            set X = ( dom <|( id c9),?>);

            

             A12: for y be object st y in X holds ( <|( id c9),?> . y) = (( id <|c9,?>) . y)

            proof

              let y be object;

              assume y in X;

              then

              reconsider z = y as Object of A by FUNCT_2:def 1;

              reconsider zz = ( id z) as Morphism of z, z;

              

               A13: ( Hom (z,z)) <> {} ;

              ( <|( id c9),?> . z) = [ [( Hom (( cod ( id c9)),z)), ( Hom (( dom ( id c9)),z))], ( hom (( id c9),( id z)))] by Def3

              .= [ [( Hom (c9,z)), ( Hom (( dom ( id c9)),z))], ( hom (( id c9),( id z)))]

              .= [ [( Hom (c9,z)), ( Hom (c9,z))], ( hom (( id c9),( id z)))]

              .= [ [( Hom (c9,z)), ( Hom (c9,z))], ( hom (c9,( id z)))] by ENS_1: 53

              .= [ [( Hom (c9,z)), ( Hom (c9,( cod ( id z))))], ( hom (c9,( id z)))]

              .= [ [( Hom (c9,( dom ( id z)))), ( Hom (c9,( cod ( id z))))], ( hom (c9,( id z)))]

              .= ( <|c9,?> qua Function . ( id z)) by ENS_1:def 21

              .= ( <|c9,?> /. zz) by A13, CAT_3:def 10

              .= ( id ( <|c9,?> . z)) by NATTRA_1: 15

              .= (( id <|c9,?>) . z) by NATTRA_1: 20

              .= (( id <|c9,?>) qua Function . z) by NATTRA_1:def 5;

              hence thesis by NATTRA_1:def 5;

            end;

            ( dom <|( id c9),?>) = the carrier of A by FUNCT_2:def 1

            .= ( dom ( id <|c9,?>)) by FUNCT_2:def 1;

            then

             A14: <|( id c9),?> = ( id <|c9,?>) by A12, FUNCT_1: 2;

            (F . ( id c9)) = [ [ <|( cod ( id c9)),?>, <|( dom ( id c9)),?>], <|( id c9),?>] by Def4

            .= [ [ <|c9,?>, <|( dom ( id c9)),?>], <|( id c9),?>]

            .= [ [ <|c9,?>, <|c9,?>], ( id <|c9,?>)] by A14

            .= ( id d1) by NATTRA_1:def 17;

            hence thesis;

          end;

          then

           A15: (( Obj F) . c9) = d1 by OPPCAT_1: 30;

          

           A16: ( cod g) = F2 by A3, NATTRA_1: 33;

          then

           A17: F2 = (F . c) by A1, CAT_1: 5;

          

           A18: (F . c9) = d1 by A11, OPPCAT_1: 30;

          

           A19: ( <|c,?> . c9) = (( hom?- (( Hom A),c)) . c9) by ENS_1:def 25

          .= (( Obj ( hom?- (( Hom A),c))) . c9)

          .= ( Hom (c,c9)) by ENS_1: 60;

          

           A20: ( dom g) = (F . c9) & ( cod g) = (F . c) by A1, CAT_1: 5;

          then

          reconsider t as natural_transformation of <|c9,?>, <|c,?> by A5, A16, A11, A10, OPPCAT_1: 30;

          (( Obj F) . c) = d by A6, OPPCAT_1: 30;

          then <|c9,?> is_transformable_to <|c,?> by A4, A5, A16, A20, A18, NATTRA_1:def 7;

          then ( Hom (( <|c9,?> . c9),( <|c,?> . c9))) <> {} by NATTRA_1:def 2;

          then

           A21: (t . c9) in ( Hom (( <|c9,?> . c9),( <|c,?> . c9))) by CAT_1:def 5;

          then

           A22: ( cod (t . c9)) = ( <|c,?> . c9) by CAT_1: 1;

          

           A23: ( EnsHom A) = CatStr (# ( Hom A), ( Maps ( Hom A)), ( fDom ( Hom A)), ( fCod ( Hom A)), ( fComp ( Hom A)) #) by ENS_1:def 13;

          then

          reconsider t1 = (t . c9) as Element of ( Maps ( Hom A));

          

           A24: ( cod (t . c9)) = (( fCod ( Hom A)) . (t . c9)) by A23

          .= ( cod t1) by ENS_1:def 10;

          t1 in ( Maps (( dom t1),( cod t1))) by ENS_1: 19;

          then

           A25: (t1 `2 ) in ( Funcs (( dom t1),( cod t1))) by ENS_1: 20;

          

           A26: ( dom (t . c9)) = ( <|c9,?> . c9) by A21, CAT_1: 1;

          then (the Source of ( EnsHom A) . (t . c9)) <> {} by A2;

          then ( dom t1) <> {} by A23, ENS_1:def 9;

          then

           A27: ( cod t1) <> {} by A25;

          then

           A28: ( cod (t . c9)) <> {} by A23, ENS_1:def 10;

          hence ( Hom (c,c9)) <> {} by A19, A21, CAT_1: 1;

          ( dom (t . c9)) = (( fDom ( Hom A)) . (t . c9)) by A23

          .= ( dom t1) by ENS_1:def 9;

          then

           A29: (t1 `2 ) is Function of ( <|c9,?> . c9), ( <|c,?> . c9) by A26, A22, A25, A24, FUNCT_2: 66;

          then

           A30: ( dom (t1 `2 )) = ( Hom (c9,c9)) by A2, A22, A28, FUNCT_2:def 1;

          then ( id c9) in ( dom (t1 `2 )) by CAT_1: 27;

          then

           A31: ((t1 `2 ) . ( id c9)) in ( rng (t1 `2 )) by FUNCT_1:def 3;

          ( rng (t1 `2 )) c= ( Hom (c,c9)) by A19, A29, RELAT_1:def 19;

          then ((t1 `2 ) . ( id c9)) in ( Hom (c,c9)) by A31;

          then

          reconsider f = ((t1 `2 ) . ( id c9)) as Morphism of c, c9 by CAT_1:def 5;

          

           A32: ( <|c,?> . c9) <> {} by A22, A23, A27, ENS_1:def 10;

          then

           A33: ( dom f) = c by A19, CAT_1: 5;

          take f;

          

           A34: ( cod f) = c9 by A19, A32, CAT_1: 5;

          

           A35: F1 = (F . c9) by A1, A5, CAT_1: 5;

          then

           A36: <|c9,?> is_transformable_to <|c,?> by A4, A17, A15, A10, NATTRA_1:def 7;

          for a be Object of A holds ( <|f,?> . a) = (t . a)

          proof

            let a be Object of A;

            

             A37: ( <|c,?> . a) = (( hom?- (( Hom A),c)) . a) by ENS_1:def 25

            .= (( Obj ( hom?- (( Hom A),c))) . a)

            .= ( Hom (c,a)) by ENS_1: 60;

            reconsider ta1 = (t . a) as Element of ( Maps ( Hom A)) by A23;

            

             A38: ( <|c9,?> . a) = (( hom?- (( Hom A),c9)) . a) by ENS_1:def 25

            .= (( Obj ( hom?- (( Hom A),c9))) . a)

            .= ( Hom (c9,a)) by ENS_1: 60;

            ta1 in ( Maps (( dom ta1),( cod ta1))) by ENS_1: 19;

            then

             A39: (ta1 `2 ) in ( Funcs (( dom ta1),( cod ta1))) by ENS_1: 20;

            then

             A40: (ta1 `2 ) is Function of ( dom ta1), ( cod ta1) by FUNCT_2: 66;

            set X = ( dom (ta1 `2 ));

            

             A41: ( dom (t . a)) = (( fDom ( Hom A)) . (t . a)) by A23

            .= ( dom ta1) by ENS_1:def 9;

            

             A42: ( Hom (( <|c9,?> . a),( <|c,?> . a))) <> {} by A36, NATTRA_1:def 2;

            then

             A43: ( dom (t . a)) = ( <|c9,?> . a) by CAT_1: 5;

            

             A44: ( cod (t . a)) = ( <|c,?> . a) by A42, CAT_1: 5;

            

             A45: ( cod (t . a)) = (( fCod ( Hom A)) . (t . a)) by A23

            .= ( cod ta1) by ENS_1:def 10;

            then

             A46: ta1 = [ [( <|c9,?> . a), ( <|c,?> . a)], (ta1 `2 )] by A43, A44, A41, ENS_1: 8;

            

             A47: (ta1 `2 ) is Function of ( dom (t . a)), ( cod (t . a)) by A41, A45, A39, FUNCT_2: 66;

            

             A48: ( dom (ta1 `2 )) = ( Hom (c9,a))

            proof

              per cases ;

                suppose ( Hom (c9,a)) = {} ;

                hence thesis by A43, A41, A38, A40;

              end;

                suppose ( Hom (c9,a)) <> {} ;

                then ( Hom (( dom f),a)) <> {} by A34, ENS_1: 42;

                hence thesis by A33, A43, A44, A38, A37, A47, FUNCT_2:def 1;

              end;

            end;

            

             A49: for x be object st x in X holds (( hom (f,( id a))) . x) = ((ta1 `2 ) . x)

            proof

              reconsider t1 = (t . c9) as Element of ( Maps ( Hom A)) by A23;

              let x be object;

              

               A50: f in ( Hom (c,( cod f))) by A33;

              assume

               A51: x in X;

              then

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

              reconsider h = y as Morphism of c9, a by A19, A22, A28, CAT_1: 5;

              

               A52: ( dom h) = c9 by A48, A51, CAT_1: 5;

              reconsider tc9 = ( <|c9,?> . h) as Element of ( Maps ( Hom A)) by A23;

              

               A53: ( cod h) = a by A48, A51, CAT_1: 5;

              reconsider tch = ( <|c,?> . h) as Element of ( Maps ( Hom A)) by A23;

              

               A54: [ [( Hom (c,( dom h))), ( Hom (c,( cod h)))], ( hom (c,h))] = ( <|c,?> qua Function . h) by ENS_1:def 21

              .= ( <|c,?> . h);

              

               A55: [ [( Hom (c9,( dom h))), ( Hom (c9,( cod h)))], ( hom (c9,h))] = ( <|c9,?> qua Function . h) by ENS_1:def 21

              .= ( <|c9,?> . h);

              

               A56: ( cod ( <|c9,?> . h)) = (( fCod ( Hom A)) . ( <|c9,?> . h)) by A23

              .= ( cod tc9) by ENS_1:def 10;

              

              then

               A57: ( cod ( <|c9,?> . h)) = ((tc9 `1 ) `2 ) by ENS_1:def 4

              .= ( [( Hom (c9,( dom h))), ( Hom (c9,( cod h)))] `2 ) by A55

              .= ( Hom (c9,( cod h)));

              then

               A58: [(t . a), ( <|c9,?> . h)] in ( dom the Comp of ( EnsHom A)) by A43, A38, A53, CAT_1: 15;

              tc9 in ( Maps (( dom tc9),( cod tc9))) by ENS_1: 19;

              then

               A59: (tc9 `2 ) in ( Funcs (( dom tc9),( cod tc9))) by ENS_1: 20;

              

               A60: ( dom ( <|c9,?> . h)) = (( fDom ( Hom A)) . ( <|c9,?> . h)) by A23

              .= ( dom tc9) by ENS_1:def 9;

              

              then ( dom ( <|c9,?> . h)) = ((tc9 `1 ) `1 ) by ENS_1:def 3

              .= ( [( Hom (c9,( dom h))), ( Hom (c9,( cod h)))] `1 ) by A55

              .= ( Hom (c9,( dom h)));

              then (tc9 `2 ) is Function of ( Hom (c9,( dom h))), ( Hom (c9,( cod h))) by A60, A56, A57, A59, FUNCT_2: 66;

              then

               A61: ( dom (tc9 `2 )) = ( Hom (c9,c9)) by A48, A51, A52, A53, FUNCT_2:def 1;

              

               A62: ( dom y) = ( cod f) by A34, A48, A51, CAT_1: 5;

              tch = [ [( dom tch), ( cod tch)], (tch `2 )] by ENS_1: 8;

              then [( Hom (c,( dom h))), ( Hom (c,( cod h))), ( hom (c,h))] = [ [( dom tch), ( cod tch)], (tch `2 )] by A54;

              then [( Hom (c,( dom h))), ( Hom (c,( cod h))), ( hom (c,h))] = [( dom tch), ( cod tch), (tch `2 )];

              then

               A63: ( hom (c,h)) = (tch `2 ) by XTUPLE_0: 3;

              tc9 = [ [( dom tc9), ( cod tc9)], (tc9 `2 )] by ENS_1: 8;

              then [( dom tc9), ( cod tc9), (tc9 `2 )] = [ [( Hom (c9,( dom h))), ( Hom (c9,( cod h)))], ( hom (c9,h))] by A55;

              then [( dom tc9), ( cod tc9), (tc9 `2 )] = [( Hom (c9,( dom h))), ( Hom (c9,( cod h))), ( hom (c9,h))];

              then

               A64: (tc9 `2 ) = ( hom (c9,h)) by XTUPLE_0: 3;

              

               A65: ( Hom (( <|c9,?> . c9),( <|c,?> . c9))) <> {} by A36, NATTRA_1:def 2;

              then (t . c9) in ( Hom (( <|c9,?> . c9),( <|c,?> . c9))) by CAT_1:def 5;

              then

               A66: ( cod (t . c9)) = ( <|c,?> . c9) by CAT_1: 1;

              ( dom ( <|c,?> . h)) = (( fDom ( Hom A)) . ( <|c,?> . h)) by A23

              .= ( dom tch) by ENS_1:def 9;

              

              then ( dom ( <|c,?> . h)) = ((tch `1 ) `1 ) by ENS_1:def 3

              .= ( [( Hom (c,( dom h))), ( Hom (c,( cod h)))] `1 ) by A54

              .= ( Hom (c,( dom h)));

              then

               A67: [( <|c,?> . h), (t . c9)] in ( dom the Comp of ( EnsHom A)) by A19, A52, A66, CAT_1: 15;

              ( cod (t . c9)) = (( fCod ( Hom A)) . (t . c9)) by A23

              .= ( cod t1) by ENS_1:def 10;

              

              then

               A68: ( cod t1) = ( [( Hom (c,( dom h))), ( Hom (c,( cod h)))] `1 ) by A19, A52, A66

              .= ((tch `1 ) `1 ) by A54

              .= ( dom tch) by ENS_1:def 3;

              

               A69: h in ( Hom (c9,a)) by A48, A51;

              then

               A70: ( <|c,?> /. h) = ( <|c,?> . h) by CAT_3:def 10;

              ( Hom (( <|c,?> . c9),( <|c,?> . a))) <> {} by A48, A51, CAT_1: 84;

              

              then

               A71: (( <|c,?> /. h) * (t . c9)) = (( <|c,?> . h) (*) (t . c9) qua Morphism of ( EnsHom A)) by A65, A70, CAT_1:def 13

              .= (( fComp ( Hom A)) . (tch,t1)) by A23, A67, CAT_1:def 1

              .= (tch * t1) by A68, ENS_1:def 11

              .= [ [( dom t1), ( cod tch)], ((tch `2 ) * (t1 `2 ))] by A68, ENS_1:def 6;

              

               A72: ( cod tc9) = ((tc9 `1 ) `2 ) by ENS_1:def 4

              .= ( [( Hom (c9,( dom h))), ( Hom (c9,( cod h)))] `2 ) by A55

              .= ( dom ta1) by A43, A41, A38, A53;

              

               A73: ( <|c9,?> /. h) = ( <|c9,?> . h) by A69, CAT_3:def 10;

              ( Hom (( <|c9,?> . c9),( <|c9,?> . a))) <> {} by A48, A51, CAT_1: 84;

              

              then

               A74: ((t . a) * ( <|c9,?> /. h)) = ((t . a) qua Morphism of ( EnsHom A) (*) ( <|c9,?> . h)) by A42, A73, CAT_1:def 13

              .= (( fComp ( Hom A)) . (ta1,tc9)) by A23, A58, CAT_1:def 1

              .= (ta1 * tc9) by A72, ENS_1:def 11

              .= [ [( dom tc9), ( cod ta1)], ((ta1 `2 ) * (tc9 `2 ))] by A72, ENS_1:def 6;

              ((t . a) * ( <|c9,?> /. h)) = (( <|c,?> /. h) * (t . c9)) by A4, A35, A17, A15, A10, A48, A51, NATTRA_1:def 8;

              then [( dom tc9), ( cod ta1), ((ta1 `2 ) * (tc9 `2 ))] = [ [( dom t1), ( cod tch)], ((tch `2 ) * (t1 `2 ))] by A74, A71;

              then [( dom tc9), ( cod ta1), ((ta1 `2 ) * (tc9 `2 ))] = [( dom t1), ( cod tch), ((tch `2 ) * (t1 `2 ))];

              then

               A75: ((ta1 `2 ) * (tc9 `2 )) = ((tch `2 ) * (t1 `2 )) by XTUPLE_0: 3;

              

               A76: ( id c9) in ( Hom (c9,( cod f))) by A34, CAT_1: 27;

              (( hom (f,( id a))) . x) = (( hom (f,a)) . y) by ENS_1: 53

              .= (y (*) f) by A34, A48, A51, ENS_1:def 20

              .= ((tch `2 ) . ((t1 `2 ) . ( id c9))) by A62, A63, A50, ENS_1:def 19

              .= (((ta1 `2 ) * (tc9 `2 )) . ( id c9)) by A30, A75, CAT_1: 27, FUNCT_1: 13

              .= ((ta1 `2 ) . (( hom (c9,h)) . ( id c9))) by A64, A61, CAT_1: 27, FUNCT_1: 13

              .= ((ta1 `2 ) . (y (*) ( id c9))) by A62, A76, ENS_1:def 19

              .= ((ta1 `2 ) . x) by A34, A62, CAT_1: 22;

              hence thesis;

            end;

            ( dom ( hom (f,a))) = ( Hom (( cod f),a))

            proof

              per cases ;

                suppose ( Hom (( cod f),a)) = {} ;

                hence thesis;

              end;

                suppose ( Hom (( cod f),a)) <> {} ;

                then ( Hom (c,a)) <> {} by A33, ENS_1: 42;

                hence thesis by A33, FUNCT_2:def 1;

              end;

            end;

            then ( dom (ta1 `2 )) = ( dom ( hom (f,( id a)))) by A34, A48, ENS_1: 53;

            then ( hom (f,( id a))) = (ta1 `2 ) by A49, FUNCT_1: 2;

            hence thesis by A33, A34, A38, A37, A46, Def3;

          end;

          then <|f,?> = t by A4, A35, A17, A15, A10, A33, A34, ISOCAT_1: 26;

          hence thesis by A3, A5, A16, A20, A15, A10, A33, A34, Def4;

        end;

        hence thesis;

      end;

    end