hereby :: thesis: ( ( 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 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 ) ) ) ) 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 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; :: thesis: ( <^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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )

thus ( <^o9,o^> <> {} implies i * m9 = m9 ) by ALTCAT_1:20; :: thesis: ( <^o,o9^> <> {} implies m99 * i = m99 )

thus ( <^o,o9^> <> {} implies m99 * i = m99 ) by ALTCAT_1:def 17; :: thesis: verum

end;( <^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; :: thesis: ( <^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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )

thus ( <^o9,o^> <> {} implies i * m9 = m9 ) by ALTCAT_1:20; :: thesis: ( <^o,o9^> <> {} implies m99 * i = m99 )

thus ( <^o,o9^> <> {} implies m99 * i = m99 ) by ALTCAT_1:def 17; :: thesis: verum

( <^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 ) ) ) ; :: thesis: C is with_units

hereby :: according to ALTCAT_1:def 7,ALTCAT_1:def 16 :: thesis: the Comp of C is with_right_units

let i be Element of C; :: according to ALTCAT_1:def 6 :: thesis: ex blet 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 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; :: 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) = f

let 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) = f

let 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) = f

reconsider 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 ; :: thesis: verum

end;( 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; :: 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) = f

let 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) = f

let 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) = f

reconsider 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 ; :: thesis: verum

( b

for b

( not b

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; :: thesis: ( e in the Arrows of C . (i,i) & ( for b

for b

( not b

A7: <^o,o^> <> {} by A2;

hence e in the Arrows of C . (i,i) ; :: thesis: for b

for b

( not b

let j be Element of C; :: thesis: for b

( not b

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 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 ; :: thesis: verum