thus ( C is associative implies for o1, o2, o3, o4 being Object of C
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f) ) by ALTCAT_1:21; :: thesis: ( ( for o1, o2, o3, o4 being Object of C
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f) ) implies C is associative )

assume A1: for o1, o2, o3, o4 being Object of C
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f) ; :: thesis: C is associative
let i, j, k, l be Element of C; :: according to ALTCAT_1:def 5,ALTCAT_1:def 15 :: thesis: for b1, b2, b3 being set holds
( not b1 in the Arrows of C . (i,j) or not b2 in the Arrows of C . (j,k) or not b3 in the Arrows of C . (k,l) or ( the Comp of C . (i,k,l)) . (b3,(( the Comp of C . (i,j,k)) . (b2,b1))) = ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (b3,b2)),b1) )

reconsider o1 = i, o2 = j, o3 = k, o4 = l as Object of C ;
let f, g, h be set ; :: thesis: ( not f in the Arrows of C . (i,j) or not g in the Arrows of C . (j,k) or not h in the Arrows of C . (k,l) or ( the Comp of C . (i,k,l)) . (h,(( the Comp of C . (i,j,k)) . (g,f))) = ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (h,g)),f) )
assume A2: f in the Arrows of C . (i,j) ; :: thesis: ( not g in the Arrows of C . (j,k) or not h in the Arrows of C . (k,l) or ( the Comp of C . (i,k,l)) . (h,(( the Comp of C . (i,j,k)) . (g,f))) = ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (h,g)),f) )
then reconsider ff = f as Morphism of o1,o2 ;
assume A3: g in the Arrows of C . (j,k) ; :: thesis: ( not h in the Arrows of C . (k,l) or ( the Comp of C . (i,k,l)) . (h,(( the Comp of C . (i,j,k)) . (g,f))) = ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (h,g)),f) )
then A4: g in <^o2,o3^> ;
f in <^o1,o2^> by A2;
then A5: <^o1,o3^> <> {} by ;
reconsider gg = g as Morphism of o2,o3 by A3;
assume A6: h in the Arrows of C . (k,l) ; :: thesis: ( the Comp of C . (i,k,l)) . (h,(( the Comp of C . (i,j,k)) . (g,f))) = ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (h,g)),f)
then reconsider hh = h as Morphism of o3,o4 ;
A7: ( the Comp of C . (j,k,l)) . (h,g) = hh * gg by ;
h in <^o3,o4^> by A6;
then A8: <^o2,o4^> <> {} by ;
( the Comp of C . (i,j,k)) . (g,f) = gg * ff by ;
hence ( the Comp of C . (i,k,l)) . (h,(( the Comp of C . (i,j,k)) . (g,f))) = hh * (gg * ff) by
.= (hh * gg) * ff by A1, A2, A3, A6
.= ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (h,g)),f) by ;
:: thesis: verum