let C be Category; :: thesis: for a, b, c, d being Object of C
for f being Morphism of a,b
for g being Morphism of b,c
for h being Morphism of c,d st Hom a,b <> {} & Hom b,c <> {} & Hom c,d <> {} holds
(h * g) * f = h * (g * f)
let a, b, c, d be Object of C; :: thesis: for f being Morphism of a,b
for g being Morphism of b,c
for h being Morphism of c,d st Hom a,b <> {} & Hom b,c <> {} & Hom c,d <> {} holds
(h * g) * f = h * (g * f)
let f be Morphism of a,b; :: thesis: for g being Morphism of b,c
for h being Morphism of c,d st Hom a,b <> {} & Hom b,c <> {} & Hom c,d <> {} holds
(h * g) * f = h * (g * f)
let g be Morphism of b,c; :: thesis: for h being Morphism of c,d st Hom a,b <> {} & Hom b,c <> {} & Hom c,d <> {} holds
(h * g) * f = h * (g * f)
let h be Morphism of c,d; :: thesis: ( Hom a,b <> {} & Hom b,c <> {} & Hom c,d <> {} implies (h * g) * f = h * (g * f) )
assume that
A1: Hom a,b <> {} and
A2: Hom b,c <> {} and
A3: Hom c,d <> {} ; :: thesis: (h * g) * f = h * (g * f)
A4: Hom a,c <> {} by A1, A2, Th51;
h in Hom c,d by A3, Def7;
then A5: dom h = c by Th18;
g in Hom b,c by A2, Def7;
then A6: ( cod g = c & dom g = b ) by Th18;
reconsider hh = h as Morphism of C ;
reconsider gg = g as Morphism of C ;
reconsider ff = f as Morphism of C ;
f in Hom a,b by A1, Def7;
then A7: cod f = b by Th18;
Hom b,d <> {} by A2, A3, Th51;
hence (h * g) * f = (h * g) * ff by A1, Def13
.= (hh * gg) * ff by A2, A3, Def13
.= hh * (gg * ff) by A5, A6, A7, Th43
.= hh * (g * f) by A1, A2, Def13
.= h * (g * f) by A3, A4, Def13 ;
:: thesis: verum