thus id A is id-preserving :: thesis: id A is comp-preserving

proof

let o be Object of A; :: according to FUNCTOR0:def 20 :: thesis: (Morph-Map ((id A),o,o)) . (idm o) = idm ((id A) . o)
<^o,o^> <> {} by ALTCAT_2:def 7;
hence (Morph-Map ((id A),o,o)) . (idm o) = idm o by Th30
.= idm ((id A) . o) by Th29 ;
:: thesis: verum

end;

set F = id A;
id A is comp-preserving

proof

let o1, o2, o3 be Object of A; :: according to FUNCTOR0:def 23 :: thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds (id A) . (g * f) = ((id A) . g) * ((id A) . f) )
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} ; :: thesis: for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds (id A) . (g * f) = ((id A) . g) * ((id A) . f)
let f be Morphism of o1,o2; :: thesis: for g being Morphism of o2,o3 holds (id A) . (g * f) = ((id A) . g) * ((id A) . f)
let g be Morphism of o2,o3; :: thesis: (id A) . (g * f) = ((id A) . g) * ((id A) . f)
A3: <^o1,o3^> <> {} by A1, A2, ALTCAT_1:def 2;
A4: (id A) . o1 = o1 by Th29;
A5: (id A) . o2 = o2 by Th29;
A6: (id A) . o3 = o3 by Th29;
A7: (id A) . g = g by A2, Th31;
(id A) . f = f by A1, Th31;
hence (id A) . (g * f) = ((id A) . g) * ((id A) . f) by A3, A4, A5, A6, A7, Th31; :: thesis: verum

end;

hence id A is comp-preserving ; :: thesis: verum