let C be composable with_identities CategoryStr ; :: thesis: for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
Hom (a,c) <> {}
let a, b, c be Object of C; :: thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies Hom (a,c) <> {} )
assume A1: Hom (a,b) <> {} ; :: thesis: ( not Hom (b,c) <> {} or Hom (a,c) <> {} )
set f1 = the Morphism of a,b;
consider f11, f12 being morphism of C such that
A2: ( a = f11 & b = f12 & the Morphism of a,b |> f11 & f12 |> the Morphism of a,b ) by A1, Th16;
assume A3: Hom (b,c) <> {} ; :: thesis: Hom (a,c) <> {}
set f2 = the Morphism of b,c;
consider f22, f23 being morphism of C such that
A4: ( b = f22 & c = f23 & the Morphism of b,c |> f22 & f23 |> the Morphism of b,c ) by A3, Th16;
A5: ( C is left_composable & C is right_composable ) by CAT_6:def 11;
not C is empty by A2, CAT_6:1;
then A6: the Morphism of b,c |> the Morphism of a,b by A2, A4, Th3, CAT_6:22;
( f23 |> the Morphism of b,c (*) the Morphism of a,b & the Morphism of b,c (*) the Morphism of a,b |> f11 ) by A2, A4, A6, A5, CAT_6:def 8, CAT_6:def 9;
then the Morphism of b,c (*) the Morphism of a,b in Hom (a,c) by A2, A4;
hence Hom (a,c) <> {} ; :: thesis: verum