let C be Category; :: thesis: for a, b being Object of C st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (f opp) opp = f

let a, b be Object of C; :: thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds (f opp) opp = f )

assume A1: Hom (a,b) <> {} ; :: thesis: for f being Morphism of a,b holds (f opp) opp = f

then A2: Hom ((b opp),(a opp)) <> {} by Th4;

let f be Morphism of a,b; :: thesis: (f opp) opp = f

thus (f opp) opp = f opp by A2, Def6

.= f by A1, Def6 ; :: thesis: verum

for f being Morphism of a,b holds (f opp) opp = f

let a, b be Object of C; :: thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds (f opp) opp = f )

assume A1: Hom (a,b) <> {} ; :: thesis: for f being Morphism of a,b holds (f opp) opp = f

then A2: Hom ((b opp),(a opp)) <> {} by Th4;

let f be Morphism of a,b; :: thesis: (f opp) opp = f

thus (f opp) opp = f opp by A2, Def6

.= f by A1, Def6 ; :: thesis: verum