let L be ( ( non empty left_add-cancelable add-right-invertible ) ( non empty left_add-cancelable add-right-invertible ) addLoopStr ) ;
let a be ( ( ) ( left_add-cancelable ) Element of ( ( ) ( ) set ) ) ;

let L be ( ( non empty left_add-cancelable add-right-invertible ) ( non empty left_add-cancelable add-right-invertible ) addLoopStr ) ;
let a, b be ( ( ) ( left_add-cancelable ) Element of ( ( ) ( ) set ) ) ;

mode doubleLoop is ( ( non empty left_zeroed Loop-like multLoop_0-like right_zeroed well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like right_zeroed unital right_unital well-unital left_unital ) doubleLoopStr ) ;

mode leftQuasi-Field is ( ( non empty non degenerated left_zeroed Loop-like multLoop_0-like Abelian add-associative right_zeroed right-distributive well-unital ) ( non empty non degenerated left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian add-associative right_zeroed unital right-distributive right_unital well-unital left_unital ) doubleLoop) ;

for L being ( ( non empty ) ( non empty ) doubleLoopStr ) holds
( L : ( ( non empty ) ( non empty ) doubleLoopStr ) is ( ( non empty non degenerated left_zeroed Loop-like multLoop_0-like Abelian add-associative right_zeroed right-distributive well-unital ) ( non empty non degenerated left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian add-associative right_zeroed unital right-distributive right_unital well-unital left_unital ) leftQuasi-Field) iff ( ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + (0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) + c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) <> 1. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * (1. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (1. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) holds
ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) holds
ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a, x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) holds
x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a, x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) & x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) holds
x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * (0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) + (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) ) ) ;

for G being ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed right-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital right-distributive right_unital well-unital left_unital ) doubleLoop)
for a, b being ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) * (- b : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) M2( the carrier of b₁ : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed right-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital right-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( ) set ) )) = - (a : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) * b : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) M2( the carrier of b₁ : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed right-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital right-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( ) set ) )) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) ;

for G being ( ( non empty left_add-cancelable add-right-invertible Abelian ) ( non empty left_add-cancelable add-right-invertible Abelian ) addLoopStr )
for a being ( ( ) ( left_add-cancelable ) Element of ( ( ) ( ) set ) ) holds - (- a : ( ( ) ( left_add-cancelable ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( left_add-cancelable ) Element of ( ( ) ( ) set ) ) : ( ( ) ( left_add-cancelable ) Element of ( ( ) ( ) set ) ) = a : ( ( ) ( left_add-cancelable ) Element of ( ( ) ( ) set ) ) ;

for G being ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed right-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital right-distributive right_unital well-unital left_unital ) doubleLoop) holds (- (1. G : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed right-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital right-distributive right_unital well-unital left_unital ) doubleLoop) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) M2( the carrier of b₁ : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed right-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital right-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( ) set ) )) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) * (- (1. G : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed right-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital right-distributive right_unital well-unital left_unital ) doubleLoop) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) M2( the carrier of b₁ : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed right-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital right-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( ) set ) )) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) M2( the carrier of b₁ : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed right-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital right-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( ) set ) )) = 1. G : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed right-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital right-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) M2( the carrier of b₁ : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed right-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital right-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( ) set ) )) ;

for G being ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed right-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital right-distributive right_unital well-unital left_unital ) doubleLoop)
for a, x, y being ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) * (x : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) - y : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) M2( the carrier of b₁ : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed right-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital right-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( ) set ) )) = (a : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) * x : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) M2( the carrier of b₁ : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed right-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital right-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( ) set ) )) - (a : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) * y : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) M2( the carrier of b₁ : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed right-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital right-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( ) set ) )) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) ;

mode rightQuasi-Field is ( ( non empty non degenerated left_zeroed Loop-like multLoop_0-like Abelian add-associative right_zeroed left-distributive well-unital ) ( non empty non degenerated left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian add-associative right_zeroed unital left-distributive right_unital well-unital left_unital ) doubleLoop) ;

for L being ( ( non empty ) ( non empty ) doubleLoopStr ) holds
( L : ( ( non empty ) ( non empty ) doubleLoopStr ) is ( ( non empty non degenerated left_zeroed Loop-like multLoop_0-like Abelian add-associative right_zeroed left-distributive well-unital ) ( non empty non degenerated left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian add-associative right_zeroed unital left-distributive right_unital well-unital left_unital ) rightQuasi-Field) iff ( ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + (0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) + c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) <> 1. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * (1. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (1. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) holds
ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) holds
ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a, x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) holds
x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a, x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) & x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) holds
x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * (0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) + (c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) ) ) ;

for G being ( ( non empty left_zeroed Loop-like multLoop_0-like right_zeroed left-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like right_zeroed unital left-distributive right_unital well-unital left_unital ) doubleLoop)
for b, a being ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) holds (- b : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) M2( the carrier of b₁ : ( ( non empty left_zeroed Loop-like multLoop_0-like right_zeroed left-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like right_zeroed unital left-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( ) set ) )) = - (b : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) M2( the carrier of b₁ : ( ( non empty left_zeroed Loop-like multLoop_0-like right_zeroed left-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like right_zeroed unital left-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( ) set ) )) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) ;

for G being ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed left-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital left-distributive right_unital well-unital left_unital ) doubleLoop) holds (- (1. G : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed left-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital left-distributive right_unital well-unital left_unital ) doubleLoop) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) M2( the carrier of b₁ : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed left-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital left-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( ) set ) )) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) * (- (1. G : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed left-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital left-distributive right_unital well-unital left_unital ) doubleLoop) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) M2( the carrier of b₁ : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed left-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital left-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( ) set ) )) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) M2( the carrier of b₁ : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed left-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital left-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( ) set ) )) = 1. G : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed left-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital left-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) M2( the carrier of b₁ : ( ( non empty left_zeroed Loop-like multLoop_0-like Abelian right_zeroed left-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian right_zeroed unital left-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( ) set ) )) ;

for G being ( ( non empty left_zeroed Loop-like multLoop_0-like right_zeroed left-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like right_zeroed unital left-distributive right_unital well-unital left_unital ) doubleLoop)
for x, y, a being ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) holds (x : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) - y : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) M2( the carrier of b₁ : ( ( non empty left_zeroed Loop-like multLoop_0-like right_zeroed left-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like right_zeroed unital left-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( ) set ) )) = (x : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) M2( the carrier of b₁ : ( ( non empty left_zeroed Loop-like multLoop_0-like right_zeroed left-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like right_zeroed unital left-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( ) set ) )) - (y : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) M2( the carrier of b₁ : ( ( non empty left_zeroed Loop-like multLoop_0-like right_zeroed left-distributive well-unital ) ( non empty left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like right_zeroed unital left-distributive right_unital well-unital left_unital ) doubleLoop) : ( ( ) ( ) set ) )) : ( ( ) ( left_add-cancelable right_add-cancelable add-cancelable ) Element of ( ( ) ( ) set ) ) ;

mode doublesidedQuasi-Field is ( ( non empty non degenerated left_zeroed Loop-like multLoop_0-like Abelian add-associative right_zeroed well-unital distributive ) ( non empty non degenerated left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doubleLoop) ;

for L being ( ( non empty ) ( non empty ) doubleLoopStr ) holds
( L : ( ( non empty ) ( non empty ) doubleLoopStr ) is ( ( non empty non degenerated left_zeroed Loop-like multLoop_0-like Abelian add-associative right_zeroed well-unital distributive ) ( non empty non degenerated left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian add-associative right_zeroed unital right-distributive left-distributive right_unital well-unital distributive left_unital ) doublesidedQuasi-Field) iff ( ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + (0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) + c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) <> 1. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * (1. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (1. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) holds
ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) holds
ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a, x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) holds
x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a, x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) & x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) holds
x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * (0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) + (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) + (c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) ) ) ;

mode _Skew-Field is ( ( non empty non degenerated left_zeroed Loop-like multLoop_0-like Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty non degenerated left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) doublesidedQuasi-Field) ;

for L being ( ( non empty ) ( non empty ) doubleLoopStr ) holds
( L : ( ( non empty ) ( non empty ) doubleLoopStr ) is ( ( non empty non degenerated left_zeroed Loop-like multLoop_0-like Abelian add-associative right_zeroed associative well-unital distributive ) ( non empty non degenerated left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian add-associative right_zeroed unital associative right-distributive left-distributive right_unital well-unital distributive left_unital ) _Skew-Field) iff ( ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + (0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) + c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) <> 1. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * (1. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) holds
ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = 1. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * (0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) * c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) + (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) + (c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) ) ) ;

mode _Field is ( ( non empty non degenerated left_zeroed Loop-like multLoop_0-like Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) _Skew-Field) ;

for L being ( ( non empty ) ( non empty ) doubleLoopStr ) holds
( L : ( ( non empty ) ( non empty ) doubleLoopStr ) is ( ( non empty non degenerated left_zeroed Loop-like multLoop_0-like Abelian add-associative right_zeroed associative commutative well-unital distributive ) ( non empty non degenerated left_add-cancelable right_add-cancelable add-cancelable almost_left_cancelable almost_right_cancelable almost_cancelable left_zeroed add-left-invertible add-right-invertible Loop-like almost_invertible multLoop_0-like Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital ) _Field) iff ( ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + (0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) + c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) <> 1. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * (1. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) holds
ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = 1. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * (0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = 0. L : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) * c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * (b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) + (a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) & ( for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) = b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) * a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) M2( the carrier of b₁ : ( ( non empty ) ( non empty ) doubleLoopStr ) : ( ( ) ( ) set ) )) ) ) ) ;