hereby ( ( for o being Object of C holds
( <^o,o^> <> {} & ex i being Morphism of o,o st
for o9 being Object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) ) implies C is with_units )
assume A1:
C is
with_units
;
for o being Object of C holds
( <^o,o^> <> {} & ex i being Morphism of o,o st
for o9 being Object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) )then reconsider C9 =
C as non
empty with_units AltCatStr ;
let o be
Object of
C;
( <^o,o^> <> {} & ex i being Morphism of o,o st
for o9 being Object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) )thus
<^o,o^> <> {}
by A1, ALTCAT_1:18;
ex i being Morphism of o,o st
for o9 being Object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )reconsider p =
o as
Object of
C9 ;
reconsider i =
idm p as
Morphism of
o,
o ;
take i =
i;
for o9 being Object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )let o9 be
Object of
C;
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )let m9 be
Morphism of
o9,
o;
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )let m99 be
Morphism of
o,
o9;
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )thus
(
<^o9,o^> <> {} implies
i * m9 = m9 )
by ALTCAT_1:20;
( <^o,o9^> <> {} implies m99 * i = m99 )thus
(
<^o,o9^> <> {} implies
m99 * i = m99 )
by ALTCAT_1:def 17;
verum
end;
assume A2:
for o being Object of C holds
( <^o,o^> <> {} & ex i being Morphism of o,o st
for o9 being Object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) )
; C is with_units
hereby ALTCAT_1:def 7,
ALTCAT_1:def 16 the Comp of C is with_right_units
let j be
Element of
C;
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
o9 being
Object of
C for
m9 being
Morphism of
o9,
o for
m99 being
Morphism of
o,
o9 holds
( (
<^o9,o^> <> {} implies
m * m9 = m9 ) & (
<^o,o9^> <> {} implies
m99 * m = m99 ) )
by A2;
reconsider e =
m as
set ;
take e =
e;
( 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)
;
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;
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 ;
( 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)
;
( the Comp of C . (i,j,j)) . (e,f) = freconsider o9 =
i as
Object of
C ;
reconsider m9 =
f as
Morphism of
o9,
o by A5;
thus ( the Comp of C . (i,j,j)) . (
e,
f) =
m * m9
by A4, A5, ALTCAT_1:def 8
.=
f
by A3, A5
;
verum
end;
let i be Element of C; ALTCAT_1:def 6 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 o9 being Object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies m * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * m = m99 ) )
by A2;
take e = m; ( 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)
; 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; 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 ; ( 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)
; ( the Comp of C . (i,i,j)) . (f,e) = f
reconsider o9 = j as Object of C ;
reconsider m9 = f as Morphism of o,o9 by A8;
thus ( the Comp of C . (i,i,j)) . (f,e) =
m9 * m
by A7, A8, ALTCAT_1:def 8
.=
f
by A6, A8
; verum