let K be Skew-Field; :: thesis: ( id K is antiisomorphism iff K is Field )
set J = id K;

A1: now :: thesis: ( K is Field implies id K is antiisomorphism )

assume A2: K is Field ; :: thesis: id K is antiisomorphism
A3: for x, y being Scalar of K holds (id K) . (x * y) = ((id K) . y) * ((id K) . x) by A2, GROUP_1:def 12;
(id K) . (1_ K) = 1_ K ;
hence id K is antiisomorphism by A3, Th22; :: thesis: verum

end;

now :: thesis: ( id K is antiisomorphism implies K is Field )

assume A4: id K is antiisomorphism ; :: thesis: K is Field
for x, y being Scalar of K holds x * y = y * x

proof

let x, y be Scalar of K; :: thesis: x * y = y * x
A5: (id K) . y = y ;
( (id K) . (x * y) = x * y & (id K) . x = x ) ;
hence x * y = y * x by A4, A5, Th22; :: thesis: verum

end;

hence K is Field by GROUP_1:def 12; :: thesis: verum

end;

hence ( id K is antiisomorphism iff K is Field ) by A1; :: thesis: verum