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