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