thus incl C is id-preserving :: thesis: incl C is comp-preserving
proof
let a be Object of C; :: according to FUNCTOR0:def 20 :: thesis: (Morph-Map ((incl C),a,a)) . (idm a) = idm ((incl C) . a)
A1: (incl C) . a = a by FUNCTOR0:27;
thus (Morph-Map ((incl C),a,a)) . (idm a) = (incl C) . (idm a) by FUNCTOR0:def 15
.= idm a by Th27
.= idm ((incl C) . a) by A1, ALTCAT_2:34 ; :: thesis: verum
end;
let o1, o2, o3 be Object of C; :: according to FUNCTOR0:def 23 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or for b1 being M3(<^o1,o2^>)
for b2 being M3(<^o2,o3^>) holds (incl C) . (b2 * b1) = ((incl C) . b2) * ((incl C) . b1) )
assume A2: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; :: thesis: for b1 being M3(<^o1,o2^>)
for b2 being M3(<^o2,o3^>) holds (incl C) . (b2 * b1) = ((incl C) . b2) * ((incl C) . b1)
let f be Morphism of o1,o2; :: thesis: for b1 being M3(<^o2,o3^>) holds (incl C) . (b1 * f) = ((incl C) . b1) * ((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 2;
then A3: ( (incl C) . o3 = o3 & (incl C) . (g * f) = g * f ) by Th27, FUNCTOR0:27;
A4: ( (incl C) . o1 = o1 & (incl C) . o2 = o2 ) by FUNCTOR0:27;
( (incl C) . g = g & (incl C) . f = f ) by A2, Th27;
hence (incl C) . (g * f) = ((incl C) . g) * ((incl C) . f) by A2, A4, A3, ALTCAT_2:32; :: thesis: verum