let i, j, k, l be Element of ; :: according to ALTCAT_1:def 7,ALTCAT_1:def 17 :: thesis: 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 i' = i, j' = j, k' = k, l' = l as object of ;
let f, g, h be set ; :: thesis: ( 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 ; :: thesis: (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 = <^i',j'^> ;
reconsider f' = f as Morphism of , by A3;
A7: the Arrows of F1() . j,k = <^j',k'^> ;
reconsider g' = g as Morphism of , by A4;
A8: the Arrows of F1() . k,l = <^k',l'^> ;
reconsider h' = h as Morphism of , by A5;
A9: <^i',k'^> <> {} by A3, A4, A6, A7, ALTCAT_1:def 4;
A10: <^j',l'^> <> {} 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,(g' * f') by A3, A4, ALTCAT_1:def 10
.= h' * (g' * f') by A5, A9, ALTCAT_1:def 10
.= F2(i,k,l,(g' * f'),h') by A1, A5, A9
.= F2(i,k,l,F2(i,j,k,f,g),h) by A1, A3, A4
.= F2(i',j',l',f,F2(j',k',l',g,h)) by A2, A3, A4, A5, A6, A7, A8
.= F2(i',j',l',f,(h' * g')) by A1, A4, A5
.= (h' * g') * f' by A1, A3, A10
.= (the Comp of F1() . i,j,l) . (h' * g'),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 ; :: thesis: verum