let i, j, k, l be Element of F1(); ALTCAT_1:def 5,ALTCAT_1:def 15 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 2;
A10:
<^j9,l9^> <> {}
by A4, A5, A7, A8, ALTCAT_1:def 2;
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 8
.=
h9 * (g9 * f9)
by A5, A9, ALTCAT_1:def 8
.=
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 8
.=
( the Comp of F1() . (i,j,l)) . ((( the Comp of F1() . (j,k,l)) . (h,g)),f)
by A4, A5, ALTCAT_1:def 8
; verum