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, Def7;
then A4: cod f = b by Th18;
A5: g in Hom b,c by A2, Def7;
then A6: dom g = b by Th18;
cod g = c by A5, Th18;
then A7: cod (g * f) = c by A6, A4, Th42;
dom f = a by A3, Th18;
then dom (g * f) = a by A6, A4, Th42;
hence g * f in Hom a,c by A7; :: thesis: verum