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) " = (f ") * (g ")
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) " = (f ") * (g ")
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) " = (f ") * (g ")
let g be Morphism of b,c; :: thesis: ( f is invertible & g is invertible implies (g * f) " = (f ") * (g ") )
assume that
A3: f is invertible and
A4: g is invertible ; :: thesis: (g * f) " = (f ") * (g ")
A1: Hom (a,b) <> {} by A3, Dfi;
A2: Hom (b,c) <> {} by A4, Dfi;
A5: Hom (c,b) <> {} by Dfi, A4;
A6: Hom (b,a) <> {} by Dfi, A3;
then A7: Hom (c,a) <> {} by A5, Th23;
then A8: ((f ") * (g ")) * (g * f) = (((f ") * (g ")) * g) * f by A1, A2, Th25
.= ((f ") * ((g ") * g)) * f by A2, A6, A5, Th25
.= ((f ") * (id b)) * f by A4, Def11
.= (f ") * f by A6, Th29
.= id a by A3, Def11 ;
A9: ( Hom (a,c) <> {} & g * f is invertible ) by A1, A2, A3, A4, Th23, Th45;
(g * f) * ((f ") * (g ")) = g * (f * ((f ") * (g "))) by A1, A2, A7, Th25
.= g * ((f * (f ")) * (g ")) by A1, A6, A5, Th25
.= g * ((id b) * (g ")) by A3, Def11
.= g * (g ") by A5, Th28
.= id c by A4, Def11 ;
hence (g * f) " = (f ") * (g ") by A8, A9, Def11; :: thesis: verum