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 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

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 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 ) )

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: verumx = 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 ) )

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 ) )

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 ) )

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 ) )

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 ) )

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 ) )

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 ) )

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 ) )

x = y :: thesis: for a, x, y being Element of L st a <> 0. L & x * a = y * a holds

x = y

x = y :: thesis: verum

end;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

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
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 (0. L) + a = a + (0. L) by A1

.= a by A1 ; :: thesis: verum

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

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
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;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

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

thus
for a, x, y being Element of L st a + x = a + y holds
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;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

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

thus
for a, x, y being Element of L st x + a = y + a holds
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;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

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

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
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;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

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

thus
for a, b being Element of L st a <> 0. L holds
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 (1. L) * a = a * (1. L) by A1, Lm7

.= a by A1 ; :: thesis: verum

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

thus
for a, b being Element of L st a <> 0. L holds
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;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

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

thus
for a, x, y being Element of L st a <> 0. L & a * x = a * y holds
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;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

x = y :: thesis: for a, x, y being Element of L st a <> 0. L & x * a = y * a holds

x = y

proof

thus
for a, x, y being Element of L st a <> 0. L & x * a = y * a holds
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;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

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;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