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