:: ALGSTR_2 semantic presentation

begin

 Lm1:  0 = 0. F_Real
by STRUCT_0:def_6, VECTSP_1:def_5;

Lm2:  for a, b being Element of F_Real st a <> 0. F_Real holds
ex x being Element of F_Real st a * x = b
proof
let a, b be Element of F_Real; ::_thesis: ( a <> 0. F_Real implies ex x being Element of F_Real st a * x = b )
assume A1: a <> 0. F_Real ; ::_thesis: ex x being Element of F_Real st a * x = b
reconsider p = a, q = b as Real by VECTSP_1:def_5;
consider r being Real such that
A2: p * r = q by A1, Lm1, ALGSTR_1:14;
reconsider x = r as Element of F_Real by VECTSP_1:def_5;
 a * x = b by A2;
hence  ex x being Element of F_Real st a * x = b ; ::_thesis: verum
end;

Lm3:  for a, b being Element of F_Real st a <> 0. F_Real holds
ex x being Element of F_Real st x * a = b
proof
let a, b be Element of F_Real; ::_thesis: ( a <> 0. F_Real implies ex x being Element of F_Real st x * a = b )
assume  a <> 0. F_Real ; ::_thesis: ex x being Element of F_Real st x * a = b
then  ex x being Element of F_Real st a * x = b by Lm2;
hence  ex x being Element of F_Real st x * a = b ; ::_thesis: verum
end;

Lm4:  ( ( for a, x, y being Element of F_Real st a <> 0. F_Real & a * x = a * y holds
x = y ) & ( for a, x, y being Element of F_Real st a <> 0. F_Real & x * a = y * a holds
x = y ) )
by VECTSP_1:5;

Lm5:  ( ( for a being Element of F_Real holds a * (0. F_Real) = 0. F_Real ) & ( for a being Element of F_Real holds (0. F_Real) * a = 0. F_Real ) )
by VECTSP_1:12;

registration
cluster F_Real  ->  multLoop_0-like ;
coherence
 F_Real is multLoop_0-like by Lm2, Lm3, Lm4, Lm5, ALGSTR_1:16;
end;

definition
let L be non empty left_add-cancelable add-right-invertible addLoopStr ;
let a be Element of L;
func - a ->  Element of L means :Def1: :: ALGSTR_2:def 1
a + it = 0. L;
existence
 ex b1 being Element of L st a + b1 = 0. L by ALGSTR_1:def_4;
uniqueness
 for b1, b2 being Element of L st a + b1 = 0. L & a + b2 = 0. L holds
b1 = b2 by ALGSTR_0:def_3;
end;

:: deftheorem Def1 defines - ALGSTR_2:def_1_:_
 for L being non empty left_add-cancelable add-right-invertible addLoopStr
for a, b3 being Element of L holds
( b3 = - a iff a + b3 = 0. L );

definition
let L be non empty left_add-cancelable add-right-invertible addLoopStr ;
let a, b be Element of L;
funca - b ->  Element of L equals :: ALGSTR_2:def 2
a + (- b);
correctness
coherence
a + (- b) is Element of L;
;
end;

:: deftheorem  defines - ALGSTR_2:def_2_:_
 for L being non empty left_add-cancelable add-right-invertible addLoopStr
for a, b being Element of L holds a - b = a + (- b);

registration
cluster non empty non degenerated strict left_zeroed Loop-like multLoop_0-like Abelian add-associative right_zeroed associative commutative well-unital distributive for doubleLoopStr ;
existence
 ex b1 being non empty doubleLoopStr st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is commutative & b1 is associative & b1 is distributive & not b1 is degenerated & b1 is left_zeroed & b1 is right_zeroed & b1 is Loop-like & b1 is well-unital & b1 is multLoop_0-like )
proof
take  F_Real ; ::_thesis: ( F_Real is strict & F_Real is Abelian & F_Real is add-associative & F_Real is commutative & F_Real is associative & F_Real is distributive & not F_Real is degenerated & F_Real is left_zeroed & F_Real is right_zeroed & F_Real is Loop-like & F_Real is well-unital & F_Real is multLoop_0-like )
thus  ( F_Real is strict & F_Real is Abelian & F_Real is add-associative & F_Real is commutative & F_Real is associative & F_Real is distributive & not F_Real is degenerated & F_Real is left_zeroed & F_Real is right_zeroed & F_Real is Loop-like & F_Real is well-unital & F_Real is multLoop_0-like ) ; ::_thesis: verum
end;
end;

definition
mode doubleLoop is non empty left_zeroed Loop-like multLoop_0-like right_zeroed well-unital doubleLoopStr ;
end;

definition
mode leftQuasi-Field is non degenerated Abelian add-associative right-distributive doubleLoop;
end;


theorem :: ALGSTR_2:1
for L being non empty doubleLoopStr holds
( L is leftQuasi-Field iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) ) )
proof
let L be non empty doubleLoopStr ; ::_thesis: ( L is leftQuasi-Field iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) ) )
thus  ( L is leftQuasi-Field implies ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) ) ) by ALGSTR_1:6, ALGSTR_1:16, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, STRUCT_0:def_8, VECTSP_1:def_2, VECTSP_1:def_6; ::_thesis: ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) implies L is leftQuasi-Field )
assume that
A1: for a being Element of L holds a + (0. L) = a and
A2: for a being Element of L ex x being Element of L st a + x = 0. L and
A3: for a, b, c being Element of L holds (a + b) + c = a + (b + c) and
A4: for a, b being Element of L holds a + b = b + a and
A5: ( 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) ) ; ::_thesis: L is leftQuasi-Field
A6: for a being Element of L holds (0. L) + a = a
proof
let a be Element of L; ::_thesis: (0. L) + a = a
thus (0. L) + a = a + (0. L) by A4
.= a by A1 ; ::_thesis: verum
end;
A7: for a, b being Element of L ex x being Element of L st a + x = b
proof
let a, b be Element of L; ::_thesis: ex x being Element of L st a + x = b
consider y being Element of L such that
A8: a + y = 0. L by A2;
take x = y + b; ::_thesis: a + x = b
thus a + x = (0. L) + b by A3, A8
.= b by A6 ; ::_thesis: verum
end;
A9: for a, b being Element of L ex x being Element of L st x + a = b
proof
let a, b be Element of L; ::_thesis: ex x being Element of L st x + a = b
consider x being Element of L such that
A10: a + x = b by A7;
take  x ; ::_thesis: x + a = b
thus  x + a = b by A4, A10; ::_thesis: verum
end;
A11: for a, x, y being Element of L st a + x = a + y holds
x = y
proof
let a, x, y be Element of L; ::_thesis: ( a + x = a + y implies x = y )
consider z being Element of L such that
A12: z + a = 0. L by A1, A2, A3, ALGSTR_1:3;
assume  a + x = a + y ; ::_thesis: x = y
then (z + a) + x = z + (a + y) by A3
.= (z + a) + y by A3 ;
hence x = (0. L) + y by A6, A12
.= y by A6 ;
::_thesis: verum
end;
 for a, x, y being Element of L st x + a = y + a holds
x = y
proof
let a, x, y be Element of L; ::_thesis: ( x + a = y + a implies x = y )
assume  x + a = y + a ; ::_thesis: x = y
then a + x = y + a by A4
.= a + y by A4 ;
hence  x = y by A11; ::_thesis: verum
end;
hence  L is leftQuasi-Field by A1, A3, A4, A5, A6, A7, A9, A11, ALGSTR_1:6, ALGSTR_1:16, ALGSTR_1:def_2, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, STRUCT_0:def_8, VECTSP_1:def_2, VECTSP_1:def_6; ::_thesis: verum
end;

theorem Th2: :: ALGSTR_2:2
for G being Abelian right-distributive doubleLoop
for a, b being Element of G holds a * (- b) = - (a * b)
proof
let G be Abelian right-distributive doubleLoop; ::_thesis: for a, b being Element of G holds a * (- b) = - (a * b)
let a, b be Element of G; ::_thesis: a * (- b) = - (a * b)
(a * b) + (a * (- b)) = a * (b + (- b)) by VECTSP_1:def_2
.= a * (0. G) by Def1
.= 0. G by ALGSTR_1:16 ;
hence  a * (- b) = - (a * b) by Def1; ::_thesis: verum
end;

theorem Th3: :: ALGSTR_2:3
for G being non empty left_add-cancelable add-right-invertible Abelian addLoopStr
for a being Element of G holds - (- a) = a
proof
let G be non empty left_add-cancelable add-right-invertible Abelian addLoopStr ; ::_thesis: for a being Element of G holds - (- a) = a
let a be Element of G; ::_thesis: - (- a) = a
 (- a) + a = 0. G by Def1;
hence  - (- a) = a by Def1; ::_thesis: verum
end;

theorem :: ALGSTR_2:4
for G being Abelian right-distributive doubleLoop holds (- (1. G)) * (- (1. G)) = 1. G
proof
let G be Abelian right-distributive doubleLoop; ::_thesis: (- (1. G)) * (- (1. G)) = 1. G
thus (- (1. G)) * (- (1. G)) = - ((- (1. G)) * (1_ G)) by Th2
.= - (- (1. G)) by VECTSP_1:def_4
.= 1. G by Th3 ; ::_thesis: verum
end;

theorem :: ALGSTR_2:5
for G being Abelian right-distributive doubleLoop
for a, x, y being Element of G holds a * (x - y) = (a * x) - (a * y)
proof
let G be Abelian right-distributive doubleLoop; ::_thesis: for a, x, y being Element of G holds a * (x - y) = (a * x) - (a * y)
let a, x, y be Element of G; ::_thesis: a * (x - y) = (a * x) - (a * y)
thus a * (x - y) = (a * x) + (a * (- y)) by VECTSP_1:def_2
.= (a * x) - (a * y) by Th2 ; ::_thesis: verum
end;

definition
mode rightQuasi-Field is non degenerated Abelian add-associative left-distributive doubleLoop;
end;

theorem :: ALGSTR_2:6
for L being non empty doubleLoopStr holds
( L is rightQuasi-Field iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) )
proof
let L be non empty doubleLoopStr ; ::_thesis: ( L is rightQuasi-Field iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) )
thus  ( L is rightQuasi-Field implies ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) ) by ALGSTR_1:6, ALGSTR_1:16, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, STRUCT_0:def_8, VECTSP_1:def_3, VECTSP_1:def_6; ::_thesis: ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) implies L is rightQuasi-Field )
assume that
A1: for a being Element of L holds a + (0. L) = a and
A2: for a being Element of L ex x being Element of L st a + x = 0. L and
A3: for a, b, c being Element of L holds (a + b) + c = a + (b + c) and
A4: for a, b being Element of L holds a + b = b + a and
A5: ( 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) ; ::_thesis: L is rightQuasi-Field
A6: for a, b being Element of L ex x being Element of L st x + a = b
proof
let a, b be Element of L; ::_thesis: ex x being Element of L st x + a = b
consider y being Element of L such that
A7: y + a = 0. L by A1, A2, A3, ALGSTR_1:3;
take x = b + y; ::_thesis: x + a = b
thus x + a = b + (0. L) by A3, A7
.= b by A1 ; ::_thesis: verum
end;
A8: for a being Element of L holds (0. L) + a = a
proof
let a be Element of L; ::_thesis: (0. L) + a = a
thus (0. L) + a = a + (0. L) by A4
.= a by A1 ; ::_thesis: verum
end;
A9: for a, x, y being Element of L st a + x = a + y holds
x = y
proof
let a, x, y be Element of L; ::_thesis: ( a + x = a + y implies x = y )
consider z being Element of L such that
A10: z + a = 0. L by A1, A2, A3, ALGSTR_1:3;
assume  a + x = a + y ; ::_thesis: x = y
then (z + a) + x = z + (a + y) by A3
.= (z + a) + y by A3 ;
hence x = (0. L) + y by A8, A10
.= y by A8 ;
::_thesis: verum
end;
A11: for a, x, y being Element of L st x + a = y + a holds
x = y
proof
let a, x, y be Element of L; ::_thesis: ( x + a = y + a implies x = y )
consider z being Element of L such that
A12: a + z = 0. L by A2;
assume  x + a = y + a ; ::_thesis: x = y
then x + (a + z) = (y + a) + z by A3
.= y + (a + z) by A3 ;
hence x = y + (0. L) by A1, A12
.= y by A1 ;
::_thesis: verum
end;
 for a, b being Element of L ex x being Element of L st a + x = b
proof
let a, b be Element of L; ::_thesis: ex x being Element of L st a + x = b
consider y being Element of L such that
A13: a + y = 0. L by A2;
take x = y + b; ::_thesis: a + x = b
thus a + x = (0. L) + b by A3, A13
.= b by A8 ; ::_thesis: verum
end;
hence  L is rightQuasi-Field by A1, A3, A4, A5, A8, A6, A9, A11, ALGSTR_1:6, ALGSTR_1:16, ALGSTR_1:def_2, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, STRUCT_0:def_8, VECTSP_1:def_3, VECTSP_1:def_6; ::_thesis: verum
end;


theorem Th7: :: ALGSTR_2:7
for G being left-distributive doubleLoop
for b, a being Element of G holds (- b) * a = - (b * a)
proof
let G be left-distributive doubleLoop; ::_thesis: for b, a being Element of G holds (- b) * a = - (b * a)
let b, a be Element of G; ::_thesis: (- b) * a = - (b * a)
(b * a) + ((- b) * a) = (b + (- b)) * a by VECTSP_1:def_3
.= (0. G) * a by Def1
.= 0. G by ALGSTR_1:16 ;
hence  (- b) * a = - (b * a) by Def1; ::_thesis: verum
end;

theorem :: ALGSTR_2:8
for G being Abelian left-distributive doubleLoop holds (- (1. G)) * (- (1. G)) = 1. G
proof
let G be Abelian left-distributive doubleLoop; ::_thesis: (- (1. G)) * (- (1. G)) = 1. G
thus (- (1. G)) * (- (1. G)) = - ((1_ G) * (- (1. G))) by Th7
.= - (- (1. G)) by VECTSP_1:def_8
.= 1. G by Th3 ; ::_thesis: verum
end;

theorem :: ALGSTR_2:9
for G being left-distributive doubleLoop
for x, y, a being Element of G holds (x - y) * a = (x * a) - (y * a)
proof
let G be left-distributive doubleLoop; ::_thesis: for x, y, a being Element of G holds (x - y) * a = (x * a) - (y * a)
let x, y, a be Element of G; ::_thesis: (x - y) * a = (x * a) - (y * a)
thus (x - y) * a = (x * a) + ((- y) * a) by VECTSP_1:def_3
.= (x * a) - (y * a) by Th7 ; ::_thesis: verum
end;

definition
mode doublesidedQuasi-Field is non degenerated Abelian add-associative distributive doubleLoop;
end;


theorem :: ALGSTR_2:10
for L being non empty doubleLoopStr holds
( L is doublesidedQuasi-Field iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) )
proof
let L be non empty doubleLoopStr ; ::_thesis: ( L is doublesidedQuasi-Field iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) )
thus  ( L is doublesidedQuasi-Field implies ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) ) by ALGSTR_1:6, ALGSTR_1:16, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, STRUCT_0:def_8, VECTSP_1:def_6, VECTSP_1:def_7; ::_thesis: ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) implies L is doublesidedQuasi-Field )
assume that
A1: for a being Element of L holds a + (0. L) = a and
A2: for a being Element of L ex x being Element of L st a + x = 0. L and
A3: for a, b, c being Element of L holds (a + b) + c = a + (b + c) and
A4: for a, b being Element of L holds a + b = b + a and
A5: ( 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) ; ::_thesis: L is doublesidedQuasi-Field
A6: for a, b being Element of L ex x being Element of L st x + a = b
proof
let a, b be Element of L; ::_thesis: ex x being Element of L st x + a = b
consider y being Element of L such that
A7: y + a = 0. L by A1, A2, A3, ALGSTR_1:3;
take x = b + y; ::_thesis: x + a = b
thus x + a = b + (0. L) by A3, A7
.= b by A1 ; ::_thesis: verum
end;
A8: for a being Element of L holds (0. L) + a = a
proof
let a be Element of L; ::_thesis: (0. L) + a = a
thus (0. L) + a = a + (0. L) by A4
.= a by A1 ; ::_thesis: verum
end;
A9: for a, x, y being Element of L st a + x = a + y holds
x = y
proof
let a, x, y be Element of L; ::_thesis: ( a + x = a + y implies x = y )
consider z being Element of L such that
A10: z + a = 0. L by A1, A2, A3, ALGSTR_1:3;
assume  a + x = a + y ; ::_thesis: x = y
then (z + a) + x = z + (a + y) by A3
.= (z + a) + y by A3 ;
hence x = (0. L) + y by A8, A10
.= y by A8 ;
::_thesis: verum
end;
A11: for a, x, y being Element of L st x + a = y + a holds
x = y
proof
let a, x, y be Element of L; ::_thesis: ( x + a = y + a implies x = y )
consider z being Element of L such that
A12: a + z = 0. L by A2;
assume  x + a = y + a ; ::_thesis: x = y
then x + (a + z) = (y + a) + z by A3
.= y + (a + z) by A3 ;
hence x = y + (0. L) by A1, A12
.= y by A1 ;
::_thesis: verum
end;
 for a, b being Element of L ex x being Element of L st a + x = b
proof
let a, b be Element of L; ::_thesis: ex x being Element of L st a + x = b
consider y being Element of L such that
A13: a + y = 0. L by A2;
take x = y + b; ::_thesis: a + x = b
thus a + x = (0. L) + b by A3, A13
.= b by A8 ; ::_thesis: verum
end;
hence  L is doublesidedQuasi-Field by A1, A3, A4, A5, A8, A6, A9, A11, ALGSTR_1:6, ALGSTR_1:16, ALGSTR_1:def_2, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, STRUCT_0:def_8, VECTSP_1:def_6, VECTSP_1:def_7; ::_thesis: verum
end;

definition
mode _Skew-Field is associative doublesidedQuasi-Field;
end;

Lm6:  for L being non empty doubleLoopStr
for a, b being Element of L st 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) & a * b = 1. L holds
b * a = 1. L
proof
let L be non empty doubleLoopStr ; ::_thesis: for a, b being Element of L st 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) & a * b = 1. L holds
b * a = 1. L
let a, b be Element of L; ::_thesis: ( 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) & a * b = 1. L implies b * a = 1. L )
assume that
A1: 0. L <> 1. L and
A2: for a being Element of L holds a * (1. L) = a and
A3: for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L and
A4: for a, b, c being Element of L holds (a * b) * c = a * (b * c) and
A5: for a being Element of L holds a * (0. L) = 0. L ; ::_thesis: ( not a * b = 1. L or b * a = 1. L )
thus  ( a * b = 1. L implies b * a = 1. L ) ::_thesis: verum
proof
assume A6: a * b = 1. L ; ::_thesis: b * a = 1. L
then  b <> 0. L by A1, A5;
then consider x being Element of L such that
A7: b * x = 1. L by A3;
thus b * a = (b * a) * (b * x) by A2, A7
.= ((b * a) * b) * x by A4
.= (b * (1. L)) * x by A4, A6
.= 1. L by A2, A7 ; ::_thesis: verum
end;
end;

Lm7:  for L being non empty doubleLoopStr
for a being Element of L st 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) holds
(1. L) * a = a * (1. L)
proof
let L be non empty doubleLoopStr ; ::_thesis: for a being Element of L st 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) holds
(1. L) * a = a * (1. L)
let a be Element of L; ::_thesis: ( 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) implies (1. L) * a = a * (1. L) )
assume that
A1: 0. L <> 1. L and
A2: for a being Element of L holds a * (1. L) = a and
A3: for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L and
A4: for a, b, c being Element of L holds (a * b) * c = a * (b * c) and
A5: for a being Element of L holds a * (0. L) = 0. L ; ::_thesis: (1. L) * a = a * (1. L)
A6: ( a <> 0. L implies (1. L) * a = a * (1. L) )
proof
assume  a <> 0. L ; ::_thesis: (1. L) * a = a * (1. L)
then consider x being Element of L such that
A7: a * x = 1. L by A3;
thus (1. L) * a = a * (x * a) by A4, A7
.= a * (1. L) by A1, A2, A3, A4, A5, A7, Lm6 ; ::_thesis: verum
end;
 ( a = 0. L implies (1. L) * a = a * (1. L) )
proof
assume A8: a = 0. L ; ::_thesis: (1. L) * a = a * (1. L)
hence (1. L) * a = 0. L by A5
.= a * (1. L) by A2, A8 ;
::_thesis: verum
end;
hence  (1. L) * a = a * (1. L) by A6; ::_thesis: verum
end;

Lm8:  for L being non empty doubleLoopStr st 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) holds
for a being Element of L st a <> 0. L holds
ex x being Element of L st x * a = 1. L
proof
let L be non empty doubleLoopStr ; ::_thesis: ( 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) implies for a being Element of L st a <> 0. L holds
ex x being Element of L st x * a = 1. L )
assume that
A1: ( 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) ) and
A2: for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L and
A3: ( ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a being Element of L holds a * (0. L) = 0. L ) ) ; ::_thesis: for a being Element of L st a <> 0. L holds
ex x being Element of L st x * a = 1. L
let a be Element of L; ::_thesis: ( a <> 0. L implies ex x being Element of L st x * a = 1. L )
assume  a <> 0. L ; ::_thesis: ex x being Element of L st x * a = 1. L
then consider x being Element of L such that
A4: a * x = 1. L by A2;
 x * a = 1. L by A1, A2, A3, A4, Lm6;
hence  ex x being Element of L st x * a = 1. L ; ::_thesis: verum
end;

theorem Th11: :: ALGSTR_2:11
for L being non empty doubleLoopStr holds
( L is _Skew-Field iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) )
proof
let L be non empty doubleLoopStr ; ::_thesis: ( L is _Skew-Field iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) )
thus  ( L is _Skew-Field implies ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) ) by ALGSTR_1:6, ALGSTR_1:16, GROUP_1:def_3, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, STRUCT_0:def_8, VECTSP_1:def_6, VECTSP_1:def_7; ::_thesis: ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) implies L is _Skew-Field )
assume A1: ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) ; ::_thesis: L is _Skew-Field
now__::_thesis:_(_(_for_a_being_Element_of_L_holds_(0._L)_+_a_=_a_)_&_(_for_a,_b_being_Element_of_L_ex_x_being_Element_of_L_st_a_+_x_=_b_)_&_(_for_a,_b_being_Element_of_L_ex_x_being_Element_of_L_st_x_+_a_=_b_)_&_(_for_a,_x,_y_being_Element_of_L_st_a_+_x_=_a_+_y_holds_
x_=_y_)_&_(_for_a,_x,_y_being_Element_of_L_st_x_+_a_=_y_+_a_holds_
x_=_y_)_&_(_for_a_being_Element_of_L_holds_(1._L)_*_a_=_a_)_&_(_for_a,_b_being_Element_of_L_st_a_<>_0._L_holds_
ex_x_being_Element_of_L_st_a_*_x_=_b_)_&_(_for_a,_b_being_Element_of_L_st_a_<>_0._L_holds_
ex_x_being_Element_of_L_st_x_*_a_=_b_)_&_(_for_a,_x,_y_being_Element_of_L_st_a_<>_0._L_&_a_*_x_=_a_*_y_holds_
x_=_y_)_&_(_for_a,_x,_y_being_Element_of_L_st_a_<>_0._L_&_x_*_a_=_y_*_a_holds_
x_=_y_)_)
thus A2: for a being Element of L holds (0. L) + a = a ::_thesis: ( ( for a, b being Element of L ex x being Element of L st a + x = b ) & ( for a, b being Element of L ex x being Element of L st x + a = b ) & ( for a, x, y being Element of L st a + x = a + y holds
x = y ) & ( for a, x, y being Element of L st x + a = y + a holds
x = y ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) )
proof
let a be Element of L; ::_thesis: (0. L) + a = a
thus (0. L) + a = a + (0. L) by A1
.= a by A1 ; ::_thesis: verum
end;
thus  for a, b being Element of L ex x being Element of L st a + x = b ::_thesis: ( ( for a, b being Element of L ex x being Element of L st x + a = b ) & ( for a, x, y being Element of L st a + x = a + y holds
x = y ) & ( for a, x, y being Element of L st x + a = y + a holds
x = y ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) )
proof
let a, b be Element of L; ::_thesis: ex x being Element of L st a + x = b
consider y being Element of L such that
A3: a + y = 0. L by A1;
take x = y + b; ::_thesis: a + x = b
thus a + x = (0. L) + b by A1, A3
.= b by A2 ; ::_thesis: verum
end;
thus  for a, b being Element of L ex x being Element of L st x + a = b ::_thesis: ( ( for a, x, y being Element of L st a + x = a + y holds
x = y ) & ( for a, x, y being Element of L st x + a = y + a holds
x = y ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) )
proof
let a, b be Element of L; ::_thesis: ex x being Element of L st x + a = b
consider y being Element of L such that
A4: y + a = 0. L by A1, ALGSTR_1:3;
take x = b + y; ::_thesis: x + a = b
thus x + a = b + (0. L) by A1, A4
.= b by A1 ; ::_thesis: verum
end;
thus  for a, x, y being Element of L st a + x = a + y holds
x = y ::_thesis: ( ( for a, x, y being Element of L st x + a = y + a holds
x = y ) & ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) )
proof
let a, x, y be Element of L; ::_thesis: ( a + x = a + y implies x = y )
consider z being Element of L such that
A5: z + a = 0. L by A1, ALGSTR_1:3;
assume  a + x = a + y ; ::_thesis: x = y
then (z + a) + x = z + (a + y) by A1
.= (z + a) + y by A1 ;
hence x = (0. L) + y by A2, A5
.= y by A2 ;
::_thesis: verum
end;
thus  for a, x, y being Element of L st x + a = y + a holds
x = y ::_thesis: ( ( for a being Element of L holds (1. L) * a = a ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) )
proof
let a, x, y be Element of L; ::_thesis: ( x + a = y + a implies x = y )
consider z being Element of L such that
A6: a + z = 0. L by A1;
assume  x + a = y + a ; ::_thesis: x = y
then x + (a + z) = (y + a) + z by A1
.= y + (a + z) by A1 ;
hence x = y + (0. L) by A1, A6
.= y by A1 ;
::_thesis: verum
end;
thus A7: for a being Element of L holds (1. L) * a = a ::_thesis: ( ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ) & ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) )
proof
let a be Element of L; ::_thesis: (1. L) * a = a
thus (1. L) * a = a * (1. L) by A1, Lm7
.= a by A1 ; ::_thesis: verum
end;
thus  for a, b being Element of L st a <> 0. L holds
ex x being Element of L st a * x = b ::_thesis: ( ( for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ) & ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) )
proof
let a, b be Element of L; ::_thesis: ( a <> 0. L implies ex x being Element of L st a * x = b )
assume  a <> 0. L ; ::_thesis: ex x being Element of L st a * x = b
then consider y being Element of L such that
A8: a * y = 1. L by A1;
take x = y * b; ::_thesis: a * x = b
thus a * x = (1. L) * b by A1, A8
.= b by A7 ; ::_thesis: verum
end;
thus  for a, b being Element of L st a <> 0. L holds
ex x being Element of L st x * a = b ::_thesis: ( ( for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ) & ( for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ) )
proof
let a, b be Element of L; ::_thesis: ( a <> 0. L implies ex x being Element of L st x * a = b )
assume  a <> 0. L ; ::_thesis: ex x being Element of L st x * a = b
then consider y being Element of L such that
A9: y * a = 1. L by A1, Lm8;
take x = b * y; ::_thesis: x * a = b
thus x * a = b * (1. L) by A1, A9
.= b by A1 ; ::_thesis: verum
end;
thus  for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
x = y ::_thesis: for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y
proof
let a, x, y be Element of L; ::_thesis: ( a <> 0. L & a * x = a * y implies x = y )
assume  a <> 0. L ; ::_thesis: ( not a * x = a * y or x = y )
then consider z being Element of L such that
A10: z * a = 1. L by A1, Lm8;
assume  a * x = a * y ; ::_thesis: x = y
then (z * a) * x = z * (a * y) by A1
.= (z * a) * y by A1 ;
hence x = (1. L) * y by A7, A10
.= y by A7 ;
::_thesis: verum
end;
thus  for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
x = y ::_thesis: verum
proof
let a, x, y be Element of L; ::_thesis: ( a <> 0. L & x * a = y * a implies x = y )
assume  a <> 0. L ; ::_thesis: ( not x * a = y * a or x = y )
then consider z being Element of L such that
A11: a * z = 1. L by A1;
assume  x * a = y * a ; ::_thesis: x = y
then x * (a * z) = (y * a) * z by A1
.= y * (a * z) by A1 ;
hence x = y * (1. L) by A1, A11
.= y by A1 ;
::_thesis: verum
end;
end;
hence  L is _Skew-Field by A1, ALGSTR_1:6, ALGSTR_1:16, ALGSTR_1:def_2, GROUP_1:def_3, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, STRUCT_0:def_8, VECTSP_1:def_6, VECTSP_1:def_7; ::_thesis: verum
end;

definition
mode _Field is commutative _Skew-Field;
end;

theorem :: ALGSTR_2:12
for L being non empty doubleLoopStr holds
( L is _Field iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b being Element of L holds a * b = b * a ) ) )
proof
let L be non empty doubleLoopStr ; ::_thesis: ( L is _Field iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b being Element of L holds a * b = b * a ) ) )
thus  ( L is _Field implies ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b being Element of L holds a * b = b * a ) ) ) by Th11, GROUP_1:def_12; ::_thesis: ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b being Element of L holds a * b = b * a ) implies L is _Field )
assume that
A1: ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) ) and
A2: for a being Element of L holds a * (0. L) = 0. L and
A3: for a, b, c being Element of L holds (a * b) * c = a * (b * c) and
A4: for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) and
A5: for a, b being Element of L holds a * b = b * a ; ::_thesis: L is _Field
A6: for a being Element of L holds (0. L) * a = 0. L
proof
let a be Element of L; ::_thesis: (0. L) * a = 0. L
thus (0. L) * a = a * (0. L) by A5
.= 0. L by A2 ; ::_thesis: verum
end;
 for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a)
proof
let a, b, c be Element of L; ::_thesis: (b + c) * a = (b * a) + (c * a)
thus (b + c) * a = a * (b + c) by A5
.= (a * b) + (a * c) by A4
.= (b * a) + (a * c) by A5
.= (b * a) + (c * a) by A5 ; ::_thesis: verum
end;
hence  L is _Field by A1, A2, A3, A4, A5, A6, Th11, GROUP_1:def_12; ::_thesis: verum
end;