let A, B be category; :: thesis: ( A,B are_opposite implies for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is coretraction iff f9 is retraction ) )
assume A1: A,B are_opposite ; :: thesis: for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is coretraction iff f9 is retraction )
let a, b be Object of A; :: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is coretraction iff f9 is retraction ) )
assume that
A2: <^a,b^> <> {} and
A3: <^b,a^> <> {} ; :: thesis: for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is coretraction iff f9 is retraction )
let a9, b9 be Object of B; :: thesis: ( a9 = a & b9 = b implies for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is coretraction iff f9 is retraction ) )
assume that
A4: a9 = a and
A5: b9 = b ; :: thesis: for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is coretraction iff f9 is retraction )
A6: <^b9,a9^> = <^a,b^> by A1, A4, A5, Th9;
<^a9,b9^> = <^b,a^> by A1, A4, A5, Th9;
hence for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is coretraction iff f9 is retraction ) by A1, A2, A3, A4, A5, A6, Lm1; :: thesis: verum