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_{1} being set st

( b_{1} in (the_hom_sets_of C) . (j,j) & ( for b_{2} being Element of the carrier of C

for b_{3} being set holds

( not b_{3} in (the_hom_sets_of C) . (j,b_{2}) or ((the_comps_of C) . (j,j,b_{2})) . (b_{3},b_{1}) = b_{3} ) ) )

take id j ; :: thesis: ( id j in (the_hom_sets_of C) . (j,j) & ( for b_{1} being Element of the carrier of C

for b_{2} being set holds

( not b_{2} in (the_hom_sets_of C) . (j,b_{1}) or ((the_comps_of C) . (j,j,b_{1})) . (b_{2},(id j)) = b_{2} ) ) )

thus id j in (the_hom_sets_of C) . (j,j) by Th12; :: thesis: for b_{1} being Element of the carrier of C

for b_{2} being set holds

( not b_{2} in (the_hom_sets_of C) . (j,b_{1}) or ((the_comps_of C) . (j,j,b_{1})) . (b_{2},(id j)) = b_{2} )

let i be Object of C; :: thesis: for b_{1} being set holds

( not b_{1} in (the_hom_sets_of C) . (j,i) or ((the_comps_of C) . (j,j,i)) . (b_{1},(id j)) = b_{1} )

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

thus the_comps_of C is with_left_units :: thesis: the_comps_of C is with_right_units

proof

let j be Object of C; :: according to ALTCAT_1:def 6 :: thesis: ex b
let i be Object of C; :: according to ALTCAT_1:def 7 :: thesis: ex b_{1} being set st

( b_{1} in (the_hom_sets_of C) . (i,i) & ( for b_{2} being Element of the carrier of C

for b_{3} being set holds

( not b_{3} in (the_hom_sets_of C) . (b_{2},i) or ((the_comps_of C) . (b_{2},i,i)) . (b_{1},b_{3}) = b_{3} ) ) )

take id i ; :: thesis: ( id i in (the_hom_sets_of C) . (i,i) & ( for b_{1} being Element of the carrier of C

for b_{2} being set holds

( not b_{2} in (the_hom_sets_of C) . (b_{1},i) or ((the_comps_of C) . (b_{1},i,i)) . ((id i),b_{2}) = b_{2} ) ) )

thus id i in (the_hom_sets_of C) . (i,i) by Th12; :: thesis: for b_{1} being Element of the carrier of C

for b_{2} being set holds

( not b_{2} in (the_hom_sets_of C) . (b_{1},i) or ((the_comps_of C) . (b_{1},i,i)) . ((id i),b_{2}) = b_{2} )

let j be Object of C; :: thesis: for b_{1} being set holds

( not b_{1} in (the_hom_sets_of C) . (j,i) or ((the_comps_of C) . (j,i,i)) . ((id i),b_{1}) = b_{1} )

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;( b

for b

( not b

take id i ; :: thesis: ( id i in (the_hom_sets_of C) . (i,i) & ( for b

for b

( not b

thus id i in (the_hom_sets_of C) . (i,i) by Th12; :: thesis: for b

for b

( not b

let j be Object of C; :: thesis: for b

( not 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

( b

for b

( not b

take id j ; :: thesis: ( id j in (the_hom_sets_of C) . (j,j) & ( for b

for b

( not b

thus id j in (the_hom_sets_of C) . (j,j) by Th12; :: thesis: for b

for b

( not b

let i be Object of C; :: thesis: for b

( not 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