let C be Category; :: thesis: for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st f is invertible & g is invertible holds
g * f is invertible
let a, b, c be Object of C; :: thesis: for f being Morphism of a,b
for g being Morphism of b,c st f is invertible & g is invertible holds
g * f is invertible
let f be Morphism of a,b; :: thesis: for g being Morphism of b,c st f is invertible & g is invertible holds
g * f is invertible
let g be Morphism of b,c; :: thesis: ( f is invertible & g is invertible implies g * f is invertible )
assume A1: f is invertible ; :: thesis: ( not g is invertible or g * f is invertible )
then A2: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) ;
consider f1 being Morphism of b,a such that
A3: f * f1 = id b and
A4: f1 * f = id a by A1;
assume A5: g is invertible ; :: thesis: g * f is invertible
then A6: ( Hom (b,c) <> {} & Hom (c,b) <> {} ) ;
consider g1 being Morphism of c,b such that
A7: g * g1 = id c and
A8: g1 * g = id b by A5;
Hom (a,c) <> {} by A2, A6, Th19;
hence g * f is invertible by A9; :: thesis: verum