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

c

c

- c

c

the addF of a . (c

[c

{c

{c

{{c

the addF of a . [c

c

- w is Element of the carrier of a

c

the addF of a . (c

[c

{c

{c

{{c

the addF of a . [c

w - c

- c

w + (- c

the addF of a . (w,(- c

[w,(- c

{w,(- c

{w} is non empty set

{{w,(- c

the addF of a . [w,(- c

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