set B = EnsHom A;
deffunc H1( Element of A) -> set = [[(Hom (cod f),$1),(Hom (dom f),$1)],(hom f,(id $1))];
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;
[[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))] in Hom (<|(cod f),?> . o),(<|(dom f),?> . o)
A2:
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;
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 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
;
dom m =
(fDom (Hom A)) . m
by A2
.=
dom m9
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
;
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;
verum
end;
A5:
for o being Element 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 A holds t . o = H1(o)
from FUNCT_2:sch 8(A5);
A7:
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;
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;
verum
end;
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;
then reconsider t = t as transformation of <|(cod f),?>,<|(dom f),?> by A7, NATTRA_1:def 3;
A9:
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;
( Hom a,b <> {} implies for g being Morphism of a,b holds (t . b) * (<|(cod f),?> . g) = (<|(dom f),?> . g) * (t . a) )
assume A10:
Hom a,
b <> {}
;
for g being Morphism of a,b holds (t . b) * (<|(cod f),?> . g) = (<|(dom f),?> . g) * (t . a)
A11:
Hom (<|(cod f),?> . a),
(<|(cod f),?> . b) <> {}
by A10, CAT_1:126;
let g be
Morphism of
a,
b;
(t . b) * (<|(cod f),?> . g) = (<|(dom f),?> . g) * (t . a)
A12:
dom g = a
by A10, CAT_1:23;
A13:
rng (hom (cod f),g) c= dom (hom f,b)
proof
A14:
cod g = b
by A10, CAT_1:23;
per cases
( Hom (dom f),b = {} or Hom (dom f),b <> {} )
;
suppose A17:
Hom (dom f),
b <> {}
;
rng (hom (cod f),g) c= dom (hom f,b)
cod g = b
by A10, CAT_1:23;
then A18:
(
rng (hom (cod f),g) c= Hom (cod f),
(cod g) &
Hom (cod f),
(cod g) = dom (hom f,b) )
by A17, FUNCT_2:def 1, RELAT_1:def 19;
let e be
set ;
TARSKI:def 3 ( not e in rng (hom (cod f),g) or e in dom (hom f,b) )assume
e in rng (hom (cod f),g)
;
e in dom (hom f,b)hence
e in dom (hom f,b)
by A18;
verum end;
end;
A19:
rng (hom f,a) c= dom (hom (dom f),g)
proof
A20:
dom g = a
by A10, CAT_1:23;
per cases
( Hom (dom f),(cod g) = {} or Hom (dom f),(cod g) <> {} )
;
suppose A23:
Hom (dom f),
(cod g) <> {}
;
rng (hom f,a) c= dom (hom (dom f),g)let e be
set ;
TARSKI:def 3 ( not e in rng (hom f,a) or e in dom (hom (dom f),g) )assume A24:
e in rng (hom f,a)
;
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 A20, A23, FUNCT_2:def 1, RELAT_1:def 19;
hence
e in dom (hom (dom f),g)
by A24;
verum end;
end;
A25:
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 A26:
Hom (cod f),
(dom g) = {}
;
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 A13, RELAT_1:46
.=
Hom (cod f),
a
by A12, A26, FUNCT_2:def 1
.=
dom (hom f,a)
by A12, A26, FUNCT_2:def 1
.=
dom ((hom (dom f),g) * (hom f,a))
by A19, RELAT_1:46
;
hence
dom ((hom f,b) * (hom (cod f),g)) = dom ((hom (dom f),g) * (hom f,a))
;
verum end; suppose A27:
Hom (cod f),
(dom g) <> {}
;
dom ((hom f,b) * (hom (cod f),g)) = dom ((hom (dom f),g) * (hom f,a))then A28:
Hom (cod f),
(cod g) <> {}
by ENS_1:42;
A29:
Hom (dom f),
a <> {}
by A12, A27, ENS_1:42;
dom ((hom f,b) * (hom (cod f),g)) =
dom (hom (cod f),g)
by A13, RELAT_1:46
.=
Hom (cod f),
a
by A12, A28, FUNCT_2:def 1
.=
dom (hom f,a)
by A29, FUNCT_2:def 1
.=
dom ((hom (dom f),g) * (hom f,a))
by A19, RELAT_1:46
;
hence
dom ((hom f,b) * (hom (cod f),g)) = dom ((hom (dom f),g) * (hom f,a))
;
verum end;
end;
A30:
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 ;
( 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 A31:
x in dom ((hom f,b) * (hom (cod f),g))
;
((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 A32:
Hom (cod f),
(dom g) <> {}
;
((hom f,b) * (hom (cod f),g)) . x = ((hom (dom f),g) * (hom f,a)) . xA33:
x in dom (hom (cod f),g)
by A31, FUNCT_1:21;
Hom (cod f),
(cod g) <> {}
by A32, ENS_1:42;
then A34:
x in Hom (cod f),
(dom g)
by A33, FUNCT_2:def 1;
then reconsider x =
x as
Morphism of
A ;
A35:
dom g = cod x
by A34, CAT_1:18;
cod g = b
by A10, CAT_1:23;
then A36:
cod (g * x) = b
by A35, CAT_1:42;
dom (g * x) =
dom x
by A35, CAT_1:42
.=
cod f
by A34, CAT_1:18
;
then A37:
g * x in Hom (cod f),
b
by A36, CAT_1:18;
A38:
dom x = cod f
by A34, CAT_1:18;
then A39:
dom (x * f) = dom f
by CAT_1:42;
A40:
(hom f,a) . x = x * f
by A12, A34, ENS_1:def 21;
then reconsider h =
(hom f,a) . x as
Morphism of
A ;
A41:
(
dom g = cod x &
dom x = cod f )
by A34, CAT_1:18;
cod (x * f) =
cod x
by A38, CAT_1:42
.=
dom g
by A34, CAT_1:18
;
then A42:
(hom f,a) . x in Hom (dom f),
(dom g)
by A40, A39, CAT_1:18;
((hom f,b) * (hom (cod f),g)) . x =
(hom f,b) . ((hom (cod f),g) . x)
by A31, FUNCT_1:22
.=
(hom f,b) . (g * x)
by A34, ENS_1:def 20
.=
(g * x) * f
by A37, ENS_1:def 21
.=
g * (x * f)
by A41, CAT_1:43
.=
g * h
by A12, A34, ENS_1:def 21
.=
(hom (dom f),g) . ((hom f,a) . x)
by A42, ENS_1:def 20
.=
((hom (dom f),g) * (hom f,a)) . x
by A25, A31, FUNCT_1:22
;
hence
((hom f,b) * (hom (cod f),g)) . x = ((hom (dom f),g) * (hom f,a)) . x
;
verum end;
end;
A44:
Hom (<|(dom f),?> . a),
(<|(dom f),?> . b) <> {}
by A10, CAT_1:126;
A45:
cod g = b
by A10, CAT_1:23;
reconsider f4 =
t . a as
Morphism of
(EnsHom A) ;
A46:
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 f49 =
f4 as
Element of
Maps (Hom A) by ENS_1:48;
A47:
Hom (<|(cod f),?> . a),
(<|(dom f),?> . a) <> {}
by A1;
reconsider f1 =
t . b as
Morphism of
(EnsHom A) ;
A48:
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 f19 =
f1 as
Element of
Maps (Hom A) by ENS_1:48;
A49:
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 A50:
cod f1 =
(fCod (Hom A)) . f1
.=
cod f19
by ENS_1:def 11
.=
(f1 `1 ) `2
by ENS_1:def 5
.=
[(Hom (cod f),b),(Hom (dom f),b)] `2
by A48, MCART_1:7
.=
Hom (dom f),
b
by MCART_1:7
;
A51:
dom f4 =
(fDom (Hom A)) . f4
by A49
.=
dom f49
by ENS_1:def 10
.=
(f4 `1 ) `1
by ENS_1:def 4
.=
[(Hom (cod f),a),(Hom (dom f),a)] `1
by A46, MCART_1:7
.=
Hom (cod f),
a
by MCART_1:7
;
A52:
cod f4 =
(fCod (Hom A)) . f4
by A49
.=
cod f49
by ENS_1:def 11
.=
(f4 `1 ) `2
by ENS_1:def 5
.=
[(Hom (cod f),a),(Hom (dom f),a)] `2
by A46, MCART_1:7
.=
Hom (dom f),
a
by MCART_1:7
;
reconsider f2 =
<|(cod f),?> . g as
Morphism of
(EnsHom A) ;
A53:
f2 =
(hom?- (cod f)) . g
by A10, 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 f29 =
f2 as
Element of
Maps (Hom A) by ENS_1:47;
A54:
dom f2 =
(fDom (Hom A)) . f2
by A49
.=
dom f29
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 A53, MCART_1:7
.=
Hom (cod f),
(dom g)
by MCART_1:7
;
A55:
cod f2 =
(fCod (Hom A)) . f2
by A49
.=
cod f29
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 A53, MCART_1:7
.=
Hom (cod f),
(cod g)
by MCART_1:7
;
A56:
dom f1 =
(fDom (Hom A)) . f1
by A49
.=
dom f19
by ENS_1:def 10
.=
(f1 `1 ) `1
by ENS_1:def 4
.=
[(Hom (cod f),b),(Hom (dom f),b)] `1
by A48, MCART_1:7
.=
Hom (cod f),
b
by MCART_1:7
;
then A57:
cod f2 = dom f1
by A10, A55, CAT_1:23;
reconsider f3 =
<|(dom f),?> . g as
Morphism of
(EnsHom A) ;
A58:
f3 =
(hom?- (dom f)) . g
by A10, 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 f39 =
f3 as
Element of
Maps (Hom A) by ENS_1:47;
A59:
cod f3 =
(fCod (Hom A)) . f3
by A49
.=
cod f39
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 A58, MCART_1:7
.=
Hom (dom f),
(cod g)
by MCART_1:7
;
A60:
dom f3 =
(fDom (Hom A)) . f3
by A49
.=
dom f39
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 A58, MCART_1:7
.=
Hom (dom f),
(dom g)
by MCART_1:7
;
then A61:
cod f4 = dom f3
by A10, A52, CAT_1:23;
Hom (<|(cod f),?> . b),
(<|(dom f),?> . b) <> {}
by A1;
then (t . b) * (<|(cod f),?> . 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 A48, A56, A50, A53, A54, A55, A57, Th1
.=
[[(Hom (cod f),a),(Hom (dom f),(cod g))],((hom (dom f),g) * (hom f,a))]
by A12, A45, A25, A30, FUNCT_1:9
.=
f3 * f4
by A58, A60, A59, A46, A51, A52, A61, Th1
.=
(<|(dom f),?> . g) * (t . a)
by A44, A47, CAT_1:def 13
;
hence
(t . b) * (<|(cod f),?> . g) = (<|(dom f),?> . g) * (t . a)
;
verum
end;
<|(cod f),?> is_naturally_transformable_to <|(dom f),?>
by Th3;
then reconsider t = t as natural_transformation of <|(cod f),?>,<|(dom f),?> by A9, NATTRA_1:def 8;
for o being Element of A holds t . o = [[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))]
proof
let o be
Object of
A;
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))]
;
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))]
; verum