set J = id K;
id K is monomorphism by Def8;
hence id K is isomorphism by Def12; :: thesis: verum