let F be non empty doubleLoopStr ; :: thesis: ( ( 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) ) ) implies F is Field )
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: F is Field
A2: for x being Scalar of F st x <> 0. F holds
ex y being Scalar of F st y * x = 1. F

proof

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

end;

A4: now :: thesis: 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) & (y + z) * x = (y * x) + (z * x) )

let x, y, z be Scalar of F; :: thesis: ( 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) & (y + z) * x = (y * x) + (z * x) )
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: (y + z) * x = (y * x) + (z * x)
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: verum

end;

F is right_complementable

proof

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

end;

hence F is Field by A2, A4, GROUP_1:def 3, GROUP_1:def 12, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, STRUCT_0:def 8, VECTSP_1:def 6, VECTSP_1:def 7, VECTSP_1:def 9; :: thesis: verum