let F be non empty doubleLoopStr ; :: thesis:
assume A1: for x, y, z being Scalar of F holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. F) = x & x + (- x) = 0. F & x * y = y * x & (x * y) * z = x * (y * z) & (1. F) * x = x & x * (1. F) = x & ( x <> 0. F implies ex y being Scalar of F st x * y = 1. F ) & 0. F <> 1. F & x * (y + z) = (x * y) + (x * z) ) ; :: thesis:
A2: for x being Scalar of F st x <> 0. F holds
ex y being Scalar of F st y * x = 1. F

let x be Scalar of F; :: thesis:
assume x <> 0. F ; :: thesis:
then consider y being Scalar of F such that
A3: x * y = 1. F by A1;
take y ; :: thesis:
thus y * x = 1. F by A1, A3; :: thesis:

end;

let x, y, z be Scalar of F; :: thesis:
thus ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. F) = x & x + (- x) = 0. F & x * y = y * x & (x * y) * z = x * (y * z) & (1. F) * x = x & x * (1. F) = x & ( x <> 0. F implies ex y being Scalar of F st x * y = 1. F ) & 0. F <> 1. F & x * (y + z) = (x * y) + (x * z) ) by A1; :: thesis:
thus (y + z) * x = x * (y + z) by A1
.= (x * y) + (x * z) by A1
.= (y * x) + (x * z) by A1
.= (y * x) + (z * x) by A1 ; :: thesis:

end;

let v be Element of F; :: according to ALGSTR_0:def 16 :: thesis:
take - v ; :: according to ALGSTR_0:def 11 :: thesis:
thus v + (- v) = 0. F by A4; :: thesis:

end;