let i, j, k, l be Element of F1(); ALTCAT_1:def 7,ALTCAT_1:def 17 for b1, b2, b3 being set holds
( not b1 in the Arrows of F1() . i,j or not b2 in the Arrows of F1() . j,k or not b3 in the Arrows of F1() . k,l or (the Comp of F1() . i,k,l) . b3,((the Comp of F1() . i,j,k) . b2,b1) = (the Comp of F1() . i,j,l) . ((the Comp of F1() . j,k,l) . b3,b2),b1 )
set alt = F1();
set IT = the Comp of F1();
set B = the Arrows of F1();
reconsider i9 = i, j9 = j, k9 = k, l9 = l as object of F1() ;
let f, g, h be set ; ( not f in the Arrows of F1() . i,j or not g in the Arrows of F1() . j,k or not h in the Arrows of F1() . k,l or (the Comp of F1() . i,k,l) . h,((the Comp of F1() . i,j,k) . g,f) = (the Comp of F1() . i,j,l) . ((the Comp of F1() . j,k,l) . h,g),f )
assume that
A3:
f in the Arrows of F1() . i,j
and
A4:
g in the Arrows of F1() . j,k
and
A5:
h in the Arrows of F1() . k,l
; (the Comp of F1() . i,k,l) . h,((the Comp of F1() . i,j,k) . g,f) = (the Comp of F1() . i,j,l) . ((the Comp of F1() . j,k,l) . h,g),f
A6:
the Arrows of F1() . i,j = <^i9,j9^>
;
reconsider f9 = f as Morphism of i9,j9 by A3;
A7:
the Arrows of F1() . j,k = <^j9,k9^>
;
reconsider g9 = g as Morphism of j9,k9 by A4;
A8:
the Arrows of F1() . k,l = <^k9,l9^>
;
reconsider h9 = h as Morphism of k9,l9 by A5;
A9:
<^i9,k9^> <> {}
by A3, A4, A6, A7, ALTCAT_1:def 4;
A10:
<^j9,l9^> <> {}
by A4, A5, A7, A8, ALTCAT_1:def 4;
thus (the Comp of F1() . i,k,l) . h,((the Comp of F1() . i,j,k) . g,f) =
(the Comp of F1() . i,k,l) . h,(g9 * f9)
by A3, A4, ALTCAT_1:def 10
.=
h9 * (g9 * f9)
by A5, A9, ALTCAT_1:def 10
.=
F2(i,k,l,(g9 * f9),h9)
by A1, A5, A9
.=
F2(i,k,l,F2(i,j,k,f,g),h)
by A1, A3, A4
.=
F2(i9,j9,l9,f,F2(j9,k9,l9,g,h))
by A2, A3, A4, A5, A6, A7, A8
.=
F2(i9,j9,l9,f,(h9 * g9))
by A1, A4, A5
.=
(h9 * g9) * f9
by A1, A3, A10
.=
(the Comp of F1() . i,j,l) . (h9 * g9),f
by A3, A10, ALTCAT_1:def 10
.=
(the Comp of F1() . i,j,l) . ((the Comp of F1() . j,k,l) . h,g),f
by A4, A5, ALTCAT_1:def 10
; verum