let C be category; :: thesis: for o1, o2 being Object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is iso holds
( A is mono & A is epi )
let o1, o2 be Object of C; :: thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 st A is iso holds
( A is mono & A is epi ) )
assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; :: thesis: for A being Morphism of o1,o2 st A is iso holds
( A is mono & A is epi )
let A be Morphism of o1,o2; :: thesis: ( A is iso implies ( A is mono & A is epi ) )
assume A is iso ; :: thesis: ( A is mono & A is epi )
then A2: ( A is retraction & A is coretraction ) by A1, Th6;
A3: for o being Object of C st <^o2,o^> <> {} holds
for B, C being Morphism of o2,o st B * A = C * A holds
B = C

proof

let o be Object of C; :: thesis: ( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds
B = C )
assume A4: <^o2,o^> <> {} ; :: thesis: for B, C being Morphism of o2,o st B * A = C * A holds
B = C
let B, C be Morphism of o2,o; :: thesis: ( B * A = C * A implies B = C )
assume B * A = C * A ; :: thesis: B = C
then B * (A * (A ")) = (C * A) * (A ") by A1, A4, ALTCAT_1:21;
then B * (idm o2) = (C * A) * (A ") by A1, A2, Th2;
then B * (idm o2) = C * (A * (A ")) by A1, A4, ALTCAT_1:21;
then B * (idm o2) = C * (idm o2) by A1, A2, Th2;
then B = C * (idm o2) by A4, ALTCAT_1:def 17;
hence B = C by A4, ALTCAT_1:def 17; :: thesis: verum

end;

for o being Object of C st <^o,o1^> <> {} holds
for B, C being Morphism of o,o1 st A * B = A * C holds
B = C

proof

let o be Object of C; :: thesis: ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st A * B = A * C holds
B = C )
assume A5: <^o,o1^> <> {} ; :: thesis: for B, C being Morphism of o,o1 st A * B = A * C holds
B = C
let B, C be Morphism of o,o1; :: thesis: ( A * B = A * C implies B = C )
assume A * B = A * C ; :: thesis: B = C
then ((A ") * A) * B = (A ") * (A * C) by A1, A5, ALTCAT_1:21;
then (idm o1) * B = (A ") * (A * C) by A1, A2, Th2;
then (idm o1) * B = ((A ") * A) * C by A1, A5, ALTCAT_1:21;
then (idm o1) * B = (idm o1) * C by A1, A2, Th2;
then B = (idm o1) * C by A5, ALTCAT_1:20;
hence B = C by A5, ALTCAT_1:20; :: thesis: verum

end;

hence ( A is mono & A is epi ) by A3; :: thesis: verum