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 b_{1}, b_{2}, b_{3} being set holds

( not b_{1} in the Arrows of C . (i,j) or not b_{2} in the Arrows of C . (j,k) or not b_{3} in the Arrows of C . (k,l) or ( the Comp of C . (i,k,l)) . (b_{3},(( the Comp of C . (i,j,k)) . (b_{2},b_{1}))) = ( the Comp of C . (i,j,l)) . ((( the Comp of C . (j,k,l)) . (b_{3},b_{2})),b_{1}) )

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 A4, ALTCAT_1:def 2;

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 A3, A6, ALTCAT_1:def 8;

h in <^o3,o4^> by A6;

then A8: <^o2,o4^> <> {} by A4, ALTCAT_1:def 2;

( the Comp of C . (i,j,k)) . (g,f) = gg * ff by A2, A3, ALTCAT_1:def 8;

hence ( the Comp of C . (i,k,l)) . (h,(( the Comp of C . (i,j,k)) . (g,f))) = hh * (gg * ff) by A6, A5, ALTCAT_1:def 8

.= (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 A2, A8, A7, ALTCAT_1:def 8 ;

:: thesis: verum

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 b

( not b

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 A4, ALTCAT_1:def 2;

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 A3, A6, ALTCAT_1:def 8;

h in <^o3,o4^> by A6;

then A8: <^o2,o4^> <> {} by A4, ALTCAT_1:def 2;

( the Comp of C . (i,j,k)) . (g,f) = gg * ff by A2, A3, ALTCAT_1:def 8;

hence ( the Comp of C . (i,k,l)) . (h,(( the Comp of C . (i,j,k)) . (g,f))) = hh * (gg * ff) by A6, A5, ALTCAT_1:def 8

.= (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 A2, A8, A7, ALTCAT_1:def 8 ;

:: thesis: verum