Hom (b,a) <> {} by Dfi, A2;
hence for b₁, b₂ being Morphism of b,a st f * b₁ = id b & b₁ * f = id a & f * b₂ = id b & b₂ * f = id a holds
b₁ = b₂ by A1, Th42; :: thesis: verum