let C be Category; :: thesis:
thus the_comps_of C is with_left_units :: thesis:
proof
let i be Object of C; :: according to ALTCAT_1:def 7 :: thesis: ex b1 being set st
( b1 in () . (i,i) & ( for b2 being Element of the carrier of C
for b3 being set holds
( not b3 in () . (b2,i) or (() . (b2,i,i)) . (b1,b3) = b3 ) ) )

take id i ; :: thesis: ( id i in () . (i,i) & ( for b1 being Element of the carrier of C
for b2 being set holds
( not b2 in () . (b1,i) or (() . (b1,i,i)) . ((id i),b2) = b2 ) ) )

thus id i in () . (i,i) by Th12; :: thesis: for b1 being Element of the carrier of C
for b2 being set holds
( not b2 in () . (b1,i) or (() . (b1,i,i)) . ((id i),b2) = b2 )

let j be Object of C; :: thesis: for b1 being set holds
( not b1 in () . (j,i) or (() . (j,i,i)) . ((id i),b1) = b1 )

let f be set ; :: thesis: ( not f in () . (j,i) or (() . (j,i,i)) . ((id i),f) = f )
assume f in () . (j,i) ; :: thesis: (() . (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 (() . (j,i,i)) . ((id i),f) = (id i) * m by
.= f by ;
:: thesis: verum
end;
let j be Object of C; :: according to ALTCAT_1:def 6 :: thesis: ex b1 being set st
( b1 in () . (j,j) & ( for b2 being Element of the carrier of C
for b3 being set holds
( not b3 in () . (j,b2) or (() . (j,j,b2)) . (b3,b1) = b3 ) ) )

take id j ; :: thesis: ( id j in () . (j,j) & ( for b1 being Element of the carrier of C
for b2 being set holds
( not b2 in () . (j,b1) or (() . (j,j,b1)) . (b2,(id j)) = b2 ) ) )

thus id j in () . (j,j) by Th12; :: thesis: for b1 being Element of the carrier of C
for b2 being set holds
( not b2 in () . (j,b1) or (() . (j,j,b1)) . (b2,(id j)) = b2 )

let i be Object of C; :: thesis: for b1 being set holds
( not b1 in () . (j,i) or (() . (j,j,i)) . (b1,(id j)) = b1 )

let f be set ; :: thesis: ( not f in () . (j,i) or (() . (j,j,i)) . (f,(id j)) = f )
assume f in () . (j,i) ; :: thesis: (() . (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 (() . (j,j,i)) . (f,(id j)) = m * (id j) by
.= f by ;
:: thesis: verum