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:25; ( ( 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 7,ALTCAT_1:def 17 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 4;
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 10;
h in <^o3,o4^>
by A6;
then A8:
<^o2,o4^> <> {}
by A4, ALTCAT_1:def 4;
(the Comp of C . i,j,k) . g,f = gg * ff
by A2, A3, ALTCAT_1:def 10;
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 10
.=
(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 10
;
verum