let C be Category; :: thesis: IdMap C = IdMap (C opp)
thus the carrier of C = the carrier of (C opp) ; :: according to FUNCT_2:def 7 :: thesis: for b₁ being Element of the carrier of C holds (IdMap C) . b₁ = (IdMap (C opp)) . b₁
let o be Element of the carrier of C; :: thesis: (IdMap C) . o = (IdMap (C opp)) . o
thus (IdMap C) . o = id o by ISOCAT_1:def 12
.= id (o opp) by OPPCAT_1:71
.= (IdMap (C opp)) . (o opp) by ISOCAT_1:def 12
.= (IdMap (C opp)) . o ; :: thesis: verum