hereby :: thesis: ( ( for o being object of C holds
( <^o,o^> <> {} & ex i being Morphism of o,o st
for o' being object of C
for m' being Morphism of o',o
for m'' being Morphism of o,o' holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) ) ) ) implies C is with_units )
assume A1:
C is
with_units
;
:: thesis: for o being object of C holds
( <^o,o^> <> {} & ex i being Morphism of o,o st
for o' being object of C
for m' being Morphism of o',o
for m'' being Morphism of o,o' holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) ) )then reconsider C' =
C as non
empty with_units AltCatStr ;
let o be
object of
C;
:: thesis: ( <^o,o^> <> {} & ex i being Morphism of o,o st
for o' being object of C
for m' being Morphism of o',o
for m'' being Morphism of o,o' holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) ) )thus
<^o,o^> <> {}
by A1, ALTCAT_1:21;
:: thesis: ex i being Morphism of o,o st
for o' being object of C
for m' being Morphism of o',o
for m'' being Morphism of o,o' holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )reconsider p =
o as
object of
C' ;
reconsider i =
idm p as
Morphism of
o,
o ;
take i =
i;
:: thesis: for o' being object of C
for m' being Morphism of o',o
for m'' being Morphism of o,o' holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )let o' be
object of
C;
:: thesis: for m' being Morphism of o',o
for m'' being Morphism of o,o' holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )let m' be
Morphism of
o',
o;
:: thesis: for m'' being Morphism of o,o' holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )let m'' be
Morphism of
o,
o';
:: thesis: ( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )thus
(
<^o',o^> <> {} implies
i * m' = m' )
by ALTCAT_1:24;
:: thesis: ( <^o,o'^> <> {} implies m'' * i = m'' )thus
(
<^o,o'^> <> {} implies
m'' * i = m'' )
by ALTCAT_1:def 19;
:: thesis: verum
end;
assume A2:
for o being object of C holds
( <^o,o^> <> {} & ex i being Morphism of o,o st
for o' being object of C
for m' being Morphism of o',o
for m'' being Morphism of o,o' holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) ) )
; :: thesis: C is with_units
hereby :: according to ALTCAT_1:def 9,
ALTCAT_1:def 18 :: thesis: the Comp of C is with_right_units
let j be
Element of
C;
:: thesis: ex e being set st
( e in the Arrows of C . j,j & ( for i being Element of C
for f being set st f in the Arrows of C . i,j holds
(the Comp of C . i,j,j) . e,f = f ) )reconsider o =
j as
object of
C ;
consider m being
Morphism of
o,
o such that A3:
for
o' being
object of
C for
m' being
Morphism of
o',
o for
m'' being
Morphism of
o,
o' holds
( (
<^o',o^> <> {} implies
m * m' = m' ) & (
<^o,o'^> <> {} implies
m'' * m = m'' ) )
by A2;
reconsider e =
m as
set ;
take e =
e;
:: thesis: ( e in the Arrows of C . j,j & ( for i being Element of C
for f being set st f in the Arrows of C . i,j holds
(the Comp of C . i,j,j) . e,f = f ) )A4:
<^o,o^> <> {}
by A2;
hence
e in the
Arrows of
C . j,
j
;
:: thesis: for i being Element of C
for f being set st f in the Arrows of C . i,j holds
(the Comp of C . i,j,j) . e,f = flet i be
Element of
C;
:: thesis: for f being set st f in the Arrows of C . i,j holds
(the Comp of C . i,j,j) . e,f = flet f be
set ;
:: thesis: ( f in the Arrows of C . i,j implies (the Comp of C . i,j,j) . e,f = f )assume A5:
f in the
Arrows of
C . i,
j
;
:: thesis: (the Comp of C . i,j,j) . e,f = freconsider o' =
i as
object of
C ;
reconsider m' =
f as
Morphism of
o',
o by A5;
thus (the Comp of C . i,j,j) . e,
f =
m * m'
by A4, A5, ALTCAT_1:def 10
.=
f
by A3, A5
;
:: thesis: verum
end;
let i be Element of C; :: according to ALTCAT_1:def 8 :: thesis: ex b1 being set st
( b1 in the Arrows of C . i,i & ( for b2 being Element of the carrier of C
for b3 being set holds
( not b3 in the Arrows of C . i,b2 or (the Comp of C . i,i,b2) . b3,b1 = b3 ) ) )
reconsider o = i as object of C ;
consider m being Morphism of o,o such that
A6:
for o' being object of C
for m' being Morphism of o',o
for m'' being Morphism of o,o' holds
( ( <^o',o^> <> {} implies m * m' = m' ) & ( <^o,o'^> <> {} implies m'' * m = m'' ) )
by A2;
take e = m; :: thesis: ( e in the Arrows of C . i,i & ( for b1 being Element of the carrier of C
for b2 being set holds
( not b2 in the Arrows of C . i,b1 or (the Comp of C . i,i,b1) . b2,e = b2 ) ) )
A7:
<^o,o^> <> {}
by A2;
hence
e in the Arrows of C . i,i
; :: thesis: for b1 being Element of the carrier of C
for b2 being set holds
( not b2 in the Arrows of C . i,b1 or (the Comp of C . i,i,b1) . b2,e = b2 )
let j be Element of C; :: thesis: for b1 being set holds
( not b1 in the Arrows of C . i,j or (the Comp of C . i,i,j) . b1,e = b1 )
let f be set ; :: thesis: ( not f in the Arrows of C . i,j or (the Comp of C . i,i,j) . f,e = f )
assume A8:
f in the Arrows of C . i,j
; :: thesis: (the Comp of C . i,i,j) . f,e = f
reconsider o' = j as object of C ;
reconsider m' = f as Morphism of o,o' by A8;
thus (the Comp of C . i,i,j) . f,e =
m' * m
by A7, A8, ALTCAT_1:def 10
.=
f
by A6, A8
; :: thesis: verum