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, Th19;
h in Hom (c,d) by A3, Def3;
then A5: dom h = c by Th1;
g in Hom (b,c) by A2, Def3;
then A6: ( cod g = c & dom g = b ) by Th1;
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, Def3;
then A7: cod f = b by Th1;
Hom (b,d) <> {} by A2, A3, Th19;
hence (h * g) * f = (h * g) (*) ff by A1, Def11
.= (hh (*) gg) (*) ff by A2, A3, Def11
.= hh (*) (gg (*) ff) by A5, A6, A7, Def6
.= hh (*) (g * f) by A1, A2, Def11
.= h * (g * f) by A3, A4, Def11 ;
:: thesis: verum