Hom (b,a) <> {} by A1, A2, Th70;
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, Th71; :: thesis: verum