let C be Category; :: thesis: for a, b being Object of (C opp )
for f being Morphism of a,b st Hom a,b <> {} holds
opp f is Morphism of opp b, opp a
let a, b be Object of (C opp ); :: thesis: for f being Morphism of a,b st Hom a,b <> {} holds
opp f is Morphism of opp b, opp a
let f be Morphism of a,b; :: thesis: ( Hom a,b <> {} implies opp f is Morphism of opp b, opp a )
assume Hom a,b <> {} ; :: thesis: opp f is Morphism of opp b, opp a
then f in Hom a,b by CAT_1:def 7;
then opp f in Hom (opp b),(opp a) by Th14;
hence opp f is Morphism of opp b, opp a by CAT_1:def 7; :: thesis: verum