let A, B be category; :: thesis: ( A,B are_opposite implies dualizing-func A,B is bijective )
assume A1: A,B are_opposite ; :: thesis: dualizing-func A,B is bijective
set F = dualizing-func A,B;
deffunc H₁( set ) -> set = $1;
deffunc H₂( set , set , set ) -> set = $3;
A2: for a being object of A holds (dualizing-func A,B) . a = H₁(a) by A1, Def5;
A3: for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (dualizing-func A,B) . f = H₂(a,b,f) by A1, Def5;
A4: for a, b being object of A st H₁(a) = H₁(b) holds
a = b ;
A5: for a, b being object of A st <^a,b^> <> {} holds
for f, g being Morphism of a,b st H₂(a,b,f) = H₂(a,b,g) holds
f = g ;

A6: now

let a, b be object of B; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( b = H₁(c) & a = H₁(d) & <^c,d^> <> {} & f = H₂(c,d,g) ) )
reconsider a9 = a, b9 = b as object of A by A1, Def3;
A7: <^a,b^> = <^b9,a9^> by A1, Th9;
assume A8: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( b = H₁(c) & a = H₁(d) & <^c,d^> <> {} & f = H₂(c,d,g) )
let f be Morphism of a,b; :: thesis: ex c, d being object of A ex g being Morphism of c,d st
( b = H₁(c) & a = H₁(d) & <^c,d^> <> {} & f = H₂(c,d,g) )
thus ex c, d being object of A ex g being Morphism of c,d st
( b = H₁(c) & a = H₁(d) & <^c,d^> <> {} & f = H₂(c,d,g) ) by A7, A8; :: thesis: verum

end;

dualizing-func A,B is bijective from YELLOW18:sch 12(A2, A3, A4, A5, A6);
hence dualizing-func A,B is bijective ; :: thesis: verum