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 :: thesis: for a, b being Object of B st <^a,b^> <> {} holds
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 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;
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