let C be Category; :: thesis: for a, b, c being Object of C st a,b are_isomorphic & b,c are_isomorphic holds
a,c are_isomorphic
let a, b, c be Object of C; :: thesis: ( a,b are_isomorphic & b,c are_isomorphic implies a,c are_isomorphic )
assume A1: Hom (a,b) <> {} ; :: according to CAT_1:def 14 :: thesis: ( for f being Morphism of a,b holds not f is invertible or not b,c are_isomorphic or a,c are_isomorphic )
given f being Morphism of a,b such that A2: f is invertible ; :: thesis: ( not b,c are_isomorphic or a,c are_isomorphic )
assume A3: Hom (b,c) <> {} ; :: according to CAT_1:def 14 :: thesis: ( for f being Morphism of b,c holds not f is invertible or a,c are_isomorphic )
given g being Morphism of b,c such that A4: g is invertible ; :: thesis: a,c are_isomorphic
thus Hom (a,c) <> {} by A1, A3, Th51; :: according to CAT_1:def 14 :: thesis: ex f being Morphism of a,c st f is invertible
take g * f ; :: thesis: g * f is invertible
thus g * f is invertible by A1, A2, A3, A4, Th75; :: thesis: verum