thus
incl C is id-preserving
:: thesis: incl C is comp-preserving _{1} being M3(<^o1,o2^>)

for b_{2} being M3(<^o2,o3^>) holds (incl C) . (b_{2} * b_{1}) = ((incl C) . b_{2}) * ((incl C) . b_{1}) )

assume A2: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; :: thesis: for b_{1} being M3(<^o1,o2^>)

for b_{2} being M3(<^o2,o3^>) holds (incl C) . (b_{2} * b_{1}) = ((incl C) . b_{2}) * ((incl C) . b_{1})

let f be Morphism of o1,o2; :: thesis: for b_{1} being M3(<^o2,o3^>) holds (incl C) . (b_{1} * f) = ((incl C) . b_{1}) * ((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

proof

let o1, o2, o3 be Object of C; :: according to FUNCTOR0:def 23 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or for b
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;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

for b

assume A2: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; :: thesis: for b

for b

let f be Morphism of o1,o2; :: thesis: for b

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