let C be Category; 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; 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; 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; ( Hom (a,b) <> {} & Hom (b,c) <> {} implies g (*) f in Hom (a,c) )
assume that
A1:
Hom (a,b) <> {}
and
A2:
Hom (b,c) <> {}
; 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; verum