let K be Field; :: thesis: opp K is strict Field
set L = opp K;
for x, y being Scalar of (opp K) holds x * y = y * x

proof

let x, y be Scalar of (opp K); :: thesis: x * y = y * x
reconsider a = x, b = y as Scalar of K ;
b * a = x * y by Lm3;
hence x * y = y * x by Lm3; :: thesis: verum

end;

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