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 2 ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies <^o1,o3^> <> {} )
assume
(
<^o1,o2^> <> {} &
<^o2,o3^> <> {} )
;
<^o1,o3^> <> {}
then
(
Funcs (
o1,
o2)
<> {} &
Funcs (
o2,
o3)
<> {} )
by Def14;
then
Funcs (
o1,
o3)
<> {}
by FUNCT_2:129;
hence
<^o1,o3^> <> {}
by Def14;
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 5,
ALTCAT_1:def 15 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 Def14;
(
<^i9,j9^> = Funcs (
i,
j) &
<^j9,k9^> = Funcs (
j,
k) )
by Def14;
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;
then A9:
h99 * g99 = h9 * g9
by A3, A4, Th10;
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;
then A11:
g99 * f99 = g9 * f9
by A2, A3, Th10;
A12:
<^i9,l9^> <> {}
by A1, A4, A6, A10;
A13:
( the Comp of (EnsCat A) . (j,k,l)) . (
h,
g)
= h99 * g99
by A3, A4, Def8;
( the Comp of (EnsCat A) . (i,j,k)) . (
g,
f)
= g99 * f99
by A2, A3, Def8;
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, Def8
.=
h9 * (g9 * f9)
by A4, A10, A12, A11, Th10
.=
(h9 * g9) * f9
by RELAT_1:36
.=
(h99 * g99) * f99
by A2, A8, A12, A9, Th10
.=
( the Comp of (EnsCat A) . (i,j,l)) . (
(( the Comp of (EnsCat A) . (j,k,l)) . (h,g)),
f)
by A2, A8, A13, Def8
;
verum
end;
thus
the Comp of (EnsCat A) is with_left_units
ALTCAT_1:def 16 the Comp of (EnsCat A) is with_right_units proof
let i be
Element of
(EnsCat A);
ALTCAT_1:def 7 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 Def14;
hence
id i in the
Arrows of
(EnsCat A) . (
i,
i)
by FUNCT_2:126;
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, FUNCT_2:126;
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 Def14;
then reconsider f9 =
f as
Function of
j,
i by A15, FUNCT_2:66;
thus ( the Comp of (EnsCat A) . (j,i,i)) . (
(id i),
f) =
I * f99
by A14, A15, Def8
.=
(id i) * f9
by A14, A15, Th10
.=
f
by FUNCT_2:17
;
verum
end;
let i be Element of (EnsCat A); ALTCAT_1:def 6 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 Def14;
hence
id i in the Arrows of (EnsCat A) . (i,i)
by FUNCT_2:126; 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, FUNCT_2:126;
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 Def14;
then reconsider f9 = f as Function of i,j by A17, FUNCT_2:66;
thus ( the Comp of (EnsCat A) . (i,i,j)) . (f,(id i)) =
f99 * I
by A16, A17, Def8
.=
f9 * (id i)
by A16, A17, Th10
.=
f
by FUNCT_2:17
; verum