let C be Category; :: thesis: for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
g (*) f in Hom (a,c)
let a, b, c be Object of C; :: thesis: for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
g (*) f in Hom (a,c)
let f be Morphism of a,b; :: thesis: for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
g (*) f in Hom (a,c)
let g be Morphism of b,c; :: thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies g (*) f in Hom (a,c) )
assume that
A1: Hom (a,b) <> {} and
A2: Hom (b,c) <> {} ; :: thesis: g (*) f in Hom (a,c)
A3: f in Hom (a,b) by A1, Def3;
then A4: cod f = b by Th1;
A5: g in Hom (b,c) by A2, Def3;
then A6: dom g = b by Th1;
cod g = c by A5, Th1;
then A7: cod (g (*) f) = c by A6, A4, Def5;
dom f = a by A3, Th1;
then dom (g (*) f) = a by A6, A4, Def5;
hence g (*) f in Hom (a,c) by A7; :: thesis: verum