f in Hom ((a opp),(b opp)) by A1, CAT_1:def 5;
then f in Hom (b,a) by Th4;
hence f is Morphism of b,a by CAT_1:def 5; :: thesis: verum