let C be Category; :: thesis: for a, b being Object of C
for f being Morphism of a,b st f is invertible holds
f " is invertible
let a, b be Object of C; :: thesis: for f being Morphism of a,b st f is invertible holds
f " is invertible
let f be Morphism of a,b; :: thesis: ( f is invertible implies f " is invertible )
assume A1: f is invertible ; :: thesis: f " is invertible
then A2: f * (f ") = id b by Def15;
A3: Hom (a,b) <> {} by A1;
( Hom (b,a) <> {} & (f ") * f = id a ) by A1, Def15;
hence f " is invertible by A3, A2; :: thesis: verum