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 & f is retraction & f is coretraction holds
f9 " = f " )
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 & f is retraction & f is coretraction holds
f9 " = f "
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 & f is retraction & f is coretraction holds
f9 " = f " )
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 & f is retraction & f is coretraction holds
f9 " = f "
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 & f is retraction & f is coretraction holds
f9 " = f " )
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 & f is retraction & f is coretraction holds
f9 " = f "
A6: <^b9,a9^> = <^a,b^> by A1, A4, A5, Th9;
A7: <^a9,b9^> = <^b,a^> by A1, A4, A5, Th9;
let f be Morphism of a,b; :: thesis: for f9 being Morphism of b9,a9 st f9 = f & f is retraction & f is coretraction holds
f9 " = f "
let f9 be Morphism of b9,a9; :: thesis: ( f9 = f & f is retraction & f is coretraction implies f9 " = f " )
assume that
A8: f9 = f and
A9: ( f is retraction & f is coretraction ) ; :: thesis: f9 " = f "
reconsider g = f " as Morphism of a9,b9 by A1, A4, A5, Th7;
A10: (f ") * f = idm a by A2, A3, A9, ALTCAT_3:2;
A11: f * (f ") = idm b by A2, A3, A9, ALTCAT_3:2;
A12: f9 * g = idm a by A1, A2, A3, A4, A5, A8, A10, Th9;
A13: g * f9 = idm b by A1, A2, A3, A4, A5, A8, A11, Th9;
A14: f9 * g = idm a9 by A1, A4, A12, Th10;
A15: g * f9 = idm b9 by A1, A5, A13, Th10;
A16: ( f9 is retraction & f9 is coretraction ) by A1, A2, A3, A4, A5, A8, A9, Lm1;
A17: g is_left_inverse_of f9 by A15;
g is_right_inverse_of f9 by A14;
hence f9 " = f " by A2, A3, A6, A7, A16, A17, ALTCAT_3:def 4; :: thesis: verum