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 )
given f being Morphism of a,b such that A1: f is invertible ; :: according to CAT_1:def 20 :: thesis: ( not b,c are_isomorphic or a,c are_isomorphic )
given g being Morphism of b,c such that A2: g is invertible ; :: according to CAT_1:def 20 :: thesis: a,c are_isomorphic
take g * f ; :: according to CAT_1:def 20 :: thesis: g * f is invertible
thus g * f is invertible by A1, A2, Th40; :: thesis: verum