let A, B be category; :: thesis: ( A,B are_opposite implies for a being Object of A
for b being Object of B st a = b holds
idm a = idm b )
assume A1: A,B are_opposite ; :: thesis: for a being Object of A
for b being Object of B st a = b holds
idm a = idm b
let a be Object of A; :: thesis: for b being Object of B st a = b holds
idm a = idm b
let b be Object of B; :: thesis: ( a = b implies idm a = idm b )
assume A2: a = b ; :: thesis: idm a = idm b
reconsider i = idm b as Morphism of a,a by A1, A2, Th9;

now :: thesis: for c being Object of A st <^a,c^> <> {} holds
for f being Morphism of a,c holds f * i = f

let c be Object of A; :: thesis: ( <^a,c^> <> {} implies for f being Morphism of a,c holds f * i = f )
assume A3: <^a,c^> <> {} ; :: thesis: for f being Morphism of a,c holds f * i = f
let f be Morphism of a,c; :: thesis: f * i = f
reconsider d = c as Object of B by A1;
A4: <^a,c^> = <^d,b^> by A1, A2, Th9;
reconsider g = f as Morphism of d,b by A1, A2, Th9;
thus f * i = (idm b) * g by A1, A2, A3, Th9
.= f by A3, A4, ALTCAT_1:20 ; :: thesis: verum

end;

hence idm a = idm b by ALTCAT_1:def 17; :: thesis: verum