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

set L = opp K;

for x, y being Scalar of (opp K) holds x * y = y * x

proof

hence
opp K is strict Field
by GROUP_1:def 12; :: thesis: verum
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;reconsider a = x, b = y as Scalar of K ;

b * a = x * y by Lm3;

hence x * y = y * x by Lm3; :: thesis: verum