let C be Category; :: thesis: for i, j, k being Object of C st Hom (i,j) <> {} & Hom (j,k) <> {} holds
for f being Morphism of i,j
for g being Morphism of j,k holds (() . (i,j,k)) . (g,f) = g * f

let i, j, k be Object of C; :: thesis: ( Hom (i,j) <> {} & Hom (j,k) <> {} implies for f being Morphism of i,j
for g being Morphism of j,k holds (() . (i,j,k)) . (g,f) = g * f )

assume that
A1: Hom (i,j) <> {} and
A2: Hom (j,k) <> {} ; :: thesis: for f being Morphism of i,j
for g being Morphism of j,k holds (() . (i,j,k)) . (g,f) = g * f

let f be Morphism of i,j; :: thesis: for g being Morphism of j,k holds (() . (i,j,k)) . (g,f) = g * f
let g be Morphism of j,k; :: thesis: (() . (i,j,k)) . (g,f) = g * f
A3: g in Hom (j,k) by ;
then A4: g in () . (j,k) by Def3;
A5: f in Hom (i,j) by ;
then f in () . (i,j) by Def3;
then A6: [g,f] in [:(() . (j,k)),(() . (i,j)):] by ;
A7: dom g = j by
.= cod f by ;
thus (() . (i,j,k)) . (g,f) = ( the Comp of C | [:(() . (j,k)),(() . (i,j)):]) . [g,f] by Def4
.= the Comp of C . (g,f) by
.= g (*) f by
.= g * f by ; :: thesis: verum