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

now

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

end;

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