thus incl C is id-preserving :: thesis: incl C is comp-preserving

proof

let a be object of C; :: according to FUNCTOR0:def 21 :: thesis: (Morph-Map (incl C),a,a) . (idm a) = idm ((incl C) . a)
A1: (incl C) . a = a by FUNCTOR0:28;
thus (Morph-Map (incl C),a,a) . (idm a) = (incl C) . (idm a) by FUNCTOR0:def 16
.= idm a by Th28
.= idm ((incl C) . a) by A1, ALTCAT_2:35 ; :: thesis: verum

end;

let o1, o2, o3 be object of C; :: according to FUNCTOR0:def 24 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or for b₁ being Element of <^o1,o2^>
for b₂ being Element of <^o2,o3^> holds (incl C) . (b₂ * b₁) = ((incl C) . b₂) * ((incl C) . b₁) )
assume A2: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; :: thesis: for b₁ being Element of <^o1,o2^>
for b₂ being Element of <^o2,o3^> holds (incl C) . (b₂ * b₁) = ((incl C) . b₂) * ((incl C) . b₁)
let f be Morphism of o1,o2; :: thesis: for b₁ being Element of <^o2,o3^> holds (incl C) . (b₁ * f) = ((incl C) . b₁) * ((incl C) . f)
let g be Morphism of o2,o3; :: thesis: (incl C) . (g * f) = ((incl C) . g) * ((incl C) . f)
<^o1,o3^> <> {} by A2, ALTCAT_1:def 4;
then ( (incl C) . o1 = o1 & (incl C) . o2 = o2 & (incl C) . o3 = o3 & (incl C) . g = g & (incl C) . f = f & (incl C) . (g * f) = g * f ) by A2, Th28, FUNCTOR0:28;
hence (incl C) . (g * f) = ((incl C) . g) * ((incl C) . f) by A2, ALTCAT_2:33; :: thesis: verum