let x1, x2 be set ; :: thesis: for C being Category
for p1, p2 being Morphism of C st x1 <> x2 holds
(x1,x2 --> p1,p2) opp = x1,x2 --> (p1 opp ),(p2 opp )
let C be Category; :: thesis: for p1, p2 being Morphism of C st x1 <> x2 holds
(x1,x2 --> p1,p2) opp = x1,x2 --> (p1 opp ),(p2 opp )
let p1, p2 be Morphism of C; :: thesis: ( x1 <> x2 implies (x1,x2 --> p1,p2) opp = x1,x2 --> (p1 opp ),(p2 opp ) )
set F = x1,x2 --> p1,p2;
set F9 = x1,x2 --> (p1 opp ),(p2 opp );
assume A1: x1 <> x2 ; :: thesis: (x1,x2 --> p1,p2) opp = x1,x2 --> (p1 opp ),(p2 opp )

now

let x be set ; :: thesis: ( x in {x1,x2} implies ((x1,x2 --> p1,p2) opp ) /. x = (x1,x2 --> (p1 opp ),(p2 opp )) /. x )
assume A2: x in {x1,x2} ; :: thesis: ((x1,x2 --> p1,p2) opp ) /. x = (x1,x2 --> (p1 opp ),(p2 opp )) /. x
then ( x = x1 or x = x2 ) by TARSKI:def 2;
then ( ( (x1,x2 --> p1,p2) /. x = p1 & (x1,x2 --> (p1 opp ),(p2 opp )) /. x = p1 opp ) or ( (x1,x2 --> p1,p2) /. x = p2 & (x1,x2 --> (p1 opp ),(p2 opp )) /. x = p2 opp ) ) by A1, Th7;
hence ((x1,x2 --> p1,p2) opp ) /. x = (x1,x2 --> (p1 opp ),(p2 opp )) /. x by A2, Def5; :: thesis: verum

end;

hence (x1,x2 --> p1,p2) opp = x1,x2 --> (p1 opp ),(p2 opp ) by Th1; :: thesis: verum