let K be Ring; :: thesis: ( id K is antiautomorphism iff K is comRing )
set J = id K;

A1: now

assume A2: K is comRing ; :: thesis: id K is antiautomorphism
A3: for x, y being Scalar of K holds (id K) . (x * y) = ((id K) . y) * ((id K) . x)

proof

let x, y be Scalar of K; :: thesis: (id K) . (x * y) = ((id K) . y) * ((id K) . x)
A4: (id K) . y = y by FUNCT_1:35;
( (id K) . (x * y) = x * y & (id K) . x = x ) by FUNCT_1:35;
hence (id K) . (x * y) = ((id K) . y) * ((id K) . x) by A2, A4, Lm5; :: thesis: verum

end;

A5: ( id K is one-to-one & rng (id K) = the carrier of K ) by Lm6;
( ( for x, y being Scalar of K holds (id K) . (x + y) = ((id K) . x) + ((id K) . y) ) & (id K) . (1_ K) = 1_ K ) by Lm6;
hence id K is antiautomorphism by A3, A5, Th28; :: thesis: verum

end;

now

assume A6: id K is antiautomorphism ; :: thesis: K is comRing
for x, y being Element of K holds x * y = y * x

proof

let x, y be Element of K; :: thesis: x * y = y * x
A7: (id K) . y = y by FUNCT_1:35;
( (id K) . (x * y) = x * y & (id K) . x = x ) by FUNCT_1:35;
hence x * y = y * x by A6, A7, Th28; :: thesis: verum

end;

hence K is comRing by GROUP_1:def 16; :: thesis: verum

end;

hence ( id K is antiautomorphism iff K is comRing ) by A1; :: thesis: verum