let C be Category; :: thesis: for a being Object of C holds (id a) opp = id (a opp)
let a be Object of C; :: thesis: (id a) opp = id (a opp)
for b being Object of (C opp) holds
( ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) & ( Hom (b,(a opp)) <> {} implies for f being Morphism of b,a opp holds ((id a) opp) (*) f = f ) ) by Lm1;
hence (id a) opp = id (a opp) by CAT_1:def 12; :: thesis: verum