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 b1 being set st
( b1 in (the_hom_sets_of C) . (i,i) & ( for b2 being Element of the carrier of C
for b3 being set holds
( not b3 in (the_hom_sets_of C) . (b2,i) or ((the_comps_of C) . (b2,i,i)) . (b1,b3) = b3 ) ) )
take id i ; :: thesis: ( id i in (the_hom_sets_of C) . (i,i) & ( for b1 being Element of the carrier of C
for b2 being set holds
( not b2 in (the_hom_sets_of C) . (b1,i) or ((the_comps_of C) . (b1,i,i)) . ((id i),b2) = b2 ) ) )
thus id i in (the_hom_sets_of C) . (i,i) by Th12; :: thesis: for b1 being Element of the carrier of C
for b2 being set holds
( not b2 in (the_hom_sets_of C) . (b1,i) or ((the_comps_of C) . (b1,i,i)) . ((id i),b2) = b2 )
let j be Object of C; :: thesis: for b1 being set holds
( not b1 in (the_hom_sets_of C) . (j,i) or ((the_comps_of C) . (j,i,i)) . ((id i),b1) = b1 )
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 b1 being set st
( b1 in (the_hom_sets_of C) . (j,j) & ( for b2 being Element of the carrier of C
for b3 being set holds
( not b3 in (the_hom_sets_of C) . (j,b2) or ((the_comps_of C) . (j,j,b2)) . (b3,b1) = b3 ) ) )
take id j ; :: thesis: ( id j in (the_hom_sets_of C) . (j,j) & ( for b1 being Element of the carrier of C
for b2 being set holds
( not b2 in (the_hom_sets_of C) . (j,b1) or ((the_comps_of C) . (j,j,b1)) . (b2,(id j)) = b2 ) ) )
thus id j in (the_hom_sets_of C) . (j,j) by Th12; :: thesis: for b1 being Element of the carrier of C
for b2 being set holds
( not b2 in (the_hom_sets_of C) . (j,b1) or ((the_comps_of C) . (j,j,b1)) . (b2,(id j)) = b2 )
let i be Object of C; :: thesis: for b1 being set holds
( not b1 in (the_hom_sets_of C) . (j,i) or ((the_comps_of C) . (j,j,i)) . (b1,(id j)) = b1 )
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