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 Hom (a,b) <> {} & Hom (b,c) <> {} & 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 Hom (a,b) <> {} & Hom (b,c) <> {} & 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 Hom (a,b) <> {} & Hom (b,c) <> {} & f is invertible & g is invertible holds
g * f is invertible
let g be Morphism of b,c; :: thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} & f is invertible & g is invertible implies g * f is invertible )
assume that
A1: Hom (a,b) <> {} and
A2: Hom (b,c) <> {} ; :: thesis: ( not f is invertible or not g is invertible or g * f is invertible )
assume A3: f is invertible ; :: thesis: ( not g is invertible or g * f is invertible )
then A4: Hom (b,a) <> {} by A1, Th70;
consider f1 being Morphism of b,a such that
A5: f * f1 = id b and
A6: f1 * f = id a by A1, A3, Th70;
assume A7: g is invertible ; :: thesis: g * f is invertible
then A8: Hom (c,b) <> {} by A2, Th70;
consider g1 being Morphism of c,b such that
A9: g * g1 = id c and
A10: g1 * g = id b by A2, A7, Th70;

A11: now

thus A12: Hom (c,a) <> {} by A4, A8, Th51; :: thesis: ex f1g1 being Morphism of c,a st
( (g * f) * f1g1 = id c & f1g1 * (g * f) = id a )
take f1g1 = f1 * g1; :: thesis: ( (g * f) * f1g1 = id c & f1g1 * (g * f) = id a )
thus (g * f) * f1g1 = g * (f * (f1 * g1)) by A1, A2, A12, Th54
.= g * ((id b) * g1) by A1, A4, A5, A8, Th54
.= id c by A8, A9, Th57 ; :: thesis: f1g1 * (g * f) = id a
Hom (a,c) <> {} by A1, A2, Th51;
hence f1g1 * (g * f) = f1 * (g1 * (g * f)) by A4, A8, Th54
.= f1 * ((id b) * f) by A1, A2, A8, A10, Th54
.= id a by A1, A6, Th57 ;
:: thesis: verum

end;

Hom (a,c) <> {} by A1, A2, Th51;
hence g * f is invertible by A11, Th70; :: thesis: verum