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

1 is non empty set

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

o is (X)
the carrier of o is set
0 is empty Element of K122()
is non empty set
o is Element of
is non empty set
is non empty set
bool is non empty set
md is V1() V4() V5() V6() V18(,) Element of bool
b is set
a is set
bool is non empty set
a is V1() V4() V5() Element of bool
x is V1() V4() V5() Element of bool
y is set
z is set
0F is Element of
p is Element of
[0F,p] is Element of
{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

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)

the carrier of F is non empty non trivial set
[: the carrier of F,:] is non empty set
[:[: the carrier of F,:],:] is non empty set
bool [:[: the carrier of F,:],:] is non empty set
S is V1() V4([: the carrier of F,:]) V5() V6() V18([: the carrier of F,:],) Element of bool [:[: the carrier of F,:],:]
b is V1() V4() V5() Element of bool
(F,,md,o,S,b) is non empty (F) (F)
the carrier of (F,,md,o,S,b) is non empty set
x is Element of the carrier of (F,,md,o,S,b)
y is Element of the carrier of (F,,md,o,S,b)
x + y is Element of the carrier of (F,,md,o,S,b)
the addF of (F,,md,o,S,b) is V1() V4([: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):]) V5( the carrier of (F,,md,o,S,b)) V6() V18([: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):], the carrier of (F,,md,o,S,b)) Element of bool [:[: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):], the carrier of (F,,md,o,S,b):]
[: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):] is non empty set
[:[: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):], the carrier of (F,,md,o,S,b):] is non empty set
bool [:[: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):], the carrier of (F,,md,o,S,b):] is non empty set
the addF of (F,,md,o,S,b) . (x,y) is Element of the carrier of (F,,md,o,S,b)
y + x is Element of the carrier of (F,,md,o,S,b)
the addF of (F,,md,o,S,b) . (y,x) is Element of the carrier of (F,,md,o,S,b)
z is Element of
0F is Element of
md . (z,0F) is Element of
the carrier of (F,,md,o,S,b) is non empty set
x is Element of the carrier of (F,,md,o,S,b)
y is Element of the carrier of (F,,md,o,S,b)
x + y is Element of the carrier of (F,,md,o,S,b)
the addF of (F,,md,o,S,b) is V1() V4([: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):]) V5( the carrier of (F,,md,o,S,b)) V6() V18([: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):], the carrier of (F,,md,o,S,b)) Element of bool [:[: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):], the carrier of (F,,md,o,S,b):]
[: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):] is non empty set
[:[: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):], the carrier of (F,,md,o,S,b):] is non empty set
bool [:[: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):], the carrier of (F,,md,o,S,b):] is non empty set
the addF of (F,,md,o,S,b) . (x,y) is Element of the carrier of (F,,md,o,S,b)
z is Element of the carrier of (F,,md,o,S,b)
(x + y) + z is Element of the carrier of (F,,md,o,S,b)
the addF of (F,,md,o,S,b) . ((x + y),z) is Element of the carrier of (F,,md,o,S,b)
y + z is Element of the carrier of (F,,md,o,S,b)
the addF of (F,,md,o,S,b) . (y,z) is Element of the carrier of (F,,md,o,S,b)
x + (y + z) is Element of the carrier of (F,,md,o,S,b)
the addF of (F,,md,o,S,b) . (x,(y + z)) is Element of the carrier of (F,,md,o,S,b)
0F is Element of
p is Element of
r is Element of
md . (p,r) is Element of
md . (0F,(md . (p,r))) is Element of
the carrier of (F,,md,o,S,b) is non empty set
x is Element of the carrier of (F,,md,o,S,b)
0. (F,,md,o,S,b) is V51((F,,md,o,S,b)) Element of the carrier of (F,,md,o,S,b)
the ZeroF of (F,,md,o,S,b) is Element of the carrier of (F,,md,o,S,b)
x + (0. (F,,md,o,S,b)) is Element of the carrier of (F,,md,o,S,b)
the addF of (F,,md,o,S,b) is V1() V4([: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):]) V5( the carrier of (F,,md,o,S,b)) V6() V18([: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):], the carrier of (F,,md,o,S,b)) Element of bool [:[: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):], the carrier of (F,,md,o,S,b):]
[: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):] is non empty set
[:[: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):], the carrier of (F,,md,o,S,b):] is non empty set
bool [:[: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):], the carrier of (F,,md,o,S,b):] is non empty set
the addF of (F,,md,o,S,b) . (x,(0. (F,,md,o,S,b))) is Element of the carrier of (F,,md,o,S,b)
y is Element of
md . (y,(0. (F,,md,o,S,b))) is set
the carrier of (F,,md,o,S,b) is non empty set
x is Element of the carrier of (F,,md,o,S,b)
- x is Element of the carrier of (F,,md,o,S,b)
x + (- x) is Element of the carrier of (F,,md,o,S,b)
the addF of (F,,md,o,S,b) is V1() V4([: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):]) V5( the carrier of (F,,md,o,S,b)) V6() V18([: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):], the carrier of (F,,md,o,S,b)) Element of bool [:[: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):], the carrier of (F,,md,o,S,b):]
[: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):] is non empty set
[:[: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):], the carrier of (F,,md,o,S,b):] is non empty set
bool [:[: the carrier of (F,,md,o,S,b), the carrier of (F,,md,o,S,b):], the carrier of (F,,md,o,S,b):] is non empty set
the addF of (F,,md,o,S,b) . (x,(- x)) is Element of the carrier of (F,,md,o,S,b)
0. (F,,md,o,S,b) is V51((F,,md,o,S,b)) Element of the carrier of (F,,md,o,S,b)
the ZeroF of (F,,md,o,S,b) is Element of the carrier of (F,,md,o,S,b)

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

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

b is V1() V4() V5() Element of bool
(F,,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
p is Element of
r is Element of
md . (p,r) is Element of
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
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

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

b is V1() V4([: the carrier of S,:]) V5() V6() V18([: the carrier of S,:],) Element of bool [:[: the carrier of S,:],:]
(S,,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
p is Element of
[0F,p] is Element of
{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
p is Element of
[0F,p] is Element of
{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

the carrier of F is non empty non trivial set
[: the carrier of F,:] is non empty set
[:[: the carrier of F,:],:] is non empty set
bool [:[: the carrier of F,:],:] is non empty set
S is V1() V4([: the carrier of F,:]) V5() V6() V18([: the carrier of F,:],) Element of bool [:[: the carrier of F,:],:]
b is V1() V4() V5() Element of bool
(F,,md,o,S,b) is non empty (F) (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
c19 is Element of the carrier of a
c20 is Element of the carrier of a
c19 + c20 is Element of the carrier of a
the addF of a . (c19,c20) is Element of the carrier of a
c20 + v is Element of the carrier of a
the addF of a . (c20,v) is Element of the carrier of a
v + c19 is Element of the carrier of a
the addF of a . (v,c19) is Element of the carrier of a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

the carrier of F is non empty non trivial set

the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
y is Element of the carrier of F
y * b is Element of the carrier of S
x - (y * b) is Element of the carrier of S
- (y * b) is Element of the carrier of S
x + (- (y * b)) is Element of the carrier of S
the addF of S is V1() V4([: the carrier of S, the carrier of S:]) V5( the carrier of S) 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

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

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

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

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

the carrier of F is non empty non trivial set

the carrier of S is non empty set
b is Element of the carrier of S
a is Element of the carrier of S
x is Element of the carrier of S
(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

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