let C be Category; 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; 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; 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; ( f is invertible & g is invertible implies (g * f) " = (f ") * (g ") )
assume that
A1:
f is invertible
and
A2:
g is invertible
; (g * f) " = (f ") * (g ")
A3:
Hom (a,b) <> {}
by A1;
A4:
Hom (b,c) <> {}
by A2;
A5:
Hom (c,b) <> {}
by A2;
A6:
Hom (b,a) <> {}
by A1;
then A7:
Hom (c,a) <> {}
by A5, Th19;
then A8: ((f ") * (g ")) * (g * f) =
(((f ") * (g ")) * g) * f
by A3, A4, Th21
.=
((f ") * ((g ") * g)) * f
by A4, A6, A5, Th21
.=
((f ") * (id b)) * f
by A2, Def15
.=
(f ") * f
by A6, Th24
.=
id a
by A1, Def15
;
A9:
( Hom (a,c) <> {} & g * f is invertible )
by A1, A2, Th19, Th40;
(g * f) * ((f ") * (g ")) =
g * (f * ((f ") * (g ")))
by A3, A4, A7, Th21
.=
g * ((f * (f ")) * (g "))
by A3, A6, A5, Th21
.=
g * ((id b) * (g "))
by A1, Def15
.=
g * (g ")
by A5, Th23
.=
id c
by A2, Def15
;
hence
(g * f) " = (f ") * (g ")
by A8, A9, Def15; verum