set F1 = <|(cod f),?>;
set F2 = <|(dom f),?>;
A1:
for o being Object of A holds [[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))] in Hom (<|(cod f),?> . o),(<|(dom f),?> . o)
proof
let o be
Object of
A;
:: thesis: [[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))] in Hom (<|(cod f),?> . o),(<|(dom f),?> . o)
A2:
hom f,
(id o) = hom f,
o
by ENS_1:53;
A3:
EnsHom A = CatStr(#
(Hom A),
(Maps (Hom A)),
(fDom (Hom A)),
(fCod (Hom A)),
(fComp (Hom A)),
(fId (Hom A)) #)
by ENS_1:def 14;
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 m' =
m as
Element of
Maps (Hom A) by A2, ENS_1:48;
A4:
dom m =
(fDom (Hom A)) . m
by A3
.=
dom m'
by ENS_1:def 10
.=
(m `1 ) `1
by ENS_1:def 4
.=
[(Hom (cod f),o),(Hom (dom f),o)] `1
by MCART_1:7
.=
Hom (cod f),
o
by MCART_1:7
.=
(Obj (hom?- (Hom A),(cod f))) . o
by ENS_1:60
.=
(hom?- (Hom A),(cod f)) . o
by CAT_1:def 20
.=
<|(cod f),?> . o
by ENS_1:def 26
;
cod m =
(fCod (Hom A)) . m
by A3
.=
cod m'
by ENS_1:def 11
.=
(m `1 ) `2
by ENS_1:def 5
.=
[(Hom (cod f),o),(Hom (dom f),o)] `2
by MCART_1:7
.=
Hom (dom f),
o
by MCART_1:7
.=
(Obj (hom?- (Hom A),(dom f))) . o
by ENS_1:60
.=
(hom?- (Hom A),(dom f)) . o
by CAT_1:def 20
.=
<|(dom f),?> . o
by ENS_1:def 26
;
hence
[[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))] in Hom (<|(cod f),?> . o),
(<|(dom f),?> . o)
by A4, CAT_1:18;
:: thesis: verum
end;
deffunc H1( Element of the carrier of A) -> set = [[(Hom (cod f),$1),(Hom (dom f),$1)],(hom f,(id $1))];
A5:
for o being Element of the carrier of A holds H1(o) in the carrier' of (EnsHom A)
consider t being Function of the carrier of A,the carrier' of (EnsHom A) such that
A6:
for o being Element of the carrier of A holds t . o = H1(o)
from FUNCT_2:sch 8(A5);
A7:
<|(cod f),?> is_naturally_transformable_to <|(dom f),?>
by Th3;
for o being Object of A holds Hom (<|(cod f),?> . o),(<|(dom f),?> . o) <> {}
by A1;
then A8:
<|(cod f),?> is_transformable_to <|(dom f),?>
by NATTRA_1:def 2;
for o being Object of A holds t . o is Morphism of <|(cod f),?> . o,<|(dom f),?> . o
proof
let o be
Object of
A;
:: thesis: t . o is Morphism of <|(cod f),?> . o,<|(dom f),?> . o
[[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))] in Hom (<|(cod f),?> . o),
(<|(dom f),?> . o)
by A1;
then
[[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))] is
Morphism of
<|(cod f),?> . o,
<|(dom f),?> . o
by CAT_1:def 7;
hence
t . o is
Morphism of
<|(cod f),?> . o,
<|(dom f),?> . o
by A6;
:: thesis: verum
end;
then reconsider t = t as transformation of <|(cod f),?>,<|(dom f),?> by A8, NATTRA_1:def 3;
set B = EnsHom A;
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
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 A9:
Hom a,
b <> {}
;
:: thesis: for g being Morphism of a,b holds (t . b) * (<|(cod f),?> . g) = (<|(dom f),?> . g) * (t . a)
let g be
Morphism of
a,
b;
:: thesis: (t . b) * (<|(cod f),?> . g) = (<|(dom f),?> . g) * (t . a)
A10:
EnsHom A = CatStr(#
(Hom A),
(Maps (Hom A)),
(fDom (Hom A)),
(fCod (Hom A)),
(fComp (Hom A)),
(fId (Hom A)) #)
by ENS_1:def 14;
reconsider f1 =
t . b as
Morphism of
(EnsHom A) ;
reconsider f2 =
<|(cod f),?> . g as
Morphism of
(EnsHom A) ;
A11:
t . b =
t . 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 f1' =
f1 as
Element of
Maps (Hom A) by ENS_1:48;
A12:
(
dom f1 = Hom (cod f),
b &
cod f1 = Hom (dom f),
b )
proof
A13:
dom f1 =
(fDom (Hom A)) . f1
by A10
.=
dom f1'
by ENS_1:def 10
.=
(f1 `1 ) `1
by ENS_1:def 4
.=
[(Hom (cod f),b),(Hom (dom f),b)] `1
by A11, MCART_1:7
.=
Hom (cod f),
b
by MCART_1:7
;
cod f1 =
(fCod (Hom A)) . f1
by A10
.=
cod f1'
by ENS_1:def 11
.=
(f1 `1 ) `2
by ENS_1:def 5
.=
[(Hom (cod f),b),(Hom (dom f),b)] `2
by A11, MCART_1:7
.=
Hom (dom f),
b
by MCART_1:7
;
hence
(
dom f1 = Hom (cod f),
b &
cod f1 = Hom (dom f),
b )
by A13;
:: thesis: verum
end;
A14:
f2 =
(hom?- (cod f)) . g
by A9, NATTRA_1:def 1
.=
[[(Hom (cod f),(dom g)),(Hom (cod f),(cod g))],(hom (cod f),g)]
by ENS_1:def 22
;
then reconsider f2' =
f2 as
Element of
Maps (Hom A) by ENS_1:47;
A15:
(
dom f2 = Hom (cod f),
(dom g) &
cod f2 = Hom (cod f),
(cod g) )
proof
A16:
dom f2 =
(fDom (Hom A)) . f2
by A10
.=
dom f2'
by ENS_1:def 10
.=
(f2 `1 ) `1
by ENS_1:def 4
.=
[(Hom (cod f),(dom g)),(Hom (cod f),(cod g))] `1
by A14, MCART_1:7
.=
Hom (cod f),
(dom g)
by MCART_1:7
;
cod f2 =
(fCod (Hom A)) . f2
by A10
.=
cod f2'
by ENS_1:def 11
.=
(f2 `1 ) `2
by ENS_1:def 5
.=
[(Hom (cod f),(dom g)),(Hom (cod f),(cod g))] `2
by A14, MCART_1:7
.=
Hom (cod f),
(cod g)
by MCART_1:7
;
hence
(
dom f2 = Hom (cod f),
(dom g) &
cod f2 = Hom (cod f),
(cod g) )
by A16;
:: thesis: verum
end;
then A17:
cod f2 = dom f1
by A9, A12, CAT_1:23;
reconsider f3 =
<|(dom f),?> . g as
Morphism of
(EnsHom A) ;
reconsider f4 =
t . a as
Morphism of
(EnsHom A) ;
A18:
f3 =
(hom?- (dom f)) . g
by A9, NATTRA_1:def 1
.=
[[(Hom (dom f),(dom g)),(Hom (dom f),(cod g))],(hom (dom f),g)]
by ENS_1:def 22
;
then reconsider f3' =
f3 as
Element of
Maps (Hom A) by ENS_1:47;
A19:
(
dom f3 = Hom (dom f),
(dom g) &
cod f3 = Hom (dom f),
(cod g) )
proof
A20:
dom f3 =
(fDom (Hom A)) . f3
by A10
.=
dom f3'
by ENS_1:def 10
.=
(f3 `1 ) `1
by ENS_1:def 4
.=
[(Hom (dom f),(dom g)),(Hom (dom f),(cod g))] `1
by A18, MCART_1:7
.=
Hom (dom f),
(dom g)
by MCART_1:7
;
cod f3 =
(fCod (Hom A)) . f3
by A10
.=
cod f3'
by ENS_1:def 11
.=
(f3 `1 ) `2
by ENS_1:def 5
.=
[(Hom (dom f),(dom g)),(Hom (dom f),(cod g))] `2
by A18, MCART_1:7
.=
Hom (dom f),
(cod g)
by MCART_1:7
;
hence
(
dom f3 = Hom (dom f),
(dom g) &
cod f3 = Hom (dom f),
(cod g) )
by A20;
:: thesis: verum
end;
A21:
t . a =
t . 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 f4' =
f4 as
Element of
Maps (Hom A) by ENS_1:48;
A22:
(
dom f4 = Hom (cod f),
a &
cod f4 = Hom (dom f),
a )
proof
A23:
dom f4 =
(fDom (Hom A)) . f4
by A10
.=
dom f4'
by ENS_1:def 10
.=
(f4 `1 ) `1
by ENS_1:def 4
.=
[(Hom (cod f),a),(Hom (dom f),a)] `1
by A21, MCART_1:7
.=
Hom (cod f),
a
by MCART_1:7
;
cod f4 =
(fCod (Hom A)) . f4
by A10
.=
cod f4'
by ENS_1:def 11
.=
(f4 `1 ) `2
by ENS_1:def 5
.=
[(Hom (cod f),a),(Hom (dom f),a)] `2
by A21, MCART_1:7
.=
Hom (dom f),
a
by MCART_1:7
;
hence
(
dom f4 = Hom (cod f),
a &
cod f4 = Hom (dom f),
a )
by A23;
:: thesis: verum
end;
then A24:
cod f4 = dom f3
by A9, A19, CAT_1:23;
A25:
rng (hom (cod f),g) c= dom (hom f,b)
proof
A26:
cod g = b
by A9, CAT_1:23;
per cases
( Hom (dom f),b = {} or Hom (dom f),b <> {} )
;
suppose A28:
Hom (dom f),
b <> {}
;
:: thesis: rng (hom (cod f),g) c= dom (hom f,b)let e be
set ;
:: according to TARSKI:def 3 :: thesis: ( not e in rng (hom (cod f),g) or e in dom (hom f,b) )assume A29:
e in rng (hom (cod f),g)
;
:: thesis: e in dom (hom f,b)A30:
cod g = b
by A9, CAT_1:23;
A31:
rng (hom (cod f),g) c= Hom (cod f),
(cod g)
by RELAT_1:def 19;
Hom (cod f),
(cod g) = dom (hom f,b)
by A28, A30, FUNCT_2:def 1;
hence
e in dom (hom f,b)
by A29, A31;
:: thesis: verum end;
end;
A32:
rng (hom f,a) c= dom (hom (dom f),g)
proof
A33:
dom g = a
by A9, CAT_1:23;
per cases
( Hom (dom f),(cod g) = {} or Hom (dom f),(cod g) <> {} )
;
suppose A35:
Hom (dom f),
(cod g) <> {}
;
:: thesis: rng (hom f,a) c= dom (hom (dom f),g)let e be
set ;
:: according to TARSKI:def 3 :: thesis: ( not e in rng (hom f,a) or e in dom (hom (dom f),g) )assume A36:
e in rng (hom f,a)
;
:: thesis: e in dom (hom (dom f),g)A37:
rng (hom f,a) c= Hom (dom f),
a
by RELAT_1:def 19;
Hom (dom f),
a = dom (hom (dom f),g)
by A33, A35, FUNCT_2:def 1;
hence
e in dom (hom (dom f),g)
by A36, A37;
:: thesis: verum end;
end;
A38:
(
dom g = a &
cod g = b )
by A9, CAT_1:23;
A39:
dom ((hom f,b) * (hom (cod f),g)) = dom ((hom (dom f),g) * (hom f,a))
proof
per cases
( Hom (cod f),(dom g) = {} or Hom (cod f),(dom g) <> {} )
;
suppose A40:
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 A25, RELAT_1:46
.=
Hom (cod f),
a
by A38, A40, FUNCT_2:def 1
.=
dom (hom f,a)
by A38, A40, FUNCT_2:def 1
.=
dom ((hom (dom f),g) * (hom f,a))
by A32, RELAT_1:46
;
hence
dom ((hom f,b) * (hom (cod f),g)) = dom ((hom (dom f),g) * (hom f,a))
;
:: thesis: verum end; suppose A41:
Hom (cod f),
(dom g) <> {}
;
:: thesis: dom ((hom f,b) * (hom (cod f),g)) = dom ((hom (dom f),g) * (hom f,a))then A42:
Hom (cod f),
(cod g) <> {}
by ENS_1:42;
A43:
Hom (dom f),
a <> {}
by A38, A41, ENS_1:42;
dom ((hom f,b) * (hom (cod f),g)) =
dom (hom (cod f),g)
by A25, RELAT_1:46
.=
Hom (cod f),
a
by A38, A42, FUNCT_2:def 1
.=
dom (hom f,a)
by A43, FUNCT_2:def 1
.=
dom ((hom (dom f),g) * (hom f,a))
by A32, RELAT_1:46
;
hence
dom ((hom f,b) * (hom (cod f),g)) = dom ((hom (dom f),g) * (hom f,a))
;
:: thesis: verum end;
end;
A44:
for
x being
set 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
set ;
:: 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 A45:
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) = {} )
;
suppose
Hom (cod f),
(dom g) <> {}
;
:: thesis: ((hom f,b) * (hom (cod f),g)) . x = ((hom (dom f),g) * (hom f,a)) . xthen A46:
Hom (cod f),
(cod g) <> {}
by ENS_1:42;
x in dom (hom (cod f),g)
by A45, FUNCT_1:21;
then A47:
x in Hom (cod f),
(dom g)
by A46, FUNCT_2:def 1;
then reconsider x =
x as
Morphism of
A ;
A48:
g * x in Hom (cod f),
b
A52:
(hom f,a) . x in Hom (dom f),
(dom g)
proof
A53:
(hom f,a) . x = x * f
by A38, A47, ENS_1:def 21;
A54:
dom x = cod f
by A47, CAT_1:18;
then A55:
dom (x * f) = dom f
by CAT_1:42;
cod (x * f) =
cod x
by A54, CAT_1:42
.=
dom g
by A47, CAT_1:18
;
hence
(hom f,a) . x in Hom (dom f),
(dom g)
by A53, A55, CAT_1:18;
:: thesis: verum
end; then reconsider h =
(hom f,a) . x as
Morphism of
A ;
A56:
dom g = cod x
by A47, CAT_1:18;
A57:
dom x = cod f
by A47, CAT_1:18;
((hom f,b) * (hom (cod f),g)) . x =
(hom f,b) . ((hom (cod f),g) . x)
by A45, FUNCT_1:22
.=
(hom f,b) . (g * x)
by A47, ENS_1:def 20
.=
(g * x) * f
by A48, ENS_1:def 21
.=
g * (x * f)
by A56, A57, CAT_1:43
.=
g * h
by A38, A47, ENS_1:def 21
.=
(hom (dom f),g) . ((hom f,a) . x)
by A52, ENS_1:def 20
.=
((hom (dom f),g) * (hom f,a)) . x
by A39, A45, FUNCT_1:22
;
hence
((hom f,b) * (hom (cod f),g)) . x = ((hom (dom f),g) * (hom f,a)) . x
;
:: thesis: verum end;
end;
A59:
(
Hom (<|(cod f),?> . b),
(<|(dom f),?> . b) <> {} &
Hom (<|(cod f),?> . a),
(<|(cod f),?> . b) <> {} )
by A1, A9, CAT_1:126;
A60:
(
Hom (<|(dom f),?> . a),
(<|(dom f),?> . b) <> {} &
Hom (<|(cod f),?> . a),
(<|(dom f),?> . a) <> {} )
by A1, A9, CAT_1:126;
(t . b) * (<|(cod f),?> . g) =
f1 * f2
by A59, CAT_1:def 13
.=
[[(Hom (cod f),(dom g)),(Hom (dom f),b)],((hom f,b) * (hom (cod f),g))]
by A11, A12, A14, A15, A17, Th1
.=
[[(Hom (cod f),a),(Hom (dom f),(cod g))],((hom (dom f),g) * (hom f,a))]
by A38, A39, A44, FUNCT_1:9
.=
f3 * f4
by A18, A19, A21, A22, A24, Th1
.=
(<|(dom f),?> . g) * (t . a)
by A60, CAT_1:def 13
;
hence
(t . b) * (<|(cod f),?> . g) = (<|(dom f),?> . g) * (t . a)
;
:: thesis: verum
end;
then reconsider t = t as natural_transformation of <|(cod f),?>,<|(dom f),?> by A7, NATTRA_1:def 8;
for o being Element of the carrier of A holds t . o = [[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))]
proof
let o be
Object of
A;
:: thesis: t . o = [[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))]
t . o =
t . o
by A8, NATTRA_1:def 5
.=
[[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))]
by A6
;
hence
t . o = [[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))]
;
:: thesis: verum
end;
hence
ex b1 being natural_transformation of <|(cod f),?>,<|(dom f),?> st
for o being Object of A holds b1 . o = [[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))]
; :: thesis: verum