:: SYMSP_1 semantic presentation

K122() is Element of bool K118()

K118() is set

bool K118() is non empty set

K117() is set

bool K117() is non empty set

bool K122() is non empty set

{} is empty set

1 is non empty set

X is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

the non empty set is non empty set

[: the non empty set , the non empty set :] is non empty set

[:[: the non empty set , the non empty set :], the non empty set :] is non empty set

bool [:[: the non empty set , the non empty set :], the non empty set :] is non empty set

the V1() V4([: the non empty set , the non empty set :]) V5( the non empty set ) V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is V1() V4([: the non empty set , the non empty set :]) V5( the non empty set ) V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :]

the Element of the non empty set is Element of the non empty set

the carrier of X is non empty non trivial set

[: the carrier of X, the non empty set :] is non empty set

[:[: the carrier of X, the non empty set :], the non empty set :] is non empty set

bool [:[: the carrier of X, the non empty set :], the non empty set :] is non empty set

the V1() V4([: the carrier of X, the non empty set :]) V5( the non empty set ) V6() V18([: the carrier of X, the non empty set :], the non empty set ) Element of bool [:[: the carrier of X, the non empty set :], the non empty set :] is V1() V4([: the carrier of X, the non empty set :]) V5( the non empty set ) V6() V18([: the carrier of X, the non empty set :], the non empty set ) Element of bool [:[: the carrier of X, the non empty set :], the non empty set :]

bool [: the non empty set , the non empty set :] is non empty set

the V1() V4( the non empty set ) V5( the non empty set ) Element of bool [: the non empty set , the non empty set :] is V1() V4( the non empty set ) V5( the non empty set ) Element of bool [: the non empty set , the non empty set :]

(X, the non empty set , the V1() V4([: the non empty set , the non empty set :]) V5( the non empty set ) V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Element of the non empty set , the V1() V4([: the carrier of X, the non empty set :]) V5( the non empty set ) V6() V18([: the carrier of X, the non empty set :], the non empty set ) Element of bool [:[: the carrier of X, the non empty set :], the non empty set :], the V1() V4( the non empty set ) V5( the non empty set ) Element of bool [: the non empty set , the non empty set :]) is (X) (X)

the carrier of (X, the non empty set , the V1() V4([: the non empty set , the non empty set :]) V5( the non empty set ) V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Element of the non empty set , the V1() V4([: the carrier of X, the non empty set :]) V5( the non empty set ) V6() V18([: the carrier of X, the non empty set :], the non empty set ) Element of bool [:[: the carrier of X, the non empty set :], the non empty set :], the V1() V4( the non empty set ) V5( the non empty set ) Element of bool [: the non empty set , the non empty set :]) is set

X is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

o is (X)

the carrier of o is set

0 is empty Element of K122()

{0} is non empty set

o is Element of {0}

[:{0},{0}:] is non empty set

[:[:{0},{0}:],{0}:] is non empty set

bool [:[:{0},{0}:],{0}:] is non empty set

md is V1() V4([:{0},{0}:]) V5({0}) V6() V18([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:]

b is set

a is set

bool [:{0},{0}:] is non empty set

a is V1() V4({0}) V5({0}) Element of bool [:{0},{0}:]

x is V1() V4({0}) V5({0}) Element of bool [:{0},{0}:]

y is set

z is set

0F is Element of {0}

p is Element of {0}

[0F,p] is Element of [:{0},{0}:]

{0F,p} is non empty set

{0F} is non empty set

{{0F,p},{0F}} is non empty set

S is non empty set

[:S,S:] is non empty set

[:[:S,S:],S:] is non empty set

bool [:[:S,S:],S:] is non empty set

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

the carrier of F is non empty non trivial set

[: the carrier of F,S:] is non empty set

[:[: the carrier of F,S:],S:] is non empty set

bool [:[: the carrier of F,S:],S:] is non empty set

bool [:S,S:] is non empty set

b is V1() V4([:S,S:]) V5(S) V6() V18([:S,S:],S) Element of bool [:[:S,S:],S:]

a is Element of S

x is V1() V4([: the carrier of F,S:]) V5(S) V6() V18([: the carrier of F,S:],S) Element of bool [:[: the carrier of F,S:],S:]

y is V1() V4(S) V5(S) Element of bool [:S,S:]

(F,S,b,a,x,y) is (F) (F)

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

the carrier of F is non empty non trivial set

[: the carrier of F,{0}:] is non empty set

[:[: the carrier of F,{0}:],{0}:] is non empty set

bool [:[: the carrier of F,{0}:],{0}:] is non empty set

S is V1() V4([: the carrier of F,{0}:]) V5({0}) V6() V18([: the carrier of F,{0}:],{0}) Element of bool [:[: the carrier of F,{0}:],{0}:]

b is V1() V4({0}) V5({0}) Element of bool [:{0},{0}:]

(F,{0},md,o,S,b) is non empty (F) (F)

the carrier of (F,{0},md,o,S,b) is non empty set

x is Element of the carrier of (F,{0},md,o,S,b)

y is Element of the carrier of (F,{0},md,o,S,b)

x + y is Element of the carrier of (F,{0},md,o,S,b)

the addF of (F,{0},md,o,S,b) is V1() V4([: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):]) V5( the carrier of (F,{0},md,o,S,b)) V6() V18([: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b)) Element of bool [:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):]

[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):] is non empty set

[:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):] is non empty set

bool [:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):] is non empty set

the addF of (F,{0},md,o,S,b) . (x,y) is Element of the carrier of (F,{0},md,o,S,b)

y + x is Element of the carrier of (F,{0},md,o,S,b)

the addF of (F,{0},md,o,S,b) . (y,x) is Element of the carrier of (F,{0},md,o,S,b)

z is Element of {0}

0F is Element of {0}

md . (z,0F) is Element of {0}

the carrier of (F,{0},md,o,S,b) is non empty set

x is Element of the carrier of (F,{0},md,o,S,b)

y is Element of the carrier of (F,{0},md,o,S,b)

x + y is Element of the carrier of (F,{0},md,o,S,b)

the addF of (F,{0},md,o,S,b) is V1() V4([: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):]) V5( the carrier of (F,{0},md,o,S,b)) V6() V18([: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b)) Element of bool [:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):]

[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):] is non empty set

[:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):] is non empty set

bool [:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):] is non empty set

the addF of (F,{0},md,o,S,b) . (x,y) is Element of the carrier of (F,{0},md,o,S,b)

z is Element of the carrier of (F,{0},md,o,S,b)

(x + y) + z is Element of the carrier of (F,{0},md,o,S,b)

the addF of (F,{0},md,o,S,b) . ((x + y),z) is Element of the carrier of (F,{0},md,o,S,b)

y + z is Element of the carrier of (F,{0},md,o,S,b)

the addF of (F,{0},md,o,S,b) . (y,z) is Element of the carrier of (F,{0},md,o,S,b)

x + (y + z) is Element of the carrier of (F,{0},md,o,S,b)

the addF of (F,{0},md,o,S,b) . (x,(y + z)) is Element of the carrier of (F,{0},md,o,S,b)

0F is Element of {0}

p is Element of {0}

r is Element of {0}

md . (p,r) is Element of {0}

md . (0F,(md . (p,r))) is Element of {0}

the carrier of (F,{0},md,o,S,b) is non empty set

x is Element of the carrier of (F,{0},md,o,S,b)

0. (F,{0},md,o,S,b) is V51((F,{0},md,o,S,b)) Element of the carrier of (F,{0},md,o,S,b)

the ZeroF of (F,{0},md,o,S,b) is Element of the carrier of (F,{0},md,o,S,b)

x + (0. (F,{0},md,o,S,b)) is Element of the carrier of (F,{0},md,o,S,b)

the addF of (F,{0},md,o,S,b) is V1() V4([: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):]) V5( the carrier of (F,{0},md,o,S,b)) V6() V18([: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b)) Element of bool [:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):]

[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):] is non empty set

[:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):] is non empty set

bool [:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):] is non empty set

the addF of (F,{0},md,o,S,b) . (x,(0. (F,{0},md,o,S,b))) is Element of the carrier of (F,{0},md,o,S,b)

y is Element of {0}

md . (y,(0. (F,{0},md,o,S,b))) is set

the carrier of (F,{0},md,o,S,b) is non empty set

x is Element of the carrier of (F,{0},md,o,S,b)

- x is Element of the carrier of (F,{0},md,o,S,b)

x + (- x) is Element of the carrier of (F,{0},md,o,S,b)

the addF of (F,{0},md,o,S,b) is V1() V4([: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):]) V5( the carrier of (F,{0},md,o,S,b)) V6() V18([: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b)) Element of bool [:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):]

[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):] is non empty set

[:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):] is non empty set

bool [:[: the carrier of (F,{0},md,o,S,b), the carrier of (F,{0},md,o,S,b):], the carrier of (F,{0},md,o,S,b):] is non empty set

the addF of (F,{0},md,o,S,b) . (x,(- x)) is Element of the carrier of (F,{0},md,o,S,b)

0. (F,{0},md,o,S,b) is V51((F,{0},md,o,S,b)) Element of the carrier of (F,{0},md,o,S,b)

the ZeroF of (F,{0},md,o,S,b) is Element of the carrier of (F,{0},md,o,S,b)

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

the V1() V4({0}) V5({0}) Element of bool [:{0},{0}:] is V1() V4({0}) V5({0}) Element of bool [:{0},{0}:]

the carrier of F is non empty non trivial set

[: the carrier of F,{0}:] is non empty set

[:[: the carrier of F,{0}:],{0}:] is non empty set

bool [:[: the carrier of F,{0}:],{0}:] is non empty set

the V1() V4([: the carrier of F,{0}:]) V5({0}) V6() V18([: the carrier of F,{0}:],{0}) Element of bool [:[: the carrier of F,{0}:],{0}:] is V1() V4([: the carrier of F,{0}:]) V5({0}) V6() V18([: the carrier of F,{0}:],{0}) Element of bool [:[: the carrier of F,{0}:],{0}:]

(F,{0},md,o, the V1() V4([: the carrier of F,{0}:]) V5({0}) V6() V18([: the carrier of F,{0}:],{0}) Element of bool [:[: the carrier of F,{0}:],{0}:], the V1() V4({0}) V5({0}) Element of bool [:{0},{0}:]) is non empty (F) (F)

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

the carrier of F is non empty non trivial set

[: the carrier of F,{0}:] is non empty set

[:[: the carrier of F,{0}:],{0}:] is non empty set

bool [:[: the carrier of F,{0}:],{0}:] is non empty set

S is V1() V4([: the carrier of F,{0}:]) V5({0}) V6() V18([: the carrier of F,{0}:],{0}) Element of bool [:[: the carrier of F,{0}:],{0}:]

a is non empty right_complementable Abelian add-associative right_zeroed (F)

b is V1() V4({0}) V5({0}) Element of bool [:{0},{0}:]

(F,{0},md,o,S,b) is non empty (F) (F)

the carrier of a is non empty set

1_ F is Element of the carrier of F

1. F is V51(F) Element of the carrier of F

the OneF of F is Element of the carrier of F

x is Element of the carrier of F

y is Element of the carrier of F

x + y is Element of the carrier of F

the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]

[: the carrier of F, the carrier of F:] is non empty set

[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set

bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set

the addF of F . (x,y) is Element of the carrier of F

x * y is Element of the carrier of F

the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]

the multF of F . (x,y) is Element of the carrier of F

z is Element of the carrier of a

0F is Element of the carrier of a

z + 0F is Element of the carrier of a

the addF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) V6() V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]

[: the carrier of a, the carrier of a:] is non empty set

[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

the addF of a . (z,0F) is Element of the carrier of a

x * (z + 0F) is Element of the carrier of a

x * z is Element of the carrier of a

x * 0F is Element of the carrier of a

(x * z) + (x * 0F) is Element of the carrier of a

the addF of a . ((x * z),(x * 0F)) is Element of the carrier of a

(x + y) * z is Element of the carrier of a

y * z is Element of the carrier of a

(x * z) + (y * z) is Element of the carrier of a

the addF of a . ((x * z),(y * z)) is Element of the carrier of a

(x * y) * z is Element of the carrier of a

x * (y * z) is Element of the carrier of a

(1_ F) * z is Element of the carrier of a

S . ((x * y),z) is set

r is Element of the carrier of a

v is Element of the carrier of a

(x * y) * v is Element of the carrier of a

v is Element of the carrier of a

S . (y,v) is set

v is Element of the carrier of a

y * v is Element of the carrier of a

x * (y * v) is Element of the carrier of a

S . (x,o) is Element of {0}

p is Element of {0}

r is Element of {0}

md . (p,r) is Element of {0}

v is Element of the carrier of a

v is Element of the carrier of a

v + v is Element of the carrier of a

the addF of a . (v,v) is Element of the carrier of a

x * (v + v) is Element of the carrier of a

S . (x,o) is Element of {0}

S . (x,v) is set

x * v is Element of the carrier of a

S . (x,v) is set

x * v is Element of the carrier of a

0. a is V51(a) Element of the carrier of a

the ZeroF of a is Element of the carrier of a

S . ((x + y),z) is set

r is Element of the carrier of a

v is Element of the carrier of a

(x + y) * v is Element of the carrier of a

v is Element of the carrier of a

S . (x,v) is set

v is Element of the carrier of a

x * v is Element of the carrier of a

v is Element of the carrier of a

S . (y,v) is set

0. a is V51(a) Element of the carrier of a

the ZeroF of a is Element of the carrier of a

v is Element of the carrier of a

y * v is Element of the carrier of a

S . ((1_ F),z) is set

r is Element of the carrier of a

S . ((1_ F),r) is set

S is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

the carrier of S is non empty non trivial set

[: the carrier of S,{0}:] is non empty set

[:[: the carrier of S,{0}:],{0}:] is non empty set

bool [:[: the carrier of S,{0}:],{0}:] is non empty set

a is V1() V4({0}) V5({0}) Element of bool [:{0},{0}:]

x is non empty right_complementable Abelian add-associative right_zeroed (S)

b is V1() V4([: the carrier of S,{0}:]) V5({0}) V6() V18([: the carrier of S,{0}:],{0}) Element of bool [:[: the carrier of S,{0}:],{0}:]

(S,{0},md,o,b,a) is non empty (S) (S)

the carrier of x is non empty set

0. x is V51(x) Element of the carrier of x

the ZeroF of x is Element of the carrier of x

y is Element of the carrier of x

y is Element of the carrier of x

z is Element of the carrier of x

[y,z] is Element of [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty set

{y,z} is non empty set

{y} is non empty set

{{y,z},{y}} is non empty set

0F is Element of {0}

p is Element of {0}

[0F,p] is Element of [:{0},{0}:]

{0F,p} is non empty set

{0F} is non empty set

{{0F,p},{0F}} is non empty set

y is Element of the carrier of x

z is Element of the carrier of x

0F is Element of the carrier of x

p is Element of the carrier of x

[y,z] is Element of [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty set

{y,z} is non empty set

{y} is non empty set

{{y,z},{y}} is non empty set

[0F,p] is Element of [: the carrier of x, the carrier of x:]

{0F,p} is non empty set

{0F} is non empty set

{{0F,p},{0F}} is non empty set

[y,z] is Element of [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty set

{y,z} is non empty set

{y} is non empty set

{{y,z},{y}} is non empty set

0F is Element of {0}

p is Element of {0}

[0F,p] is Element of [:{0},{0}:]

{0F,p} is non empty set

{0F} is non empty set

{{0F,p},{0F}} is non empty set

y is Element of the carrier of x

z is Element of the carrier of x

0F is Element of the carrier of S

0F * y is Element of the carrier of x

z is Element of the carrier of x

y is Element of the carrier of x

0F is Element of the carrier of x

z + 0F is Element of the carrier of x

the addF of x is V1() V4([: the carrier of x, the carrier of x:]) V5( the carrier of x) V6() V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty set

[:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set

bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set

the addF of x . (z,0F) is Element of the carrier of x

z is Element of the carrier of x

y is Element of the carrier of x

0F is Element of the carrier of x

y is Element of the carrier of x

z is Element of the carrier of x

0F is Element of the carrier of x

z + 0F is Element of the carrier of x

the addF of x is V1() V4([: the carrier of x, the carrier of x:]) V5( the carrier of x) V6() V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty set

[:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set

bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set

the addF of x . (z,0F) is Element of the carrier of x

0F + y is Element of the carrier of x

the addF of x . (0F,y) is Element of the carrier of x

y + z is Element of the carrier of x

the addF of x . (y,z) is Element of the carrier of x

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

the carrier of F is non empty non trivial set

[: the carrier of F,{0}:] is non empty set

[:[: the carrier of F,{0}:],{0}:] is non empty set

bool [:[: the carrier of F,{0}:],{0}:] is non empty set

S is V1() V4([: the carrier of F,{0}:]) V5({0}) V6() V18([: the carrier of F,{0}:],{0}) Element of bool [:[: the carrier of F,{0}:],{0}:]

b is V1() V4({0}) V5({0}) Element of bool [:{0},{0}:]

(F,{0},md,o,S,b) is non empty (F) (F)

a is non empty right_complementable Abelian add-associative right_zeroed (F)

the carrier of a is non empty set

0. a is V51(a) Element of the carrier of a

the ZeroF of a is Element of the carrier of a

x is Element of the carrier of a

y is Element of the carrier of a

z is Element of the carrier of a

0F is Element of the carrier of F

0F * y is Element of the carrier of a

r is Element of the carrier of a

p is Element of the carrier of a

v is Element of the carrier of a

r + v is Element of the carrier of a

the addF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) V6() V18([: the carrier of a, the carrier of a:], the carrier of a) Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]

[: the carrier of a, the carrier of a:] is non empty set

[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

the addF of a . (r,v) is Element of the carrier of a

v is Element of the carrier of a

v is Element of the carrier of a

v is Element of the carrier of a

v is Element of the carrier of a

c

c

c

the addF of a . (c

c

the addF of a . (c

v + c

the addF of a . (v,c

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)

the carrier of S is non empty set

0. S is V51(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

b is Element of the carrier of S

0. F is V51(F) Element of the carrier of F

the carrier of F is non empty non trivial set

the ZeroF of F is Element of the carrier of F

y is Element of the carrier of F

y * b is Element of the carrier of S

(0. S) - (y * b) is Element of the carrier of S

- (y * b) is Element of the carrier of S

(0. S) + (- (y * b)) is Element of the carrier of S

the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

the addF of S . ((0. S),(- (y * b))) is Element of the carrier of S

(0. F) * ((0. S) - (y * b)) is Element of the carrier of S

(0. F) * b is Element of the carrier of S

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)

the carrier of S is non empty set

b is Element of the carrier of S

a is Element of the carrier of S

0. S is V51(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

(0. S) + a is Element of the carrier of S

the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

the addF of S . ((0. S),a) is Element of the carrier of S

a + b is Element of the carrier of S

the addF of S . (a,b) is Element of the carrier of S

b + (0. S) is Element of the carrier of S

the addF of S . (b,(0. S)) is Element of the carrier of S

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)

the carrier of S is non empty set

b is Element of the carrier of S

a is Element of the carrier of S

x is Element of the carrier of S

x + b is Element of the carrier of S

the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

the addF of S . (x,b) is Element of the carrier of S

1_ F is Element of the carrier of F

the carrier of F is non empty non trivial set

1. F is V51(F) Element of the carrier of F

the OneF of F is Element of the carrier of F

- (1_ F) is Element of the carrier of F

(- (1_ F)) * x is Element of the carrier of S

- x is Element of the carrier of S

(- x) + (x + b) is Element of the carrier of S

the addF of S . ((- x),(x + b)) is Element of the carrier of S

x + (- x) is Element of the carrier of S

the addF of S . (x,(- x)) is Element of the carrier of S

(x + (- x)) + b is Element of the carrier of S

the addF of S . ((x + (- x)),b) is Element of the carrier of S

0. S is V51(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

(0. S) + b is Element of the carrier of S

the addF of S . ((0. S),b) is Element of the carrier of S

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)

the carrier of S is non empty set

b is Element of the carrier of S

a is Element of the carrier of S

x is Element of the carrier of S

b + x is Element of the carrier of S

the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

the addF of S . (b,x) is Element of the carrier of S

1_ F is Element of the carrier of F

the carrier of F is non empty non trivial set

1. F is V51(F) Element of the carrier of F

the OneF of F is Element of the carrier of F

- (1_ F) is Element of the carrier of F

(- (1_ F)) * x is Element of the carrier of S

- x is Element of the carrier of S

(b + x) + (- x) is Element of the carrier of S

the addF of S . ((b + x),(- x)) is Element of the carrier of S

x + (- x) is Element of the carrier of S

the addF of S . (x,(- x)) is Element of the carrier of S

b + (x + (- x)) is Element of the carrier of S

the addF of S . (b,(x + (- x))) is Element of the carrier of S

0. S is V51(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

b + (0. S) is Element of the carrier of S

the addF of S . (b,(0. S)) is Element of the carrier of S

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

the carrier of F is non empty non trivial set

0. F is V51(F) Element of the carrier of F

the ZeroF of F is Element of the carrier of F

S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)

the carrier of S is non empty set

b is Element of the carrier of S

a is Element of the carrier of S

x is Element of the carrier of F

x * b is Element of the carrier of S

x * a is Element of the carrier of S

1. F is V51(F) Element of the carrier of F

the OneF of F is Element of the carrier of F

z is Element of the carrier of F

z * x is Element of the carrier of F

the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]

[: the carrier of F, the carrier of F:] is non empty set

[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set

bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set

the multF of F . (z,x) is Element of the carrier of F

z * (x * a) is Element of the carrier of S

(1. F) * a is Element of the carrier of S

z is Element of the carrier of F

z * x is Element of the carrier of F

the multF of F . (z,x) is Element of the carrier of F

z * (x * b) is Element of the carrier of S

(1. F) * b is Element of the carrier of S

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)

the carrier of S is non empty set

b is Element of the carrier of S

- b is Element of the carrier of S

a is Element of the carrier of S

1_ F is Element of the carrier of F

the carrier of F is non empty non trivial set

1. F is V51(F) Element of the carrier of F

the OneF of F is Element of the carrier of F

- (1_ F) is Element of the carrier of F

(- (1_ F)) * b is Element of the carrier of S

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

1_ F is Element of the carrier of F

the carrier of F is non empty non trivial set

1. F is V51(F) Element of the carrier of F

the OneF of F is Element of the carrier of F

(1_ F) + (1_ F) is Element of the carrier of F

the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]

[: the carrier of F, the carrier of F:] is non empty set

[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set

bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set

the addF of F . ((1_ F),(1_ F)) is Element of the carrier of F

S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)

the carrier of S is non empty set

b is Element of the carrier of S

((1_ F) + (1_ F)) * b is Element of the carrier of S

a is Element of the carrier of S

x is Element of the carrier of S

b + x is Element of the carrier of S

the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

the addF of S . (b,x) is Element of the carrier of S

(((1_ F) + (1_ F)) * b) + x is Element of the carrier of S

the addF of S . ((((1_ F) + (1_ F)) * b),x) is Element of the carrier of S

(1_ F) * b is Element of the carrier of S

((1_ F) * b) + ((1_ F) * b) is Element of the carrier of S

the addF of S . (((1_ F) * b),((1_ F) * b)) is Element of the carrier of S

(((1_ F) * b) + ((1_ F) * b)) + x is Element of the carrier of S

the addF of S . ((((1_ F) * b) + ((1_ F) * b)),x) is Element of the carrier of S

b + ((1_ F) * b) is Element of the carrier of S

the addF of S . (b,((1_ F) * b)) is Element of the carrier of S

(b + ((1_ F) * b)) + x is Element of the carrier of S

the addF of S . ((b + ((1_ F) * b)),x) is Element of the carrier of S

b + b is Element of the carrier of S

the addF of S . (b,b) is Element of the carrier of S

(b + b) + x is Element of the carrier of S

the addF of S . ((b + b),x) is Element of the carrier of S

b + (b + x) is Element of the carrier of S

the addF of S . (b,(b + x)) is Element of the carrier of S

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)

the carrier of S is non empty set

b is Element of the carrier of S

a is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

b + y is Element of the carrier of S

the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

the addF of S . (b,y) is Element of the carrier of S

0. S is V51(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

1_ F is Element of the carrier of F

the carrier of F is non empty non trivial set

1. F is V51(F) Element of the carrier of F

the OneF of F is Element of the carrier of F

- (1_ F) is Element of the carrier of F

(- (1_ F)) * y is Element of the carrier of S

(- (1_ F)) * b is Element of the carrier of S

- y is Element of the carrier of S

- b is Element of the carrier of S

(b + y) + (- y) is Element of the carrier of S

the addF of S . ((b + y),(- y)) is Element of the carrier of S

(- b) + (b + y) is Element of the carrier of S

the addF of S . ((- b),(b + y)) is Element of the carrier of S

y + (- y) is Element of the carrier of S

the addF of S . (y,(- y)) is Element of the carrier of S

b + (y + (- y)) is Element of the carrier of S

the addF of S . (b,(y + (- y))) is Element of the carrier of S

(- b) + b is Element of the carrier of S

the addF of S . ((- b),b) is Element of the carrier of S

((- b) + b) + y is Element of the carrier of S

the addF of S . (((- b) + b),y) is Element of the carrier of S

b + (0. S) is Element of the carrier of S

the addF of S . (b,(0. S)) is Element of the carrier of S

(0. S) + y is Element of the carrier of S

the addF of S . ((0. S),y) is Element of the carrier of S

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)

the carrier of S is non empty set

0. S is V51(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

b is Element of the carrier of S

a is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

x + y is Element of the carrier of S

the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

the addF of S . (x,y) is Element of the carrier of S

z is Element of the carrier of S

y is Element of the carrier of S

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

1_ F is Element of the carrier of F

the carrier of F is non empty non trivial set

1. F is V51(F) Element of the carrier of F

the OneF of F is Element of the carrier of F

(1_ F) + (1_ F) is Element of the carrier of F

the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]

[: the carrier of F, the carrier of F:] is non empty set

[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set

bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set

the addF of F . ((1_ F),(1_ F)) is Element of the carrier of F

0. F is V51(F) Element of the carrier of F

the ZeroF of F is Element of the carrier of F

S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)

the carrier of S is non empty set

0. S is V51(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

b is Element of the carrier of S

a is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

((1_ F) + (1_ F)) * y is Element of the carrier of S

(((1_ F) + (1_ F)) * y) + z is Element of the carrier of S

the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

the addF of S . ((((1_ F) + (1_ F)) * y),z) is Element of the carrier of S

y + z is Element of the carrier of S

the addF of S . (y,z) is Element of the carrier of S

0F is Element of the carrier of S

p is Element of the carrier of S

0F is Element of the carrier of S

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)

the carrier of S is non empty set

b is Element of the carrier of S

a is Element of the carrier of S

b - a is Element of the carrier of S

- a is Element of the carrier of S

b + (- a) is Element of the carrier of S

the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

the addF of S . (b,(- a)) is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

b - y is Element of the carrier of S

- y is Element of the carrier of S

b + (- y) is Element of the carrier of S

the addF of S . (b,(- y)) is Element of the carrier of S

a - y is Element of the carrier of S

a + (- y) is Element of the carrier of S

the addF of S . (a,(- y)) is Element of the carrier of S

- (b - a) is Element of the carrier of S

- b is Element of the carrier of S

(- b) + a is Element of the carrier of S

the addF of S . ((- b),a) is Element of the carrier of S

a + (- b) is Element of the carrier of S

the addF of S . (a,(- b)) is Element of the carrier of S

(a + (- b)) + (b - y) is Element of the carrier of S

the addF of S . ((a + (- b)),(b - y)) is Element of the carrier of S

(- b) + (b - y) is Element of the carrier of S

the addF of S . ((- b),(b - y)) is Element of the carrier of S

a + ((- b) + (b - y)) is Element of the carrier of S

the addF of S . (a,((- b) + (b - y))) is Element of the carrier of S

(- b) + b is Element of the carrier of S

the addF of S . ((- b),b) is Element of the carrier of S

((- b) + b) + (- y) is Element of the carrier of S

the addF of S . (((- b) + b),(- y)) is Element of the carrier of S

a + (((- b) + b) + (- y)) is Element of the carrier of S

the addF of S . (a,(((- b) + b) + (- y))) is Element of the carrier of S

0. S is V51(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

(0. S) + (- y) is Element of the carrier of S

the addF of S . ((0. S),(- y)) is Element of the carrier of S

a + ((0. S) + (- y)) is Element of the carrier of S

the addF of S . (a,((0. S) + (- y))) is Element of the carrier of S

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

the carrier of F is non empty non trivial set

S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)

the carrier of S is non empty set

b is Element of the carrier of S

a is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of F

y * b is Element of the carrier of S

x - (y * b) is Element of the carrier of S

- (y * b) is Element of the carrier of S

x + (- (y * b)) is Element of the carrier of S

the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

the addF of S . (x,(- (y * b))) is Element of the carrier of S

z is Element of the carrier of F

z * b is Element of the carrier of S

x - (z * b) is Element of the carrier of S

- (z * b) is Element of the carrier of S

x + (- (z * b)) is Element of the carrier of S

the addF of S . (x,(- (z * b))) is Element of the carrier of S

1_ F is Element of the carrier of F

1. F is V51(F) Element of the carrier of F

the OneF of F is Element of the carrier of F

(y * b) - (z * b) is Element of the carrier of S

(y * b) + (- (z * b)) is Element of the carrier of S

the addF of S . ((y * b),(- (z * b))) is Element of the carrier of S

- (1_ F) is Element of the carrier of F

(- (1_ F)) * (z * b) is Element of the carrier of S

(y * b) + ((- (1_ F)) * (z * b)) is Element of the carrier of S

the addF of S . ((y * b),((- (1_ F)) * (z * b))) is Element of the carrier of S

(- (1_ F)) * z is Element of the carrier of F

the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]

[: the carrier of F, the carrier of F:] is non empty set

[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set

bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set

the multF of F . ((- (1_ F)),z) is Element of the carrier of F

((- (1_ F)) * z) * b is Element of the carrier of S

(y * b) + (((- (1_ F)) * z) * b) is Element of the carrier of S

the addF of S . ((y * b),(((- (1_ F)) * z) * b)) is Element of the carrier of S

z * (1_ F) is Element of the carrier of F

the multF of F . (z,(1_ F)) is Element of the carrier of F

- (z * (1_ F)) is Element of the carrier of F

(- (z * (1_ F))) * b is Element of the carrier of S

(y * b) + ((- (z * (1_ F))) * b) is Element of the carrier of S

the addF of S . ((y * b),((- (z * (1_ F))) * b)) is Element of the carrier of S

- z is Element of the carrier of F

(- z) * b is Element of the carrier of S

(y * b) + ((- z) * b) is Element of the carrier of S

the addF of S . ((y * b),((- z) * b)) is Element of the carrier of S

y + (- z) is Element of the carrier of F

the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]

the addF of F . (y,(- z)) is Element of the carrier of F

(y + (- z)) * b is Element of the carrier of S

(y + (- z)) " is Element of the carrier of F

((y + (- z)) ") * ((y + (- z)) * b) is Element of the carrier of S

((y + (- z)) ") * (y + (- z)) is Element of the carrier of F

the multF of F . (((y + (- z)) "),(y + (- z))) is Element of the carrier of F

(((y + (- z)) ") * (y + (- z))) * b is Element of the carrier of S

y - z is Element of the carrier of F

y + (- z) is Element of the carrier of F

0. F is V51(F) Element of the carrier of F

the ZeroF of F is Element of the carrier of F

(1_ F) * b is Element of the carrier of S

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

1_ F is Element of the carrier of F

the carrier of F is non empty non trivial set

1. F is V51(F) Element of the carrier of F

the OneF of F is Element of the carrier of F

(1_ F) + (1_ F) is Element of the carrier of F

the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]

[: the carrier of F, the carrier of F:] is non empty set

[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set

bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set

the addF of F . ((1_ F),(1_ F)) is Element of the carrier of F

0. F is V51(F) Element of the carrier of F

the ZeroF of F is Element of the carrier of F

S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)

the carrier of S is non empty set

b is Element of the carrier of S

0. S is V51(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of F

y * x is Element of the carrier of S

b - (y * x) is Element of the carrier of S

- (y * x) is Element of the carrier of S

b + (- (y * x)) is Element of the carrier of S

the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

the addF of S . (b,(- (y * x))) is Element of the carrier of S

b + (- (y * x)) is Element of the carrier of S

b + b is Element of the carrier of S

the addF of S . (b,b) is Element of the carrier of S

(1_ F) * b is Element of the carrier of S

b + ((1_ F) * b) is Element of the carrier of S

the addF of S . (b,((1_ F) * b)) is Element of the carrier of S

((1_ F) * b) + ((1_ F) * b) is Element of the carrier of S

the addF of S . (((1_ F) * b),((1_ F) * b)) is Element of the carrier of S

- (1_ F) is Element of the carrier of F

(- (1_ F)) * (y * x) is Element of the carrier of S

((1_ F) + (1_ F)) * b is Element of the carrier of S

(- (1_ F)) * y is Element of the carrier of F

the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]

the multF of F . ((- (1_ F)),y) is Element of the carrier of F

((- (1_ F)) * y) * x is Element of the carrier of S

y * (1_ F) is Element of the carrier of F

the multF of F . (y,(1_ F)) is Element of the carrier of F

- (y * (1_ F)) is Element of the carrier of F

(- (y * (1_ F))) * x is Element of the carrier of S

- y is Element of the carrier of F

(- y) * x is Element of the carrier of S

((1_ F) + (1_ F)) " is Element of the carrier of F

(((1_ F) + (1_ F)) ") * (((1_ F) + (1_ F)) * b) is Element of the carrier of S

b + ((- y) * x) is Element of the carrier of S

the addF of S . (b,((- y) * x)) is Element of the carrier of S

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)

the carrier of S is non empty set

a is Element of the carrier of S

b is Element of the carrier of S

the carrier of F is non empty non trivial set

x is Element of the carrier of S

y is Element of the carrier of F

y * a is Element of the carrier of S

x - (y * a) is Element of the carrier of S

- (y * a) is Element of the carrier of S

x + (- (y * a)) is Element of the carrier of S

the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

the addF of S . (x,(- (y * a))) is Element of the carrier of S

z is Element of the carrier of F

z * a is Element of the carrier of S

x - (z * a) is Element of the carrier of S

- (z * a) is Element of the carrier of S

x + (- (z * a)) is Element of the carrier of S

the addF of S . (x,(- (z * a))) is Element of the carrier of S

y is Element of the carrier of F

z is Element of the carrier of F

0F is Element of the carrier of F

0F * a is Element of the carrier of S

x - (0F * a) is Element of the carrier of S

- (0F * a) is Element of the carrier of S

x + (- (0F * a)) is Element of the carrier of S

the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

the addF of S . (x,(- (0F * a))) is Element of the carrier of S

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)

the carrier of S is non empty set

b is Element of the carrier of S

a is Element of the carrier of S

x is Element of the carrier of S

(F,S,a,b,x) is Element of the carrier of F

the carrier of F is non empty non trivial set

(F,S,a,b,x) * b is Element of the carrier of S

x - ((F,S,a,b,x) * b) is Element of the carrier of S

- ((F,S,a,b,x) * b) is Element of the carrier of S

x + (- ((F,S,a,b,x) * b)) is Element of the carrier of S

the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

the addF of S . (x,(- ((F,S,a,b,x) * b))) is Element of the carrier of S

y is Element of the carrier of F

y * b is Element of the carrier of S

x - (y * b) is Element of the carrier of S

- (y * b) is Element of the carrier of S

x + (- (y * b)) is Element of the carrier of S

the addF of S . (x,(- (y * b))) is Element of the carrier of S

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

the carrier of F is non empty non trivial set

S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)

the carrier of S is non empty set

b is Element of the carrier of S

a is Element of the carrier of S

x is Element of the carrier of S

(F,S,a,b,x) is Element of the carrier of F

y is Element of the carrier of F

y * x is Element of the carrier of S

(F,S,a,b,(y * x)) is Element of the carrier of F

y * (F,S,a,b,x) is Element of the carrier of F

the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]

[: the carrier of F, the carrier of F:] is non empty set

[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set

bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set

the multF of F . (y,(F,S,a,b,x)) is Element of the carrier of F

(F,S,a,b,x) * b is Element of the carrier of S

x - ((F,S,a,b,x) * b) is Element of the carrier of S

- ((F,S,a,b,x) * b) is Element of the carrier of S

x + (- ((F,S,a,b,x) * b)) is Element of the carrier of S

the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

the addF of S . (x,(- ((F,S,a,b,x) * b))) is Element of the carrier of S

y * (x - ((F,S,a,b,x) * b)) is Element of the carrier of S

y * ((F,S,a,b,x) * b) is Element of the carrier of S

(y * x) - (y * ((F,S,a,b,x) * b)) is Element of the carrier of S

- (y * ((F,S,a,b,x) * b)) is Element of the carrier of S

(y * x) + (- (y * ((F,S,a,b,x) * b))) is Element of the carrier of S

the addF of S . ((y * x),(- (y * ((F,S,a,b,x) * b)))) is Element of the carrier of S

(y * (F,S,a,b,x)) * b is Element of the carrier of S

(y * x) - ((y * (F,S,a,b,x)) * b) is Element of the carrier of S

- ((y * (F,S,a,b,x)) * b) is Element of the carrier of S

(y * x) + (- ((y * (F,S,a,b,x)) * b)) is Element of the carrier of S

the addF of S . ((y * x),(- ((y * (F,S,a,b,x)) * b))) is Element of the carrier of S

(F,S,a,b,(y * x)) * b is Element of the carrier of S

(y * x) - ((F,S,a,b,(y * x)) * b) is Element of the carrier of S

- ((F,S,a,b,(y * x)) * b) is Element of the carrier of S

(y * x) + (- ((F,S,a,b,(y * x)) * b)) is Element of the carrier of S

the addF of S . ((y * x),(- ((F,S,a,b,(y * x)) * b))) is Element of the carrier of S

F is non empty non degenerated non trivial right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital V114() left_unital doubleLoopStr

S is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital (F) (F)

the carrier of S is non empty set

b is Element of the carrier of S

a is Element of the carrier of S

x is Element of the carrier of S

(F,S,a,b,x) is Element of the carrier of F

the carrier of F is non empty non trivial set

y is Element of the carrier of S

x + y is Element of the carrier of S

the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) V6() V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

the addF of S . (x,y) is Element of the carrier of S

(F,S,a,b,(x + y)) is Element of the carrier of F

(F,S,a,b,y) is Element of the carrier of F

(F,S,a,b,x) + (F,S,a,b,y) is Element of the carrier of F

the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) V6() V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]

[: the carrier of F, the carrier of F:] is non empty set

[:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set

bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is non empty set

the addF of F . ((F,S,a,b,x),(F,S,a,b,y)) is Element of the carrier of F

1_ F is Element of the carrier of F

1. F is V51(F) Element of the carrier of F

the OneF of F is Element of the carrier of F

(F,S,a,b,x) * b is Element of the carrier of S

x - ((F,S,a,b,x) * b) is Element of the carrier of S

- ((F,S,a,b,x) * b) is Element of the carrier of S

x + (- ((F,S,a,b,x) * b)) is Element of the carrier of S

the addF of S . (x,(- ((F,S,a,b,x) * b))) is Element of the carrier of S

(F,S,a,b,y) * b is Element of the carrier of S

y - ((F,S,a,b,y) * b) is Element of the carrier of S

- ((F,S,a,b,y) *