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; ( ( 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)
; C is associative
let i, j, k, l be Element of C; ALTCAT_1:def 5,ALTCAT_1:def 15 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 ; ( 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)
; ( 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)
; ( 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)
; ( 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
;
verum