hereby :: thesis: ( ( for o being object of holds
( <^o,o^> <> {} & ex i being Morphism of , st
for o' being object of
for m' being Morphism of ,
for m'' being Morphism of , 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 holds
( <^o,o^> <> {} & ex i being Morphism of , st
for o' being object of
for m' being Morphism of ,
for m'' being Morphism of , 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 ; :: thesis: ( <^o,o^> <> {} & ex i being Morphism of , st
for o' being object of
for m' being Morphism of ,
for m'' being Morphism of , 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 , st
for o' being object of
for m' being Morphism of ,
for m'' being Morphism of , holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )
reconsider p = o as object of ;
reconsider i = idm p as Morphism of , ;
take i = i; :: thesis: for o' being object of
for m' being Morphism of ,
for m'' being Morphism of , holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )
let o' be object of ; :: thesis: for m' being Morphism of ,
for m'' being Morphism of , holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )
let m' be Morphism of ,; :: thesis: for m'' being Morphism of , holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )
let m'' be Morphism of ,; :: 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 holds
( <^o,o^> <> {} & ex i being Morphism of , st
for o' being object of
for m' being Morphism of ,
for m'' being Morphism of , 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 ; :: thesis: ex e being set st
( e in the Arrows of C . j,j & ( for i being Element of
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 ;
consider m being Morphism of , such that
A3: for o' being object of
for m' being Morphism of ,
for m'' being Morphism of , 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
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
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 ; :: 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 o' = i as object of ;
reconsider m' = f as Morphism of , 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 ; :: according to ALTCAT_1:def 8 :: thesis: ex b₁ being set st
( b₁ in the Arrows of C . i,i & ( for b₂ being Element of the carrier of C
for b₃ being set holds
( not b₃ in the Arrows of C . i,b₂ or (the Comp of C . i,i,b₂) . b₃,b₁ = b₃ ) ) )
reconsider o = i as object of ;
consider m being Morphism of , such that
A6: for o' being object of
for m' being Morphism of ,
for m'' being Morphism of , 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 b₁ being Element of the carrier of C
for b₂ being set holds
( not b₂ in the Arrows of C . i,b₁ or (the Comp of C . i,i,b₁) . b₂,e = b₂ ) ) )
A7: <^o,o^> <> {} by A2;
hence e in the Arrows of C . i,i ; :: thesis: for b₁ being Element of the carrier of C
for b₂ being set holds
( not b₂ in the Arrows of C . i,b₁ or (the Comp of C . i,i,b₁) . b₂,e = b₂ )
let j be Element of ; :: thesis: for b₁ being set holds
( not b₁ in the Arrows of C . i,j or (the Comp of C . i,i,j) . b₁,e = 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 o' = j as object of ;
reconsider m' = f as Morphism of , 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