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

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