let C be Category; :: thesis:
let i, j, k, l be Object of C; :: according to ALTCAT_1:def 5 :: thesis: for b1, b2, b3 being set holds
( not b1 in () . (i,j) or not b2 in () . (j,k) or not b3 in () . (k,l) or (() . (i,k,l)) . (b3,((() . (i,j,k)) . (b2,b1))) = (() . (i,j,l)) . (((() . (j,k,l)) . (b3,b2)),b1) )

let f, g, h be set ; :: thesis: ( not f in () . (i,j) or not g in () . (j,k) or not h in () . (k,l) or (() . (i,k,l)) . (h,((() . (i,j,k)) . (g,f))) = (() . (i,j,l)) . (((() . (j,k,l)) . (h,g)),f) )
assume f in () . (i,j) ; :: thesis: ( not g in () . (j,k) or not h in () . (k,l) or (() . (i,k,l)) . (h,((() . (i,j,k)) . (g,f))) = (() . (i,j,l)) . (((() . (j,k,l)) . (h,g)),f) )
then A1: f in Hom (i,j) by Def3;
then reconsider f9 = f as Morphism of i,j by CAT_1:def 5;
assume g in () . (j,k) ; :: thesis: ( not h in () . (k,l) or (() . (i,k,l)) . (h,((() . (i,j,k)) . (g,f))) = (() . (i,j,l)) . (((() . (j,k,l)) . (h,g)),f) )
then A2: g in Hom (j,k) by Def3;
then reconsider g9 = g as Morphism of j,k by CAT_1:def 5;
assume h in () . (k,l) ; :: thesis: (() . (i,k,l)) . (h,((() . (i,j,k)) . (g,f))) = (() . (i,j,l)) . (((() . (j,k,l)) . (h,g)),f)
then A3: h in Hom (k,l) by Def3;
then reconsider h9 = h as Morphism of k,l by CAT_1:def 5;
A4: ( Hom (j,l) <> {} & (() . (j,k,l)) . (h,g) = h9 * g9 ) by ;
( Hom (i,k) <> {} & (() . (i,j,k)) . (g,f) = g9 * f9 ) by ;
hence (() . (i,k,l)) . (h,((() . (i,j,k)) . (g,f))) = h9 * (g9 * f9) by
.= (h9 * g9) * f9 by
.= (() . (i,j,l)) . (((() . (j,k,l)) . (h,g)),f) by A1, A4, Th13 ;
:: thesis: verum