let A be Category; :: thesis: for f being Morphism of A holds <|(cod f),?> is_naturally_transformable_to <|(dom f),?>

let f be Morphism of A; :: thesis: <|(cod f),?> is_naturally_transformable_to <|(dom f),?>

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

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

set B = EnsHom A;

deffunc H_{1}( Element of A) -> object = [[(Hom ((cod f),$1)),(Hom ((dom f),$1))],(hom (f,$1))];

A1: 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))_{1}(a) in the carrier' of (EnsHom A)

A5: for o being Element of A holds t . o = H_{1}(o)
from FUNCT_2:sch 8(A4);

A6: for a being Object of A holds t . a is Morphism of <|(cod f),?> . a,<|(dom f),?> . a

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

then reconsider t = t as transformation of <|(cod f),?>,<|(dom f),?> by A6, NATTRA_1:def 3;

for a, b being Object of A st Hom (a,b) <> {} holds

for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a)

let f be Morphism of A; :: thesis: <|(cod f),?> is_naturally_transformable_to <|(dom f),?>

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

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

set B = EnsHom A;

deffunc H

A1: 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

A4:
for a being Element of A holds H
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))

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

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

.= <|(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 A3; :: thesis: verum

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

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

.= <|(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 A3; :: thesis: verum

proof

consider t being Function of the carrier of A, the carrier' of (EnsHom A) such that
let a be Object of A; :: thesis: H_{1}(a) in the carrier' of (EnsHom A)

[[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) by A1;

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

end;[[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) by A1;

hence H

A5: for o being Element of A holds t . o = H

A6: for a being Object of A holds t . a is Morphism of <|(cod f),?> . a,<|(dom f),?> . a

proof

for a being Object of A holds Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) <> {}
by A1;
let a be Object of A; :: thesis: t . a is Morphism of <|(cod f),?> . a,<|(dom f),?> . a

[[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) by A1;

then [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] is Morphism of <|(cod f),?> . a,<|(dom f),?> . a by CAT_1:def 5;

hence t . a is Morphism of <|(cod f),?> . a,<|(dom f),?> . a by A5; :: thesis: verum

end;[[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] in Hom ((<|(cod f),?> . a),(<|(dom f),?> . a)) by A1;

then [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] is Morphism of <|(cod f),?> . a,<|(dom f),?> . a by CAT_1:def 5;

hence t . a is Morphism of <|(cod f),?> . a,<|(dom f),?> . a by A5; :: thesis: verum

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

then reconsider t = t as transformation of <|(cod f),?>,<|(dom f),?> by A6, NATTRA_1:def 3;

for a, b being Object of A st Hom (a,b) <> {} holds

for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a)

proof

hence
<|(cod f),?> is_naturally_transformable_to <|(dom f),?>
by A7, NATTRA_1:def 7; :: thesis: verum
let a, b be Object of A; :: thesis: ( Hom (a,b) <> {} implies for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a) )

assume A8: Hom (a,b) <> {} ; :: thesis: for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a)

A9: Hom ((<|(cod f),?> . a),(<|(cod f),?> . b)) <> {} by A8, CAT_1:84;

let g be Morphism of a,b; :: thesis: (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a)

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

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

((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x

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

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

A42: t . a = t . 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 ((<|(cod f),?> . a),(<|(dom f),?> . a)) <> {} by A1;

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

A44: t . b = t . 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 = <|(cod f),?> /. 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 = <|(dom f),?> /. 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 ((<|(cod f),?> . b),(<|(dom f),?> . b)) <> {} by A1;

then (t . b) * (<|(cod f),?> /. 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

.= (<|(dom f),?> /. g) * (t . a) by A40, A43, CAT_1:def 13 ;

hence (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a) ; :: thesis: verum

end;assume A8: Hom (a,b) <> {} ; :: thesis: for g being Morphism of a,b holds (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a)

A9: Hom ((<|(cod f),?> . a),(<|(cod f),?> . b)) <> {} by A8, CAT_1:84;

let g be Morphism of a,b; :: thesis: (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a)

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

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

proof

A16:
rng (hom (f,a)) c= dom (hom ((dom f),g))
A12:
cod g = b
by A8, CAT_1:5;

end;per cases
( Hom ((dom f),b) = {} or Hom ((dom f),b) <> {} )
;

end;

suppose A13:
Hom ((dom f),b) = {}
; :: thesis: rng (hom ((cod f),g)) c= dom (hom (f,b))

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

hence rng (hom ((cod f),g)) c= dom (hom (f,b)) by A12; :: thesis: verum

end;hence rng (hom ((cod f),g)) c= dom (hom (f,b)) by A12; :: thesis: verum

suppose A14:
Hom ((dom f),b) <> {}
; :: thesis: rng (hom ((cod f),g)) c= dom (hom (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 ; :: according to TARSKI:def 3 :: thesis: ( not e in rng (hom ((cod f),g)) or e in dom (hom (f,b)) )

assume e in rng (hom ((cod f),g)) ; :: thesis: e in dom (hom (f,b))

hence e in dom (hom (f,b)) by A15; :: thesis: verum

end;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 ; :: according to TARSKI:def 3 :: thesis: ( not e in rng (hom ((cod f),g)) or e in dom (hom (f,b)) )

assume e in rng (hom ((cod f),g)) ; :: thesis: e in dom (hom (f,b))

hence e in dom (hom (f,b)) by A15; :: thesis: verum

proof

A21:
dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a)))
A17:
dom g = a
by A8, CAT_1:5;

end;per cases
( Hom ((dom f),(cod g)) = {} or Hom ((dom f),(cod g)) <> {} )
;

end;

suppose A18:
Hom ((dom f),(cod g)) = {}
; :: thesis: rng (hom (f,a)) c= dom (hom ((dom f),g))

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

hence rng (hom (f,a)) c= dom (hom ((dom f),g)) by A17; :: thesis: verum

end;hence rng (hom (f,a)) c= dom (hom ((dom f),g)) by A17; :: thesis: verum

suppose A19:
Hom ((dom f),(cod g)) <> {}
; :: thesis: rng (hom (f,a)) c= dom (hom ((dom f),g))

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in rng (hom (f,a)) or e in dom (hom ((dom f),g)) )

assume A20: e in rng (hom (f,a)) ; :: thesis: e in dom (hom ((dom f),g))

( 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 e in dom (hom ((dom f),g)) by A20; :: thesis: verum

end;assume A20: e in rng (hom (f,a)) ; :: thesis: e in dom (hom ((dom f),g))

( 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 e in dom (hom ((dom f),g)) by A20; :: thesis: verum

proof
end;

A26:
for x being object st x in dom ((hom (f,b)) * (hom ((cod f),g))) holds per cases
( Hom ((cod f),(dom g)) = {} or Hom ((cod f),(dom g)) <> {} )
;

end;

suppose A22:
Hom ((cod f),(dom g)) = {}
; :: thesis: dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a)))

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 dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) ; :: thesis: verum

end;.= 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 dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) ; :: thesis: verum

suppose A23:
Hom ((cod f),(dom g)) <> {}
; :: thesis: dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a)))

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 dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) ; :: thesis: verum

end;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 dom ((hom (f,b)) * (hom ((cod f),g))) = dom ((hom ((dom f),g)) * (hom (f,a))) ; :: thesis: verum

((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x

proof

A40:
Hom ((<|(dom f),?> . a),(<|(dom f),?> . b)) <> {}
by A8, CAT_1:84;
let x be object ; :: thesis: ( x in dom ((hom (f,b)) * (hom ((cod f),g))) implies ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x )

assume A27: x in dom ((hom (f,b)) * (hom ((cod f),g))) ; :: thesis: ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x

end;assume A27: x in dom ((hom (f,b)) * (hom ((cod f),g))) ; :: thesis: ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x

per cases
( Hom ((cod f),(dom g)) <> {} or Hom ((cod f),(dom g)) = {} )
;

end;

suppose A28:
Hom ((cod f),(dom g)) <> {}
; :: thesis: ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x

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 = 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 ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x ; :: thesis: verum

end;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 = 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 ((hom (f,b)) * (hom ((cod f),g))) . x = ((hom ((dom f),g)) * (hom (f,a))) . x ; :: thesis: verum

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

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

A42: t . a = t . 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 ((<|(cod f),?> . a),(<|(dom f),?> . a)) <> {} by A1;

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

A44: t . b = t . 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 = <|(cod f),?> /. 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 = <|(dom f),?> /. 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 ((<|(cod f),?> . b),(<|(dom f),?> . b)) <> {} by A1;

then (t . b) * (<|(cod f),?> /. 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

.= (<|(dom f),?> /. g) * (t . a) by A40, A43, CAT_1:def 13 ;

hence (t . b) * (<|(cod f),?> /. g) = (<|(dom f),?> /. g) * (t . a) ; :: thesis: verum