let C be Category; :: thesis: ( the_comps_of C is with_left_units & the_comps_of C is with_right_units )
thus the_comps_of C is with_left_units :: thesis: the_comps_of C is with_right_units

proof

let i be Object of C; :: according to ALTCAT_1:def 9 :: thesis: ex b₁ being set st
( b₁ in (the_hom_sets_of C) . i,i & ( for b₂ being Element of the carrier of C
for b₃ being set holds
( not b₃ in (the_hom_sets_of C) . b₂,i or ((the_comps_of C) . b₂,i,i) . b₁,b₃ = b₃ ) ) )
take id i ; :: thesis: ( id i in (the_hom_sets_of C) . i,i & ( for b₁ being Element of the carrier of C
for b₂ being set holds
( not b₂ in (the_hom_sets_of C) . b₁,i or ((the_comps_of C) . b₁,i,i) . (id i),b₂ = b₂ ) ) )
thus id i in (the_hom_sets_of C) . i,i by Th13; :: thesis: for b₁ being Element of the carrier of C
for b₂ being set holds
( not b₂ in (the_hom_sets_of C) . b₁,i or ((the_comps_of C) . b₁,i,i) . (id i),b₂ = b₂ )
let j be Object of C; :: thesis: for b₁ being set holds
( not b₁ in (the_hom_sets_of C) . j,i or ((the_comps_of C) . j,i,i) . (id i),b₁ = b₁ )
let f be set ; :: thesis: ( not f in (the_hom_sets_of C) . j,i or ((the_comps_of C) . j,i,i) . (id i),f = f )
assume f in (the_hom_sets_of C) . j,i ; :: thesis: ((the_comps_of C) . j,i,i) . (id i),f = f
then A1: f in Hom j,i by Def3;
then reconsider m = f as Morphism of j,i by CAT_1:def 7;
Hom i,i <> {} by CAT_1:56;
hence ((the_comps_of C) . j,i,i) . (id i),f = (id i) * m by A1, Th14
.= f by A1, CAT_1:57 ;
:: thesis: verum

end;

let j be Object of C; :: according to ALTCAT_1:def 8 :: thesis: ex b₁ being set st
( b₁ in (the_hom_sets_of C) . j,j & ( for b₂ being Element of the carrier of C
for b₃ being set holds
( not b₃ in (the_hom_sets_of C) . j,b₂ or ((the_comps_of C) . j,j,b₂) . b₃,b₁ = b₃ ) ) )
take id j ; :: thesis: ( id j in (the_hom_sets_of C) . j,j & ( for b₁ being Element of the carrier of C
for b₂ being set holds
( not b₂ in (the_hom_sets_of C) . j,b₁ or ((the_comps_of C) . j,j,b₁) . b₂,(id j) = b₂ ) ) )
thus id j in (the_hom_sets_of C) . j,j by Th13; :: thesis: for b₁ being Element of the carrier of C
for b₂ being set holds
( not b₂ in (the_hom_sets_of C) . j,b₁ or ((the_comps_of C) . j,j,b₁) . b₂,(id j) = b₂ )
let i be Object of C; :: thesis: for b₁ being set holds
( not b₁ in (the_hom_sets_of C) . j,i or ((the_comps_of C) . j,j,i) . b₁,(id j) = b₁ )
let f be set ; :: thesis: ( not f in (the_hom_sets_of C) . j,i or ((the_comps_of C) . j,j,i) . f,(id j) = f )
assume f in (the_hom_sets_of C) . j,i ; :: thesis: ((the_comps_of C) . j,j,i) . f,(id j) = f
then A2: f in Hom j,i by Def3;
then reconsider m = f as Morphism of j,i by CAT_1:def 7;
Hom j,j <> {} by CAT_1:56;
hence ((the_comps_of C) . j,j,i) . f,(id j) = m * (id j) by A2, Th14
.= f by A2, CAT_1:58 ;
:: thesis: verum