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) " = (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 Hom a,b <> {} & Hom b,c <> {} & 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 Hom a,b <> {} & Hom b,c <> {} & f is invertible & g is invertible holds
(g * f) " = (f " ) * (g " )
let g be Morphism of b,c; :: thesis: ( Hom a,b <> {} & Hom b,c <> {} & f is invertible & g is invertible implies (g * f) " = (f " ) * (g " ) )
assume that
A1: Hom a,b <> {} and
A2: Hom b,c <> {} and
A3: f is invertible and
A4: g is invertible ; :: thesis: (g * f) " = (f " ) * (g " )
A5: Hom c,b <> {} by A2, A4, Th70;
A6: Hom b,a <> {} by A1, A3, Th70;
then A7: Hom c,a <> {} by A5, Th51;
then A8: ((f " ) * (g " )) * (g * f) = (((f " ) * (g " )) * g) * f by A1, A2, Th54
.= ((f " ) * ((g " ) * g)) * f by A2, A6, A5, Th54
.= ((f " ) * (id b)) * f by A2, A4, Def14
.= (f " ) * f by A6, Th58
.= id a by A1, A3, Def14 ;
A9: ( Hom a,c <> {} & g * f is invertible ) by A1, A2, A3, A4, Th51, Th75;
(g * f) * ((f " ) * (g " )) = g * (f * ((f " ) * (g " ))) by A1, A2, A7, Th54
.= g * ((f * (f " )) * (g " )) by A1, A6, A5, Th54
.= g * ((id b) * (g " )) by A1, A3, Def14
.= g * (g " ) by A5, Th57
.= id c by A2, A4, Def14 ;
hence (g * f) " = (f " ) * (g " ) by A8, A9, Def14; :: thesis: verum