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 a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( f is retraction iff f' is coretraction ) )
assume A1: A,B are_opposite ; :: thesis: for a, b being object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( f is retraction iff f' is coretraction )
let a, b be object of A; :: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies for a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( f is retraction iff f' is coretraction ) )
assume that
A2: <^a,b^> <> {} and
A3: <^b,a^> <> {} ; :: thesis: for a', b' being object of B st a' = a & b' = b holds
for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( f is retraction iff f' is coretraction )
let a', b' be object of B; :: thesis: ( a' = a & b' = b implies for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( f is retraction iff f' is coretraction ) )
assume that
A4: a' = a and
A5: b' = b ; :: thesis: for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( f is retraction iff f' is coretraction )
A6: <^b',a'^> = <^a,b^> by A1, A4, A5, Th9;
<^a',b'^> = <^b,a^> by A1, A4, A5, Th9;
hence for f being Morphism of a,b
for f' being Morphism of b',a' st f' = f holds
( f is retraction iff f' is coretraction ) by A1, A2, A3, A4, A5, A6, Lm1; :: thesis: verum