:: SYMSP_1 semantic presentation

K122() is Element of bool K118()
K118() is set
bool K118() is non empty set
K117() is set
bool K117() is non empty set
bool K122() is non empty set
{} is empty set
1 is non empty set
X is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
the non empty set is non empty set
[: the non empty set , the non empty set :] is non empty set
[:[: the non empty set , the non empty set :], the non empty set :] is non empty set
bool [:[: the non empty set , the non empty set :], the non empty set :] is non empty set
the V1() V4([: the non empty set , the non empty set :]) V5( the non empty set ) V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is V1() V4([: the non empty set , the non empty set :]) V5( the non empty set ) V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :]
the Element of the non empty set is Element of the non empty set
the carrier of X is non empty non trivial set
[: the carrier of X, the non empty set :] is non empty set
[:[: the carrier of X, the non empty set :], the non empty set :] is non empty set
bool [:[: the carrier of X, the non empty set :], the non empty set :] is non empty set
the V1() V4([: the carrier of X, the non empty set :]) V5( the non empty set ) V6() V18([: the carrier of X, the non empty set :], the non empty set ) Element of bool [:[: the carrier of X, the non empty set :], the non empty set :] is V1() V4([: the carrier of X, the non empty set :]) V5( the non empty set ) V6() V18([: the carrier of X, the non empty set :], the non empty set ) Element of bool [:[: the carrier of X, the non empty set :], the non empty set :]
bool [: the non empty set , the non empty set :] is non empty set
the V1() V4( the non empty set ) V5( the non empty set ) Element of bool [: the non empty set , the non empty set :] is V1() V4( the non empty set ) V5( the non empty set ) Element of bool [: the non empty set , the non empty set :]
(X, the non empty set , the V1() V4([: the non empty set , the non empty set :]) V5( the non empty set ) V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Element of the non empty set , the V1() V4([: the carrier of X, the non empty set :]) V5( the non empty set ) V6() V18([: the carrier of X, the non empty set :], the non empty set ) Element of bool [:[: the carrier of X, the non empty set :], the non empty set :], the V1() V4( the non empty set ) V5( the non empty set ) Element of bool [: the non empty set , the non empty set :]) is (X) (X)
the carrier of (X, the non empty set , the V1() V4([: the non empty set , the non empty set :]) V5( the non empty set ) V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Element of the non empty set , the V1() V4([: the carrier of X, the non empty set :]) V5( the non empty set ) V6() V18([: the carrier of X, the non empty set :], the non empty set ) Element of bool [:[: the carrier of X, the non empty set :], the non empty set :], the V1() V4( the non empty set ) V5( the non empty set ) Element of bool [: the non empty set , the non empty set :]) is set
X is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
o is (X)
the carrier of o is set
0 is empty Element of K122()
{0} is non empty set
o is Element of {0}
[:{0},{0}:] is non empty set
[:[:{0},{0}:],{0}:] is non empty set
bool [:[:{0},{0}:],{0}:] is non empty set
md is V1() V4([:{0},{0}:]) V5({0}) V6() V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:]
b is set
a is set
bool [:{0},{0}:] is non empty set
a is V1() V4({0}) V5({0}) Element of bool [:{0},{0}:]
x is V1() V4({0}) V5({0}) Element of bool [:{0},{0}:]
y is set
z is set
0F is Element of {0}
p is Element of {0}
[0F,p] is Element of [:{0},{0}:]
{0F,p} is non empty set
{0F} is non empty set
{{0F,p},{0F}} is non empty set
S is non empty set
[:S,S:] is non empty set
[:[:S,S:],S:] is non empty set
bool [:[:S,S:],S:] is non empty set
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
the carrier of F is non empty non trivial set
[: the carrier of F,S:] is non empty set
[:[: the carrier of F,S:],S:] is non empty set
bool [:[: the carrier of F,S:],S:] is non empty set
bool [:S,S:] is non empty set
b is V1() V4([:S,S:]) V5(S) V6() V18([:S,S:],S) Element of bool [:[:S,S:],S:]
a is Element of S
x is V1() V4([: the carrier of F,S:]) V5(S) V6() V18([: the carrier of F,S:],S) Element of bool [:[: the carrier of F,S:],S:]
y is V1() V4(S) V5(S) Element of bool [:S,S:]
(F,S,b,a,x,y) is (F) (F)
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
the carrier of F is non empty non trivial set
[: the carrier of F,{0}:] is non empty set
[:[: the carrier of F,{0}:],{0}:] is non empty set
bool [:[: the carrier of F,{0}:],{0}:] is non empty set
S is V1() V4([: the carrier of F,{0}:]) V5({0}) V6() V18([: the carrier of F,{0}:],{0}) Element of bool [:[: the carrier of F,{0}:],{0}:]
b is V1() V4({0}) V5({0}) Element of bool [:{0},{0}:]
(F,{0},md,o,S,b) is non empty (F) (F)
the carrier of (F,{0},md,o,S,b) is non empty set
x is Element of the carrier of (F,{0},md,o,S,b)
y is Element of the carrier of (F,{0},md,o,S,b)
x + y is Element of the carrier of (F,{0},md,o,S,b)
the addF of (F,{0},md,o,S,b) is V1() V4([: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):]) V5( the carrier of (F,{0},md,o,S,b)) V6() V18([: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b)) Element of bool [:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):]
[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):] is non empty set
[:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):] is non empty set
bool [:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):] is non empty set
the addF of (F,{0},md,o,S,b) . (x,y) is Element of the carrier of (F,{0},md,o,S,b)
y + x is Element of the carrier of (F,{0},md,o,S,b)
the addF of (F,{0},md,o,S,b) . (y,x) is Element of the carrier of (F,{0},md,o,S,b)
z is Element of {0}
0F is Element of {0}
md . (z,0F) is Element of {0}
the carrier of (F,{0},md,o,S,b) is non empty set
x is Element of the carrier of (F,{0},md,o,S,b)
y is Element of the carrier of (F,{0},md,o,S,b)
x + y is Element of the carrier of (F,{0},md,o,S,b)
the addF of (F,{0},md,o,S,b) is V1() V4([: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):]) V5( the carrier of (F,{0},md,o,S,b)) V6() V18([: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b)) Element of bool [:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):]
[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):] is non empty set
[:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):] is non empty set
bool [:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):] is non empty set
the addF of (F,{0},md,o,S,b) . (x,y) is Element of the carrier of (F,{0},md,o,S,b)
z is Element of the carrier of (F,{0},md,o,S,b)
(x + y) + z is Element of the carrier of (F,{0},md,o,S,b)
the addF of (F,{0},md,o,S,b) . ((x + y),z) is Element of the carrier of (F,{0},md,o,S,b)
y + z is Element of the carrier of (F,{0},md,o,S,b)
the addF of (F,{0},md,o,S,b) . (y,z) is Element of the carrier of (F,{0},md,o,S,b)
x + (y + z) is Element of the carrier of (F,{0},md,o,S,b)
the addF of (F,{0},md,o,S,b) . (x,(y + z)) is Element of the carrier of (F,{0},md,o,S,b)
0F is Element of {0}
p is Element of {0}
r is Element of {0}
md . (p,r) is Element of {0}
md . (0F,(md . (p,r))) is Element of {0}
the carrier of (F,{0},md,o,S,b) is non empty set
x is Element of the carrier of (F,{0},md,o,S,b)
0. (F,{0},md,o,S,b) is V51((F,{0},md,o,S,b)) Element of the carrier of (F,{0},md,o,S,b)
the ZeroF of (F,{0},md,o,S,b) is Element of the carrier of (F,{0},md,o,S,b)
x + (0. (F,{0},md,o,S,b)) is Element of the carrier of (F,{0},md,o,S,b)
the addF of (F,{0},md,o,S,b) is V1() V4([: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):]) V5( the carrier of (F,{0},md,o,S,b)) V6() V18([: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b)) Element of bool [:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):]
[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):] is non empty set
[:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):] is non empty set
bool [:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):] is non empty set
the addF of (F,{0},md,o,S,b) . (x,(0. (F,{0},md,o,S,b))) is Element of the carrier of (F,{0},md,o,S,b)
y is Element of {0}
md . (y,(0. (F,{0},md,o,S,b))) is set
the carrier of (F,{0},md,o,S,b) is non empty set
x is Element of the carrier of (F,{0},md,o,S,b)
- x is Element of the carrier of (F,{0},md,o,S,b)
x + (- x) is Element of the carrier of (F,{0},md,o,S,b)
the addF of (F,{0},md,o,S,b) is V1() V4([: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):]) V5( the carrier of (F,{0},md,o,S,b)) V6() V18([: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b)) Element of bool [:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):]
[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):] is non empty set
[:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):] is non empty set
bool [:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):] is non empty set
the addF of (F,{0},md,o,S,b) . (x,(- x)) is Element of the carrier of (F,{0},md,o,S,b)
0. (F,{0},md,o,S,b) is V51((F,{0},md,o,S,b)) Element of the carrier of (F,{0},md,o,S,b)
the ZeroF of (F,{0},md,o,S,b) is Element of the carrier of (F,{0},md,o,S,b)
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
the V1() V4({0}) V5({0}) Element of bool [:{0},{0}:] is V1() V4({0}) V5({0}) Element of bool [:{0},{0}:]
the carrier of F is non empty non trivial set
[: the carrier of F,{0}:] is non empty set
[:[: the carrier of F,{0}:],{0}:] is non empty set
bool [:[: the carrier of F,{0}:],{0}:] is non empty set
the V1() V4([: the carrier of F,{0}:]) V5({0}) V6() V18([: the carrier of F,{0}:],{0}) Element of bool [:[: the carrier of F,{0}:],{0}:] is V1() V4([: the carrier of F,{0}:]) V5({0}) V6() V18([: the carrier of F,{0}:],{0}) Element of bool [:[: the carrier of F,{0}:],{0}:]
(F,{0},md,o, the V1() V4([: the carrier of F,{0}:]) V5({0}) V6() V18([: the carrier of F,{0}:],{0}) Element of bool [:[: the carrier of F,{0}:],{0}:], the V1() V4({0}) V5({0}) Element of bool [:{0},{0}:]) is non empty (F) (F)
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
the carrier of F is non empty non trivial set
[: the carrier of F,{0}:] is non empty set
[:[: the carrier of F,{0}:],{0}:] is non empty set
bool [:[: the carrier of F,{0}:],{0}:] is non empty set
S is V1() V4([: the carrier of F,{0}:]) V5({0}) V6() V18([: the carrier of F,{0}:],{0}) Element of bool [:[: the carrier of F,{0}:],{0}:]
a is non empty right_complementable Abelian add-associative right_zeroed (F)
b is V1() V4({0}) V5({0}) Element of bool [:{0},{0}:]
(F,{0},md,o,S,b) is non empty (F) (F)
the carrier of a is non empty set
1_ F is Element of the carrier of F
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
x is Element of the carrier of F
y is Element of the carrier of F
x + y is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the addF of F . (x,y) is Element of the carrier of F
x * y is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
the multF of F . (x,y) is Element of the carrier of F
z is Element of the carrier of a
0F is Element of the carrier of a
z + 0F is Element of the carrier of a
the addF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) V6() V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
the addF of a . (z,0F) is Element of the carrier of a
x * (z + 0F) is Element of the carrier of a
x * z is Element of the carrier of a
x * 0F is Element of the carrier of a
(x * z) + (x * 0F) is Element of the carrier of a
the addF of a . ((x * z),(x * 0F)) is Element of the carrier of a
(x + y) * z is Element of the carrier of a
y * z is Element of the carrier of a
(x * z) + (y * z) is Element of the carrier of a
the addF of a . ((x * z),(y * z)) is Element of the carrier of a
(x * y) * z is Element of the carrier of a
x * (y * z) is Element of the carrier of a
(1_ F) * z is Element of the carrier of a
S . ((x * y),z) is set
r is Element of the carrier of a
v is Element of the carrier of a
(x * y) * v is Element of the carrier of a
v is Element of the carrier of a
S . (y,v) is set
v is Element of the carrier of a
y * v is Element of the carrier of a
x * (y * v) is Element of the carrier of a
S . (x,o) is Element of {0}
p is Element of {0}
r is Element of {0}
md . (p,r) is Element of {0}
v is Element of the carrier of a
v is Element of the carrier of a
v + v is Element of the carrier of a
the addF of a . (v,v) is Element of the carrier of a
x * (v + v) is Element of the carrier of a
S . (x,o) is Element of {0}
S . (x,v) is set
x * v is Element of the carrier of a
S . (x,v) is set
x * v is Element of the carrier of a
0. a is V51(a) Element of the carrier of a
the ZeroF of a is Element of the carrier of a
S . ((x + y),z) is set
r is Element of the carrier of a
v is Element of the carrier of a
(x + y) * v is Element of the carrier of a
v is Element of the carrier of a
S . (x,v) is set
v is Element of the carrier of a
x * v is Element of the carrier of a
v is Element of the carrier of a
S . (y,v) is set
0. a is V51(a) Element of the carrier of a
the ZeroF of a is Element of the carrier of a
v is Element of the carrier of a
y * v is Element of the carrier of a
S . ((1_ F),z) is set
r is Element of the carrier of a
S . ((1_ F),r) is set
S is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
the carrier of S is non empty non trivial set
[: the carrier of S,{0}:] is non empty set
[:[: the carrier of S,{0}:],{0}:] is non empty set
bool [:[: the carrier of S,{0}:],{0}:] is non empty set
a is V1() V4({0}) V5({0}) Element of bool [:{0},{0}:]
x is non empty right_complementable Abelian add-associative right_zeroed (S)
b is V1() V4([: the carrier of S,{0}:]) V5({0}) V6() V18([: the carrier of S,{0}:],{0}) Element of bool [:[: the carrier of S,{0}:],{0}:]
(S,{0},md,o,b,a) is non empty (S) (S)
the carrier of x is non empty set
0. x is V51(x) Element of the carrier of x
the ZeroF of x is Element of the carrier of x
y is Element of the carrier of x
y is Element of the carrier of x
z is Element of the carrier of x
[y,z] is Element of [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
0F is Element of {0}
p is Element of {0}
[0F,p] is Element of [:{0},{0}:]
{0F,p} is non empty set
{0F} is non empty set
{{0F,p},{0F}} is non empty set
y is Element of the carrier of x
z is Element of the carrier of x
0F is Element of the carrier of x
p is Element of the carrier of x
[y,z] is Element of [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
[0F,p] is Element of [: the carrier of x, the carrier of x:]
{0F,p} is non empty set
{0F} is non empty set
{{0F,p},{0F}} is non empty set
[y,z] is Element of [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
0F is Element of {0}
p is Element of {0}
[0F,p] is Element of [:{0},{0}:]
{0F,p} is non empty set
{0F} is non empty set
{{0F,p},{0F}} is non empty set
y is Element of the carrier of x
z is Element of the carrier of x
0F is Element of the carrier of S
0F * y is Element of the carrier of x
z is Element of the carrier of x
y is Element of the carrier of x
0F is Element of the carrier of x
z + 0F is Element of the carrier of x
the addF of x is V1() V4([: the carrier of x, the carrier of x:]) V5( the carrier of x) V6() V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the addF of x . (z,0F) is Element of the carrier of x
z is Element of the carrier of x
y is Element of the carrier of x
0F is Element of the carrier of x
y is Element of the carrier of x
z is Element of the carrier of x
0F is Element of the carrier of x
z + 0F is Element of the carrier of x
the addF of x is V1() V4([: the carrier of x, the carrier of x:]) V5( the carrier of x) V6() V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the addF of x . (z,0F) is Element of the carrier of x
0F + y is Element of the carrier of x
the addF of x . (0F,y) is Element of the carrier of x
y + z is Element of the carrier of x
the addF of x . (y,z) is Element of the carrier of x
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
the carrier of F is non empty non trivial set
[: the carrier of F,{0}:] is non empty set
[:[: the carrier of F,{0}:],{0}:] is non empty set
bool [:[: the carrier of F,{0}:],{0}:] is non empty set
S is V1() V4([: the carrier of F,{0}:]) V5({0}) V6() V18([: the carrier of F,{0}:],{0}) Element of bool [:[: the carrier of F,{0}:],{0}:]
b is V1() V4({0}) V5({0}) Element of bool [:{0},{0}:]
(F,{0},md,o,S,b) is non empty (F) (F)
a is non empty right_complementable Abelian add-associative right_zeroed (F)
the carrier of a is non empty set
0. a is V51(a) Element of the carrier of a
the ZeroF of a is Element of the carrier of a
x is Element of the carrier of a
y is Element of the carrier of a
z is Element of the carrier of a
0F is Element of the carrier of F
0F * y is Element of the carrier of a
r is Element of the carrier of a
p is Element of the carrier of a
v is Element of the carrier of a
r + v is Element of the carrier of a
the addF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) V6() V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
the addF of a . (r,v) is Element of the carrier of a
v is Element of the carrier of a
v is Element of the carrier of a
v is Element of the carrier of a
v is Element of the carrier of a
c₁₉ is Element of the carrier of a
c₂₀ is Element of the carrier of a
c₁₉ + c₂₀ is Element of the carrier of a
the addF of a . (c₁₉,c₂₀) is Element of the carrier of a
c₂₀ + v is Element of the carrier of a
the addF of a . (c₂₀,v) is Element of the carrier of a
v + c₁₉ is Element of the carrier of a
the addF of a . (v,c₁₉) is Element of the carrier of a
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
0. S is V51(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
b is Element of the carrier of S
0. F is V51(F) Element of the carrier of F
the carrier of F is non empty non trivial set
the ZeroF of F is Element of the carrier of F
y is Element of the carrier of F
y * b is Element of the carrier of S
(0. S) - (y * b) is Element of the carrier of S
- (y * b) is Element of the carrier of S
(0. S) + (- (y * b)) is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . ((0. S),(- (y * b))) is Element of the carrier of S
(0. F) * ((0. S) - (y * b)) is Element of the carrier of S
(0. F) * b is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
0. S is V51(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(0. S) + a is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . ((0. S),a) is Element of the carrier of S
a + b is Element of the carrier of S
the addF of S . (a,b) is Element of the carrier of S
b + (0. S) is Element of the carrier of S
the addF of S . (b,(0. S)) is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
x + b is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (x,b) is Element of the carrier of S
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
- (1_ F) is Element of the carrier of F
(- (1_ F)) * x is Element of the carrier of S
- x is Element of the carrier of S
(- x) + (x + b) is Element of the carrier of S
the addF of S . ((- x),(x + b)) is Element of the carrier of S
x + (- x) is Element of the carrier of S
the addF of S . (x,(- x)) is Element of the carrier of S
(x + (- x)) + b is Element of the carrier of S
the addF of S . ((x + (- x)),b) is Element of the carrier of S
0. S is V51(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(0. S) + b is Element of the carrier of S
the addF of S . ((0. S),b) is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
b + x is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (b,x) is Element of the carrier of S
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
- (1_ F) is Element of the carrier of F
(- (1_ F)) * x is Element of the carrier of S
- x is Element of the carrier of S
(b + x) + (- x) is Element of the carrier of S
the addF of S . ((b + x),(- x)) is Element of the carrier of S
x + (- x) is Element of the carrier of S
the addF of S . (x,(- x)) is Element of the carrier of S
b + (x + (- x)) is Element of the carrier of S
the addF of S . (b,(x + (- x))) is Element of the carrier of S
0. S is V51(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
b + (0. S) is Element of the carrier of S
the addF of S . (b,(0. S)) is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
the carrier of F is non empty non trivial set
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of F
x * b is Element of the carrier of S
x * a is Element of the carrier of S
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
z is Element of the carrier of F
z * x is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the multF of F . (z,x) is Element of the carrier of F
z * (x * a) is Element of the carrier of S
(1. F) * a is Element of the carrier of S
z is Element of the carrier of F
z * x is Element of the carrier of F
the multF of F . (z,x) is Element of the carrier of F
z * (x * b) is Element of the carrier of S
(1. F) * b is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
- b is Element of the carrier of S
a is Element of the carrier of S
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
- (1_ F) is Element of the carrier of F
(- (1_ F)) * b is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(1_ F) + (1_ F) is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the addF of F . ((1_ F),(1_ F)) is Element of the carrier of F
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
((1_ F) + (1_ F)) * b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
b + x is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (b,x) is Element of the carrier of S
(((1_ F) + (1_ F)) * b) + x is Element of the carrier of S
the addF of S . ((((1_ F) + (1_ F)) * b),x) is Element of the carrier of S
(1_ F) * b is Element of the carrier of S
((1_ F) * b) + ((1_ F) * b) is Element of the carrier of S
the addF of S . (((1_ F) * b),((1_ F) * b)) is Element of the carrier of S
(((1_ F) * b) + ((1_ F) * b)) + x is Element of the carrier of S
the addF of S . ((((1_ F) * b) + ((1_ F) * b)),x) is Element of the carrier of S
b + ((1_ F) * b) is Element of the carrier of S
the addF of S . (b,((1_ F) * b)) is Element of the carrier of S
(b + ((1_ F) * b)) + x is Element of the carrier of S
the addF of S . ((b + ((1_ F) * b)),x) is Element of the carrier of S
b + b is Element of the carrier of S
the addF of S . (b,b) is Element of the carrier of S
(b + b) + x is Element of the carrier of S
the addF of S . ((b + b),x) is Element of the carrier of S
b + (b + x) is Element of the carrier of S
the addF of S . (b,(b + x)) is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
y is Element of the carrier of S
b + y is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (b,y) is Element of the carrier of S
0. S is V51(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
- (1_ F) is Element of the carrier of F
(- (1_ F)) * y is Element of the carrier of S
(- (1_ F)) * b is Element of the carrier of S
- y is Element of the carrier of S
- b is Element of the carrier of S
(b + y) + (- y) is Element of the carrier of S
the addF of S . ((b + y),(- y)) is Element of the carrier of S
(- b) + (b + y) is Element of the carrier of S
the addF of S . ((- b),(b + y)) is Element of the carrier of S
y + (- y) is Element of the carrier of S
the addF of S . (y,(- y)) is Element of the carrier of S
b + (y + (- y)) is Element of the carrier of S
the addF of S . (b,(y + (- y))) is Element of the carrier of S
(- b) + b is Element of the carrier of S
the addF of S . ((- b),b) is Element of the carrier of S
((- b) + b) + y is Element of the carrier of S
the addF of S . (((- b) + b),y) is Element of the carrier of S
b + (0. S) is Element of the carrier of S
the addF of S . (b,(0. S)) is Element of the carrier of S
(0. S) + y is Element of the carrier of S
the addF of S . ((0. S),y) is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
0. S is V51(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
y is Element of the carrier of S
x + y is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (x,y) is Element of the carrier of S
z is Element of the carrier of S
y is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(1_ F) + (1_ F) is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the addF of F . ((1_ F),(1_ F)) is Element of the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
0. S is V51(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
y is Element of the carrier of S
z is Element of the carrier of S
((1_ F) + (1_ F)) * y is Element of the carrier of S
(((1_ F) + (1_ F)) * y) + z is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . ((((1_ F) + (1_ F)) * y),z) is Element of the carrier of S
y + z is Element of the carrier of S
the addF of S . (y,z) is Element of the carrier of S
0F is Element of the carrier of S
p is Element of the carrier of S
0F is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
b - a is Element of the carrier of S
- a is Element of the carrier of S
b + (- a) is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (b,(- a)) is Element of the carrier of S
x is Element of the carrier of S
y is Element of the carrier of S
b - y is Element of the carrier of S
- y is Element of the carrier of S
b + (- y) is Element of the carrier of S
the addF of S . (b,(- y)) is Element of the carrier of S
a - y is Element of the carrier of S
a + (- y) is Element of the carrier of S
the addF of S . (a,(- y)) is Element of the carrier of S
- (b - a) is Element of the carrier of S
- b is Element of the carrier of S
(- b) + a is Element of the carrier of S
the addF of S . ((- b),a) is Element of the carrier of S
a + (- b) is Element of the carrier of S
the addF of S . (a,(- b)) is Element of the carrier of S
(a + (- b)) + (b - y) is Element of the carrier of S
the addF of S . ((a + (- b)),(b - y)) is Element of the carrier of S
(- b) + (b - y) is Element of the carrier of S
the addF of S . ((- b),(b - y)) is Element of the carrier of S
a + ((- b) + (b - y)) is Element of the carrier of S
the addF of S . (a,((- b) + (b - y))) is Element of the carrier of S
(- b) + b is Element of the carrier of S
the addF of S . ((- b),b) is Element of the carrier of S
((- b) + b) + (- y) is Element of the carrier of S
the addF of S . (((- b) + b),(- y)) is Element of the carrier of S
a + (((- b) + b) + (- y)) is Element of the carrier of S
the addF of S . (a,(((- b) + b) + (- y))) is Element of the carrier of S
0. S is V51(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(0. S) + (- y) is Element of the carrier of S
the addF of S . ((0. S),(- y)) is Element of the carrier of S
a + ((0. S) + (- y)) is Element of the carrier of S
the addF of S . (a,((0. S) + (- y))) is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
the carrier of F is non empty non trivial set
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
y is Element of the carrier of F
y * b is Element of the carrier of S
x - (y * b) is Element of the carrier of S
- (y * b) is Element of the carrier of S
x + (- (y * b)) is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (x,(- (y * b))) is Element of the carrier of S
z is Element of the carrier of F
z * b is Element of the carrier of S
x - (z * b) is Element of the carrier of S
- (z * b) is Element of the carrier of S
x + (- (z * b)) is Element of the carrier of S
the addF of S . (x,(- (z * b))) is Element of the carrier of S
1_ F is Element of the carrier of F
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(y * b) - (z * b) is Element of the carrier of S
(y * b) + (- (z * b)) is Element of the carrier of S
the addF of S . ((y * b),(- (z * b))) is Element of the carrier of S
- (1_ F) is Element of the carrier of F
(- (1_ F)) * (z * b) is Element of the carrier of S
(y * b) + ((- (1_ F)) * (z * b)) is Element of the carrier of S
the addF of S . ((y * b),((- (1_ F)) * (z * b))) is Element of the carrier of S
(- (1_ F)) * z is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the multF of F . ((- (1_ F)),z) is Element of the carrier of F
((- (1_ F)) * z) * b is Element of the carrier of S
(y * b) + (((- (1_ F)) * z) * b) is Element of the carrier of S
the addF of S . ((y * b),(((- (1_ F)) * z) * b)) is Element of the carrier of S
z * (1_ F) is Element of the carrier of F
the multF of F . (z,(1_ F)) is Element of the carrier of F
- (z * (1_ F)) is Element of the carrier of F
(- (z * (1_ F))) * b is Element of the carrier of S
(y * b) + ((- (z * (1_ F))) * b) is Element of the carrier of S
the addF of S . ((y * b),((- (z * (1_ F))) * b)) is Element of the carrier of S
- z is Element of the carrier of F
(- z) * b is Element of the carrier of S
(y * b) + ((- z) * b) is Element of the carrier of S
the addF of S . ((y * b),((- z) * b)) is Element of the carrier of S
y + (- z) is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
the addF of F . (y,(- z)) is Element of the carrier of F
(y + (- z)) * b is Element of the carrier of S
(y + (- z)) " is Element of the carrier of F
((y + (- z)) ") * ((y + (- z)) * b) is Element of the carrier of S
((y + (- z)) ") * (y + (- z)) is Element of the carrier of F
the multF of F . (((y + (- z)) "),(y + (- z))) is Element of the carrier of F
(((y + (- z)) ") * (y + (- z))) * b is Element of the carrier of S
y - z is Element of the carrier of F
y + (- z) is Element of the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
(1_ F) * b is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(1_ F) + (1_ F) is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the addF of F . ((1_ F),(1_ F)) is Element of the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
0. S is V51(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
x is Element of the carrier of S
y is Element of the carrier of F
y * x is Element of the carrier of S
b - (y * x) is Element of the carrier of S
- (y * x) is Element of the carrier of S
b + (- (y * x)) is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (b,(- (y * x))) is Element of the carrier of S
b + (- (y * x)) is Element of the carrier of S
b + b is Element of the carrier of S
the addF of S . (b,b) is Element of the carrier of S
(1_ F) * b is Element of the carrier of S
b + ((1_ F) * b) is Element of the carrier of S
the addF of S . (b,((1_ F) * b)) is Element of the carrier of S
((1_ F) * b) + ((1_ F) * b) is Element of the carrier of S
the addF of S . (((1_ F) * b),((1_ F) * b)) is Element of the carrier of S
- (1_ F) is Element of the carrier of F
(- (1_ F)) * (y * x) is Element of the carrier of S
((1_ F) + (1_ F)) * b is Element of the carrier of S
(- (1_ F)) * y is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
the multF of F . ((- (1_ F)),y) is Element of the carrier of F
((- (1_ F)) * y) * x is Element of the carrier of S
y * (1_ F) is Element of the carrier of F
the multF of F . (y,(1_ F)) is Element of the carrier of F
- (y * (1_ F)) is Element of the carrier of F
(- (y * (1_ F))) * x is Element of the carrier of S
- y is Element of the carrier of F
(- y) * x is Element of the carrier of S
((1_ F) + (1_ F)) " is Element of the carrier of F
(((1_ F) + (1_ F)) ") * (((1_ F) + (1_ F)) * b) is Element of the carrier of S
b + ((- y) * x) is Element of the carrier of S
the addF of S . (b,((- y) * x)) is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
a is Element of the carrier of S
b is Element of the carrier of S
the carrier of F is non empty non trivial set
x is Element of the carrier of S
y is Element of the carrier of F
y * a is Element of the carrier of S
x - (y * a) is Element of the carrier of S
- (y * a) is Element of the carrier of S
x + (- (y * a)) is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (x,(- (y * a))) is Element of the carrier of S
z is Element of the carrier of F
z * a is Element of the carrier of S
x - (z * a) is Element of the carrier of S
- (z * a) is Element of the carrier of S
x + (- (z * a)) is Element of the carrier of S
the addF of S . (x,(- (z * a))) is Element of the carrier of S
y is Element of the carrier of F
z is Element of the carrier of F
0F is Element of the carrier of F
0F * a is Element of the carrier of S
x - (0F * a) is Element of the carrier of S
- (0F * a) is Element of the carrier of S
x + (- (0F * a)) is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (x,(- (0F * a))) is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
(F,S,a,b,x) is Element of the carrier of F
the carrier of F is non empty non trivial set
(F,S,a,b,x) * b is Element of the carrier of S
x - ((F,S,a,b,x) * b) is Element of the carrier of S
- ((F,S,a,b,x) * b) is Element of the carrier of S
x + (- ((F,S,a,b,x) * b)) is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (x,(- ((F,S,a,b,x) * b))) is Element of the carrier of S
y is Element of the carrier of F
y * b is Element of the carrier of S
x - (y * b) is Element of the carrier of S
- (y * b) is Element of the carrier of S
x + (- (y * b)) is Element of the carrier of S
the addF of S . (x,(- (y * b))) is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
the carrier of F is non empty non trivial set
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
(F,S,a,b,x) is Element of the carrier of F
y is Element of the carrier of F
y * x is Element of the carrier of S
(F,S,a,b,(y * x)) is Element of the carrier of F
y * (F,S,a,b,x) is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the multF of F . (y,(F,S,a,b,x)) is Element of the carrier of F
(F,S,a,b,x) * b is Element of the carrier of S
x - ((F,S,a,b,x) * b) is Element of the carrier of S
- ((F,S,a,b,x) * b) is Element of the carrier of S
x + (- ((F,S,a,b,x) * b)) is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (x,(- ((F,S,a,b,x) * b))) is Element of the carrier of S
y * (x - ((F,S,a,b,x) * b)) is Element of the carrier of S
y * ((F,S,a,b,x) * b) is Element of the carrier of S
(y * x) - (y * ((F,S,a,b,x) * b)) is Element of the carrier of S
- (y * ((F,S,a,b,x) * b)) is Element of the carrier of S
(y * x) + (- (y * ((F,S,a,b,x) * b))) is Element of the carrier of S
the addF of S . ((y * x),(- (y * ((F,S,a,b,x) * b)))) is Element of the carrier of S
(y * (F,S,a,b,x)) * b is Element of the carrier of S
(y * x) - ((y * (F,S,a,b,x)) * b) is Element of the carrier of S
- ((y * (F,S,a,b,x)) * b) is Element of the carrier of S
(y * x) + (- ((y * (F,S,a,b,x)) * b)) is Element of the carrier of S
the addF of S . ((y * x),(- ((y * (F,S,a,b,x)) * b))) is Element of the carrier of S
(F,S,a,b,(y * x)) * b is Element of the carrier of S
(y * x) - ((F,S,a,b,(y * x)) * b) is Element of the carrier of S
- ((F,S,a,b,(y * x)) * b) is Element of the carrier of S
(y * x) + (- ((F,S,a,b,(y * x)) * b)) is Element of the carrier of S
the addF of S . ((y * x),(- ((F,S,a,b,(y * x)) * b))) is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
(F,S,a,b,x) is Element of the carrier of F
the carrier of F is non empty non trivial set
y is Element of the carrier of S
x + y is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (x,y) is Element of the carrier of S
(F,S,a,b,(x + y)) is Element of the carrier of F
(F,S,a,b,y) is Element of the carrier of F
(F,S,a,b,x) + (F,S,a,b,y) is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the addF of F . ((F,S,a,b,x),(F,S,a,b,y)) is Element of the carrier of F
1_ F is Element of the carrier of F
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(F,S,a,b,x) * b is Element of the carrier of S
x - ((F,S,a,b,x) * b) is Element of the carrier of S
- ((F,S,a,b,x) * b) is Element of the carrier of S
x + (- ((F,S,a,b,x) * b)) is Element of the carrier of S
the addF of S . (x,(- ((F,S,a,b,x) * b))) is Element of the carrier of S
(F,S,a,b,y) * b is Element of the carrier of S
y - ((F,S,a,b,y) * b) is Element of the carrier of S
- ((F,S,a,b,y) * b) is Element of the carrier of S
y + (- ((F,S,a,b,y) * b)) is Element of the carrier of S
the addF of S . (y,(- ((F,S,a,b,y) * b))) is Element of the carrier of S
(x - ((F,S,a,b,x) * b)) + (y - ((F,S,a,b,y) * b)) is Element of the carrier of S
the addF of S . ((x - ((F,S,a,b,x) * b)),(y - ((F,S,a,b,y) * b))) is Element of the carrier of S
(- ((F,S,a,b,x) * b)) + x is Element of the carrier of S
the addF of S . ((- ((F,S,a,b,x) * b)),x) is Element of the carrier of S
((- ((F,S,a,b,x) * b)) + x) + y is Element of the carrier of S
the addF of S . (((- ((F,S,a,b,x) * b)) + x),y) is Element of the carrier of S
(((- ((F,S,a,b,x) * b)) + x) + y) + (- ((F,S,a,b,y) * b)) is Element of the carrier of S
the addF of S . ((((- ((F,S,a,b,x) * b)) + x) + y),(- ((F,S,a,b,y) * b))) is Element of the carrier of S
(x + y) + (- ((F,S,a,b,x) * b)) is Element of the carrier of S
the addF of S . ((x + y),(- ((F,S,a,b,x) * b))) is Element of the carrier of S
((x + y) + (- ((F,S,a,b,x) * b))) + (- ((F,S,a,b,y) * b)) is Element of the carrier of S
the addF of S . (((x + y) + (- ((F,S,a,b,x) * b))),(- ((F,S,a,b,y) * b))) is Element of the carrier of S
(- ((F,S,a,b,x) * b)) + (- ((F,S,a,b,y) * b)) is Element of the carrier of S
the addF of S . ((- ((F,S,a,b,x) * b)),(- ((F,S,a,b,y) * b))) is Element of the carrier of S
(x + y) + ((- ((F,S,a,b,x) * b)) + (- ((F,S,a,b,y) * b))) is Element of the carrier of S
the addF of S . ((x + y),((- ((F,S,a,b,x) * b)) + (- ((F,S,a,b,y) * b)))) is Element of the carrier of S
(1_ F) * (- ((F,S,a,b,x) * b)) is Element of the carrier of S
((1_ F) * (- ((F,S,a,b,x) * b))) + (- ((F,S,a,b,y) * b)) is Element of the carrier of S
the addF of S . (((1_ F) * (- ((F,S,a,b,x) * b))),(- ((F,S,a,b,y) * b))) is Element of the carrier of S
(x + y) + (((1_ F) * (- ((F,S,a,b,x) * b))) + (- ((F,S,a,b,y) * b))) is Element of the carrier of S
the addF of S . ((x + y),(((1_ F) * (- ((F,S,a,b,x) * b))) + (- ((F,S,a,b,y) * b)))) is Element of the carrier of S
(1_ F) * (- ((F,S,a,b,y) * b)) is Element of the carrier of S
((1_ F) * (- ((F,S,a,b,x) * b))) + ((1_ F) * (- ((F,S,a,b,y) * b))) is Element of the carrier of S
the addF of S . (((1_ F) * (- ((F,S,a,b,x) * b))),((1_ F) * (- ((F,S,a,b,y) * b)))) is Element of the carrier of S
(x + y) + (((1_ F) * (- ((F,S,a,b,x) * b))) + ((1_ F) * (- ((F,S,a,b,y) * b)))) is Element of the carrier of S
the addF of S . ((x + y),(((1_ F) * (- ((F,S,a,b,x) * b))) + ((1_ F) * (- ((F,S,a,b,y) * b))))) is Element of the carrier of S
- (F,S,a,b,x) is Element of the carrier of F
(- (F,S,a,b,x)) * b is Element of the carrier of S
(1_ F) * ((- (F,S,a,b,x)) * b) is Element of the carrier of S
((1_ F) * ((- (F,S,a,b,x)) * b)) + ((1_ F) * (- ((F,S,a,b,y) * b))) is Element of the carrier of S
the addF of S . (((1_ F) * ((- (F,S,a,b,x)) * b)),((1_ F) * (- ((F,S,a,b,y) * b)))) is Element of the carrier of S
(x + y) + (((1_ F) * ((- (F,S,a,b,x)) * b)) + ((1_ F) * (- ((F,S,a,b,y) * b)))) is Element of the carrier of S
the addF of S . ((x + y),(((1_ F) * ((- (F,S,a,b,x)) * b)) + ((1_ F) * (- ((F,S,a,b,y) * b))))) is Element of the carrier of S
- (F,S,a,b,y) is Element of the carrier of F
(- (F,S,a,b,y)) * b is Element of the carrier of S
(1_ F) * ((- (F,S,a,b,y)) * b) is Element of the carrier of S
((1_ F) * ((- (F,S,a,b,x)) * b)) + ((1_ F) * ((- (F,S,a,b,y)) * b)) is Element of the carrier of S
the addF of S . (((1_ F) * ((- (F,S,a,b,x)) * b)),((1_ F) * ((- (F,S,a,b,y)) * b))) is Element of the carrier of S
(x + y) + (((1_ F) * ((- (F,S,a,b,x)) * b)) + ((1_ F) * ((- (F,S,a,b,y)) * b))) is Element of the carrier of S
the addF of S . ((x + y),(((1_ F) * ((- (F,S,a,b,x)) * b)) + ((1_ F) * ((- (F,S,a,b,y)) * b)))) is Element of the carrier of S
(1_ F) * (- (F,S,a,b,x)) is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
the multF of F . ((1_ F),(- (F,S,a,b,x))) is Element of the carrier of F
((1_ F) * (- (F,S,a,b,x))) * b is Element of the carrier of S
(((1_ F) * (- (F,S,a,b,x))) * b) + ((1_ F) * ((- (F,S,a,b,y)) * b)) is Element of the carrier of S
the addF of S . ((((1_ F) * (- (F,S,a,b,x))) * b),((1_ F) * ((- (F,S,a,b,y)) * b))) is Element of the carrier of S
(x + y) + ((((1_ F) * (- (F,S,a,b,x))) * b) + ((1_ F) * ((- (F,S,a,b,y)) * b))) is Element of the carrier of S
the addF of S . ((x + y),((((1_ F) * (- (F,S,a,b,x))) * b) + ((1_ F) * ((- (F,S,a,b,y)) * b)))) is Element of the carrier of S
(- (F,S,a,b,x)) * (1_ F) is Element of the carrier of F
the multF of F . ((- (F,S,a,b,x)),(1_ F)) is Element of the carrier of F
((- (F,S,a,b,x)) * (1_ F)) * b is Element of the carrier of S
(1_ F) * (- (F,S,a,b,y)) is Element of the carrier of F
the multF of F . ((1_ F),(- (F,S,a,b,y))) is Element of the carrier of F
((1_ F) * (- (F,S,a,b,y))) * b is Element of the carrier of S
(((- (F,S,a,b,x)) * (1_ F)) * b) + (((1_ F) * (- (F,S,a,b,y))) * b) is Element of the carrier of S
the addF of S . ((((- (F,S,a,b,x)) * (1_ F)) * b),(((1_ F) * (- (F,S,a,b,y))) * b)) is Element of the carrier of S
(x + y) + ((((- (F,S,a,b,x)) * (1_ F)) * b) + (((1_ F) * (- (F,S,a,b,y))) * b)) is Element of the carrier of S
the addF of S . ((x + y),((((- (F,S,a,b,x)) * (1_ F)) * b) + (((1_ F) * (- (F,S,a,b,y))) * b))) is Element of the carrier of S
(- (F,S,a,b,y)) * (1_ F) is Element of the carrier of F
the multF of F . ((- (F,S,a,b,y)),(1_ F)) is Element of the carrier of F
((- (F,S,a,b,y)) * (1_ F)) * b is Element of the carrier of S
((- (F,S,a,b,x)) * b) + (((- (F,S,a,b,y)) * (1_ F)) * b) is Element of the carrier of S
the addF of S . (((- (F,S,a,b,x)) * b),(((- (F,S,a,b,y)) * (1_ F)) * b)) is Element of the carrier of S
(x + y) + (((- (F,S,a,b,x)) * b) + (((- (F,S,a,b,y)) * (1_ F)) * b)) is Element of the carrier of S
the addF of S . ((x + y),(((- (F,S,a,b,x)) * b) + (((- (F,S,a,b,y)) * (1_ F)) * b))) is Element of the carrier of S
((- (F,S,a,b,x)) * b) + ((- (F,S,a,b,y)) * b) is Element of the carrier of S
the addF of S . (((- (F,S,a,b,x)) * b),((- (F,S,a,b,y)) * b)) is Element of the carrier of S
(x + y) + (((- (F,S,a,b,x)) * b) + ((- (F,S,a,b,y)) * b)) is Element of the carrier of S
the addF of S . ((x + y),(((- (F,S,a,b,x)) * b) + ((- (F,S,a,b,y)) * b))) is Element of the carrier of S
(- (F,S,a,b,x)) + (- (F,S,a,b,y)) is Element of the carrier of F
the addF of F . ((- (F,S,a,b,x)),(- (F,S,a,b,y))) is Element of the carrier of F
((- (F,S,a,b,x)) + (- (F,S,a,b,y))) * b is Element of the carrier of S
(x + y) + (((- (F,S,a,b,x)) + (- (F,S,a,b,y))) * b) is Element of the carrier of S
the addF of S . ((x + y),(((- (F,S,a,b,x)) + (- (F,S,a,b,y))) * b)) is Element of the carrier of S
- ((F,S,a,b,x) + (F,S,a,b,y)) is Element of the carrier of F
(- ((F,S,a,b,x) + (F,S,a,b,y))) * b is Element of the carrier of S
(x + y) + ((- ((F,S,a,b,x) + (F,S,a,b,y))) * b) is Element of the carrier of S
the addF of S . ((x + y),((- ((F,S,a,b,x) + (F,S,a,b,y))) * b)) is Element of the carrier of S
((F,S,a,b,x) + (F,S,a,b,y)) * b is Element of the carrier of S
(x + y) - (((F,S,a,b,x) + (F,S,a,b,y)) * b) is Element of the carrier of S
- (((F,S,a,b,x) + (F,S,a,b,y)) * b) is Element of the carrier of S
(x + y) + (- (((F,S,a,b,x) + (F,S,a,b,y)) * b)) is Element of the carrier of S
the addF of S . ((x + y),(- (((F,S,a,b,x) + (F,S,a,b,y)) * b))) is Element of the carrier of S
(F,S,a,b,(x + y)) * b is Element of the carrier of S
(x + y) - ((F,S,a,b,(x + y)) * b) is Element of the carrier of S
- ((F,S,a,b,(x + y)) * b) is Element of the carrier of S
(x + y) + (- ((F,S,a,b,(x + y)) * b)) is Element of the carrier of S
the addF of S . ((x + y),(- ((F,S,a,b,(x + y)) * b))) is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
the carrier of F is non empty non trivial set
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
(F,S,a,b,x) is Element of the carrier of F
y is Element of the carrier of F
y * b is Element of the carrier of S
(F,S,a,(y * b),x) is Element of the carrier of F
y " is Element of the carrier of F
(y ") * (F,S,a,b,x) is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the multF of F . ((y "),(F,S,a,b,x)) is Element of the carrier of F
(F,S,a,(y * b),x) * (y * b) is Element of the carrier of S
x - ((F,S,a,(y * b),x) * (y * b)) is Element of the carrier of S
- ((F,S,a,(y * b),x) * (y * b)) is Element of the carrier of S
x + (- ((F,S,a,(y * b),x) * (y * b))) is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (x,(- ((F,S,a,(y * b),x) * (y * b)))) is Element of the carrier of S
(F,S,a,(y * b),x) * y is Element of the carrier of F
the multF of F . ((F,S,a,(y * b),x),y) is Element of the carrier of F
((F,S,a,(y * b),x) * y) * b is Element of the carrier of S
x - (((F,S,a,(y * b),x) * y) * b) is Element of the carrier of S
- (((F,S,a,(y * b),x) * y) * b) is Element of the carrier of S
x + (- (((F,S,a,(y * b),x) * y) * b)) is Element of the carrier of S
the addF of S . (x,(- (((F,S,a,(y * b),x) * y) * b))) is Element of the carrier of S
(F,S,a,b,x) * b is Element of the carrier of S
x - ((F,S,a,b,x) * b) is Element of the carrier of S
- ((F,S,a,b,x) * b) is Element of the carrier of S
x + (- ((F,S,a,b,x) * b)) is Element of the carrier of S
the addF of S . (x,(- ((F,S,a,b,x) * b))) is Element of the carrier of S
(F,S,a,b,x) * (y ") is Element of the carrier of F
the multF of F . ((F,S,a,b,x),(y ")) is Element of the carrier of F
((F,S,a,(y * b),x) * y) * (y ") is Element of the carrier of F
the multF of F . (((F,S,a,(y * b),x) * y),(y ")) is Element of the carrier of F
y * (y ") is Element of the carrier of F
the multF of F . (y,(y ")) is Element of the carrier of F
(F,S,a,(y * b),x) * (y * (y ")) is Element of the carrier of F
the multF of F . ((F,S,a,(y * b),x),(y * (y "))) is Element of the carrier of F
1_ F is Element of the carrier of F
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(F,S,a,(y * b),x) * (1_ F) is Element of the carrier of F
the multF of F . ((F,S,a,(y * b),x),(1_ F)) is Element of the carrier of F
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
the carrier of F is non empty non trivial set
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
(F,S,a,b,x) is Element of the carrier of F
y is Element of the carrier of F
y * a is Element of the carrier of S
(F,S,(y * a),b,x) is Element of the carrier of F
(F,S,(y * a),b,x) * b is Element of the carrier of S
x - ((F,S,(y * a),b,x) * b) is Element of the carrier of S
- ((F,S,(y * a),b,x) * b) is Element of the carrier of S
x + (- ((F,S,(y * a),b,x) * b)) is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (x,(- ((F,S,(y * a),b,x) * b))) is Element of the carrier of S
y " is Element of the carrier of F
(y ") * (y * a) is Element of the carrier of S
(y ") * y is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the multF of F . ((y "),y) is Element of the carrier of F
((y ") * y) * a is Element of the carrier of S
1_ F is Element of the carrier of F
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(1_ F) * a is Element of the carrier of S
(F,S,a,b,x) * b is Element of the carrier of S
x - ((F,S,a,b,x) * b) is Element of the carrier of S
- ((F,S,a,b,x) * b) is Element of the carrier of S
x + (- ((F,S,a,b,x) * b)) is Element of the carrier of S
the addF of S . (x,(- ((F,S,a,b,x) * b))) is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
b + x is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (b,x) is Element of the carrier of S
y is Element of the carrier of S
(F,S,a,(b + x),y) is Element of the carrier of F
the carrier of F is non empty non trivial set
(F,S,a,b,y) is Element of the carrier of F
y + x is Element of the carrier of S
the addF of S . (y,x) is Element of the carrier of S
(F,S,a,b,(y + x)) is Element of the carrier of F
0. S is V51(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(F,S,a,(b + x),y) * (b + x) is Element of the carrier of S
y - ((F,S,a,(b + x),y) * (b + x)) is Element of the carrier of S
- ((F,S,a,(b + x),y) * (b + x)) is Element of the carrier of S
y + (- ((F,S,a,(b + x),y) * (b + x))) is Element of the carrier of S
the addF of S . (y,(- ((F,S,a,(b + x),y) * (b + x)))) is Element of the carrier of S
(F,S,a,(b + x),y) * b is Element of the carrier of S
(F,S,a,(b + x),y) * x is Element of the carrier of S
((F,S,a,(b + x),y) * b) + ((F,S,a,(b + x),y) * x) is Element of the carrier of S
the addF of S . (((F,S,a,(b + x),y) * b),((F,S,a,(b + x),y) * x)) is Element of the carrier of S
y - (((F,S,a,(b + x),y) * b) + ((F,S,a,(b + x),y) * x)) is Element of the carrier of S
- (((F,S,a,(b + x),y) * b) + ((F,S,a,(b + x),y) * x)) is Element of the carrier of S
y + (- (((F,S,a,(b + x),y) * b) + ((F,S,a,(b + x),y) * x))) is Element of the carrier of S
the addF of S . (y,(- (((F,S,a,(b + x),y) * b) + ((F,S,a,(b + x),y) * x)))) is Element of the carrier of S
y - ((F,S,a,(b + x),y) * b) is Element of the carrier of S
- ((F,S,a,(b + x),y) * b) is Element of the carrier of S
y + (- ((F,S,a,(b + x),y) * b)) is Element of the carrier of S
the addF of S . (y,(- ((F,S,a,(b + x),y) * b))) is Element of the carrier of S
(y - ((F,S,a,(b + x),y) * b)) - ((F,S,a,(b + x),y) * x) is Element of the carrier of S
- ((F,S,a,(b + x),y) * x) is Element of the carrier of S
(y - ((F,S,a,(b + x),y) * b)) + (- ((F,S,a,(b + x),y) * x)) is Element of the carrier of S
the addF of S . ((y - ((F,S,a,(b + x),y) * b)),(- ((F,S,a,(b + x),y) * x))) is Element of the carrier of S
(F,S,a,b,(y + x)) * b is Element of the carrier of S
(y + x) - ((F,S,a,b,(y + x)) * b) is Element of the carrier of S
- ((F,S,a,b,(y + x)) * b) is Element of the carrier of S
(y + x) + (- ((F,S,a,b,(y + x)) * b)) is Element of the carrier of S
the addF of S . ((y + x),(- ((F,S,a,b,(y + x)) * b))) is Element of the carrier of S
- x is Element of the carrier of S
x + y is Element of the carrier of S
the addF of S . (x,y) is Element of the carrier of S
(x + y) - ((F,S,a,b,(y + x)) * b) is Element of the carrier of S
(x + y) + (- ((F,S,a,b,(y + x)) * b)) is Element of the carrier of S
the addF of S . ((x + y),(- ((F,S,a,b,(y + x)) * b))) is Element of the carrier of S
(- x) + ((x + y) - ((F,S,a,b,(y + x)) * b)) is Element of the carrier of S
the addF of S . ((- x),((x + y) - ((F,S,a,b,(y + x)) * b))) is Element of the carrier of S
y + (- ((F,S,a,b,(y + x)) * b)) is Element of the carrier of S
the addF of S . (y,(- ((F,S,a,b,(y + x)) * b))) is Element of the carrier of S
x + (y + (- ((F,S,a,b,(y + x)) * b))) is Element of the carrier of S
the addF of S . (x,(y + (- ((F,S,a,b,(y + x)) * b)))) is Element of the carrier of S
(- x) + (x + (y + (- ((F,S,a,b,(y + x)) * b)))) is Element of the carrier of S
the addF of S . ((- x),(x + (y + (- ((F,S,a,b,(y + x)) * b))))) is Element of the carrier of S
(- x) + x is Element of the carrier of S
the addF of S . ((- x),x) is Element of the carrier of S
((- x) + x) + (y + (- ((F,S,a,b,(y + x)) * b))) is Element of the carrier of S
the addF of S . (((- x) + x),(y + (- ((F,S,a,b,(y + x)) * b)))) is Element of the carrier of S
(0. S) + (y + (- ((F,S,a,b,(y + x)) * b))) is Element of the carrier of S
the addF of S . ((0. S),(y + (- ((F,S,a,b,(y + x)) * b)))) is Element of the carrier of S
y - ((F,S,a,b,(y + x)) * b) is Element of the carrier of S
y + (- ((F,S,a,b,(y + x)) * b)) is Element of the carrier of S
y + (- ((F,S,a,(b + x),y) * b)) is Element of the carrier of S
(y + (- ((F,S,a,(b + x),y) * b))) - ((F,S,a,(b + x),y) * x) is Element of the carrier of S
(y + (- ((F,S,a,(b + x),y) * b))) + (- ((F,S,a,(b + x),y) * x)) is Element of the carrier of S
the addF of S . ((y + (- ((F,S,a,(b + x),y) * b))),(- ((F,S,a,(b + x),y) * x))) is Element of the carrier of S
((y + (- ((F,S,a,(b + x),y) * b))) - ((F,S,a,(b + x),y) * x)) + ((F,S,a,(b + x),y) * x) is Element of the carrier of S
the addF of S . (((y + (- ((F,S,a,(b + x),y) * b))) - ((F,S,a,(b + x),y) * x)),((F,S,a,(b + x),y) * x)) is Element of the carrier of S
(- ((F,S,a,(b + x),y) * x)) + ((F,S,a,(b + x),y) * x) is Element of the carrier of S
the addF of S . ((- ((F,S,a,(b + x),y) * x)),((F,S,a,(b + x),y) * x)) is Element of the carrier of S
(y + (- ((F,S,a,(b + x),y) * b))) + ((- ((F,S,a,(b + x),y) * x)) + ((F,S,a,(b + x),y) * x)) is Element of the carrier of S
the addF of S . ((y + (- ((F,S,a,(b + x),y) * b))),((- ((F,S,a,(b + x),y) * x)) + ((F,S,a,(b + x),y) * x))) is Element of the carrier of S
(y + (- ((F,S,a,(b + x),y) * b))) + (0. S) is Element of the carrier of S
the addF of S . ((y + (- ((F,S,a,(b + x),y) * b))),(0. S)) is Element of the carrier of S
(F,S,a,b,y) * b is Element of the carrier of S
y - ((F,S,a,b,y) * b) is Element of the carrier of S
- ((F,S,a,b,y) * b) is Element of the carrier of S
y + (- ((F,S,a,b,y) * b)) is Element of the carrier of S
the addF of S . (y,(- ((F,S,a,b,y) * b))) is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
a + x is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (a,x) is Element of the carrier of S
y is Element of the carrier of S
(F,S,(a + x),b,y) is Element of the carrier of F
the carrier of F is non empty non trivial set
(F,S,a,b,y) is Element of the carrier of F
(F,S,a,b,y) * b is Element of the carrier of S
- ((F,S,a,b,y) * b) is Element of the carrier of S
y + (- ((F,S,a,b,y) * b)) is Element of the carrier of S
the addF of S . (y,(- ((F,S,a,b,y) * b))) is Element of the carrier of S
y - ((F,S,a,b,y) * b) is Element of the carrier of S
y + (- ((F,S,a,b,y) * b)) is Element of the carrier of S
(F,S,(a + x),b,y) * b is Element of the carrier of S
y - ((F,S,(a + x),b,y) * b) is Element of the carrier of S
- ((F,S,(a + x),b,y) * b) is Element of the carrier of S
y + (- ((F,S,(a + x),b,y) * b)) is Element of the carrier of S
the addF of S . (y,(- ((F,S,(a + x),b,y) * b))) is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
x - b is Element of the carrier of S
- b is Element of the carrier of S
x + (- b) is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (x,(- b)) is Element of the carrier of S
(F,S,a,b,x) is Element of the carrier of F
(1_ F) * b is Element of the carrier of S
x - ((1_ F) * b) is Element of the carrier of S
- ((1_ F) * b) is Element of the carrier of S
x + (- ((1_ F) * b)) is Element of the carrier of S
the addF of S . (x,(- ((1_ F) * b))) is Element of the carrier of S
(F,S,a,b,x) * b is Element of the carrier of S
x - ((F,S,a,b,x) * b) is Element of the carrier of S
- ((F,S,a,b,x) * b) is Element of the carrier of S
x + (- ((F,S,a,b,x) * b)) is Element of the carrier of S
the addF of S . (x,(- ((F,S,a,b,x) * b))) is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
(F,S,a,b,b) is Element of the carrier of F
b - b is Element of the carrier of S
- b is Element of the carrier of S
b + (- b) is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (b,(- b)) is Element of the carrier of S
0. S is V51(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
0. F is V51(F) Element of the carrier of F
the carrier of F is non empty non trivial set
the ZeroF of F is Element of the carrier of F
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
(F,S,a,b,x) is Element of the carrier of F
0. S is V51(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
x + (0. S) is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (x,(0. S)) is Element of the carrier of S
- (0. S) is Element of the carrier of S
x + (- (0. S)) is Element of the carrier of S
the addF of S . (x,(- (0. S))) is Element of the carrier of S
(0. F) * b is Element of the carrier of S
x - ((0. F) * b) is Element of the carrier of S
- ((0. F) * b) is Element of the carrier of S
x + (- ((0. F) * b)) is Element of the carrier of S
the addF of S . (x,(- ((0. F) * b))) is Element of the carrier of S
(F,S,a,b,x) * b is Element of the carrier of S
x - ((F,S,a,b,x) * b) is Element of the carrier of S
- ((F,S,a,b,x) * b) is Element of the carrier of S
x + (- ((F,S,a,b,x) * b)) is Element of the carrier of S
the addF of S . (x,(- ((F,S,a,b,x) * b))) is Element of the carrier of S
x - (0. S) is Element of the carrier of S
x + (- (0. S)) is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
(F,S,a,b,x) is Element of the carrier of F
the carrier of F is non empty non trivial set
(F,S,a,b,x) " is Element of the carrier of F
y is Element of the carrier of S
(F,S,a,b,y) is Element of the carrier of F
(F,S,a,b,y) * ((F,S,a,b,x) ") is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the multF of F . ((F,S,a,b,y),((F,S,a,b,x) ")) is Element of the carrier of F
(F,S,a,x,y) is Element of the carrier of F
(F,S,a,x,y) * x is Element of the carrier of S
(F,S,a,b,((F,S,a,x,y) * x)) is Element of the carrier of F
(F,S,a,b,((F,S,a,x,y) * x)) * b is Element of the carrier of S
((F,S,a,x,y) * x) - ((F,S,a,b,((F,S,a,x,y) * x)) * b) is Element of the carrier of S
- ((F,S,a,b,((F,S,a,x,y) * x)) * b) is Element of the carrier of S
((F,S,a,x,y) * x) + (- ((F,S,a,b,((F,S,a,x,y) * x)) * b)) is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (((F,S,a,x,y) * x),(- ((F,S,a,b,((F,S,a,x,y) * x)) * b))) is Element of the carrier of S
y - ((F,S,a,x,y) * x) is Element of the carrier of S
- ((F,S,a,x,y) * x) is Element of the carrier of S
y + (- ((F,S,a,x,y) * x)) is Element of the carrier of S
the addF of S . (y,(- ((F,S,a,x,y) * x))) is Element of the carrier of S
y + (- ((F,S,a,x,y) * x)) is Element of the carrier of S
(y + (- ((F,S,a,x,y) * x))) + (((F,S,a,x,y) * x) - ((F,S,a,b,((F,S,a,x,y) * x)) * b)) is Element of the carrier of S
the addF of S . ((y + (- ((F,S,a,x,y) * x))),(((F,S,a,x,y) * x) - ((F,S,a,b,((F,S,a,x,y) * x)) * b))) is Element of the carrier of S
(y + (- ((F,S,a,x,y) * x))) + ((F,S,a,x,y) * x) is Element of the carrier of S
the addF of S . ((y + (- ((F,S,a,x,y) * x))),((F,S,a,x,y) * x)) is Element of the carrier of S
((y + (- ((F,S,a,x,y) * x))) + ((F,S,a,x,y) * x)) + (- ((F,S,a,b,((F,S,a,x,y) * x)) * b)) is Element of the carrier of S
the addF of S . (((y + (- ((F,S,a,x,y) * x))) + ((F,S,a,x,y) * x)),(- ((F,S,a,b,((F,S,a,x,y) * x)) * b))) is Element of the carrier of S
(- ((F,S,a,x,y) * x)) + ((F,S,a,x,y) * x) is Element of the carrier of S
the addF of S . ((- ((F,S,a,x,y) * x)),((F,S,a,x,y) * x)) is Element of the carrier of S
y + ((- ((F,S,a,x,y) * x)) + ((F,S,a,x,y) * x)) is Element of the carrier of S
the addF of S . (y,((- ((F,S,a,x,y) * x)) + ((F,S,a,x,y) * x))) is Element of the carrier of S
(y + ((- ((F,S,a,x,y) * x)) + ((F,S,a,x,y) * x))) + (- ((F,S,a,b,((F,S,a,x,y) * x)) * b)) is Element of the carrier of S
the addF of S . ((y + ((- ((F,S,a,x,y) * x)) + ((F,S,a,x,y) * x))),(- ((F,S,a,b,((F,S,a,x,y) * x)) * b))) is Element of the carrier of S
0. S is V51(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
y + (0. S) is Element of the carrier of S
the addF of S . (y,(0. S)) is Element of the carrier of S
(y + (0. S)) + (- ((F,S,a,b,((F,S,a,x,y) * x)) * b)) is Element of the carrier of S
the addF of S . ((y + (0. S)),(- ((F,S,a,b,((F,S,a,x,y) * x)) * b))) is Element of the carrier of S
y + (- ((F,S,a,b,((F,S,a,x,y) * x)) * b)) is Element of the carrier of S
the addF of S . (y,(- ((F,S,a,b,((F,S,a,x,y) * x)) * b))) is Element of the carrier of S
(F,S,a,x,y) * (F,S,a,b,x) is Element of the carrier of F
the multF of F . ((F,S,a,x,y),(F,S,a,b,x)) is Element of the carrier of F
((F,S,a,x,y) * (F,S,a,b,x)) * b is Element of the carrier of S
y - (((F,S,a,x,y) * (F,S,a,b,x)) * b) is Element of the carrier of S
- (((F,S,a,x,y) * (F,S,a,b,x)) * b) is Element of the carrier of S
y + (- (((F,S,a,x,y) * (F,S,a,b,x)) * b)) is Element of the carrier of S
the addF of S . (y,(- (((F,S,a,x,y) * (F,S,a,b,x)) * b))) is Element of the carrier of S
(F,S,a,b,y) * b is Element of the carrier of S
y - ((F,S,a,b,y) * b) is Element of the carrier of S
- ((F,S,a,b,y) * b) is Element of the carrier of S
y + (- ((F,S,a,b,y) * b)) is Element of the carrier of S
the addF of S . (y,(- ((F,S,a,b,y) * b))) is Element of the carrier of S
(F,S,a,b,x) * ((F,S,a,b,x) ") is Element of the carrier of F
the multF of F . ((F,S,a,b,x),((F,S,a,b,x) ")) is Element of the carrier of F
(F,S,a,x,y) * ((F,S,a,b,x) * ((F,S,a,b,x) ")) is Element of the carrier of F
the multF of F . ((F,S,a,x,y),((F,S,a,b,x) * ((F,S,a,b,x) "))) is Element of the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
1_ F is Element of the carrier of F
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(F,S,a,x,y) * (1_ F) is Element of the carrier of F
the multF of F . ((F,S,a,x,y),(1_ F)) is Element of the carrier of F
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
(F,S,a,b,x) is Element of the carrier of F
the carrier of F is non empty non trivial set
(F,S,a,x,b) is Element of the carrier of F
(F,S,a,x,b) " is Element of the carrier of F
1_ F is Element of the carrier of F
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
(F,S,a,b,b) is Element of the carrier of F
(F,S,a,b,x) " is Element of the carrier of F
(F,S,a,b,b) * ((F,S,a,b,x) ") is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the multF of F . ((F,S,a,b,b),((F,S,a,b,x) ")) is Element of the carrier of F
((F,S,a,b,x) ") * (1_ F) is Element of the carrier of F
the multF of F . (((F,S,a,b,x) "),(1_ F)) is Element of the carrier of F
(F,S,a,x,b) * (F,S,a,b,x) is Element of the carrier of F
the multF of F . ((F,S,a,x,b),(F,S,a,b,x)) is Element of the carrier of F
((F,S,a,x,b) ") * ((F,S,a,x,b) * (F,S,a,b,x)) is Element of the carrier of F
the multF of F . (((F,S,a,x,b) "),((F,S,a,x,b) * (F,S,a,b,x))) is Element of the carrier of F
((F,S,a,x,b) ") * (F,S,a,x,b) is Element of the carrier of F
the multF of F . (((F,S,a,x,b) "),(F,S,a,x,b)) is Element of the carrier of F
(((F,S,a,x,b) ") * (F,S,a,x,b)) * (F,S,a,b,x) is Element of the carrier of F
the multF of F . ((((F,S,a,x,b) ") * (F,S,a,x,b)),(F,S,a,b,x)) is Element of the carrier of F
(F,S,a,b,x) * (1_ F) is Element of the carrier of F
the multF of F . ((F,S,a,b,x),(1_ F)) is Element of the carrier of F
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
x + a is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (x,a) is Element of the carrier of S
(F,S,a,b,x) is Element of the carrier of F
the carrier of F is non empty non trivial set
(F,S,x,b,a) is Element of the carrier of F
(F,S,a,b,x) * b is Element of the carrier of S
- ((F,S,a,b,x) * b) is Element of the carrier of S
x - ((F,S,a,b,x) * b) is Element of the carrier of S
x + (- ((F,S,a,b,x) * b)) is Element of the carrier of S
the addF of S . (x,(- ((F,S,a,b,x) * b))) is Element of the carrier of S
(- ((F,S,a,b,x) * b)) + x is Element of the carrier of S
the addF of S . ((- ((F,S,a,b,x) * b)),x) is Element of the carrier of S
a + (- ((F,S,a,b,x) * b)) is Element of the carrier of S
the addF of S . (a,(- ((F,S,a,b,x) * b))) is Element of the carrier of S
a - ((F,S,a,b,x) * b) is Element of the carrier of S
a + (- ((F,S,a,b,x) * b)) is Element of the carrier of S
(F,S,x,b,a) * b is Element of the carrier of S
a - ((F,S,x,b,a) * b) is Element of the carrier of S
- ((F,S,x,b,a) * b) is Element of the carrier of S
a + (- ((F,S,x,b,a) * b)) is Element of the carrier of S
the addF of S . (a,(- ((F,S,x,b,a) * b))) is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
(F,S,x,a,b) is Element of the carrier of F
the carrier of F is non empty non trivial set
(F,S,a,b,x) is Element of the carrier of F
(F,S,a,b,x) " is Element of the carrier of F
- ((F,S,a,b,x) ") is Element of the carrier of F
(F,S,b,a,x) is Element of the carrier of F
(- ((F,S,a,b,x) ")) * (F,S,b,a,x) is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the multF of F . ((- ((F,S,a,b,x) ")),(F,S,b,a,x)) is Element of the carrier of F
1_ F is Element of the carrier of F
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
- (1_ F) is Element of the carrier of F
((F,S,a,b,x) ") * (F,S,a,b,x) is Element of the carrier of F
the multF of F . (((F,S,a,b,x) "),(F,S,a,b,x)) is Element of the carrier of F
(- (1_ F)) * (((F,S,a,b,x) ") * (F,S,a,b,x)) is Element of the carrier of F
the multF of F . ((- (1_ F)),(((F,S,a,b,x) ") * (F,S,a,b,x))) is Element of the carrier of F
(- (1_ F)) * (1_ F) is Element of the carrier of F
the multF of F . ((- (1_ F)),(1_ F)) is Element of the carrier of F
(- (1_ F)) * ((F,S,a,b,x) ") is Element of the carrier of F
the multF of F . ((- (1_ F)),((F,S,a,b,x) ")) is Element of the carrier of F
((- (1_ F)) * ((F,S,a,b,x) ")) * (F,S,a,b,x) is Element of the carrier of F
the multF of F . (((- (1_ F)) * ((F,S,a,b,x) ")),(F,S,a,b,x)) is Element of the carrier of F
((F,S,a,b,x) ") * (1_ F) is Element of the carrier of F
the multF of F . (((F,S,a,b,x) "),(1_ F)) is Element of the carrier of F
- (((F,S,a,b,x) ") * (1_ F)) is Element of the carrier of F
(- (((F,S,a,b,x) ") * (1_ F))) * (F,S,a,b,x) is Element of the carrier of F
the multF of F . ((- (((F,S,a,b,x) ") * (1_ F))),(F,S,a,b,x)) is Element of the carrier of F
(- ((F,S,a,b,x) ")) * (F,S,a,b,x) is Element of the carrier of F
the multF of F . ((- ((F,S,a,b,x) ")),(F,S,a,b,x)) is Element of the carrier of F
(- ((F,S,a,b,x) ")) * x is Element of the carrier of S
(F,S,a,b,((- ((F,S,a,b,x) ")) * x)) is Element of the carrier of F
(- (1_ F)) * b is Element of the carrier of S
((- ((F,S,a,b,x) ")) * x) - ((- (1_ F)) * b) is Element of the carrier of S
- ((- (1_ F)) * b) is Element of the carrier of S
((- ((F,S,a,b,x) ")) * x) + (- ((- (1_ F)) * b)) is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (((- ((F,S,a,b,x) ")) * x),(- ((- (1_ F)) * b))) is Element of the carrier of S
- b is Element of the carrier of S
((- ((F,S,a,b,x) ")) * x) - (- b) is Element of the carrier of S
- (- b) is Element of the carrier of S
((- ((F,S,a,b,x) ")) * x) + (- (- b)) is Element of the carrier of S
the addF of S . (((- ((F,S,a,b,x) ")) * x),(- (- b))) is Element of the carrier of S
((- ((F,S,a,b,x) ")) * x) + b is Element of the carrier of S
the addF of S . (((- ((F,S,a,b,x) ")) * x),b) is Element of the carrier of S
(F,S,b,a,((- ((F,S,a,b,x) ")) * x)) is Element of the carrier of F
(F,S,((- ((F,S,a,b,x) ")) * x),a,b) is Element of the carrier of F
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(1_ F) + (1_ F) is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the addF of F . ((1_ F),(1_ F)) is Element of the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
(F,S,b,a,x) is Element of the carrier of F
y is Element of the carrier of S
(F,S,y,x,a) is Element of the carrier of F
(F,S,b,a,x) * (F,S,y,x,a) is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
the multF of F . ((F,S,b,a,x),(F,S,y,x,a)) is Element of the carrier of F
(F,S,a,b,y) is Element of the carrier of F
(F,S,x,y,b) is Element of the carrier of F
(F,S,a,b,y) * (F,S,x,y,b) is Element of the carrier of F
the multF of F . ((F,S,a,b,y),(F,S,x,y,b)) is Element of the carrier of F
a + b is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (a,b) is Element of the carrier of S
(F,S,y,x,(a + b)) is Element of the carrier of F
(F,S,x,(a + b),y) is Element of the carrier of F
(F,S,x,(a + b),y) " is Element of the carrier of F
- ((F,S,x,(a + b),y) ") is Element of the carrier of F
(F,S,(a + b),x,y) is Element of the carrier of F
(- ((F,S,x,(a + b),y) ")) * (F,S,(a + b),x,y) is Element of the carrier of F
the multF of F . ((- ((F,S,x,(a + b),y) ")),(F,S,(a + b),x,y)) is Element of the carrier of F
(F,S,b,(a + b),x) is Element of the carrier of F
(F,S,(a + b),x,b) is Element of the carrier of F
(F,S,(a + b),x,b) " is Element of the carrier of F
- ((F,S,(a + b),x,b) ") is Element of the carrier of F
(F,S,x,(a + b),b) is Element of the carrier of F
(- ((F,S,(a + b),x,b) ")) * (F,S,x,(a + b),b) is Element of the carrier of F
the multF of F . ((- ((F,S,(a + b),x,b) ")),(F,S,x,(a + b),b)) is Element of the carrier of F
(F,S,x,(a + b),b) * (- ((F,S,(a + b),x,b) ")) is Element of the carrier of F
the multF of F . ((F,S,x,(a + b),b),(- ((F,S,(a + b),x,b) "))) is Element of the carrier of F
((F,S,x,(a + b),b) * (- ((F,S,(a + b),x,b) "))) * (- ((F,S,x,(a + b),y) ")) is Element of the carrier of F
the multF of F . (((F,S,x,(a + b),b) * (- ((F,S,(a + b),x,b) "))),(- ((F,S,x,(a + b),y) "))) is Element of the carrier of F
(((F,S,x,(a + b),b) * (- ((F,S,(a + b),x,b) "))) * (- ((F,S,x,(a + b),y) "))) * (F,S,(a + b),x,y) is Element of the carrier of F
the multF of F . ((((F,S,x,(a + b),b) * (- ((F,S,(a + b),x,b) "))) * (- ((F,S,x,(a + b),y) "))),(F,S,(a + b),x,y)) is Element of the carrier of F
(- ((F,S,(a + b),x,b) ")) * (- ((F,S,x,(a + b),y) ")) is Element of the carrier of F
the multF of F . ((- ((F,S,(a + b),x,b) ")),(- ((F,S,x,(a + b),y) "))) is Element of the carrier of F
(F,S,x,(a + b),b) * ((- ((F,S,(a + b),x,b) ")) * (- ((F,S,x,(a + b),y) "))) is Element of the carrier of F
the multF of F . ((F,S,x,(a + b),b),((- ((F,S,(a + b),x,b) ")) * (- ((F,S,x,(a + b),y) ")))) is Element of the carrier of F
((F,S,x,(a + b),b) * ((- ((F,S,(a + b),x,b) ")) * (- ((F,S,x,(a + b),y) ")))) * (F,S,(a + b),x,y) is Element of the carrier of F
the multF of F . (((F,S,x,(a + b),b) * ((- ((F,S,(a + b),x,b) ")) * (- ((F,S,x,(a + b),y) ")))),(F,S,(a + b),x,y)) is Element of the carrier of F
((F,S,x,(a + b),y) ") * ((F,S,(a + b),x,b) ") is Element of the carrier of F
the multF of F . (((F,S,x,(a + b),y) "),((F,S,(a + b),x,b) ")) is Element of the carrier of F
(F,S,x,(a + b),b) * (((F,S,x,(a + b),y) ") * ((F,S,(a + b),x,b) ")) is Element of the carrier of F
the multF of F . ((F,S,x,(a + b),b),(((F,S,x,(a + b),y) ") * ((F,S,(a + b),x,b) "))) is Element of the carrier of F
((F,S,x,(a + b),b) * (((F,S,x,(a + b),y) ") * ((F,S,(a + b),x,b) "))) * (F,S,(a + b),x,y) is Element of the carrier of F
the multF of F . (((F,S,x,(a + b),b) * (((F,S,x,(a + b),y) ") * ((F,S,(a + b),x,b) "))),(F,S,(a + b),x,y)) is Element of the carrier of F
(F,S,x,(a + b),b) * ((F,S,x,(a + b),y) ") is Element of the carrier of F
the multF of F . ((F,S,x,(a + b),b),((F,S,x,(a + b),y) ")) is Element of the carrier of F
((F,S,x,(a + b),b) * ((F,S,x,(a + b),y) ")) * ((F,S,(a + b),x,b) ") is Element of the carrier of F
the multF of F . (((F,S,x,(a + b),b) * ((F,S,x,(a + b),y) ")),((F,S,(a + b),x,b) ")) is Element of the carrier of F
(((F,S,x,(a + b),b) * ((F,S,x,(a + b),y) ")) * ((F,S,(a + b),x,b) ")) * (F,S,(a + b),x,y) is Element of the carrier of F
the multF of F . ((((F,S,x,(a + b),b) * ((F,S,x,(a + b),y) ")) * ((F,S,(a + b),x,b) ")),(F,S,(a + b),x,y)) is Element of the carrier of F
(F,S,x,y,b) * ((F,S,(a + b),x,b) ") is Element of the carrier of F
the multF of F . ((F,S,x,y,b),((F,S,(a + b),x,b) ")) is Element of the carrier of F
((F,S,x,y,b) * ((F,S,(a + b),x,b) ")) * (F,S,(a + b),x,y) is Element of the carrier of F
the multF of F . (((F,S,x,y,b) * ((F,S,(a + b),x,b) ")),(F,S,(a + b),x,y)) is Element of the carrier of F
(F,S,(a + b),x,y) * ((F,S,(a + b),x,b) ") is Element of the carrier of F
the multF of F . ((F,S,(a + b),x,y),((F,S,(a + b),x,b) ")) is Element of the carrier of F
(F,S,x,y,b) * ((F,S,(a + b),x,y) * ((F,S,(a + b),x,b) ")) is Element of the carrier of F
the multF of F . ((F,S,x,y,b),((F,S,(a + b),x,y) * ((F,S,(a + b),x,b) "))) is Element of the carrier of F
(F,S,(a + b),b,y) is Element of the carrier of F
(F,S,x,y,b) * (F,S,(a + b),b,y) is Element of the carrier of F
the multF of F . ((F,S,x,y,b),(F,S,(a + b),b,y)) is Element of the carrier of F
(F,S,x,y,b) * (F,S,a,b,y) is Element of the carrier of F
the multF of F . ((F,S,x,y,b),(F,S,a,b,y)) is Element of the carrier of F
(F,S,y,b,x) is Element of the carrier of F
(F,S,y,b,x) " is Element of the carrier of F
- ((F,S,y,b,x) ") is Element of the carrier of F
(F,S,b,y,x) is Element of the carrier of F
(- ((F,S,y,b,x) ")) * (F,S,b,y,x) is Element of the carrier of F
the multF of F . ((- ((F,S,y,b,x) ")),(F,S,b,y,x)) is Element of the carrier of F
(F,S,b,y,a) is Element of the carrier of F
(F,S,b,y,a) " is Element of the carrier of F
- ((F,S,b,y,a) ") is Element of the carrier of F
(F,S,y,b,a) is Element of the carrier of F
(- ((F,S,b,y,a) ")) * (F,S,y,b,a) is Element of the carrier of F
the multF of F . ((- ((F,S,b,y,a) ")),(F,S,y,b,a)) is Element of the carrier of F
(F,S,y,b,a) * (- ((F,S,b,y,a) ")) is Element of the carrier of F
the multF of F . ((F,S,y,b,a),(- ((F,S,b,y,a) "))) is Element of the carrier of F
((F,S,y,b,a) * (- ((F,S,b,y,a) "))) * (- ((F,S,y,b,x) ")) is Element of the carrier of F
the multF of F . (((F,S,y,b,a) * (- ((F,S,b,y,a) "))),(- ((F,S,y,b,x) "))) is Element of the carrier of F
(((F,S,y,b,a) * (- ((F,S,b,y,a) "))) * (- ((F,S,y,b,x) "))) * (F,S,b,y,x) is Element of the carrier of F
the multF of F . ((((F,S,y,b,a) * (- ((F,S,b,y,a) "))) * (- ((F,S,y,b,x) "))),(F,S,b,y,x)) is Element of the carrier of F
(- ((F,S,b,y,a) ")) * (- ((F,S,y,b,x) ")) is Element of the carrier of F
the multF of F . ((- ((F,S,b,y,a) ")),(- ((F,S,y,b,x) "))) is Element of the carrier of F
(F,S,y,b,a) * ((- ((F,S,b,y,a) ")) * (- ((F,S,y,b,x) "))) is Element of the carrier of F
the multF of F . ((F,S,y,b,a),((- ((F,S,b,y,a) ")) * (- ((F,S,y,b,x) ")))) is Element of the carrier of F
((F,S,y,b,a) * ((- ((F,S,b,y,a) ")) * (- ((F,S,y,b,x) ")))) * (F,S,b,y,x) is Element of the carrier of F
the multF of F . (((F,S,y,b,a) * ((- ((F,S,b,y,a) ")) * (- ((F,S,y,b,x) ")))),(F,S,b,y,x)) is Element of the carrier of F
((F,S,y,b,x) ") * ((F,S,b,y,a) ") is Element of the carrier of F
the multF of F . (((F,S,y,b,x) "),((F,S,b,y,a) ")) is Element of the carrier of F
(F,S,y,b,a) * (((F,S,y,b,x) ") * ((F,S,b,y,a) ")) is Element of the carrier of F
the multF of F . ((F,S,y,b,a),(((F,S,y,b,x) ") * ((F,S,b,y,a) "))) is Element of the carrier of F
((F,S,y,b,a) * (((F,S,y,b,x) ") * ((F,S,b,y,a) "))) * (F,S,b,y,x) is Element of the carrier of F
the multF of F . (((F,S,y,b,a) * (((F,S,y,b,x) ") * ((F,S,b,y,a) "))),(F,S,b,y,x)) is Element of the carrier of F
(F,S,y,b,a) * ((F,S,y,b,x) ") is Element of the carrier of F
the multF of F . ((F,S,y,b,a),((F,S,y,b,x) ")) is Element of the carrier of F
((F,S,y,b,a) * ((F,S,y,b,x) ")) * ((F,S,b,y,a) ") is Element of the carrier of F
the multF of F . (((F,S,y,b,a) * ((F,S,y,b,x) ")),((F,S,b,y,a) ")) is Element of the carrier of F
(((F,S,y,b,a) * ((F,S,y,b,x) ")) * ((F,S,b,y,a) ")) * (F,S,b,y,x) is Element of the carrier of F
the multF of F . ((((F,S,y,b,a) * ((F,S,y,b,x) ")) * ((F,S,b,y,a) ")),(F,S,b,y,x)) is Element of the carrier of F
(F,S,y,x,a) * ((F,S,b,y,a) ") is Element of the carrier of F
the multF of F . ((F,S,y,x,a),((F,S,b,y,a) ")) is Element of the carrier of F
((F,S,y,x,a) * ((F,S,b,y,a) ")) * (F,S,b,y,x) is Element of the carrier of F
the multF of F . (((F,S,y,x,a) * ((F,S,b,y,a) ")),(F,S,b,y,x)) is Element of the carrier of F
(F,S,b,y,x) * ((F,S,b,y,a) ") is Element of the carrier of F
the multF of F . ((F,S,b,y,x),((F,S,b,y,a) ")) is Element of the carrier of F
(F,S,y,x,a) * ((F,S,b,y,x) * ((F,S,b,y,a) ")) is Element of the carrier of F
the multF of F . ((F,S,y,x,a),((F,S,b,y,x) * ((F,S,b,y,a) "))) is Element of the carrier of F
(F,S,y,x,a) * (F,S,b,a,x) is Element of the carrier of F
the multF of F . ((F,S,y,x,a),(F,S,b,a,x)) is Element of the carrier of F
(F,S,x,a,y) is Element of the carrier of F
(F,S,x,a,y) " is Element of the carrier of F
- ((F,S,x,a,y) ") is Element of the carrier of F
(F,S,a,x,y) is Element of the carrier of F
(- ((F,S,x,a,y) ")) * (F,S,a,x,y) is Element of the carrier of F
the multF of F . ((- ((F,S,x,a,y) ")),(F,S,a,x,y)) is Element of the carrier of F
(F,S,a,x,b) is Element of the carrier of F
(F,S,a,x,b) " is Element of the carrier of F
- ((F,S,a,x,b) ") is Element of the carrier of F
(F,S,x,a,b) is Element of the carrier of F
(- ((F,S,a,x,b) ")) * (F,S,x,a,b) is Element of the carrier of F
the multF of F . ((- ((F,S,a,x,b) ")),(F,S,x,a,b)) is Element of the carrier of F
(F,S,x,a,b) * (- ((F,S,a,x,b) ")) is Element of the carrier of F
the multF of F . ((F,S,x,a,b),(- ((F,S,a,x,b) "))) is Element of the carrier of F
((F,S,x,a,b) * (- ((F,S,a,x,b) "))) * (- ((F,S,x,a,y) ")) is Element of the carrier of F
the multF of F . (((F,S,x,a,b) * (- ((F,S,a,x,b) "))),(- ((F,S,x,a,y) "))) is Element of the carrier of F
(((F,S,x,a,b) * (- ((F,S,a,x,b) "))) * (- ((F,S,x,a,y) "))) * (F,S,a,x,y) is Element of the carrier of F
the multF of F . ((((F,S,x,a,b) * (- ((F,S,a,x,b) "))) * (- ((F,S,x,a,y) "))),(F,S,a,x,y)) is Element of the carrier of F
(- ((F,S,a,x,b) ")) * (- ((F,S,x,a,y) ")) is Element of the carrier of F
the multF of F . ((- ((F,S,a,x,b) ")),(- ((F,S,x,a,y) "))) is Element of the carrier of F
(F,S,x,a,b) * ((- ((F,S,a,x,b) ")) * (- ((F,S,x,a,y) "))) is Element of the carrier of F
the multF of F . ((F,S,x,a,b),((- ((F,S,a,x,b) ")) * (- ((F,S,x,a,y) ")))) is Element of the carrier of F
((F,S,x,a,b) * ((- ((F,S,a,x,b) ")) * (- ((F,S,x,a,y) ")))) * (F,S,a,x,y) is Element of the carrier of F
the multF of F . (((F,S,x,a,b) * ((- ((F,S,a,x,b) ")) * (- ((F,S,x,a,y) ")))),(F,S,a,x,y)) is Element of the carrier of F
((F,S,x,a,y) ") * ((F,S,a,x,b) ") is Element of the carrier of F
the multF of F . (((F,S,x,a,y) "),((F,S,a,x,b) ")) is Element of the carrier of F
(F,S,x,a,b) * (((F,S,x,a,y) ") * ((F,S,a,x,b) ")) is Element of the carrier of F
the multF of F . ((F,S,x,a,b),(((F,S,x,a,y) ") * ((F,S,a,x,b) "))) is Element of the carrier of F
((F,S,x,a,b) * (((F,S,x,a,y) ") * ((F,S,a,x,b) "))) * (F,S,a,x,y) is Element of the carrier of F
the multF of F . (((F,S,x,a,b) * (((F,S,x,a,y) ") * ((F,S,a,x,b) "))),(F,S,a,x,y)) is Element of the carrier of F
(F,S,x,a,b) * ((F,S,x,a,y) ") is Element of the carrier of F
the multF of F . ((F,S,x,a,b),((F,S,x,a,y) ")) is Element of the carrier of F
((F,S,x,a,b) * ((F,S,x,a,y) ")) * ((F,S,a,x,b) ") is Element of the carrier of F
the multF of F . (((F,S,x,a,b) * ((F,S,x,a,y) ")),((F,S,a,x,b) ")) is Element of the carrier of F
(((F,S,x,a,b) * ((F,S,x,a,y) ")) * ((F,S,a,x,b) ")) * (F,S,a,x,y) is Element of the carrier of F
the multF of F . ((((F,S,x,a,b) * ((F,S,x,a,y) ")) * ((F,S,a,x,b) ")),(F,S,a,x,y)) is Element of the carrier of F
(F,S,x,y,b) * ((F,S,a,x,b) ") is Element of the carrier of F
the multF of F . ((F,S,x,y,b),((F,S,a,x,b) ")) is Element of the carrier of F
((F,S,x,y,b) * ((F,S,a,x,b) ")) * (F,S,a,x,y) is Element of the carrier of F
the multF of F . (((F,S,x,y,b) * ((F,S,a,x,b) ")),(F,S,a,x,y)) is Element of the carrier of F
(F,S,a,x,y) * ((F,S,a,x,b) ") is Element of the carrier of F
the multF of F . ((F,S,a,x,y),((F,S,a,x,b) ")) is Element of the carrier of F
(F,S,x,y,b) * ((F,S,a,x,y) * ((F,S,a,x,b) ")) is Element of the carrier of F
the multF of F . ((F,S,x,y,b),((F,S,a,x,y) * ((F,S,a,x,b) "))) is Element of the carrier of F
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(1_ F) + (1_ F) is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the addF of F . ((1_ F),(1_ F)) is Element of the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
(F,S,b,a,x) is Element of the carrier of F
y is Element of the carrier of S
(F,S,a,y,b) is Element of the carrier of F
(F,S,a,y,b) * (F,S,b,a,x) is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
the multF of F . ((F,S,a,y,b),(F,S,b,a,x)) is Element of the carrier of F
(F,S,x,y,b) is Element of the carrier of F
(F,S,y,a,x) is Element of the carrier of F
(F,S,x,y,b) * (F,S,y,a,x) is Element of the carrier of F
the multF of F . ((F,S,x,y,b),(F,S,y,a,x)) is Element of the carrier of F
(F,S,y,x,a) is Element of the carrier of F
(F,S,b,a,x) * (F,S,y,x,a) is Element of the carrier of F
the multF of F . ((F,S,b,a,x),(F,S,y,x,a)) is Element of the carrier of F
(F,S,a,b,y) is Element of the carrier of F
(F,S,a,b,y) * (F,S,x,y,b) is Element of the carrier of F
the multF of F . ((F,S,a,b,y),(F,S,x,y,b)) is Element of the carrier of F
(F,S,a,y,b) " is Element of the carrier of F
((F,S,a,y,b) ") * (F,S,x,y,b) is Element of the carrier of F
the multF of F . (((F,S,a,y,b) "),(F,S,x,y,b)) is Element of the carrier of F
(F,S,a,y,b) * ((F,S,b,a,x) * (F,S,y,x,a)) is Element of the carrier of F
the multF of F . ((F,S,a,y,b),((F,S,b,a,x) * (F,S,y,x,a))) is Element of the carrier of F
(F,S,a,y,b) * ((F,S,a,y,b) ") is Element of the carrier of F
the multF of F . ((F,S,a,y,b),((F,S,a,y,b) ")) is Element of the carrier of F
((F,S,a,y,b) * ((F,S,a,y,b) ")) * (F,S,x,y,b) is Element of the carrier of F
the multF of F . (((F,S,a,y,b) * ((F,S,a,y,b) ")),(F,S,x,y,b)) is Element of the carrier of F
(F,S,x,y,b) * (1_ F) is Element of the carrier of F
the multF of F . ((F,S,x,y,b),(1_ F)) is Element of the carrier of F
((F,S,a,y,b) * (F,S,b,a,x)) * (F,S,y,x,a) is Element of the carrier of F
the multF of F . (((F,S,a,y,b) * (F,S,b,a,x)),(F,S,y,x,a)) is Element of the carrier of F
(F,S,y,a,x) " is Element of the carrier of F
((F,S,a,y,b) * (F,S,b,a,x)) * ((F,S,y,a,x) ") is Element of the carrier of F
the multF of F . (((F,S,a,y,b) * (F,S,b,a,x)),((F,S,y,a,x) ")) is Element of the carrier of F
((F,S,y,a,x) ") * (F,S,y,a,x) is Element of the carrier of F
the multF of F . (((F,S,y,a,x) "),(F,S,y,a,x)) is Element of the carrier of F
((F,S,a,y,b) * (F,S,b,a,x)) * (((F,S,y,a,x) ") * (F,S,y,a,x)) is Element of the carrier of F
the multF of F . (((F,S,a,y,b) * (F,S,b,a,x)),(((F,S,y,a,x) ") * (F,S,y,a,x))) is Element of the carrier of F
((F,S,a,y,b) * (F,S,b,a,x)) * (1_ F) is Element of the carrier of F
the multF of F . (((F,S,a,y,b) * (F,S,b,a,x)),(1_ F)) is Element of the carrier of F
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(1_ F) + (1_ F) is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the addF of F . ((1_ F),(1_ F)) is Element of the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
(F,S,b,a,x) is Element of the carrier of F
y is Element of the carrier of S
(F,S,y,a,x) is Element of the carrier of F
z is Element of the carrier of S
(F,S,a,z,b) is Element of the carrier of F
(F,S,a,z,b) * (F,S,b,a,x) is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
the multF of F . ((F,S,a,z,b),(F,S,b,a,x)) is Element of the carrier of F
(F,S,a,z,y) is Element of the carrier of F
(F,S,a,z,y) * (F,S,y,a,x) is Element of the carrier of F
the multF of F . ((F,S,a,z,y),(F,S,y,a,x)) is Element of the carrier of F
0F is Element of the carrier of S
(F,S,x,b,0F) is Element of the carrier of F
((F,S,a,z,b) * (F,S,b,a,x)) * (F,S,x,b,0F) is Element of the carrier of F
the multF of F . (((F,S,a,z,b) * (F,S,b,a,x)),(F,S,x,b,0F)) is Element of the carrier of F
(F,S,x,y,0F) is Element of the carrier of F
((F,S,a,z,y) * (F,S,y,a,x)) * (F,S,x,y,0F) is Element of the carrier of F
the multF of F . (((F,S,a,z,y) * (F,S,y,a,x)),(F,S,x,y,0F)) is Element of the carrier of F
(F,S,a,y,b) is Element of the carrier of F
(F,S,a,y,b) * (F,S,b,a,x) is Element of the carrier of F
the multF of F . ((F,S,a,y,b),(F,S,b,a,x)) is Element of the carrier of F
(F,S,x,y,b) is Element of the carrier of F
(F,S,x,y,b) * (F,S,y,a,x) is Element of the carrier of F
the multF of F . ((F,S,x,y,b),(F,S,y,a,x)) is Element of the carrier of F
(F,S,a,z,y) " is Element of the carrier of F
(F,S,a,z,b) * ((F,S,a,z,y) ") is Element of the carrier of F
the multF of F . ((F,S,a,z,b),((F,S,a,z,y) ")) is Element of the carrier of F
((F,S,a,z,b) * ((F,S,a,z,y) ")) * (F,S,b,a,x) is Element of the carrier of F
the multF of F . (((F,S,a,z,b) * ((F,S,a,z,y) ")),(F,S,b,a,x)) is Element of the carrier of F
((F,S,a,z,y) ") * (F,S,a,z,b) is Element of the carrier of F
the multF of F . (((F,S,a,z,y) "),(F,S,a,z,b)) is Element of the carrier of F
(((F,S,a,z,y) ") * (F,S,a,z,b)) * (F,S,b,a,x) is Element of the carrier of F
the multF of F . ((((F,S,a,z,y) ") * (F,S,a,z,b)),(F,S,b,a,x)) is Element of the carrier of F
(F,S,x,0F,b) is Element of the carrier of F
(F,S,x,0F,y) is Element of the carrier of F
(F,S,x,0F,y) " is Element of the carrier of F
(F,S,x,0F,b) * ((F,S,x,0F,y) ") is Element of the carrier of F
the multF of F . ((F,S,x,0F,b),((F,S,x,0F,y) ")) is Element of the carrier of F
((F,S,x,0F,b) * ((F,S,x,0F,y) ")) * (F,S,y,a,x) is Element of the carrier of F
the multF of F . (((F,S,x,0F,b) * ((F,S,x,0F,y) ")),(F,S,y,a,x)) is Element of the carrier of F
((F,S,a,z,y) ") * ((F,S,a,z,b) * (F,S,b,a,x)) is Element of the carrier of F
the multF of F . (((F,S,a,z,y) "),((F,S,a,z,b) * (F,S,b,a,x))) is Element of the carrier of F
(F,S,a,z,y) * (((F,S,a,z,y) ") * ((F,S,a,z,b) * (F,S,b,a,x))) is Element of the carrier of F
the multF of F . ((F,S,a,z,y),(((F,S,a,z,y) ") * ((F,S,a,z,b) * (F,S,b,a,x)))) is Element of the carrier of F
(F,S,a,z,y) * (((F,S,x,0F,b) * ((F,S,x,0F,y) ")) * (F,S,y,a,x)) is Element of the carrier of F
the multF of F . ((F,S,a,z,y),(((F,S,x,0F,b) * ((F,S,x,0F,y) ")) * (F,S,y,a,x))) is Element of the carrier of F
(F,S,a,z,y) * ((F,S,a,z,y) ") is Element of the carrier of F
the multF of F . ((F,S,a,z,y),((F,S,a,z,y) ")) is Element of the carrier of F
((F,S,a,z,y) * ((F,S,a,z,y) ")) * ((F,S,a,z,b) * (F,S,b,a,x)) is Element of the carrier of F
the multF of F . (((F,S,a,z,y) * ((F,S,a,z,y) ")),((F,S,a,z,b) * (F,S,b,a,x))) is Element of the carrier of F
((F,S,a,z,b) * (F,S,b,a,x)) * (1_ F) is Element of the carrier of F
the multF of F . (((F,S,a,z,b) * (F,S,b,a,x)),(1_ F)) is Element of the carrier of F
(F,S,x,b,0F) " is Element of the carrier of F
((F,S,x,0F,y) ") * ((F,S,x,b,0F) ") is Element of the carrier of F
the multF of F . (((F,S,x,0F,y) "),((F,S,x,b,0F) ")) is Element of the carrier of F
(((F,S,x,0F,y) ") * ((F,S,x,b,0F) ")) * (F,S,y,a,x) is Element of the carrier of F
the multF of F . ((((F,S,x,0F,y) ") * ((F,S,x,b,0F) ")),(F,S,y,a,x)) is Element of the carrier of F
(F,S,a,z,y) * ((((F,S,x,0F,y) ") * ((F,S,x,b,0F) ")) * (F,S,y,a,x)) is Element of the carrier of F
the multF of F . ((F,S,a,z,y),((((F,S,x,0F,y) ") * ((F,S,x,b,0F) ")) * (F,S,y,a,x))) is Element of the carrier of F
(F,S,a,z,y) * (((F,S,x,0F,y) ") * ((F,S,x,b,0F) ")) is Element of the carrier of F
the multF of F . ((F,S,a,z,y),(((F,S,x,0F,y) ") * ((F,S,x,b,0F) "))) is Element of the carrier of F
((F,S,a,z,y) * (((F,S,x,0F,y) ") * ((F,S,x,b,0F) "))) * (F,S,y,a,x) is Element of the carrier of F
the multF of F . (((F,S,a,z,y) * (((F,S,x,0F,y) ") * ((F,S,x,b,0F) "))),(F,S,y,a,x)) is Element of the carrier of F
(F,S,a,z,y) * ((F,S,x,0F,y) ") is Element of the carrier of F
the multF of F . ((F,S,a,z,y),((F,S,x,0F,y) ")) is Element of the carrier of F
((F,S,a,z,y) * ((F,S,x,0F,y) ")) * ((F,S,x,b,0F) ") is Element of the carrier of F
the multF of F . (((F,S,a,z,y) * ((F,S,x,0F,y) ")),((F,S,x,b,0F) ")) is Element of the carrier of F
(F,S,y,a,x) * (((F,S,a,z,y) * ((F,S,x,0F,y) ")) * ((F,S,x,b,0F) ")) is Element of the carrier of F
the multF of F . ((F,S,y,a,x),(((F,S,a,z,y) * ((F,S,x,0F,y) ")) * ((F,S,x,b,0F) "))) is Element of the carrier of F
(F,S,y,a,x) * ((F,S,a,z,y) * ((F,S,x,0F,y) ")) is Element of the carrier of F
the multF of F . ((F,S,y,a,x),((F,S,a,z,y) * ((F,S,x,0F,y) "))) is Element of the carrier of F
((F,S,y,a,x) * ((F,S,a,z,y) * ((F,S,x,0F,y) "))) * ((F,S,x,b,0F) ") is Element of the carrier of F
the multF of F . (((F,S,y,a,x) * ((F,S,a,z,y) * ((F,S,x,0F,y) "))),((F,S,x,b,0F) ")) is Element of the carrier of F
(((F,S,y,a,x) * ((F,S,a,z,y) * ((F,S,x,0F,y) "))) * ((F,S,x,b,0F) ")) * (F,S,x,b,0F) is Element of the carrier of F
the multF of F . ((((F,S,y,a,x) * ((F,S,a,z,y) * ((F,S,x,0F,y) "))) * ((F,S,x,b,0F) ")),(F,S,x,b,0F)) is Element of the carrier of F
((F,S,x,b,0F) ") * (F,S,x,b,0F) is Element of the carrier of F
the multF of F . (((F,S,x,b,0F) "),(F,S,x,b,0F)) is Element of the carrier of F
((F,S,y,a,x) * ((F,S,a,z,y) * ((F,S,x,0F,y) "))) * (((F,S,x,b,0F) ") * (F,S,x,b,0F)) is Element of the carrier of F
the multF of F . (((F,S,y,a,x) * ((F,S,a,z,y) * ((F,S,x,0F,y) "))),(((F,S,x,b,0F) ") * (F,S,x,b,0F))) is Element of the carrier of F
((F,S,y,a,x) * ((F,S,a,z,y) * ((F,S,x,0F,y) "))) * (1_ F) is Element of the carrier of F
the multF of F . (((F,S,y,a,x) * ((F,S,a,z,y) * ((F,S,x,0F,y) "))),(1_ F)) is Element of the carrier of F
(F,S,a,z,y) * (F,S,x,y,0F) is Element of the carrier of F
the multF of F . ((F,S,a,z,y),(F,S,x,y,0F)) is Element of the carrier of F
(F,S,y,a,x) * ((F,S,a,z,y) * (F,S,x,y,0F)) is Element of the carrier of F
the multF of F . ((F,S,y,a,x),((F,S,a,z,y) * (F,S,x,y,0F))) is Element of the carrier of F
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
(F,S,a,b,x) is Element of the carrier of F
the carrier of F is non empty non trivial set
y is Element of the carrier of S
(F,S,x,a,y) is Element of the carrier of F
(F,S,a,b,x) * (F,S,x,a,y) is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the multF of F . ((F,S,a,b,x),(F,S,x,a,y)) is Element of the carrier of F
(F,S,a,b,y) is Element of the carrier of F
- (F,S,a,b,y) is Element of the carrier of F
(F,S,y,a,x) is Element of the carrier of F
(- (F,S,a,b,y)) * (F,S,y,a,x) is Element of the carrier of F
the multF of F . ((- (F,S,a,b,y)),(F,S,y,a,x)) is Element of the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
1_ F is Element of the carrier of F
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(F,S,a,b,x) " is Element of the carrier of F
(F,S,a,b,y) * ((F,S,a,b,x) ") is Element of the carrier of F
the multF of F . ((F,S,a,b,y),((F,S,a,b,x) ")) is Element of the carrier of F
(F,S,a,x,y) is Element of the carrier of F
((F,S,a,b,y) * ((F,S,a,b,x) ")) * (F,S,a,b,x) is Element of the carrier of F
the multF of F . (((F,S,a,b,y) * ((F,S,a,b,x) ")),(F,S,a,b,x)) is Element of the carrier of F
(F,S,x,y,a) is Element of the carrier of F
(F,S,x,y,a) " is Element of the carrier of F
- ((F,S,x,y,a) ") is Element of the carrier of F
(F,S,y,x,a) is Element of the carrier of F
(- ((F,S,x,y,a) ")) * (F,S,y,x,a) is Element of the carrier of F
the multF of F . ((- ((F,S,x,y,a) ")),(F,S,y,x,a)) is Element of the carrier of F
((- ((F,S,x,y,a) ")) * (F,S,y,x,a)) * (F,S,a,b,x) is Element of the carrier of F
the multF of F . (((- ((F,S,x,y,a) ")) * (F,S,y,x,a)),(F,S,a,b,x)) is Element of the carrier of F
((F,S,a,b,x) ") * (F,S,a,b,x) is Element of the carrier of F
the multF of F . (((F,S,a,b,x) "),(F,S,a,b,x)) is Element of the carrier of F
(F,S,a,b,y) * (((F,S,a,b,x) ") * (F,S,a,b,x)) is Element of the carrier of F
the multF of F . ((F,S,a,b,y),(((F,S,a,b,x) ") * (F,S,a,b,x))) is Element of the carrier of F
(F,S,a,b,y) * (1_ F) is Element of the carrier of F
the multF of F . ((F,S,a,b,y),(1_ F)) is Element of the carrier of F
(F,S,y,x,a) * (- ((F,S,x,y,a) ")) is Element of the carrier of F
the multF of F . ((F,S,y,x,a),(- ((F,S,x,y,a) "))) is Element of the carrier of F
((F,S,y,x,a) * (- ((F,S,x,y,a) "))) * (F,S,a,b,x) is Element of the carrier of F
the multF of F . (((F,S,y,x,a) * (- ((F,S,x,y,a) "))),(F,S,a,b,x)) is Element of the carrier of F
(- ((F,S,x,y,a) ")) * (F,S,a,b,x) is Element of the carrier of F
the multF of F . ((- ((F,S,x,y,a) ")),(F,S,a,b,x)) is Element of the carrier of F
(F,S,y,x,a) * ((- ((F,S,x,y,a) ")) * (F,S,a,b,x)) is Element of the carrier of F
the multF of F . ((F,S,y,x,a),((- ((F,S,x,y,a) ")) * (F,S,a,b,x))) is Element of the carrier of F
(F,S,y,a,x) * (F,S,a,b,y) is Element of the carrier of F
the multF of F . ((F,S,y,a,x),(F,S,a,b,y)) is Element of the carrier of F
(F,S,y,a,x) " is Element of the carrier of F
((F,S,y,a,x) ") * ((- ((F,S,x,y,a) ")) * (F,S,a,b,x)) is Element of the carrier of F
the multF of F . (((F,S,y,a,x) "),((- ((F,S,x,y,a) ")) * (F,S,a,b,x))) is Element of the carrier of F
(F,S,y,a,x) * (((F,S,y,a,x) ") * ((- ((F,S,x,y,a) ")) * (F,S,a,b,x))) is Element of the carrier of F
the multF of F . ((F,S,y,a,x),(((F,S,y,a,x) ") * ((- ((F,S,x,y,a) ")) * (F,S,a,b,x)))) is Element of the carrier of F
(F,S,y,a,x) * ((F,S,y,a,x) ") is Element of the carrier of F
the multF of F . ((F,S,y,a,x),((F,S,y,a,x) ")) is Element of the carrier of F
((F,S,y,a,x) * ((F,S,y,a,x) ")) * ((- ((F,S,x,y,a) ")) * (F,S,a,b,x)) is Element of the carrier of F
the multF of F . (((F,S,y,a,x) * ((F,S,y,a,x) ")),((- ((F,S,x,y,a) ")) * (F,S,a,b,x))) is Element of the carrier of F
((- ((F,S,x,y,a) ")) * (F,S,a,b,x)) * (1_ F) is Element of the carrier of F
the multF of F . (((- ((F,S,x,y,a) ")) * (F,S,a,b,x)),(1_ F)) is Element of the carrier of F
(F,S,a,b,y) * (F,S,y,a,x) is Element of the carrier of F
the multF of F . ((F,S,a,b,y),(F,S,y,a,x)) is Element of the carrier of F
- ((F,S,a,b,y) * (F,S,y,a,x)) is Element of the carrier of F
((F,S,x,y,a) ") * (F,S,a,b,x) is Element of the carrier of F
the multF of F . (((F,S,x,y,a) "),(F,S,a,b,x)) is Element of the carrier of F
- (((F,S,x,y,a) ") * (F,S,a,b,x)) is Element of the carrier of F
- (- (((F,S,x,y,a) ") * (F,S,a,b,x))) is Element of the carrier of F
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
y is Element of the carrier of S
x is Element of the carrier of S
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(1_ F) + (1_ F) is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the addF of F . ((1_ F),(1_ F)) is Element of the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
b is Element of the carrier of S
a is Element of the carrier of S
z is Element of the carrier of S
(F,S,x,y,z) is Element of the carrier of F
(F,S,z,x,b) is Element of the carrier of F
(F,S,x,y,z) * (F,S,z,x,b) is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
the multF of F . ((F,S,x,y,z),(F,S,z,x,b)) is Element of the carrier of F
(F,S,b,z,a) is Element of the carrier of F
((F,S,x,y,z) * (F,S,z,x,b)) * (F,S,b,z,a) is Element of the carrier of F
the multF of F . (((F,S,x,y,z) * (F,S,z,x,b)),(F,S,b,z,a)) is Element of the carrier of F
0F is Element of the carrier of S
(F,S,x,y,0F) is Element of the carrier of F
(F,S,0F,x,b) is Element of the carrier of F
(F,S,x,y,0F) * (F,S,0F,x,b) is Element of the carrier of F
the multF of F . ((F,S,x,y,0F),(F,S,0F,x,b)) is Element of the carrier of F
(F,S,b,0F,a) is Element of the carrier of F
((F,S,x,y,0F) * (F,S,0F,x,b)) * (F,S,b,0F,a) is Element of the carrier of F
the multF of F . (((F,S,x,y,0F) * (F,S,0F,x,b)),(F,S,b,0F,a)) is Element of the carrier of F
z is Element of the carrier of F
0F is Element of the carrier of F
p is Element of the carrier of S
r is Element of the carrier of S
(F,S,x,y,r) is Element of the carrier of F
(F,S,r,x,b) is Element of the carrier of F
(F,S,x,y,r) * (F,S,r,x,b) is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
the multF of F . ((F,S,x,y,r),(F,S,r,x,b)) is Element of the carrier of F
(F,S,b,r,a) is Element of the carrier of F
((F,S,x,y,r) * (F,S,r,x,b)) * (F,S,b,r,a) is Element of the carrier of F
the multF of F . (((F,S,x,y,r) * (F,S,r,x,b)),(F,S,b,r,a)) is Element of the carrier of F
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(1_ F) + (1_ F) is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the addF of F . ((1_ F),(1_ F)) is Element of the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
0. S is V51(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
y is Element of the carrier of S
(F,S,x,y,a,b) is Element of the carrier of F
z is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(1_ F) + (1_ F) is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the addF of F . ((1_ F),(1_ F)) is Element of the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
y is Element of the carrier of S
(F,S,x,y,a,b) is Element of the carrier of F
0. S is V51(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
0F is Element of the carrier of S
(F,S,0F,a,x) is Element of the carrier of F
(F,S,a,b,0F) is Element of the carrier of F
(F,S,a,b,0F) * (F,S,0F,a,x) is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
the multF of F . ((F,S,a,b,0F),(F,S,0F,a,x)) is Element of the carrier of F
(F,S,x,0F,y) is Element of the carrier of F
((F,S,a,b,0F) * (F,S,0F,a,x)) * (F,S,x,0F,y) is Element of the carrier of F
the multF of F . (((F,S,a,b,0F) * (F,S,0F,a,x)),(F,S,x,0F,y)) is Element of the carrier of F
0F is Element of the carrier of S
0F is Element of the carrier of S
(F,S,x,0F,y) is Element of the carrier of F
(F,S,a,b,0F) is Element of the carrier of F
(F,S,0F,a,x) is Element of the carrier of F
(F,S,a,b,0F) * (F,S,0F,a,x) is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
the multF of F . ((F,S,a,b,0F),(F,S,0F,a,x)) is Element of the carrier of F
((F,S,a,b,0F) * (F,S,0F,a,x)) * (F,S,x,0F,y) is Element of the carrier of F
the multF of F . (((F,S,a,b,0F) * (F,S,0F,a,x)),(F,S,x,0F,y)) is Element of the carrier of F
0F is Element of the carrier of S
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(1_ F) + (1_ F) is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the addF of F . ((1_ F),(1_ F)) is Element of the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
y is Element of the carrier of S
(F,S,x,y,a,b) is Element of the carrier of F
(F,S,y,x,a,b) is Element of the carrier of F
- (F,S,y,x,a,b) is Element of the carrier of F
0. S is V51(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
p is Element of the carrier of S
(F,S,a,b,p) is Element of the carrier of F
(F,S,p,a,y) is Element of the carrier of F
(F,S,a,b,p) * (F,S,p,a,y) is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
the multF of F . ((F,S,a,b,p),(F,S,p,a,y)) is Element of the carrier of F
(F,S,y,p,x) is Element of the carrier of F
((F,S,a,b,p) * (F,S,p,a,y)) * (F,S,y,p,x) is Element of the carrier of F
the multF of F . (((F,S,a,b,p) * (F,S,p,a,y)),(F,S,y,p,x)) is Element of the carrier of F
(F,S,p,a,y) * (F,S,y,p,x) is Element of the carrier of F
the multF of F . ((F,S,p,a,y),(F,S,y,p,x)) is Element of the carrier of F
(F,S,a,b,p) * ((F,S,p,a,y) * (F,S,y,p,x)) is Element of the carrier of F
the multF of F . ((F,S,a,b,p),((F,S,p,a,y) * (F,S,y,p,x))) is Element of the carrier of F
(F,S,p,a,x) is Element of the carrier of F
- (F,S,p,a,x) is Element of the carrier of F
(F,S,x,p,y) is Element of the carrier of F
(- (F,S,p,a,x)) * (F,S,x,p,y) is Element of the carrier of F
the multF of F . ((- (F,S,p,a,x)),(F,S,x,p,y)) is Element of the carrier of F
(F,S,a,b,p) * ((- (F,S,p,a,x)) * (F,S,x,p,y)) is Element of the carrier of F
the multF of F . ((F,S,a,b,p),((- (F,S,p,a,x)) * (F,S,x,p,y))) is Element of the carrier of F
(- (F,S,p,a,x)) * (F,S,a,b,p) is Element of the carrier of F
the multF of F . ((- (F,S,p,a,x)),(F,S,a,b,p)) is Element of the carrier of F
((- (F,S,p,a,x)) * (F,S,a,b,p)) * (F,S,x,p,y) is Element of the carrier of F
the multF of F . (((- (F,S,p,a,x)) * (F,S,a,b,p)),(F,S,x,p,y)) is Element of the carrier of F
(F,S,p,a,x) * (F,S,a,b,p) is Element of the carrier of F
the multF of F . ((F,S,p,a,x),(F,S,a,b,p)) is Element of the carrier of F
- ((F,S,p,a,x) * (F,S,a,b,p)) is Element of the carrier of F
(- ((F,S,p,a,x) * (F,S,a,b,p))) * (F,S,x,p,y) is Element of the carrier of F
the multF of F . ((- ((F,S,p,a,x) * (F,S,a,b,p))),(F,S,x,p,y)) is Element of the carrier of F
- (1_ F) is Element of the carrier of F
(- (1_ F)) * (F,S,y,x,a,b) is Element of the carrier of F
the multF of F . ((- (1_ F)),(F,S,y,x,a,b)) is Element of the carrier of F
(F,S,a,b,p) * (F,S,p,a,x) is Element of the carrier of F
the multF of F . ((F,S,a,b,p),(F,S,p,a,x)) is Element of the carrier of F
((F,S,a,b,p) * (F,S,p,a,x)) * (F,S,x,p,y) is Element of the carrier of F
the multF of F . (((F,S,a,b,p) * (F,S,p,a,x)),(F,S,x,p,y)) is Element of the carrier of F
- (((F,S,a,b,p) * (F,S,p,a,x)) * (F,S,x,p,y)) is Element of the carrier of F
(- (1_ F)) * (- (((F,S,a,b,p) * (F,S,p,a,x)) * (F,S,x,p,y))) is Element of the carrier of F
the multF of F . ((- (1_ F)),(- (((F,S,a,b,p) * (F,S,p,a,x)) * (F,S,x,p,y)))) is Element of the carrier of F
(F,S,y,x,a,b) * (1_ F) is Element of the carrier of F
the multF of F . ((F,S,y,x,a,b),(1_ F)) is Element of the carrier of F
- ((F,S,y,x,a,b) * (1_ F)) is Element of the carrier of F
(((F,S,a,b,p) * (F,S,p,a,x)) * (F,S,x,p,y)) * (1_ F) is Element of the carrier of F
the multF of F . ((((F,S,a,b,p) * (F,S,p,a,x)) * (F,S,x,p,y)),(1_ F)) is Element of the carrier of F
(- (1_ F)) * (0. F) is Element of the carrier of F
the multF of F . ((- (1_ F)),(0. F)) is Element of the carrier of F
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
the carrier of F is non empty non trivial set
1_ F is Element of the carrier of F
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(1_ F) + (1_ F) is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the addF of F . ((1_ F),(1_ F)) is Element of the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
y is Element of the carrier of S
(F,S,x,y,a,b) is Element of the carrier of F
z is Element of the carrier of F
z * y is Element of the carrier of S
(F,S,x,(z * y),a,b) is Element of the carrier of F
z * (F,S,x,y,a,b) is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
the multF of F . (z,(F,S,x,y,a,b)) is Element of the carrier of F
0. S is V51(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
p is Element of the carrier of S
(F,S,a,b,p) is Element of the carrier of F
(F,S,p,a,x) is Element of the carrier of F
(F,S,a,b,p) * (F,S,p,a,x) is Element of the carrier of F
the multF of F . ((F,S,a,b,p),(F,S,p,a,x)) is Element of the carrier of F
(F,S,x,p,(z * y)) is Element of the carrier of F
((F,S,a,b,p) * (F,S,p,a,x)) * (F,S,x,p,(z * y)) is Element of the carrier of F
the multF of F . (((F,S,a,b,p) * (F,S,p,a,x)),(F,S,x,p,(z * y))) is Element of the carrier of F
(F,S,x,p,y) is Element of the carrier of F
z * (F,S,x,p,y) is Element of the carrier of F
the multF of F . (z,(F,S,x,p,y)) is Element of the carrier of F
(z * (F,S,x,p,y)) * ((F,S,a,b,p) * (F,S,p,a,x)) is Element of the carrier of F
the multF of F . ((z * (F,S,x,p,y)),((F,S,a,b,p) * (F,S,p,a,x))) is Element of the carrier of F
((F,S,a,b,p) * (F,S,p,a,x)) * (F,S,x,p,y) is Element of the carrier of F
the multF of F . (((F,S,a,b,p) * (F,S,p,a,x)),(F,S,x,p,y)) is Element of the carrier of F
z * (0. F) is Element of the carrier of F
the multF of F . (z,(0. F)) is Element of the carrier of F
F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(1_ F) + (1_ F) is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is non empty set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set
the addF of F . ((1_ F),(1_ F)) is Element of the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)
the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
y is Element of the carrier of S
(F,S,x,y,a,b) is Element of the carrier of F
z is Element of the carrier of S
y + z is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of S . (y,z) is Element of the carrier of S
(F,S,x,(y + z),a,b) is Element of the carrier of F
(F,S,x,z,a,b) is Element of the carrier of F
(F,S,x,y,a,b) + (F,S,x,z,a,b) is Element of the carrier of F
the addF of F . ((F,S,x,y,a,b),(F,S,x,z,a,b)) is Element of the carrier of F
0. S is V51(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
0F is Element of the carrier of S
(F,S,a,b,0F) is Element of the carrier of F
(F,S,0F,a,x) is Element of the carrier of F
(F,S,a,b,0F) * (F,S,0F,a,x) is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
the multF of F . ((F,S,a,b,0F),(F,S,0F,a,x)) is Element of the carrier of F
(F,S,x,0F,(y + z)) is Element of the carrier of F
((F,S,a,b,0F) * (F,S,0F,a,x)) * (F,S,x,0F,(y + z)) is Element of the carrier of F
the multF of F . (((F,S,a,b,0F) * (F,S,0F,a,x)),(F,S,x,0F,(y + z))) is Element of the carrier of F
(F,S,x,0F,y) is Element of the carrier of F
((F,S,a,b,0F) * (F,S,0F,a,x)) * (F,S,x,0F,y) is Element of the carrier of F
the multF of F . (((F,S,a,b,0F) * (F,S,0F,a,x)),(F,S,x,0F,y)) is Element of the carrier of F
(F,S,x,0F,z) is Element of the carrier of F
((F,S,a,b,0F) * (F,S,0F,a,x)) * (F,S,x,0F,z) is Element of the carrier of F
the multF of F . (((F,S,a,b,0F) * (F,S,0F,a,x)),(F,S,x,0F,z)) is Element of the carrier of F
(F,S,x,0F,y) + (F,S,x,0F,z) is Element of the carrier of F
the addF of F . ((F,S,x,0F,y),(F,S,x,0F,z)) is Element of the carrier of F