theorem Th26: :: MOD_2:26

for F being non empty doubleLoopStr st ( 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) ) ) holds
F is Field