let C be composable with_identities CategoryStr ; :: thesis: for a, b, c being Object of C
for f1 being Morphism of a,b
for f2 being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
f2 |> f1
let a, b, c be Object of C; :: thesis: for f1 being Morphism of a,b
for f2 being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
f2 |> f1
let f1 be Morphism of a,b; :: thesis: for f2 being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
f2 |> f1
let f2 be Morphism of b,c; :: thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies f2 |> f1 )
assume Hom (a,b) <> {} ; :: thesis: ( not Hom (b,c) <> {} or f2 |> f1 )
then consider f11, f12 being morphism of C such that
A1: ( a = f11 & b = f12 & f1 |> f11 & f12 |> f1 ) by Th16;
assume Hom (b,c) <> {} ; :: thesis: f2 |> f1
then consider f21, f22 being morphism of C such that
A2: ( b = f21 & c = f22 & f2 |> f21 & f22 |> f2 ) by Th16;
not C is empty by A1, CAT_6:1;
hence f2 |> f1 by A1, A2, Th3, CAT_6:22; :: thesis: verum