deffunc H_{1}( Element of the carrier' of A) -> object = [[<|(cod $1),?>,<|(dom $1),?>],<|$1,?>];

A1: for f being Element of the carrier' of A holds H_{1}(f) in the carrier' of (Functors (A,(EnsHom A)))

A2: for f being Element of the carrier' of A holds F . f = H_{1}(f)
from FUNCT_2:sch 8(A1);

A3: for f, g being Morphism of A st dom g = cod f holds

F . (g (*) f) = (F . f) (*) (F . g)

( F . (id (dom f)) = id (cod (F . f)) & F . (id (cod f)) = id (dom (F . f)) )

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

hence ex b_{1} being Contravariant_Functor of A, Functors (A,(EnsHom A)) st

for f being Morphism of A holds b_{1} . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>]
; :: thesis: verum

A1: for f being Element of the carrier' of A holds H

proof

consider F being Function of the carrier' of A, the carrier' of (Functors (A,(EnsHom A))) such that
let f be Morphism of A; :: thesis: H_{1}(f) in the carrier' of (Functors (A,(EnsHom A)))

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

hence H_{1}(f) in the carrier' of (Functors (A,(EnsHom A)))
; :: thesis: verum

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

hence H

A2: for f being Element of the carrier' of A holds F . f = H

A3: for f, g being Morphism of A st dom g = cod f holds

F . (g (*) f) = (F . f) (*) (F . g)

proof

A31:
for f being Morphism of A holds
let f, g be Morphism of A; :: thesis: ( dom g = cod f implies F . (g (*) f) = (F . f) (*) (F . g) )

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

assume A4: dom g = cod f ; :: thesis: F . (g (*) f) = (F . f) (*) (F . g)

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 being Object of A holds <|(g (*) f),?> . o = tt . o

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 being Functor of A, EnsHom A, t9 being natural_transformation of F9,F19, t19 being 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 F . (g (*) f) = (F . f) (*) (F . g) by A2, A6, A7, A22; :: thesis: verum

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

assume A4: dom g = cod f ; :: thesis: F . (g (*) f) = (F . f) (*) (F . g)

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 being Object of A holds <|(g (*) f),?> . o = tt . o

proof

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

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

let o be Object of A; :: thesis: <|(g (*) f),?> . o = tt . o

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 being Object of A holds [[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] in Hom ((<|(cod g),?> . a),(<|(dom g),?> . a))

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

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 <|(g (*) f),?> . o = tt . o by A15; :: thesis: verum

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

let o be Object of A; :: thesis: <|(g (*) f),?> . o = tt . o

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 being Object of A holds [[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] in Hom ((<|(cod g),?> . a),(<|(dom g),?> . a))

proof

then A11:
Hom ((<|(cod g),?> . o),(<|(dom g),?> . o)) <> {}
;
let a be Object of A; :: thesis: [[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] in Hom ((<|(cod g),?> . a),(<|(dom g),?> . 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 [[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] in Hom ((<|(cod g),?> . a),(<|(dom g),?> . a)) by A10; :: thesis: verum

end;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 [[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] in Hom ((<|(cod g),?> . a),(<|(dom g),?> . a)) by A10; :: thesis: verum

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

proof

then A14:
Hom ((<|(cod f),?> . o),(<|(dom f),?> . o)) <> {}
;
let a be Object of A; :: thesis: [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . 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

.= <|(dom f),?> . 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

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

hence [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) by A13; :: thesis: verum

end;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

.= <|(dom f),?> . 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

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

hence [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) by A13; :: thesis: verum

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 <|(g (*) f),?> . o = tt . o by A15; :: thesis: verum

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 being Functor of A, EnsHom A, t9 being natural_transformation of F9,F19, t19 being 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 F . (g (*) f) = (F . f) (*) (F . g) by A2, A6, A7, A22; :: thesis: verum

( F . (id (dom f)) = id (cod (F . f)) & F . (id (cod f)) = id (dom (F . f)) )

proof

for c being Object of A ex d being Object of (Functors (A,(EnsHom A))) st F . (id c) = id d
let f be Morphism of A; :: thesis: ( F . (id (dom f)) = id (cod (F . f)) & F . (id (cod f)) = id (dom (F . 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: F . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] by A2;

then cod (F . f) = <|(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 being object st y in dom <|(id (dom f)),?> holds

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

A38: for y being object st y in dom <|(id (cod f)),?> holds

<|(id (cod f)),?> . y = (id <|(cod f),?>) . y

.= 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 (F . f) = <|(cod f),?> by A34, NATTRA_1:33;

hence ( F . (id (dom f)) = id (cod (F . f)) & F . (id (cod f)) = id (dom (F . f)) ) by A33, A35, A32, A36, A41, A40, FUNCT_1:2, NATTRA_1:def 17; :: thesis: verum

end;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: F . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] by A2;

then cod (F . f) = <|(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 being object st y in dom <|(id (dom f)),?> holds

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

proof

set X = dom <|(id (cod f)),?>;
let y be object ; :: thesis: ( y in dom <|(id (dom f)),?> implies <|(id (dom f)),?> . y = (id <|(dom f),?>) . y )

assume y in dom <|(id (dom f)),?> ; :: thesis: <|(id (dom f)),?> . y = (id <|(dom f),?>) . y

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),?> . (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),?>) . z by NATTRA_1:def 5 ;

hence <|(id (dom f)),?> . y = (id <|(dom f),?>) . y by NATTRA_1:def 5; :: thesis: verum

end;assume y in dom <|(id (dom f)),?> ; :: thesis: <|(id (dom f)),?> . y = (id <|(dom f),?>) . y

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),?> . (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),?>) . z by NATTRA_1:def 5 ;

hence <|(id (dom f)),?> . y = (id <|(dom f),?>) . y by NATTRA_1:def 5; :: thesis: verum

A38: for y being object st y in dom <|(id (cod f)),?> holds

<|(id (cod f)),?> . y = (id <|(cod f),?>) . y

proof

dom <|(id (cod f)),?> =
the carrier of A
by FUNCT_2:def 1
let y be object ; :: thesis: ( y in dom <|(id (cod f)),?> implies <|(id (cod f)),?> . y = (id <|(cod f),?>) . y )

assume y in dom <|(id (cod f)),?> ; :: thesis: <|(id (cod f)),?> . y = (id <|(cod f),?>) . y

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),?> . (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),?>) . z by NATTRA_1:def 5 ;

hence <|(id (cod f)),?> . y = (id <|(cod f),?>) . y by NATTRA_1:def 5; :: thesis: verum

end;assume y in dom <|(id (cod f)),?> ; :: thesis: <|(id (cod f)),?> . y = (id <|(cod f),?>) . y

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),?> . (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),?>) . z by NATTRA_1:def 5 ;

hence <|(id (cod f)),?> . y = (id <|(cod f),?>) . y by NATTRA_1:def 5; :: thesis: verum

.= 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 (F . f) = <|(cod f),?> by A34, NATTRA_1:33;

hence ( F . (id (dom f)) = id (cod (F . f)) & F . (id (cod f)) = id (dom (F . f)) ) by A33, A35, A32, A36, A41, A40, FUNCT_1:2, NATTRA_1:def 17; :: thesis: verum

proof

then reconsider F = F as Contravariant_Functor of A, Functors (A,(EnsHom A)) by A31, A3, OPPCAT_1:def 9;
let c be Object of A; :: thesis: ex d being Object of (Functors (A,(EnsHom A))) st F . (id c) = id d

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 ; :: thesis: F . (id c) = id d

A42: for y being object st y in dom <|(id c),?> holds

<|(id c),?> . y = (id <|c,?>) . y

.= 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 F . (id c) = id d ; :: thesis: verum

end;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 ; :: thesis: F . (id c) = id d

A42: for y being object st y in dom <|(id c),?> holds

<|(id c),?> . y = (id <|c,?>) . y

proof

dom <|(id c),?> =
the carrier of A
by FUNCT_2:def 1
let y be object ; :: thesis: ( y in dom <|(id c),?> implies <|(id c),?> . y = (id <|c,?>) . y )

assume y in dom <|(id c),?> ; :: thesis: <|(id c),?> . y = (id <|c,?>) . y

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,?> . (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,?>) . z by NATTRA_1:def 5 ;

hence <|(id c),?> . y = (id <|c,?>) . y by NATTRA_1:def 5; :: thesis: verum

end;assume y in dom <|(id c),?> ; :: thesis: <|(id c),?> . y = (id <|c,?>) . y

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,?> . (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,?>) . z by NATTRA_1:def 5 ;

hence <|(id c),?> . y = (id <|c,?>) . y by NATTRA_1:def 5; :: thesis: verum

.= 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 F . (id c) = id d ; :: thesis: verum

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

hence ex b

for f being Morphism of A holds b