:: MIDSP_2 semantic presentation

K122() is Element of bool K118()

K118() is set

bool K118() is set

K117() is set

bool K117() is set

bool K122() is set

{} is empty set

1 is non empty set

M is non empty addLoopStr

the carrier of M is non empty set

W is Element of the carrier of M

W + W is Element of the carrier of M

M is non empty MidStr

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is set

W is non empty addLoopStr

the carrier of W is non empty set

[:[: the carrier of M, the carrier of M:], the carrier of W:] is set

bool [:[: the carrier of M, the carrier of M:], the carrier of W:] is set

M is non empty addLoopStr

the carrier of M is non empty set

W is non empty MidStr

the carrier of W is non empty set

[: the carrier of W, the carrier of W:] is set

[:[: the carrier of W, the carrier of W:], the carrier of M:] is set

bool [:[: the carrier of W, the carrier of W:], the carrier of M:] is set

a is Element of the carrier of W

a @ a is Element of the carrier of W

b is V1() V4([: the carrier of W, the carrier of W:]) V5( the carrier of M) V6() V18([: the carrier of W, the carrier of W:], the carrier of M) Element of bool [:[: the carrier of W, the carrier of W:], the carrier of M:]

b . (a,a) is Element of the carrier of M

M is non empty set

[:M,M:] is set

W is non empty addLoopStr

the carrier of W is non empty set

[:[:M,M:], the carrier of W:] is set

bool [:[:M,M:], the carrier of W:] is set

M is non empty set

[:M,M:] is set

W is non empty addLoopStr

the carrier of W is non empty set

[:[:M,M:], the carrier of W:] is set

bool [:[:M,M:], the carrier of W:] is set

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

b is Element of M

c is Element of the carrier of W

d is Element of M

a . (b,d) is Element of the carrier of W

x is Element of M

a . (b,x) is Element of the carrier of W

M is non empty set

[:M,M:] is set

W is Element of M

a is non empty right_complementable add-associative right_zeroed addLoopStr

the carrier of a is non empty set

[:[:M,M:], the carrier of a:] is set

bool [:[:M,M:], the carrier of a:] is set

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

the ZeroF of a is Element of the carrier of a

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

b . (W,W) is Element of the carrier of a

(b . (W,W)) + (b . (W,W)) is Element of the carrier of a

M is non empty set

[:M,M:] is set

W is Element of M

a is Element of M

b is non empty right_complementable add-associative right_zeroed addLoopStr

the carrier of b is non empty set

[:[:M,M:], the carrier of b:] is set

bool [:[:M,M:], the carrier of b:] is set

0. b is V49(b) Element of the carrier of b

the ZeroF of b is Element of the carrier of b

c is V1() V4([:M,M:]) V5( the carrier of b) V6() V18([:M,M:], the carrier of b) Element of bool [:[:M,M:], the carrier of b:]

c . (W,a) is Element of the carrier of b

c . (W,W) is Element of the carrier of b

M is non empty set

[:M,M:] is set

W is Element of M

a is Element of M

b is non empty right_complementable add-associative right_zeroed addLoopStr

the carrier of b is non empty set

[:[:M,M:], the carrier of b:] is set

bool [:[:M,M:], the carrier of b:] is set

c is V1() V4([:M,M:]) V5( the carrier of b) V6() V18([:M,M:], the carrier of b) Element of bool [:[:M,M:], the carrier of b:]

c . (W,a) is Element of the carrier of b

c . (a,W) is Element of the carrier of b

- (c . (a,W)) is Element of the carrier of b

(c . (a,W)) + (c . (W,a)) is Element of the carrier of b

c . (a,a) is Element of the carrier of b

0. b is V49(b) Element of the carrier of b

the ZeroF of b is Element of the carrier of b

- (c . (W,a)) is Element of the carrier of b

- (- (c . (W,a))) is Element of the carrier of b

M is non empty set

[:M,M:] is set

W is Element of M

a is Element of M

b is Element of M

c is Element of M

d is non empty right_complementable add-associative right_zeroed addLoopStr

the carrier of d is non empty set

[:[:M,M:], the carrier of d:] is set

bool [:[:M,M:], the carrier of d:] is set

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

x . (W,a) is Element of the carrier of d

x . (b,c) is Element of the carrier of d

x . (a,W) is Element of the carrier of d

x . (c,b) is Element of the carrier of d

- (x . (b,c)) is Element of the carrier of d

M is non empty set

[:M,M:] is set

W is non empty right_complementable add-associative right_zeroed addLoopStr

the carrier of W is non empty set

[:[:M,M:], the carrier of W:] is set

bool [:[:M,M:], the carrier of W:] is set

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

b is Element of M

c is Element of the carrier of W

- c is Element of the carrier of W

d is Element of M

a . (b,d) is Element of the carrier of W

a . (d,b) is Element of the carrier of W

- (- c) is Element of the carrier of W

M is non empty set

[:M,M:] is set

W is Element of M

a is Element of M

b is Element of M

c is non empty right_complementable add-associative right_zeroed addLoopStr

the carrier of c is non empty set

[:[:M,M:], the carrier of c:] is set

bool [:[:M,M:], the carrier of c:] is set

d is V1() V4([:M,M:]) V5( the carrier of c) V6() V18([:M,M:], the carrier of c) Element of bool [:[:M,M:], the carrier of c:]

d . (W,a) is Element of the carrier of c

d . (b,a) is Element of the carrier of c

d . (a,W) is Element of the carrier of c

d . (a,b) is Element of the carrier of c

M is non empty MidStr

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is set

W is Element of the carrier of M

a is Element of the carrier of M

W @ a is Element of the carrier of M

a @ W is Element of the carrier of M

b is non empty right_complementable add-associative right_zeroed addLoopStr

the carrier of b is non empty set

[:[: the carrier of M, the carrier of M:], the carrier of b:] is set

bool [:[: the carrier of M, the carrier of M:], the carrier of b:] is set

c is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of b) V6() V18([: the carrier of M, the carrier of M:], the carrier of b) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of b:]

c . (W,(W @ a)) is Element of the carrier of b

c . ((W @ a),a) is Element of the carrier of b

c . ((W @ a),W) is Element of the carrier of b

c . (a,(W @ a)) is Element of the carrier of b

M is non empty MidStr

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is set

W is Element of the carrier of M

a is Element of the carrier of M

b is non empty right_complementable add-associative right_zeroed addLoopStr

the carrier of b is non empty set

[:[: the carrier of M, the carrier of M:], the carrier of b:] is set

bool [:[: the carrier of M, the carrier of M:], the carrier of b:] is set

c is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of b) V6() V18([: the carrier of M, the carrier of M:], the carrier of b) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of b:]

c . (a,W) is Element of the carrier of b

d is Element of the carrier of M

c . (d,a) is Element of the carrier of b

d @ W is Element of the carrier of M

M is non empty Abelian add-associative addLoopStr

the carrier of M is non empty set

W is Element of the carrier of M

a is Element of the carrier of M

W + a is Element of the carrier of M

b is Element of the carrier of M

c is Element of the carrier of M

b + c is Element of the carrier of M

(W + a) + (b + c) is Element of the carrier of M

W + b is Element of the carrier of M

a + c is Element of the carrier of M

(W + b) + (a + c) is Element of the carrier of M

a + (b + c) is Element of the carrier of M

W + (a + (b + c)) is Element of the carrier of M

b + (a + c) is Element of the carrier of M

W + (b + (a + c)) is Element of the carrier of M

M is non empty Abelian add-associative addLoopStr

the carrier of M is non empty set

W is Element of the carrier of M

a is Element of the carrier of M

W + a is Element of the carrier of M

(M,(W + a)) is Element of the carrier of M

(W + a) + (W + a) is Element of the carrier of M

(M,W) is Element of the carrier of M

W + W is Element of the carrier of M

(M,a) is Element of the carrier of M

a + a is Element of the carrier of M

(M,W) + (M,a) is Element of the carrier of M

M is non empty right_complementable Abelian add-associative right_zeroed addLoopStr

the carrier of M is non empty set

W is Element of the carrier of M

- W is Element of the carrier of M

(M,(- W)) is Element of the carrier of M

(- W) + (- W) is Element of the carrier of M

(M,W) is Element of the carrier of M

W + W is Element of the carrier of M

- (M,W) is Element of the carrier of M

0. M is V49(M) Element of the carrier of M

the ZeroF of M is Element of the carrier of M

(M,(0. M)) is Element of the carrier of M

(0. M) + (0. M) is Element of the carrier of M

W + (- W) is Element of the carrier of M

(M,(W + (- W))) is Element of the carrier of M

(W + (- W)) + (W + (- W)) is Element of the carrier of M

(M,W) + (M,(- W)) is Element of the carrier of M

M is non empty MidStr

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is set

W is non empty right_complementable Abelian add-associative right_zeroed addLoopStr

the carrier of W is non empty set

[:[: the carrier of M, the carrier of M:], the carrier of W:] is set

bool [:[: the carrier of M, the carrier of M:], the carrier of W:] is set

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

b is Element of the carrier of M

c is Element of the carrier of M

b @ c is Element of the carrier of M

d is Element of the carrier of M

x is Element of the carrier of M

d @ x is Element of the carrier of M

a . (b,x) is Element of the carrier of W

a . (d,c) is Element of the carrier of W

a . (d,(b @ c)) is Element of the carrier of W

a . ((b @ c),x) is Element of the carrier of W

a . (b,(b @ c)) is Element of the carrier of W

a . ((b @ c),c) is Element of the carrier of W

(a . (d,(b @ c))) + (a . ((b @ c),c)) is Element of the carrier of W

a . ((b @ c),c) is Element of the carrier of W

a . ((b @ c),x) is Element of the carrier of W

(a . ((b @ c),c)) + (a . ((b @ c),x)) is Element of the carrier of W

a . (b,(b @ c)) is Element of the carrier of W

(a . (b,(b @ c))) + (a . ((b @ c),x)) is Element of the carrier of W

a . (d,(b @ c)) is Element of the carrier of W

(a . ((b @ c),c)) + (a . (d,(b @ c))) is Element of the carrier of W

M is non empty set

[:M,M:] is set

W is non empty right_complementable Abelian add-associative right_zeroed addLoopStr

the carrier of W is non empty set

[:[:M,M:], the carrier of W:] is set

bool [:[:M,M:], the carrier of W:] is set

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

b is Element of M

c is Element of M

a . (b,c) is Element of the carrier of W

d is Element of M

a . (b,d) is Element of the carrier of W

a . (c,d) is Element of the carrier of W

(W,(a . (c,d))) is Element of the carrier of W

(a . (c,d)) + (a . (c,d)) is Element of the carrier of W

x is Element of M

a . (c,x) is Element of the carrier of W

w is Element of M

a . (d,w) is Element of the carrier of W

a . (x,w) is Element of the carrier of W

a . (x,d) is Element of the carrier of W

(a . (x,d)) + (a . (d,w)) is Element of the carrier of W

a . (x,b) is Element of the carrier of W

(a . (x,b)) + (a . (b,d)) is Element of the carrier of W

((a . (x,b)) + (a . (b,d))) + (a . (d,w)) is Element of the carrier of W

a . (x,c) is Element of the carrier of W

a . (c,b) is Element of the carrier of W

(a . (x,c)) + (a . (c,b)) is Element of the carrier of W

((a . (x,c)) + (a . (c,b))) + (a . (b,d)) is Element of the carrier of W

(((a . (x,c)) + (a . (c,b))) + (a . (b,d))) + (a . (d,w)) is Element of the carrier of W

(W,(a . (c,b))) is Element of the carrier of W

(a . (c,b)) + (a . (c,b)) is Element of the carrier of W

(W,(a . (c,b))) + (a . (b,d)) is Element of the carrier of W

((W,(a . (c,b))) + (a . (b,d))) + (a . (b,d)) is Element of the carrier of W

(W,(a . (b,d))) is Element of the carrier of W

(a . (b,d)) + (a . (b,d)) is Element of the carrier of W

(W,(a . (c,b))) + (W,(a . (b,d))) is Element of the carrier of W

(a . (c,b)) + (a . (b,d)) is Element of the carrier of W

(W,((a . (c,b)) + (a . (b,d)))) is Element of the carrier of W

((a . (c,b)) + (a . (b,d))) + ((a . (c,b)) + (a . (b,d))) is Element of the carrier of W

M is non empty MidSp-like MidStr

vectgroup M is non empty strict addLoopStr

M is non empty MidSp-like MidStr

vectgroup M is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr

the carrier of (vectgroup M) is non empty set

the carrier of M is non empty set

0. (vectgroup M) is V49( vectgroup M) Element of the carrier of (vectgroup M)

the ZeroF of (vectgroup M) is Element of the carrier of (vectgroup M)

ID M is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

a is set

setvect M is non empty set

zerovect M is Element of setvect M

setvect M is non empty set

a is Element of the carrier of (vectgroup M)

b is Element of the carrier of (vectgroup M)

a + b is Element of the carrier of (vectgroup M)

c is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

d is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

c + d is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

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

[: the carrier of (vectgroup M), the carrier of (vectgroup M):] is set

[:[: the carrier of (vectgroup M), the carrier of (vectgroup M):], the carrier of (vectgroup M):] is set

bool [:[: the carrier of (vectgroup M), the carrier of (vectgroup M):], the carrier of (vectgroup M):] is set

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

addvect M is V1() V4([:(setvect M),(setvect M):]) V5( setvect M) V6() V18([:(setvect M),(setvect M):], setvect M) Element of bool [:[:(setvect M),(setvect M):],(setvect M):]

[:(setvect M),(setvect M):] is set

[:[:(setvect M),(setvect M):],(setvect M):] is set

bool [:[:(setvect M),(setvect M):],(setvect M):] is set

x is Element of setvect M

w is Element of setvect M

(addvect M) . (x,w) is Element of setvect M

x + w is Element of setvect M

M is non empty MidSp-like MidStr

vectgroup M is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr

the carrier of (vectgroup M) is non empty set

0. (vectgroup M) is V49( vectgroup M) Element of the carrier of (vectgroup M)

the ZeroF of (vectgroup M) is Element of the carrier of (vectgroup M)

the carrier of M is non empty set

the Element of the carrier of M is Element of the carrier of M

c is Element of the carrier of (vectgroup M)

d is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

x is Element of the carrier of M

vect ( the Element of the carrier of M,x) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

the Element of the carrier of M @ x is Element of the carrier of M

vect ( the Element of the carrier of M,( the Element of the carrier of M @ x)) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

G is Element of the carrier of (vectgroup M)

((vectgroup M),G) is Element of the carrier of (vectgroup M)

G + G is Element of the carrier of (vectgroup M)

(vect ( the Element of the carrier of M,( the Element of the carrier of M @ x))) + (vect ( the Element of the carrier of M,( the Element of the carrier of M @ x))) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

b is Element of the carrier of (vectgroup M)

((vectgroup M),b) is Element of the carrier of (vectgroup M)

b + b is Element of the carrier of (vectgroup M)

c is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

d is Element of the carrier of M

vect ( the Element of the carrier of M,d) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

x is Element of the carrier of M

vect (d,x) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

c + c is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

ID M is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

(vect ( the Element of the carrier of M,d)) + (vect (d,x)) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

vect ( the Element of the carrier of M, the Element of the carrier of M) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

vect ( the Element of the carrier of M,x) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

vect (d, the Element of the carrier of M) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

the Element of the carrier of M @ the Element of the carrier of M is Element of the carrier of M

d @ d is Element of the carrier of M

M is non empty addLoopStr

the carrier of M is non empty set

W is Element of the carrier of M

W + W is Element of the carrier of M

0. M is V49(M) Element of the carrier of M

the ZeroF of M is Element of the carrier of M

(M,W) is Element of the carrier of M

the non empty MidSp-like MidStr is non empty MidSp-like MidStr

vectgroup the non empty MidSp-like MidStr is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr

the carrier of (vectgroup the non empty MidSp-like MidStr ) is non empty set

0. (vectgroup the non empty MidSp-like MidStr ) is V49( vectgroup the non empty MidSp-like MidStr ) Element of the carrier of (vectgroup the non empty MidSp-like MidStr )

the ZeroF of (vectgroup the non empty MidSp-like MidStr ) is Element of the carrier of (vectgroup the non empty MidSp-like MidStr )

a is Element of the carrier of (vectgroup the non empty MidSp-like MidStr )

b is Element of the carrier of (vectgroup the non empty MidSp-like MidStr )

((vectgroup the non empty MidSp-like MidStr ),b) is Element of the carrier of (vectgroup the non empty MidSp-like MidStr )

b + b is Element of the carrier of (vectgroup the non empty MidSp-like MidStr )

M is non empty right_complementable Fanoian add-associative right_zeroed addLoopStr

the carrier of M is non empty set

0. M is V49(M) Element of the carrier of M

the ZeroF of M is Element of the carrier of M

W is Element of the carrier of M

- W is Element of the carrier of M

(- W) + W is Element of the carrier of M

M is non empty right_complementable Fanoian Abelian add-associative right_zeroed addLoopStr

the carrier of M is non empty set

W is Element of the carrier of M

(M,W) is Element of the carrier of M

W + W is Element of the carrier of M

a is Element of the carrier of M

(M,a) is Element of the carrier of M

a + a is Element of the carrier of M

0. M is V49(M) Element of the carrier of M

the ZeroF of M is Element of the carrier of M

W + W is Element of the carrier of M

a + a is Element of the carrier of M

- (a + a) is Element of the carrier of M

(W + W) + (- (a + a)) is Element of the carrier of M

- a is Element of the carrier of M

(- a) + (- a) is Element of the carrier of M

(W + W) + ((- a) + (- a)) is Element of the carrier of M

W + ((- a) + (- a)) is Element of the carrier of M

W + (W + ((- a) + (- a))) is Element of the carrier of M

W + (- a) is Element of the carrier of M

(W + (- a)) + (- a) is Element of the carrier of M

W + ((W + (- a)) + (- a)) is Element of the carrier of M

(W + (- a)) + (W + (- a)) is Element of the carrier of M

(- a) + W is Element of the carrier of M

- (- a) is Element of the carrier of M

M is non empty right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

the carrier of M is non empty set

W is Element of the carrier of M

a is Element of the carrier of M

(M,a) is Element of the carrier of M

a + a is Element of the carrier of M

b is Element of the carrier of M

(M,b) is Element of the carrier of M

b + b is Element of the carrier of M

M is non empty right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

the carrier of M is non empty set

0. M is V49(M) Element of the carrier of M

the ZeroF of M is Element of the carrier of M

(M,(0. M)) is Element of the carrier of M

W is Element of the carrier of M

(M,W) is Element of the carrier of M

(M,W) is Element of the carrier of M

W + W is Element of the carrier of M

(M,(M,W)) is Element of the carrier of M

a is Element of the carrier of M

W + a is Element of the carrier of M

(M,(W + a)) is Element of the carrier of M

(M,a) is Element of the carrier of M

(M,W) + (M,a) is Element of the carrier of M

(M,(0. M)) is Element of the carrier of M

(0. M) + (0. M) is Element of the carrier of M

(M,((M,W) + (M,a))) is Element of the carrier of M

((M,W) + (M,a)) + ((M,W) + (M,a)) is Element of the carrier of M

(M,(M,W)) is Element of the carrier of M

(M,W) + (M,W) is Element of the carrier of M

(M,(M,a)) is Element of the carrier of M

(M,a) + (M,a) is Element of the carrier of M

(M,(M,W)) + (M,(M,a)) is Element of the carrier of M

W + (M,(M,a)) is Element of the carrier of M

M is non empty right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

the carrier of M is non empty set

W is non empty MidStr

the carrier of W is non empty set

[: the carrier of W, the carrier of W:] is set

[:[: the carrier of W, the carrier of W:], the carrier of M:] is set

bool [:[: the carrier of W, the carrier of W:], the carrier of M:] is set

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

b is Element of the carrier of W

c is Element of the carrier of W

b @ c is Element of the carrier of W

d is Element of the carrier of W

x is Element of the carrier of W

d @ x is Element of the carrier of W

(b @ c) @ (d @ x) is Element of the carrier of W

b @ d is Element of the carrier of W

c @ x is Element of the carrier of W

(b @ d) @ (c @ x) is Element of the carrier of W

a . (c,(b @ c)) is Element of the carrier of M

c @ b is Element of the carrier of W

a . (c,(c @ b)) is Element of the carrier of M

a . ((c @ b),b) is Element of the carrier of M

a . ((b @ c),b) is Element of the carrier of M

a . (d,(d @ x)) is Element of the carrier of M

a . ((d @ x),x) is Element of the carrier of M

a . (c,(c @ x)) is Element of the carrier of M

a . ((c @ x),x) is Element of the carrier of M

a . (d,(b @ d)) is Element of the carrier of M

d @ b is Element of the carrier of W

a . (d,(d @ b)) is Element of the carrier of M

a . ((d @ b),b) is Element of the carrier of M

a . ((b @ d),b) is Element of the carrier of M

a . ((b @ d),(d @ x)) is Element of the carrier of M

(M,(a . ((b @ d),(d @ x)))) is Element of the carrier of M

(a . ((b @ d),(d @ x))) + (a . ((b @ d),(d @ x))) is Element of the carrier of M

a . (b,x) is Element of the carrier of M

a . (x,b) is Element of the carrier of M

- (a . (x,b)) is Element of the carrier of M

a . ((c @ x),(b @ c)) is Element of the carrier of M

(M,(a . ((c @ x),(b @ c)))) is Element of the carrier of M

(a . ((c @ x),(b @ c))) + (a . ((c @ x),(b @ c))) is Element of the carrier of M

- (M,(a . ((c @ x),(b @ c)))) is Element of the carrier of M

- (a . ((c @ x),(b @ c))) is Element of the carrier of M

(M,(- (a . ((c @ x),(b @ c))))) is Element of the carrier of M

(- (a . ((c @ x),(b @ c)))) + (- (a . ((c @ x),(b @ c)))) is Element of the carrier of M

a . ((b @ c),(c @ x)) is Element of the carrier of M

(M,(a . ((b @ c),(c @ x)))) is Element of the carrier of M

(a . ((b @ c),(c @ x))) + (a . ((b @ c),(c @ x))) is Element of the carrier of M

a . ((b @ d),((b @ c) @ (d @ x))) is Element of the carrier of M

a . (((b @ c) @ (d @ x)),(d @ x)) is Element of the carrier of M

(a . ((b @ d),((b @ c) @ (d @ x)))) + (a . (((b @ c) @ (d @ x)),(d @ x))) is Element of the carrier of M

a . (((b @ c) @ (d @ x)),(c @ x)) is Element of the carrier of M

a . ((b @ c),((b @ c) @ (d @ x))) is Element of the carrier of M

(a . (((b @ c) @ (d @ x)),(c @ x))) + (a . ((b @ c),((b @ c) @ (d @ x)))) is Element of the carrier of M

M is non empty right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

the carrier of M is non empty set

W is non empty MidStr

the carrier of W is non empty set

[: the carrier of W, the carrier of W:] is set

[:[: the carrier of W, the carrier of W:], the carrier of M:] is set

bool [:[: the carrier of W, the carrier of W:], the carrier of M:] is set

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

b is Element of the carrier of W

b @ b is Element of the carrier of W

c is Element of the carrier of W

d is Element of the carrier of W

c @ d is Element of the carrier of W

d @ c is Element of the carrier of W

x is Element of the carrier of W

w is Element of the carrier of W

x @ w is Element of the carrier of W

G is Element of the carrier of W

b is Element of the carrier of W

G @ b is Element of the carrier of W

(x @ w) @ (G @ b) is Element of the carrier of W

x @ G is Element of the carrier of W

w @ b is Element of the carrier of W

(x @ G) @ (w @ b) is Element of the carrier of W

x is Element of the carrier of W

a is Element of the carrier of W

M is non empty MidSp-like MidStr

vectgroup M is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr

the carrier of (vectgroup M) is non empty set

0. (vectgroup M) is V49( vectgroup M) Element of the carrier of (vectgroup M)

the ZeroF of (vectgroup M) is Element of the carrier of (vectgroup M)

a is Element of the carrier of (vectgroup M)

b is Element of the carrier of (vectgroup M)

((vectgroup M),b) is Element of the carrier of (vectgroup M)

b + b is Element of the carrier of (vectgroup M)

M is non empty MidSp-like MidStr

the carrier of M is non empty set

W is Element of the carrier of M

a is Element of the carrier of M

vect (W,a) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

vectgroup M is non empty strict right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

the carrier of (vectgroup M) is non empty set

M is non empty MidSp-like MidStr

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is set

vectgroup M is non empty strict right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

the carrier of (vectgroup M) is non empty set

[:[: the carrier of M, the carrier of M:], the carrier of (vectgroup M):] is set

bool [:[: the carrier of M, the carrier of M:], the carrier of (vectgroup M):] is set

W is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of (vectgroup M)) V6() V18([: the carrier of M, the carrier of M:], the carrier of (vectgroup M)) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of (vectgroup M):]

a is Element of the carrier of M

b is Element of the carrier of M

W . (a,b) is Element of the carrier of (vectgroup M)

vect (a,b) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

(M,a,b) is Element of the carrier of (vectgroup M)

a is Element of the carrier of M

b is Element of the carrier of M

W . (a,b) is Element of the carrier of (vectgroup M)

vect (a,b) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

W is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of (vectgroup M)) V6() V18([: the carrier of M, the carrier of M:], the carrier of (vectgroup M)) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of (vectgroup M):]

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

b is Element of the carrier of M

c is Element of the carrier of M

W . (b,c) is Element of the carrier of (vectgroup M)

a . (b,c) is Element of the carrier of (vectgroup M)

vect (b,c) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

M is non empty MidSp-like MidStr

the carrier of M is non empty set

vectgroup M is non empty strict right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

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

[: the carrier of M, the carrier of M:] is set

the carrier of (vectgroup M) is non empty set

[:[: the carrier of M, the carrier of M:], the carrier of (vectgroup M):] is set

bool [:[: the carrier of M, the carrier of M:], the carrier of (vectgroup M):] is set

a is Element of the carrier of M

b is Element of the carrier of (vectgroup M)

c is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

d is Element of the carrier of M

vect (a,d) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

(M) . (a,d) is Element of the carrier of (vectgroup M)

a is Element of the carrier of M

b is Element of the carrier of M

(M) . (a,b) is Element of the carrier of (vectgroup M)

c is Element of the carrier of M

(M) . (a,c) is Element of the carrier of (vectgroup M)

vect (a,b) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

vect (a,c) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

a is Element of the carrier of M

b is Element of the carrier of M

(M) . (a,b) is Element of the carrier of (vectgroup M)

c is Element of the carrier of M

(M) . (b,c) is Element of the carrier of (vectgroup M)

((M) . (a,b)) + ((M) . (b,c)) is Element of the carrier of (vectgroup M)

(M) . (a,c) is Element of the carrier of (vectgroup M)

vect (a,b) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

vect (b,c) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

(vect (a,b)) + (vect (b,c)) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

vect (a,c) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

M is non empty MidSp-like MidStr

the carrier of M is non empty set

W is Element of the carrier of M

a is Element of the carrier of M

vect (W,a) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

b is Element of the carrier of M

a @ b is Element of the carrier of M

c is Element of the carrier of M

vect (b,c) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

W @ c is Element of the carrier of M

[W,a] is Element of [: the carrier of M, the carrier of M:]

[: the carrier of M, the carrier of M:] is set

[b,c] is Element of [: the carrier of M, the carrier of M:]

M is non empty MidSp-like MidStr

the carrier of M is non empty set

W is Element of the carrier of M

a is Element of the carrier of M

W @ a is Element of the carrier of M

b is Element of the carrier of M

vect (W,b) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

vect (b,a) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

b @ b is Element of the carrier of M

M is non empty MidSp-like MidStr

vectgroup M is non empty strict right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

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

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is set

the carrier of (vectgroup M) is non empty set

[:[: the carrier of M, the carrier of M:], the carrier of (vectgroup M):] is set

bool [:[: the carrier of M, the carrier of M:], the carrier of (vectgroup M):] is set

W is Element of the carrier of M

a is Element of the carrier of M

W @ a is Element of the carrier of M

b is Element of the carrier of M

(M) . (W,b) is Element of the carrier of (vectgroup M)

(M) . (b,a) is Element of the carrier of (vectgroup M)

vect (W,b) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

vect (b,a) is V1() V4( the carrier of M) V5( the carrier of M) non empty Vector of M

M is non empty MidSp-like MidStr

vectgroup M is non empty strict right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

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

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is set

the carrier of (vectgroup M) is non empty set

[:[: the carrier of M, the carrier of M:], the carrier of (vectgroup M):] is set

bool [:[: the carrier of M, the carrier of M:], the carrier of (vectgroup M):] is set

M is non empty set

[:M,M:] is set

W is non empty right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

the carrier of W is non empty set

[:[:M,M:], the carrier of W:] is set

bool [:[:M,M:], the carrier of W:] is set

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

[:[:M,M:],M:] is set

bool [:[:M,M:],M:] is set

b is Element of M

c is Element of M

a . (b,c) is Element of the carrier of W

(W,(a . (b,c))) is Element of the carrier of W

x is Element of M

a . (b,x) is Element of the carrier of W

a . (x,c) is Element of the carrier of W

(W,(a . (b,c))) + (W,(a . (b,c))) is Element of the carrier of W

(W,(W,(a . (b,c)))) is Element of the carrier of W

(W,(a . (b,c))) + (W,(a . (b,c))) is Element of the carrier of W

(W,(a . (b,c))) + (a . (x,c)) is Element of the carrier of W

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

c is Element of M

d is Element of M

b . (c,d) is Element of M

a . (c,(b . (c,d))) is Element of the carrier of W

a . ((b . (c,d)),d) is Element of the carrier of W

b is Element of M

c is Element of M

d is Element of M

a . (b,d) is Element of the carrier of W

a . (d,c) is Element of the carrier of W

x is Element of M

a . (b,x) is Element of the carrier of W

a . (x,c) is Element of the carrier of W

a . (d,x) is Element of the carrier of W

a . (d,b) is Element of the carrier of W

(a . (d,b)) + (a . (b,x)) is Element of the carrier of W

a . (c,d) is Element of the carrier of W

(a . (x,c)) + (a . (c,d)) is Element of the carrier of W

a . (x,d) is Element of the carrier of W

- (a . (d,x)) is Element of the carrier of W

0. W is V49(W) Element of the carrier of W

the ZeroF of W is Element of the carrier of W

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

c is V1() V4([:M,M:]) V5(M) V6() V18([:M,M:],M) Element of bool [:[:M,M:],M:]

d is Element of M

x is Element of M

b . (d,x) is Element of M

c . (d,x) is Element of M

a . (d,(b . (d,x))) is Element of the carrier of W

a . ((b . (d,x)),x) is Element of the carrier of W

a . (d,(c . (d,x))) is Element of the carrier of W

a . ((c . (d,x)),x) is Element of the carrier of W

M is non empty set

[:M,M:] is set

W is non empty right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

the carrier of W is non empty set

[:[:M,M:], the carrier of W:] is set

bool [:[:M,M:], the carrier of W:] is set

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

(M,W,a) is V1() V4([:M,M:]) V5(M) V6() V18([:M,M:],M) Element of bool [:[:M,M:],M:]

[:[:M,M:],M:] is set

bool [:[:M,M:],M:] is set

b is Element of M

c is Element of M

(M,W,a) . (b,c) is Element of M

d is Element of M

a . (b,d) is Element of the carrier of W

a . (d,c) is Element of the carrier of W

x is Element of M

w is Element of M

G is Element of M

a . (x,G) is Element of the carrier of W

a . (G,w) is Element of the carrier of W

b is Element of M

a . (x,b) is Element of the carrier of W

a . (b,w) is Element of the carrier of W

a . (G,b) is Element of the carrier of W

a . (G,x) is Element of the carrier of W

(a . (G,x)) + (a . (x,b)) is Element of the carrier of W

a . (w,G) is Element of the carrier of W

(a . (b,w)) + (a . (w,G)) is Element of the carrier of W

a . (b,G) is Element of the carrier of W

- (a . (G,b)) is Element of the carrier of W

0. W is V49(W) Element of the carrier of W

the ZeroF of W is Element of the carrier of W

a . (b,((M,W,a) . (b,c))) is Element of the carrier of W

a . (((M,W,a) . (b,c)),c) is Element of the carrier of W

M is non empty set

[:M,M:] is set

[:[:M,M:],M:] is set

bool [:[:M,M:],M:] is set

W is V1() V4([:M,M:]) V5(M) V6() V18([:M,M:],M) Element of bool [:[:M,M:],M:]

MidStr(# M,W #) is strict MidStr

M is non empty set

[:M,M:] is set

W is non empty right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

the carrier of W is non empty set

[:[:M,M:], the carrier of W:] is set

bool [:[:M,M:], the carrier of W:] is set

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

(M,W,a) is V1() V4([:M,M:]) V5(M) V6() V18([:M,M:],M) Element of bool [:[:M,M:],M:]

[:[:M,M:],M:] is set

bool [:[:M,M:],M:] is set

MidStr(# M,(M,W,a) #) is non empty strict MidStr

the carrier of MidStr(# M,(M,W,a) #) is non empty set

[: the carrier of MidStr(# M,(M,W,a) #), the carrier of MidStr(# M,(M,W,a) #):] is set

[:[: the carrier of MidStr(# M,(M,W,a) #), the carrier of MidStr(# M,(M,W,a) #):], the carrier of W:] is set

bool [:[: the carrier of MidStr(# M,(M,W,a) #), the carrier of MidStr(# M,(M,W,a) #):], the carrier of W:] is set

M is non empty set

[:M,M:] is set

W is non empty right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

the carrier of W is non empty set

[:[:M,M:], the carrier of W:] is set

bool [:[:M,M:], the carrier of W:] is set

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

(M,W,a) is V1() V4([:M,M:]) V5(M) V6() V18([:M,M:],M) Element of bool [:[:M,M:],M:]

[:[:M,M:],M:] is set

bool [:[:M,M:],M:] is set

MidStr(# M,(M,W,a) #) is non empty strict MidStr

(M,W,a) is V1() V4([: the carrier of MidStr(# M,(M,W,a) #), the carrier of MidStr(# M,(M,W,a) #):]) V5( the carrier of W) V6() V18([: the carrier of MidStr(# M,(M,W,a) #), the carrier of MidStr(# M,(M,W,a) #):], the carrier of W) Element of bool [:[: the carrier of MidStr(# M,(M,W,a) #), the carrier of MidStr(# M,(M,W,a) #):], the carrier of W:]

the carrier of MidStr(# M,(M,W,a) #) is non empty set

[: the carrier of MidStr(# M,(M,W,a) #), the carrier of MidStr(# M,(M,W,a) #):] is set

[:[: the carrier of MidStr(# M,(M,W,a) #), the carrier of MidStr(# M,(M,W,a) #):], the carrier of W:] is set

bool [:[: the carrier of MidStr(# M,(M,W,a) #), the carrier of MidStr(# M,(M,W,a) #):], the carrier of W:] is set

b is Element of the carrier of MidStr(# M,(M,W,a) #)

c is Element of the carrier of MidStr(# M,(M,W,a) #)

b @ c is Element of the carrier of MidStr(# M,(M,W,a) #)

d is Element of the carrier of MidStr(# M,(M,W,a) #)

(M,W,a) . (b,d) is Element of the carrier of W

(M,W,a) . (d,c) is Element of the carrier of W

(M,W,a) . (b,c) is set

a . (b,d) is set

a . (d,c) is set

M is non empty set

[:M,M:] is set

W is non empty right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

the carrier of W is non empty set

[:[:M,M:], the carrier of W:] is set

bool [:[:M,M:], the carrier of W:] is set

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

(M,W,a) is V1() V4([:M,M:]) V5(M) V6() V18([:M,M:],M) Element of bool [:[:M,M:],M:]

[:[:M,M:],M:] is set

bool [:[:M,M:],M:] is set

MidStr(# M,(M,W,a) #) is non empty strict MidStr

(M,W,a) is V1() V4([: the carrier of MidStr(# M,(M,W,a) #), the carrier of MidStr(# M,(M,W,a) #):]) V5( the carrier of W) V6() V18([: the carrier of MidStr(# M,(M,W,a) #), the carrier of MidStr(# M,(M,W,a) #):], the carrier of W) Element of bool [:[: the carrier of MidStr(# M,(M,W,a) #), the carrier of MidStr(# M,(M,W,a) #):], the carrier of W:]

the carrier of MidStr(# M,(M,W,a) #) is non empty set

[: the carrier of MidStr(# M,(M,W,a) #), the carrier of MidStr(# M,(M,W,a) #):] is set

[:[: the carrier of MidStr(# M,(M,W,a) #), the carrier of MidStr(# M,(M,W,a) #):], the carrier of W:] is set

bool [:[: the carrier of MidStr(# M,(M,W,a) #), the carrier of MidStr(# M,(M,W,a) #):], the carrier of W:] is set

M is non empty MidStr

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is set

W is non empty MidSp-like MidStr

vectgroup W is non empty strict right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

the carrier of (vectgroup W) is non empty set

[:[: the carrier of M, the carrier of M:], the carrier of (vectgroup W):] is set

bool [:[: the carrier of M, the carrier of M:], the carrier of (vectgroup W):] is set

the carrier of W is non empty set

[: the carrier of W, the carrier of W:] is set

[:[: the carrier of W, the carrier of W:], the carrier of (vectgroup W):] is set

bool [:[: the carrier of W, the carrier of W:], the carrier of (vectgroup W):] is set

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

b is V1() V4([: the carrier of W, the carrier of W:]) V5( the carrier of (vectgroup W)) V6() V18([: the carrier of W, the carrier of W:], the carrier of (vectgroup W)) Element of bool [:[: the carrier of W, the carrier of W:], the carrier of (vectgroup W):]

W is non empty right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

the carrier of W is non empty set

[:[: the carrier of M, the carrier of M:], the carrier of W:] is set

bool [:[: the carrier of M, the carrier of M:], the carrier of W:] is set

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

M is non empty MidStr

M is non empty MidSp-like MidStr

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is set

W is non empty right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

the carrier of W is non empty set

[:[: the carrier of M, the carrier of M:], the carrier of W:] is set

bool [:[: the carrier of M, the carrier of M:], the carrier of W:] is set

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

(M,W,a) is (M) (M)

M is non empty MidStr

M is non empty MidSp-like MidStr

the carrier of M is non empty set

W is (M)

the of W is non empty addLoopStr

the carrier of the of W is non empty set

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

[: the carrier of M, the carrier of M:] is set

[:[: the carrier of M, the carrier of M:], the carrier of the of W:] is set

bool [:[: the carrier of M, the carrier of M:], the carrier of the of W:] is set

a is Element of the carrier of M

b is Element of the carrier of M

the of W . (a,b) is Element of the carrier of the of W

M is non empty MidSp-like MidStr

the carrier of M is non empty set

W is (M)

the of W is non empty addLoopStr

the carrier of the of W is non empty set

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

[: the carrier of M, the carrier of M:] is set

[:[: the carrier of M, the carrier of M:], the carrier of the of W:] is set

bool [:[: the carrier of M, the carrier of M:], the carrier of the of W:] is set

a is Element of the carrier of M

b is Element of the carrier of the of W

( the carrier of M, the of W, the of W,a,b) is Element of the carrier of M

M is non empty MidSp-like MidStr

W is (M) (M)

the of W is non empty addLoopStr

0. the of W is V49( the of W) Element of the carrier of the of W

the carrier of the of W is non empty set

the ZeroF of the of W is Element of the carrier of the of W

M is non empty right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

the carrier of M is non empty set

W is non empty MidStr

the carrier of W is non empty set

[: the carrier of W, the carrier of W:] is set

[:[: the carrier of W, the carrier of W:], the carrier of M:] is set

bool [:[: the carrier of W, the carrier of W:], the carrier of M:] is set

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

b is Element of the carrier of W

c is Element of the carrier of W

b @ c is Element of the carrier of W

a . (b,c) is Element of the carrier of M

d is Element of the carrier of W

a . (b,d) is Element of the carrier of M

x is Element of the carrier of W

d @ x is Element of the carrier of W

a . (b,x) is Element of the carrier of M

(a . (b,d)) + (a . (b,x)) is Element of the carrier of M

a . (d,c) is Element of the carrier of M

(a . (b,d)) + (a . (d,c)) is Element of the carrier of M

M is non empty right_complementable Fanoian Abelian add-associative right_zeroed () addLoopStr

the carrier of M is non empty set

W is non empty MidStr

the carrier of W is non empty set

[: the carrier of W, the carrier of W:] is set

[:[: the carrier of W, the carrier of W:], the carrier of M:] is set

bool [:[: the carrier of W, the carrier of W:], the carrier of M:] is set

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

b is Element of the carrier of W

c is Element of the carrier of W

b @ c is Element of the carrier of W

a . (b,c) is Element of the carrier of M

d is Element of the carrier of W

a . (b,d) is Element of the carrier of M

(M,(a . (b,d))) is Element of the carrier of M

(a . (b,d)) + (a . (b,d)) is Element of the carrier of M

x is non empty MidSp-like MidStr

the carrier of x is non empty set

w is Element of the carrier of x

w @ w is Element of the carrier of x

M is non empty MidSp-like MidStr

the carrier of M is non empty set

W is (M) (M)

the of W is non empty addLoopStr

a is Element of the carrier of M

b is Element of the carrier of M

a @ b is Element of the carrier of M

(M,W,a,b) is Element of the carrier of the of W

the carrier of the of W is non empty set

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

[: the carrier of M, the carrier of M:] is set

[:[: the carrier of M, the carrier of M:], the carrier of the of W:] is set

bool [:[: the carrier of M, the carrier of M:], the carrier of the of W:] is set

the of W . (a,b) is Element of the carrier of the of W

c is Element of the carrier of M

(M,W,a,c) is Element of the carrier of the of W

the of W . (a,c) is Element of the carrier of the of W

d is Element of the carrier of M

c @ d is Element of the carrier of M

(M,W,a,d) is Element of the carrier of the of W

the of W . (a,d) is Element of the carrier of the of W

(M,W,a,c) + (M,W,a,d) is Element of the carrier of the of W

M is non empty MidSp-like MidStr

the carrier of M is non empty set

W is (M) (M)

the of W is non empty addLoopStr

a is Element of the carrier of M

b is Element of the carrier of M

a @ b is Element of the carrier of M

(M,W,a,b) is Element of the carrier of the of W

the carrier of the of W is non empty set

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

[: the carrier of M, the carrier of M:] is set

[:[: the carrier of M, the carrier of M:], the carrier of the of W:] is set

bool [:[: the carrier of M, the carrier of M:], the carrier of the of W:] is set

the of W . (a,b) is Element of the carrier of the of W

c is Element of the carrier of M

(M,W,a,c) is Element of the carrier of the of W

the of W . (a,c) is Element of the carrier of the of W

( the of W,(M,W,a,c)) is Element of the carrier of the of W

(M,W,a,c) + (M,W,a,c) is Element of the carrier of the of W

M is non empty MidSp-like MidStr

the carrier of M is non empty set

W is (M) (M)

the of W is non empty addLoopStr

the carrier of the of W is non empty set

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

[: the carrier of M, the carrier of M:] is set

[:[: the carrier of M, the carrier of M:], the carrier of the of W:] is set

bool [:[: the carrier of M, the carrier of M:], the carrier of the of W:] is set

c is Element of the carrier of M

d is Element of the carrier of the of W

x is Element of the carrier of M

the of W . (c,x) is Element of the carrier of the of W

(M,W,c,x) is Element of the carrier of the of W

c is Element of the carrier of M

d is Element of the carrier of M

(M,W,c,d) is Element of the carrier of the of W

the of W . (c,d) is Element of the carrier of the of W

x is Element of the carrier of M

(M,W,c,x) is Element of the carrier of the of W

the of W . (c,x) is Element of the carrier of the of W

b is Element of the carrier of M

c is Element of the carrier of M

(M,W,b,c) is Element of the carrier of the of W

the of W . (b,c) is Element of the carrier of the of W

d is Element of the carrier of M

(M,W,c,d) is Element of the carrier of the of W

the of W . (c,d) is Element of the carrier of the of W

(M,W,b,c) + (M,W,c,d) is Element of the carrier of the of W

(M,W,b,d) is Element of the carrier of the of W

the of W . (b,d) is Element of the carrier of the of W

M is non empty MidSp-like MidStr

the carrier of M is non empty set

W is (M) (M)

the of W is non empty addLoopStr

the carrier of the of W is non empty set

(M,W) is Element of the carrier of the of W

0. the of W is V49( the of W) Element of the carrier of the of W

the ZeroF of the of W is Element of the carrier of the of W

a is Element of the carrier of M

(M,W,a,a) is Element of the carrier of the of W

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

[: the carrier of M, the carrier of M:] is set

[:[: the carrier of M, the carrier of M:], the carrier of the of W:] is set

bool [:[: the carrier of M, the carrier of M:], the carrier of the of W:] is set

the of W . (a,a) is Element of the carrier of the of W

b is Element of the carrier of M

(M,W,a,b) is Element of the carrier of the of W

the of W . (a,b) is Element of the carrier of the of W

(M,W,b,a) is Element of the carrier of the of W

the of W . (b,a) is Element of the carrier of the of W

- (M,W,b,a) is Element of the carrier of the of W

a @ b is Element of the carrier of M

c is Element of the carrier of M

(M,W,c,a) is Element of the carrier of the of W

the of W . (c,a) is Element of the carrier of the of W

(M,W,a,c) is Element of the carrier of the of W

the of W . (a,c) is Element of the carrier of the of W

(M,W,c,b) is Element of the carrier of the of W

the of W . (c,b) is Element of the carrier of the of W

d is Element of the carrier of M

(M,W,c,d) is Element of the carrier of the of W

the of W . (c,d) is Element of the carrier of the of W

(M,W,d,c) is Element of the carrier of the of W

the of W . (d,c) is Element of the carrier of the of W

c @ d is Element of the carrier of M

(M,W,a,d) is Element of the carrier of the of W

the of W . (a,d) is Element of the carrier of the of W

x is Element of the carrier of the of W

(M,W,a,x) is Element of the carrier of M

( the carrier of M, the of W, the of W,a,x) is Element of the carrier of M

b is Element of the carrier of M

x is Element of the carrier of the of W

a is Element of the carrier of M

the of W . (a,b) is Element of the carrier of the of W

(M,W,a,b) is Element of the carrier of the of W

M is non empty MidSp-like MidStr

the carrier of M is non empty set

W is (M) (M)

(M,W) is Element of the carrier of the of W

the of W is non empty addLoopStr

the carrier of the of W is non empty set

0. the of W is V49( the of W) Element of the carrier of the of W

the ZeroF of the of W is Element of the carrier of the of W

a is Element of the carrier of M

(M,W,a,(M,W)) is Element of the carrier of M

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

[: the carrier of M, the carrier of M:] is set

[:[: the carrier of M, the carrier of M:], the carrier of the of W:] is set

bool [:[: the carrier of M, the carrier of M:], the carrier of the of W:] is set

( the carrier of M, the of W, the of W,a,(M,W)) is Element of the carrier of M

(M,W,a,a) is Element of the carrier of the of W

the of W . (a,a) is Element of the carrier of the of W