let A be non empty set ; ( EnsCat A is transitive & EnsCat A is associative & EnsCat A is with_units )
set G = the Arrows of (EnsCat A);
set C = the Comp of (EnsCat A);
thus A1:
EnsCat A is transitive
( EnsCat A is associative & EnsCat A is with_units )proof
let o1,
o2,
o3 be
object of
(EnsCat A);
ALTCAT_1:def 4 ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies <^o1,o3^> <> {} )
assume
(
<^o1,o2^> <> {} &
<^o2,o3^> <> {} )
;
<^o1,o3^> <> {}
then
(
Funcs o1,
o2 <> {} &
Funcs o2,
o3 <> {} )
by Def16;
then
Funcs o1,
o3 <> {}
by Th5;
hence
<^o1,o3^> <> {}
by Def16;
verum
end;
thus
EnsCat A is associative
EnsCat A is with_units proof
let i,
j,
k,
l be
Element of
(EnsCat A);
ALTCAT_1:def 7,
ALTCAT_1:def 17 for f, g, h being set st f in the Arrows of (EnsCat A) . i,j & g in the Arrows of (EnsCat A) . j,k & h in the Arrows of (EnsCat A) . k,l holds
(the Comp of (EnsCat A) . i,k,l) . h,((the Comp of (EnsCat A) . i,j,k) . g,f) = (the Comp of (EnsCat A) . i,j,l) . ((the Comp of (EnsCat A) . j,k,l) . h,g),f
reconsider i9 =
i,
j9 =
j,
k9 =
k,
l9 =
l as
object of
(EnsCat A) ;
let f,
g,
h be
set ;
( f in the Arrows of (EnsCat A) . i,j & g in the Arrows of (EnsCat A) . j,k & h in the Arrows of (EnsCat A) . k,l implies (the Comp of (EnsCat A) . i,k,l) . h,((the Comp of (EnsCat A) . i,j,k) . g,f) = (the Comp of (EnsCat A) . i,j,l) . ((the Comp of (EnsCat A) . j,k,l) . h,g),f )
assume that A2:
f in the
Arrows of
(EnsCat A) . i,
j
and A3:
g in the
Arrows of
(EnsCat A) . j,
k
and A4:
h in the
Arrows of
(EnsCat A) . k,
l
;
(the Comp of (EnsCat A) . i,k,l) . h,((the Comp of (EnsCat A) . i,j,k) . g,f) = (the Comp of (EnsCat A) . i,j,l) . ((the Comp of (EnsCat A) . j,k,l) . h,g),f
reconsider h99 =
h as
Morphism of
k9,
l9 by A4;
reconsider g99 =
g as
Morphism of
j9,
k9 by A3;
A5:
<^k9,l9^> = Funcs k,
l
by Def16;
(
<^i9,j9^> = Funcs i,
j &
<^j9,k9^> = Funcs j,
k )
by Def16;
then reconsider f9 =
f,
g9 =
g,
h9 =
h as
Function by A2, A3, A4, A5;
A6:
the
Arrows of
(EnsCat A) . k,
l = <^k9,l9^>
;
A7:
<^j9,k9^> <> {}
by A3;
then A8:
<^j9,l9^> <> {}
by A1, A4, A6, Def4;
then A9:
h99 * g99 = h9 * g9
by A3, A4, Th18;
reconsider f99 =
f as
Morphism of
i9,
j9 by A2;
the
Arrows of
(EnsCat A) . i,
j = <^i9,j9^>
;
then A10:
<^i9,k9^> <> {}
by A1, A2, A7, Def4;
then A11:
g99 * f99 = g9 * f9
by A2, A3, Th18;
A12:
<^i9,l9^> <> {}
by A1, A4, A6, A10, Def4;
A13:
(the Comp of (EnsCat A) . j,k,l) . h,
g = h99 * g99
by A3, A4, Def10;
(the Comp of (EnsCat A) . i,j,k) . g,
f = g99 * f99
by A2, A3, Def10;
hence (the Comp of (EnsCat A) . i,k,l) . h,
((the Comp of (EnsCat A) . i,j,k) . g,f) =
h99 * (g99 * f99)
by A4, A10, Def10
.=
h9 * (g9 * f9)
by A4, A10, A12, A11, Th18
.=
(h9 * g9) * f9
by RELAT_1:55
.=
(h99 * g99) * f99
by A2, A8, A12, A9, Th18
.=
(the Comp of (EnsCat A) . i,j,l) . ((the Comp of (EnsCat A) . j,k,l) . h,g),
f
by A2, A8, A13, Def10
;
verum
end;
thus
the Comp of (EnsCat A) is with_left_units
ALTCAT_1:def 18 the Comp of (EnsCat A) is with_right_units proof
let i be
Element of
(EnsCat A);
ALTCAT_1:def 9 ex e being set st
( e in the Arrows of (EnsCat A) . i,i & ( for i being Element of the carrier of (EnsCat A)
for f being set st f in the Arrows of (EnsCat A) . i,i holds
(the Comp of (EnsCat A) . i,i,i) . e,f = f ) )
reconsider i9 =
i as
object of
(EnsCat A) ;
take
id i
;
( id i in the Arrows of (EnsCat A) . i,i & ( for i being Element of the carrier of (EnsCat A)
for f being set st f in the Arrows of (EnsCat A) . i,i holds
(the Comp of (EnsCat A) . i,i,i) . (id i),f = f ) )
A14:
<^i9,i9^> = Funcs i,
i
by Def16;
hence
id i in the
Arrows of
(EnsCat A) . i,
i
by Th2;
for i being Element of the carrier of (EnsCat A)
for f being set st f in the Arrows of (EnsCat A) . i,i holds
(the Comp of (EnsCat A) . i,i,i) . (id i),f = f
reconsider I =
id i as
Morphism of
i9,
i9 by A14, Th2;
let j be
Element of
(EnsCat A);
for f being set st f in the Arrows of (EnsCat A) . j,i holds
(the Comp of (EnsCat A) . j,i,i) . (id i),f = flet f be
set ;
( f in the Arrows of (EnsCat A) . j,i implies (the Comp of (EnsCat A) . j,i,i) . (id i),f = f )
reconsider j9 =
j as
object of
(EnsCat A) ;
assume A15:
f in the
Arrows of
(EnsCat A) . j,
i
;
(the Comp of (EnsCat A) . j,i,i) . (id i),f = f
then reconsider f99 =
f as
Morphism of
j9,
i9 ;
<^j9,i9^> = Funcs j,
i
by Def16;
then reconsider f9 =
f as
Function of
j,
i by A15, FUNCT_2:121;
thus (the Comp of (EnsCat A) . j,i,i) . (id i),
f =
I * f99
by A14, A15, Def10
.=
(id i) * f9
by A14, A15, Th18
.=
f
by FUNCT_2:23
;
verum
end;
let i be Element of (EnsCat A); ALTCAT_1:def 8 ex e being set st
( e in the Arrows of (EnsCat A) . i,i & ( for j being Element of the carrier of (EnsCat A)
for f being set st f in the Arrows of (EnsCat A) . i,j holds
(the Comp of (EnsCat A) . i,i,j) . f,e = f ) )
reconsider i9 = i as object of (EnsCat A) ;
take
id i
; ( id i in the Arrows of (EnsCat A) . i,i & ( for j being Element of the carrier of (EnsCat A)
for f being set st f in the Arrows of (EnsCat A) . i,j holds
(the Comp of (EnsCat A) . i,i,j) . f,(id i) = f ) )
A16:
<^i9,i9^> = Funcs i,i
by Def16;
hence
id i in the Arrows of (EnsCat A) . i,i
by Th2; for j being Element of the carrier of (EnsCat A)
for f being set st f in the Arrows of (EnsCat A) . i,j holds
(the Comp of (EnsCat A) . i,i,j) . f,(id i) = f
reconsider I = id i as Morphism of i9,i9 by A16, Th2;
let j be Element of (EnsCat A); for f being set st f in the Arrows of (EnsCat A) . i,j holds
(the Comp of (EnsCat A) . i,i,j) . f,(id i) = f
let f be set ; ( f in the Arrows of (EnsCat A) . i,j implies (the Comp of (EnsCat A) . i,i,j) . f,(id i) = f )
reconsider j9 = j as object of (EnsCat A) ;
assume A17:
f in the Arrows of (EnsCat A) . i,j
; (the Comp of (EnsCat A) . i,i,j) . f,(id i) = f
then reconsider f99 = f as Morphism of i9,j9 ;
<^i9,j9^> = Funcs i,j
by Def16;
then reconsider f9 = f as Function of i,j by A17, FUNCT_2:121;
thus (the Comp of (EnsCat A) . i,i,j) . f,(id i) =
f99 * I
by A16, A17, Def10
.=
f9 * (id i)
by A16, A17, Th18
.=
f
by FUNCT_2:23
; verum