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 7 :: 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 Th12; :: 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 5;
Hom (i,i) <> {} ;
hence ((the_comps_of C) . (j,i,i)) . ((id i),f) = (id i) * m by A1, Th13
.= f by A1, CAT_1:28 ;
:: thesis: verum

end;

let j be Object of C; :: according to ALTCAT_1:def 6 :: 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 Th12; :: 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 5;
Hom (j,j) <> {} ;
hence ((the_comps_of C) . (j,j,i)) . (f,(id j)) = m * (id j) by A2, Th13
.= f by A2, CAT_1:29 ;
:: thesis: verum