:: ORTSP_1 semantic presentation

K140() is Element of bool K136()
K136() is set
bool K136() is non empty set
K135() is set
bool K135() is non empty set
bool K140() is non empty set
{} is empty set
1 is non empty set
0 is empty Element of K140()
{0} is non empty set
X is non empty set
o is Element of X
[:X,X:] is non empty set
[:[:X,X:],X:] is non empty set
bool [:[:X,X:],X:] is non empty set
md is V1() V4([:X,X:]) V5(X) Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]
b is set
a is set
bool [:X,X:] is non empty set
a is V1() V4(X) V5(X) Element of bool [:X,X:]
x is V1() V4(X) V5(X) Element of bool [:X,X:]
y is set
z is set
0F is Element of X
p is Element of X
[0F,p] is Element of [:X,X:]
{0F,p} is non empty set
{0F} is non empty set
{{0F,p},{0F}} 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 V116() left_unital doubleLoopStr
the carrier of F is non empty non trivial set
[: the carrier of F,X:] is non empty set
[:[: the carrier of F,X:],X:] is non empty set
bool [:[: the carrier of F,X:],X:] is non empty set
S is V1() V4([: the carrier of F,X:]) V5(X) Function-like V18([: the carrier of F,X:],X) Element of bool [:[: the carrier of F,X:],X:]
b is V1() V4(X) V5(X) Element of bool [:X,X:]
SymStr(# X,md,o,S,b #) is non empty strict SymStr over F
the carrier of SymStr(# X,md,o,S,b #) is non empty set
0. SymStr(# X,md,o,S,b #) is V53( SymStr(# X,md,o,S,b #)) Element of the carrier of SymStr(# X,md,o,S,b #)
x is Element of the carrier of SymStr(# X,md,o,S,b #)
x + (0. SymStr(# X,md,o,S,b #)) is Element of the carrier of SymStr(# X,md,o,S,b #)
the addF of SymStr(# X,md,o,S,b #) is V1() V4([: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):]) V5( the carrier of SymStr(# X,md,o,S,b #)) Function-like V18([: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):], the carrier of SymStr(# X,md,o,S,b #)) Element of bool [:[: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):], the carrier of SymStr(# X,md,o,S,b #):]
[: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):] is non empty set
[:[: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):], the carrier of SymStr(# X,md,o,S,b #):] is non empty set
bool [:[: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):], the carrier of SymStr(# X,md,o,S,b #):] is non empty set
the addF of SymStr(# X,md,o,S,b #) . (x,(0. SymStr(# X,md,o,S,b #))) is Element of the carrier of SymStr(# X,md,o,S,b #)
[x,(0. SymStr(# X,md,o,S,b #))] is set
{x,(0. SymStr(# X,md,o,S,b #))} is non empty set
{x} is non empty set
{{x,(0. SymStr(# X,md,o,S,b #))},{x}} is non empty set
the addF of SymStr(# X,md,o,S,b #) . [x,(0. SymStr(# X,md,o,S,b #))] is set
md . (x,(0. SymStr(# X,md,o,S,b #))) is set
md . [x,(0. SymStr(# X,md,o,S,b #))] is set
x is Element of the carrier of SymStr(# X,md,o,S,b #)
- x is Element of the carrier of SymStr(# X,md,o,S,b #)
x + (- x) is Element of the carrier of SymStr(# X,md,o,S,b #)
the addF of SymStr(# X,md,o,S,b #) is V1() V4([: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):]) V5( the carrier of SymStr(# X,md,o,S,b #)) Function-like V18([: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):], the carrier of SymStr(# X,md,o,S,b #)) Element of bool [:[: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):], the carrier of SymStr(# X,md,o,S,b #):]
[: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):] is non empty set
[:[: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):], the carrier of SymStr(# X,md,o,S,b #):] is non empty set
bool [:[: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):], the carrier of SymStr(# X,md,o,S,b #):] is non empty set
the addF of SymStr(# X,md,o,S,b #) . (x,(- x)) is Element of the carrier of SymStr(# X,md,o,S,b #)
[x,(- x)] is set
{x,(- x)} is non empty set
{x} is non empty set
{{x,(- x)},{x}} is non empty set
the addF of SymStr(# X,md,o,S,b #) . [x,(- x)] is set
x is Element of the carrier of SymStr(# X,md,o,S,b #)
y is Element of the carrier of SymStr(# X,md,o,S,b #)
x + y is Element of the carrier of SymStr(# X,md,o,S,b #)
the addF of SymStr(# X,md,o,S,b #) is V1() V4([: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):]) V5( the carrier of SymStr(# X,md,o,S,b #)) Function-like V18([: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):], the carrier of SymStr(# X,md,o,S,b #)) Element of bool [:[: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):], the carrier of SymStr(# X,md,o,S,b #):]
[: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):] is non empty set
[:[: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):], the carrier of SymStr(# X,md,o,S,b #):] is non empty set
bool [:[: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):], the carrier of SymStr(# X,md,o,S,b #):] is non empty set
the addF of SymStr(# X,md,o,S,b #) . (x,y) is Element of the carrier of SymStr(# X,md,o,S,b #)
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the addF of SymStr(# X,md,o,S,b #) . [x,y] is set
z is Element of the carrier of SymStr(# X,md,o,S,b #)
(x + y) + z is Element of the carrier of SymStr(# X,md,o,S,b #)
the addF of SymStr(# X,md,o,S,b #) . ((x + y),z) is Element of the carrier of SymStr(# X,md,o,S,b #)
[(x + y),z] is set
{(x + y),z} is non empty set
{(x + y)} is non empty set
{{(x + y),z},{(x + y)}} is non empty set
the addF of SymStr(# X,md,o,S,b #) . [(x + y),z] is set
y + z is Element of the carrier of SymStr(# X,md,o,S,b #)
the addF of SymStr(# X,md,o,S,b #) . (y,z) is Element of the carrier of SymStr(# X,md,o,S,b #)
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
the addF of SymStr(# X,md,o,S,b #) . [y,z] is set
x + (y + z) is Element of the carrier of SymStr(# X,md,o,S,b #)
the addF of SymStr(# X,md,o,S,b #) . (x,(y + z)) is Element of the carrier of SymStr(# X,md,o,S,b #)
[x,(y + z)] is set
{x,(y + z)} is non empty set
{{x,(y + z)},{x}} is non empty set
the addF of SymStr(# X,md,o,S,b #) . [x,(y + z)] is set
0F is Element of X
p is Element of X
r is Element of X
md . (p,r) is Element of X
[p,r] is set
{p,r} is non empty set
{p} is non empty set
{{p,r},{p}} is non empty set
md . [p,r] is set
md . (0F,(md . (p,r))) is Element of X
[0F,(md . (p,r))] is set
{0F,(md . (p,r))} is non empty set
{0F} is non empty set
{{0F,(md . (p,r))},{0F}} is non empty set
md . [0F,(md . (p,r))] is set
x is Element of the carrier of SymStr(# X,md,o,S,b #)
y is Element of the carrier of SymStr(# X,md,o,S,b #)
x + y is Element of the carrier of SymStr(# X,md,o,S,b #)
the addF of SymStr(# X,md,o,S,b #) is V1() V4([: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):]) V5( the carrier of SymStr(# X,md,o,S,b #)) Function-like V18([: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):], the carrier of SymStr(# X,md,o,S,b #)) Element of bool [:[: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):], the carrier of SymStr(# X,md,o,S,b #):]
[: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):] is non empty set
[:[: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):], the carrier of SymStr(# X,md,o,S,b #):] is non empty set
bool [:[: the carrier of SymStr(# X,md,o,S,b #), the carrier of SymStr(# X,md,o,S,b #):], the carrier of SymStr(# X,md,o,S,b #):] is non empty set
the addF of SymStr(# X,md,o,S,b #) . (x,y) is Element of the carrier of SymStr(# X,md,o,S,b #)
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the addF of SymStr(# X,md,o,S,b #) . [x,y] is set
y + x is Element of the carrier of SymStr(# X,md,o,S,b #)
the addF of SymStr(# X,md,o,S,b #) . (y,x) is Element of the carrier of SymStr(# X,md,o,S,b #)
[y,x] is set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
the addF of SymStr(# X,md,o,S,b #) . [y,x] is set
md . (x,y) is set
md . [x,y] is 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 V116() left_unital doubleLoopStr
the carrier of F is non empty non trivial set
[: the carrier of F,X:] is non empty set
[:[: the carrier of F,X:],X:] is non empty set
bool [:[: the carrier of F,X:],X:] is non empty set
S is V1() V4([: the carrier of F,X:]) V5(X) Function-like V18([: the carrier of F,X:],X) Element of bool [:[: the carrier of F,X:],X:]
a is non empty right_complementable Abelian add-associative right_zeroed SymStr over F
b is V1() V4(X) V5(X) Element of bool [:X,X:]
SymStr(# X,md,o,S,b #) is non empty strict SymStr over F
the carrier of a is non empty set
1_ F is Element of the carrier of F
K173(F) is V53(F) 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) Function-like 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 set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the addF of F . [x,y] is set
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) Function-like 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
the multF of F . [x,y] is set
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) Function-like 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
[z,0F] is set
{z,0F} is non empty set
{z} is non empty set
{{z,0F},{z}} is non empty set
the addF of a . [z,0F] is set
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 * z),(x * 0F)] is set
{(x * z),(x * 0F)} is non empty set
{(x * z)} is non empty set
{{(x * z),(x * 0F)},{(x * z)}} is non empty set
the addF of a . [(x * z),(x * 0F)] is set
(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 * z),(y * z)] is set
{(x * z),(y * z)} is non empty set
{{(x * z),(y * z)},{(x * z)}} is non empty set
the addF of a . [(x * z),(y * z)] is set
(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
[(x * y),z] is set
{(x * y),z} is non empty set
{(x * y)} is non empty set
{{(x * y),z},{(x * y)}} is non empty set
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
[y,v] is set
{y,v} is non empty set
{y} is non empty set
{{y,v},{y}} is non empty set
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 X
[x,o] is set
{x,o} is non empty set
{{x,o},{x}} is non empty set
S . [x,o] is set
0. a is V53(a) Element of the carrier of a
p is Element of the carrier of a
r is Element of the carrier of a
v is Element of X
v is Element of X
md . (v,v) is Element of X
[v,v] is set
{v,v} is non empty set
{v} is non empty set
{{v,v},{v}} is non empty set
md . [v,v] is set
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
[v,v] is set
{v,v} is non empty set
{v} is non empty set
{{v,v},{v}} is non empty set
the addF of a . [v,v] is set
x * (v + v) is Element of the carrier of a
S . (x,o) is Element of X
[x,o] is set
{x,o} is non empty set
{{x,o},{x}} is non empty set
S . [x,o] is set
v is Element of the carrier of a
S . (x,v) is set
[x,v] is set
{x,v} is non empty set
{{x,v},{x}} is non empty set
S . [x,v] is set
v is Element of the carrier of a
S . (x,v) is set
[x,v] is set
{x,v} is non empty set
{{x,v},{x}} is non empty set
S . [x,v] is set
w is Element of the carrier of a
x * w is Element of the carrier of a
v is Element of the carrier of a
x * v is Element of the carrier of a
S . ((x + y),z) is set
[(x + y),z] is set
{(x + y),z} is non empty set
{(x + y)} is non empty set
{{(x + y),z},{(x + y)}} is non empty set
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
[x,v] is set
{x,v} is non empty set
{{x,v},{x}} is non empty set
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
[y,v] is set
{y,v} is non empty set
{y} is non empty set
{{y,v},{y}} is non empty set
S . [y,v] is set
0. a is V53(a) 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
[(1_ F),z] is set
{(1_ F),z} is non empty set
{(1_ F)} is non empty set
{{(1_ F),z},{(1_ F)}} is non empty set
S . [(1_ F),z] is set
r is Element of the carrier of a
S . ((1_ F),r) is set
[(1_ F),r] is set
{(1_ F),r} is non empty set
{{(1_ F),r},{(1_ F)}} is non empty set
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 V116() left_unital doubleLoopStr
the carrier of S is non empty non trivial set
[: the carrier of S,X:] is non empty set
[:[: the carrier of S,X:],X:] is non empty set
bool [:[: the carrier of S,X:],X:] is non empty set
a is V1() V4(X) V5(X) Element of bool [:X,X:]
x is non empty right_complementable Abelian add-associative right_zeroed SymStr over S
b is V1() V4([: the carrier of S,X:]) V5(X) Function-like V18([: the carrier of S,X:],X) Element of bool [:[: the carrier of S,X:],X:]
SymStr(# X,md,o,b,a #) is non empty strict SymStr over S
0. x is V53(x) Element of the carrier of x
the carrier of x 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 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 X
p is Element of X
[0F,p] is Element of [:X,X:]
{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 X
p is Element of X
[0F,p] is Element of [:X,X:]
{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) Function-like 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,0F] is set
{z,0F} is non empty set
{z} is non empty set
{{z,0F},{z}} is non empty set
the addF of x . [z,0F] is set
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
- 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) Function-like 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,(- 0F)] is set
{z,(- 0F)} is non empty set
{z} is non empty set
{{z,(- 0F)},{z}} is non empty set
the addF of x . [z,(- 0F)] is set
0F - y is Element of the carrier of x
- y 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
[0F,(- y)] is set
{0F,(- y)} is non empty set
{0F} is non empty set
{{0F,(- y)},{0F}} is non empty set
the addF of x . [0F,(- y)] is set
y - z 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 addF of x . (y,(- z)) is Element of the carrier of x
[y,(- z)] is set
{y,(- z)} is non empty set
{y} is non empty set
{{y,(- z)},{y}} is non empty set
the addF of x . [y,(- z)] is 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 V116() 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 V116() left_unital doubleLoopStr
the carrier of F is non empty non trivial set
[: the carrier of F,X:] is non empty set
[:[: the carrier of F,X:],X:] is non empty set
bool [:[: the carrier of F,X:],X:] is non empty set
[: the carrier of F,X:] --> o is V1() V4([: the carrier of F,X:]) V5(X) Function-like V18([: the carrier of F,X:],X) Element of bool [:[: the carrier of F,X:],X:]
b is V1() V4(X) V5(X) Element of bool [:X,X:]
S is V1() V4([: the carrier of F,X:]) V5(X) Function-like V18([: the carrier of F,X:],X) Element of bool [:[: the carrier of F,X:],X:]
SymStr(# X,md,o,S,b #) is non empty strict SymStr over F
a is non empty right_complementable Abelian add-associative right_zeroed SymStr over F
the carrier of a is non empty set
0. a is V53(a) 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 a
p is Element of the carrier of a
r is Element of the carrier of a
v is Element of the carrier of F
v * p 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 + 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) Function-like 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 . (v,v) is Element of the carrier of a
[v,v] is set
{v,v} is non empty set
{v} is non empty set
{{v,v},{v}} is non empty set
the addF of a . [v,v] is set
v is Element of the carrier of a
v is Element of the carrier of a
v is Element of the carrier of a
w 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
- 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₂₂,(- c₂₃)] is set
{c₂₂,(- c₂₃)} is non empty set
{c₂₂} is non empty set
{{c₂₂,(- c₂₃)},{c₂₂}} is non empty set
the addF of a . [c₂₂,(- c₂₃)] is set
c₂₃ - w is Element of the carrier of a
- w is Element of the carrier of a
c₂₃ + (- w) is Element of the carrier of a
the addF of a . (c₂₃,(- w)) is Element of the carrier of a
[c₂₃,(- w)] is set
{c₂₃,(- w)} is non empty set
{c₂₃} is non empty set
{{c₂₃,(- w)},{c₂₃}} is non empty set
the addF of a . [c₂₃,(- w)] is set
w - c₂₂ is Element of the carrier of a
- c₂₂ is Element of the carrier of a
w + (- c₂₂) is Element of the carrier of a
the addF of a . (w,(- c₂₂)) is Element of the carrier of a
[w,(- c₂₂)] is set
{w,(- c₂₂)} is non empty set
{w} is non empty set
{{w,(- c₂₂)},{w}} is non empty set
the addF of a . [w,(- c₂₂)] is set
x is Element of the carrier of F
y is Element of X
[x,y] is Element of [: the carrier of F,X:]
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
S . [x,y] is Element 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 V116() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) SymStr over F
the carrier of S is non empty set
0. S is V53(S) Element of the carrier of S
b is Element of the carrier of S
0. F is V53(F) Element of the carrier of F
the carrier of F is non empty non trivial set
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) Function-like 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. S),(- (y * b))] is set
{(0. S),(- (y * b))} is non empty set
{(0. S)} is non empty set
{{(0. S),(- (y * b))},{(0. S)}} is non empty set
the addF of S . [(0. S),(- (y * b))] is set
(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 V116() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) SymStr over 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 V53(S) Element of the carrier of S
- a is Element of the carrier of S
- (- a) is Element of the carrier of S
(0. S) - (- a) 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) Function-like 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
[(0. S),(- (- a))] is set
{(0. S),(- (- a))} is non empty set
{(0. S)} is non empty set
{{(0. S),(- (- a))},{(0. S)}} is non empty set
the addF of S . [(0. S),(- (- a))] is set
(- a) - b is Element of the carrier of S
- b 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)] is set
{(- a),(- b)} is non empty set
{(- a)} is non empty set
{{(- a),(- b)},{(- a)}} is non empty set
the addF of S . [(- a),(- b)] is set
b - (0. S) is Element of the carrier of S
- (0. 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
[b,(- (0. S))] is set
{b,(- (0. S))} is non empty set
{b} is non empty set
{{b,(- (0. S))},{b}} is non empty set
the addF of S . [b,(- (0. S))] is set
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
K173(F) is V53(F) Element of the carrier of F
- (1_ F) is Element of the carrier of F
(- (1_ F)) * (- 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 V116() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) SymStr over 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) Function-like 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
[x,b] is set
{x,b} is non empty set
{x} is non empty set
{{x,b},{x}} is non empty set
the addF of S . [x,b] is set
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
K173(F) is V53(F) 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 + b)] is set
{(- x),(x + b)} is non empty set
{(- x)} is non empty set
{{(- x),(x + b)},{(- x)}} is non empty set
the addF of S . [(- x),(x + b)] is set
x + (- x) is Element of the carrier of S
the addF of S . (x,(- x)) is Element of the carrier of S
[x,(- x)] is set
{x,(- x)} is non empty set
{{x,(- x)},{x}} is non empty set
the addF of S . [x,(- x)] is set
(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)),b] is set
{(x + (- x)),b} is non empty set
{(x + (- x))} is non empty set
{{(x + (- x)),b},{(x + (- x))}} is non empty set
the addF of S . [(x + (- x)),b] is set
0. S is V53(S) 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
[(0. S),b] is set
{(0. S),b} is non empty set
{(0. S)} is non empty set
{{(0. S),b},{(0. S)}} is non empty set
the addF of S . [(0. S),b] is 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 V116() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) SymStr over 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) Function-like 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
[b,x] is set
{b,x} is non empty set
{b} is non empty set
{{b,x},{b}} is non empty set
the addF of S . [b,x] is set
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
K173(F) is V53(F) 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
[(b + x),(- x)] is set
{(b + x),(- x)} is non empty set
{(b + x)} is non empty set
{{(b + x),(- x)},{(b + x)}} is non empty set
the addF of S . [(b + x),(- x)] is set
x + (- x) is Element of the carrier of S
the addF of S . (x,(- x)) is Element of the carrier of S
[x,(- x)] is set
{x,(- x)} is non empty set
{x} is non empty set
{{x,(- x)},{x}} is non empty set
the addF of S . [x,(- x)] is set
b + (x + (- x)) is Element of the carrier of S
the addF of S . (b,(x + (- x))) is Element of the carrier of S
[b,(x + (- x))] is set
{b,(x + (- x))} is non empty set
{{b,(x + (- x))},{b}} is non empty set
the addF of S . [b,(x + (- x))] is set
0. S is V53(S) 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
[b,(0. S)] is set
{b,(0. S)} is non empty set
{{b,(0. S)},{b}} is non empty set
the addF of S . [b,(0. S)] is 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 V116() left_unital doubleLoopStr
the carrier of F is non empty non trivial set
0. F is V53(F) 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) SymStr over 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 Element of the carrier of F
K173(F) is V53(F) 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) Function-like 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] is set
{z,x} is non empty set
{z} is non empty set
{{z,x},{z}} is non empty set
the multF of F . [z,x] is set
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] is set
{z,x} is non empty set
{z} is non empty set
{{z,x},{z}} is non empty set
the multF of F . [z,x] is set
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 V116() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) SymStr over 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
K173(F) is V53(F) 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 V116() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) SymStr over 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) Function-like 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
[b,(- a)] is set
{b,(- a)} is non empty set
{b} is non empty set
{{b,(- a)},{b}} is non empty set
the addF of S . [b,(- a)] is set
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
[b,(- y)] is set
{b,(- y)} is non empty set
{{b,(- y)},{b}} is non empty set
the addF of S . [b,(- y)] is set
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
[a,(- y)] is set
{a,(- y)} is non empty set
{a} is non empty set
{{a,(- y)},{a}} is non empty set
the addF of S . [a,(- y)] is set
- (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
[(- b),a] is set
{(- b),a} is non empty set
{(- b)} is non empty set
{{(- b),a},{(- b)}} is non empty set
the addF of S . [(- b),a] is set
a + (- b) is Element of the carrier of S
the addF of S . (a,(- b)) is Element of the carrier of S
[a,(- b)] is set
{a,(- b)} is non empty set
{{a,(- b)},{a}} is non empty set
the addF of S . [a,(- b)] is set
(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
[(a + (- b)),(b - y)] is set
{(a + (- b)),(b - y)} is non empty set
{(a + (- b))} is non empty set
{{(a + (- b)),(b - y)},{(a + (- b))}} is non empty set
the addF of S . [(a + (- b)),(b - y)] is set
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
[(- b),(b + (- y))] is set
{(- b),(b + (- y))} is non empty set
{{(- b),(b + (- y))},{(- b)}} is non empty set
the addF of S . [(- b),(b + (- y))] is set
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
[a,((- b) + (b + (- y)))] is set
{a,((- b) + (b + (- y)))} is non empty set
{{a,((- b) + (b + (- y)))},{a}} is non empty set
the addF of S . [a,((- b) + (b + (- y)))] is set
(- b) + b is Element of the carrier of S
the addF of S . ((- b),b) is Element of the carrier of S
[(- b),b] is set
{(- b),b} is non empty set
{{(- b),b},{(- b)}} is non empty set
the addF of S . [(- b),b] is set
((- 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) + b),(- y)] is set
{((- b) + b),(- y)} is non empty set
{((- b) + b)} is non empty set
{{((- b) + b),(- y)},{((- b) + b)}} is non empty set
the addF of S . [((- b) + b),(- y)] is set
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
[a,(((- b) + b) + (- y))] is set
{a,(((- b) + b) + (- y))} is non empty set
{{a,(((- b) + b) + (- y))},{a}} is non empty set
the addF of S . [a,(((- b) + b) + (- y))] is set
0. S is V53(S) 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
[(0. S),(- y)] is set
{(0. S),(- y)} is non empty set
{(0. S)} is non empty set
{{(0. S),(- y)},{(0. S)}} is non empty set
the addF of S . [(0. S),(- y)] is set
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
[a,((0. S) + (- y))] is set
{a,((0. S) + (- y))} is non empty set
{{a,((0. S) + (- y))},{a}} is non empty set
the addF of S . [a,((0. S) + (- y))] is 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 V116() 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) SymStr over 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) Function-like 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
[x,(- (y * b))] is set
{x,(- (y * b))} is non empty set
{x} is non empty set
{{x,(- (y * b))},{x}} is non empty set
the addF of S . [x,(- (y * b))] is set
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
[x,(- (z * b))] is set
{x,(- (z * b))} is non empty set
{{x,(- (z * b))},{x}} is non empty set
the addF of S . [x,(- (z * b))] is set
1_ F is Element of the carrier of F
K173(F) is V53(F) 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
[(y * b),(- (z * b))] is set
{(y * b),(- (z * b))} is non empty set
{(y * b)} is non empty set
{{(y * b),(- (z * b))},{(y * b)}} is non empty set
the addF of S . [(y * b),(- (z * b))] is set
- (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
[(y * b),((- (1_ F)) * (z * b))] is set
{(y * b),((- (1_ F)) * (z * b))} is non empty set
{{(y * b),((- (1_ F)) * (z * b))},{(y * b)}} is non empty set
the addF of S . [(y * b),((- (1_ F)) * (z * b))] is set
(- (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) Function-like 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] is set
{(- (1_ F)),z} is non empty set
{(- (1_ F))} is non empty set
{{(- (1_ F)),z},{(- (1_ F))}} is non empty set
the multF of F . [(- (1_ F)),z] is set
((- (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
[(y * b),(((- (1_ F)) * z) * b)] is set
{(y * b),(((- (1_ F)) * z) * b)} is non empty set
{{(y * b),(((- (1_ F)) * z) * b)},{(y * b)}} is non empty set
the addF of S . [(y * b),(((- (1_ F)) * z) * b)] is set
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 set
{z,(1_ F)} is non empty set
{z} is non empty set
{{z,(1_ F)},{z}} is non empty set
the multF of F . [z,(1_ F)] is set
- (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
[(y * b),((- (z * (1_ F))) * b)] is set
{(y * b),((- (z * (1_ F))) * b)} is non empty set
{{(y * b),((- (z * (1_ F))) * b)},{(y * b)}} is non empty set
the addF of S . [(y * b),((- (z * (1_ F))) * b)] is set
- 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 * b),((- z) * b)] is set
{(y * b),((- z) * b)} is non empty set
{{(y * b),((- z) * b)},{(y * b)}} is non empty set
the addF of S . [(y * b),((- z) * b)] is set
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) Function-like 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)] is set
{y,(- z)} is non empty set
{y} is non empty set
{{y,(- z)},{y}} is non empty set
the addF of F . [y,(- z)] is set
(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))] is set
{((y + (- z)) "),(y + (- z))} is non empty set
{((y + (- z)) ")} is non empty set
{{((y + (- z)) "),(y + (- z))},{((y + (- z)) ")}} is non empty set
the multF of F . [((y + (- z)) "),(y + (- z))] is set
(((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 V53(F) 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 V116() left_unital doubleLoopStr
S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) SymStr over 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
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) Function-like 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
[b,a] is set
{b,a} is non empty set
{b} is non empty set
{{b,a},{b}} is non empty set
the addF of S . [b,a] is set
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 . (b,(- a)) is Element of the carrier of S
[b,(- a)] is set
{b,(- a)} is non empty set
{{b,(- a)},{b}} is non empty set
the addF of S . [b,(- a)] is set
0. S is V53(S) 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
K173(F) is V53(F) 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
- b 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
[(0. S),(- b)] is set
{(0. S),(- b)} is non empty set
{(0. S)} is non empty set
{{(0. S),(- b)},{(0. S)}} is non empty set
the addF of S . [(0. S),(- b)] is set
a + (- a) is Element of the carrier of S
the addF of S . (a,(- a)) is Element of the carrier of S
[a,(- a)] is set
{a,(- a)} is non empty set
{a} is non empty set
{{a,(- a)},{a}} is non empty set
the addF of S . [a,(- a)] is set
(a + (- a)) + (- b) is Element of the carrier of S
the addF of S . ((a + (- a)),(- b)) is Element of the carrier of S
[(a + (- a)),(- b)] is set
{(a + (- a)),(- b)} is non empty set
{(a + (- a))} is non empty set
{{(a + (- a)),(- b)},{(a + (- a))}} is non empty set
the addF of S . [(a + (- a)),(- b)] is set
(- a) - b 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)] is set
{(- a),(- b)} is non empty set
{(- a)} is non empty set
{{(- a),(- b)},{(- a)}} is non empty set
the addF of S . [(- a),(- b)] is set
a + ((- a) - b) is Element of the carrier of S
the addF of S . (a,((- a) - b)) is Element of the carrier of S
[a,((- a) - b)] is set
{a,((- a) - b)} is non empty set
{{a,((- a) - b)},{a}} is non empty set
the addF of S . [a,((- a) - b)] is set
a - (b + a) is Element of the carrier of S
- (b + a) is Element of the carrier of S
a + (- (b + a)) is Element of the carrier of S
the addF of S . (a,(- (b + a))) is Element of the carrier of S
[a,(- (b + a))] is set
{a,(- (b + a))} is non empty set
{{a,(- (b + a))},{a}} is non empty set
the addF of S . [a,(- (b + a))] is set
a + (0. S) is Element of the carrier of S
the addF of S . (a,(0. S)) is Element of the carrier of S
[a,(0. S)] is set
{a,(0. S)} is non empty set
{{a,(0. S)},{a}} is non empty set
the addF of S . [a,(0. S)] is set
b + (- b) is Element of the carrier of S
the addF of S . (b,(- b)) is Element of the carrier of S
[b,(- b)] is set
{b,(- b)} is non empty set
{{b,(- b)},{b}} is non empty set
the addF of S . [b,(- b)] is set
a + (b + (- b)) is Element of the carrier of S
the addF of S . (a,(b + (- b))) is Element of the carrier of S
[a,(b + (- b))] is set
{a,(b + (- b))} is non empty set
{{a,(b + (- b))},{a}} is non empty set
the addF of S . [a,(b + (- b))] is set
(b + a) - b is Element of the carrier of S
(b + a) + (- b) is Element of the carrier of S
the addF of S . ((b + a),(- b)) is Element of the carrier of S
[(b + a),(- b)] is set
{(b + a),(- b)} is non empty set
{(b + a)} is non empty set
{{(b + a),(- b)},{(b + a)}} is non empty set
the addF of S . [(b + a),(- b)] is 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 V116() left_unital doubleLoopStr
1_ F is Element of the carrier of F
the carrier of F is non empty non trivial set
K173(F) is V53(F) 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) Function-like 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
[(1_ F),(1_ F)] is set
{(1_ F),(1_ F)} is non empty set
{(1_ F)} is non empty set
{{(1_ F),(1_ F)},{(1_ F)}} is non empty set
the addF of F . [(1_ F),(1_ F)] is set
0. F is V53(F) 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) SymStr over F
the carrier of S is non empty set
0. S is V53(S) Element of the carrier of S
x 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
z + 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) Function-like V18([: the carrier of S, the