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

1 is non empty set
0 is empty Element of K140()
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

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

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

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

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

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

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
c22 is Element of the carrier of a
c23 is Element of the carrier of a
c22 - c23 is Element of the carrier of a
- c23 is Element of the carrier of a
c22 + (- c23) is Element of the carrier of a
the addF of a . (c22,(- c23)) is Element of the carrier of a
[c22,(- c23)] is set
{c22,(- c23)} is non empty set
{c22} is non empty set
{{c22,(- c23)},{c22}} is non empty set
the addF of a . [c22,(- c23)] is set
c23 - w is Element of the carrier of a
- w is Element of the carrier of a
c23 + (- w) is Element of the carrier of a
the addF of a . (c23,(- w)) is Element of the carrier of a
[c23,(- w)] is set
{c23,(- w)} is non empty set
{c23} is non empty set
{{c23,(- w)},{c23}} is non empty set
the addF of a . [c23,(- w)] is set
w - c22 is Element of the carrier of a
- c22 is Element of the carrier of a
w + (- c22) is Element of the carrier of a
the addF of a . (w,(- c22)) is Element of the carrier of a
[w,(- c22)] is set
{w,(- c22)} is non empty set
{w} is non empty set
{{w,(- c22)},{w}} is non empty set
the addF of a . [w,(- c22)] 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

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

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

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

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

the carrier of F is non empty non trivial set
0. F is V53(F) Element of the carrier of 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

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

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

the carrier of F is non empty non trivial set

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

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

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

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