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

proof

let o be object of A; :: according to FUNCTOR0:def 21 :: 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 Th31
.= idm ((id A) . o) by Th30 ;
:: 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 24 :: 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 4;
A4: ( (id A) . o1 = o1 & (id A) . o2 = o2 & (id A) . o3 = o3 ) by Th30;
( (id A) . g = g & (id A) . f = f ) by A1, A2, Th32;
hence (id A) . (g * f) = ((id A) . g) * ((id A) . f) by A3, A4, Th32; :: thesis: verum

end;

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