:: HAHNBAN1 semantic presentation

REAL is non empty V35() V192() V193() V194() V198() set
NAT is V192() V193() V194() V195() V196() V197() V198() Element of bool REAL
bool REAL is set
F_Complex is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible strict Abelian add-associative right_zeroed V105() unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
the carrier of F_Complex is non empty non trivial set
COMPLEX is non empty V35() V192() V198() set
RAT is non empty V35() V192() V193() V194() V195() V198() set
INT is non empty V35() V192() V193() V194() V195() V196() V198() set
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is set
[:[:NAT,NAT:],NAT:] is set
bool [:[:NAT,NAT:],NAT:] is set
omega is V192() V193() V194() V195() V196() V197() V198() set
bool omega is set
bool NAT is set
{} is empty Function-like functional V192() V193() V194() V195() V196() V197() V198() set
1 is non empty natural complex real ext-real V33() V34() V192() V193() V194() V195() V196() V197() Element of NAT
{{},1} is non empty set
K445() is L16()
the carrier of K445() is set
ExtREAL is non empty V193() set
0 is empty natural complex real ext-real Function-like functional V33() V34() V192() V193() V194() V195() V196() V197() V198() Element of NAT
<i> is complex Element of COMPLEX
K169() is V16() V19([:COMPLEX,COMPLEX:]) V20( COMPLEX ) Function-like V30([:COMPLEX,COMPLEX:], COMPLEX ) Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
K171() is V16() V19([:COMPLEX,COMPLEX:]) V20( COMPLEX ) Function-like V30([:COMPLEX,COMPLEX:], COMPLEX ) Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
1r is complex Element of COMPLEX
0c is empty complex Function-like functional V192() V193() V194() V195() V196() V197() V198() Element of COMPLEX
0. F_Complex is complex zero left_complementable right_complementable complementable Element of the carrier of F_Complex
the ZeroF of F_Complex is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
1_ F_Complex is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
1. F_Complex is complex non zero left_complementable right_complementable complementable Element of the carrier of F_Complex
the OneF of F_Complex is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
x is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V105() right-distributive doubleLoopStr
the carrier of x is non empty set
n is left_complementable right_complementable complementable Element of the carrier of x
p1 is left_complementable right_complementable complementable Element of the carrier of x
- p1 is left_complementable right_complementable complementable Element of the carrier of x
n * (- p1) is left_complementable right_complementable complementable Element of the carrier of x
the multF of x is V16() V19([: the carrier of x, the carrier of x:]) V20( the carrier of x) Function-like V30([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the multF of x . (n,(- p1)) is left_complementable right_complementable complementable Element of the carrier of x
[n,(- p1)] is set
{n,(- p1)} is non empty set
{n} is non empty set
{{n,(- p1)},{n}} is non empty set
the multF of x . [n,(- p1)] is set
n * p1 is left_complementable right_complementable complementable Element of the carrier of x
the multF of x . (n,p1) is left_complementable right_complementable complementable Element of the carrier of x
[n,p1] is set
{n,p1} is non empty set
{{n,p1},{n}} is non empty set
the multF of x . [n,p1] is set
- (n * p1) is left_complementable right_complementable complementable Element of the carrier of x
(n * p1) + (n * (- p1)) is left_complementable right_complementable complementable Element of the carrier of x
the addF of x is V16() V19([: the carrier of x, the carrier of x:]) V20( the carrier of x) Function-like V30([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
the addF of x . ((n * p1),(n * (- p1))) is left_complementable right_complementable complementable Element of the carrier of x
[(n * p1),(n * (- p1))] is set
{(n * p1),(n * (- p1))} is non empty set
{(n * p1)} is non empty set
{{(n * p1),(n * (- p1))},{(n * p1)}} is non empty set
the addF of x . [(n * p1),(n * (- p1))] is set
p1 + (- p1) is left_complementable right_complementable complementable Element of the carrier of x
the addF of x . (p1,(- p1)) is left_complementable right_complementable complementable Element of the carrier of x
[p1,(- p1)] is set
{p1,(- p1)} is non empty set
{p1} is non empty set
{{p1,(- p1)},{p1}} is non empty set
the addF of x . [p1,(- p1)] is set
n * (p1 + (- p1)) is left_complementable right_complementable complementable Element of the carrier of x
the multF of x . (n,(p1 + (- p1))) is left_complementable right_complementable complementable Element of the carrier of x
[n,(p1 + (- p1))] is set
{n,(p1 + (- p1))} is non empty set
{{n,(p1 + (- p1))},{n}} is non empty set
the multF of x . [n,(p1 + (- p1))] is set
0. x is zero left_complementable right_complementable complementable Element of the carrier of x
the ZeroF of x is left_complementable right_complementable complementable Element of the carrier of x
n * (0. x) is left_complementable right_complementable complementable Element of the carrier of x
the multF of x . (n,(0. x)) is left_complementable right_complementable complementable Element of the carrier of x
[n,(0. x)] is set
{n,(0. x)} is non empty set
{{n,(0. x)},{n}} is non empty set
the multF of x . [n,(0. x)] is set
x is complex real ext-real set
n is complex real ext-real set
n * <i> is complex set
x + (n * <i>) is complex set
p1 is complex real ext-real set
M is complex real ext-real set
M * <i> is complex set
p1 + (M * <i>) is complex set
(x + (n * <i>)) * (p1 + (M * <i>)) is complex set
x * p1 is complex real ext-real set
n * M is complex real ext-real set
(x * p1) - (n * M) is complex real ext-real set
x * M is complex real ext-real set
p1 * n is complex real ext-real set
(x * M) + (p1 * n) is complex real ext-real set
((x * M) + (p1 * n)) * <i> is complex set
((x * p1) - (n * M)) + (((x * M) + (p1 * n)) * <i>) is complex set
0 * <i> is complex set
x is complex Element of COMPLEX
|.x.| is complex real ext-real Element of REAL
Re x is complex real ext-real Element of REAL
(Re x) ^2 is complex real ext-real Element of REAL
(Re x) * (Re x) is complex real ext-real set
Im x is complex real ext-real Element of REAL
(Im x) ^2 is complex real ext-real Element of REAL
(Im x) * (Im x) is complex real ext-real set
((Re x) ^2) + ((Im x) ^2) is complex real ext-real Element of REAL
sqrt (((Re x) ^2) + ((Im x) ^2)) is complex real ext-real Element of REAL
|.x.| + (0 * <i>) is complex set
x *' is complex Element of COMPLEX
(Im x) * <i> is complex set
(Re x) - ((Im x) * <i>) is complex set
(x *') / (|.x.| + (0 * <i>)) is complex Element of COMPLEX
((x *') / (|.x.| + (0 * <i>))) * x is complex Element of COMPLEX
x * (x *') is complex Element of COMPLEX
Im (x * (x *')) is complex real ext-real Element of REAL
Re |.x.| is complex real ext-real Element of REAL
Im |.x.| is complex real ext-real Element of REAL
(x *') / |.x.| is complex Element of COMPLEX
((x *') / |.x.|) * x is complex Element of COMPLEX
(x * (x *')) / |.x.| is complex Element of COMPLEX
Re (x * (x *')) is complex real ext-real Element of REAL
Im (((x *') / |.x.|) * x) is complex real ext-real Element of REAL
|.x.| * 0 is complex real ext-real Element of REAL
(((Re x) ^2) + ((Im x) ^2)) * 0 is complex real ext-real Element of REAL
(|.x.| * 0) - ((((Re x) ^2) + ((Im x) ^2)) * 0) is complex real ext-real Element of REAL
|.x.| ^2 is complex real ext-real Element of REAL
|.x.| * |.x.| is complex real ext-real set
0 ^2 is complex real ext-real Element of REAL
0 * 0 is complex real ext-real set
(|.x.| ^2) + (0 ^2) is complex real ext-real Element of REAL
((|.x.| * 0) - ((((Re x) ^2) + ((Im x) ^2)) * 0)) / ((|.x.| ^2) + (0 ^2)) is complex real ext-real Element of REAL
Re (((x *') / |.x.|) * x) is complex real ext-real Element of REAL
(((Re x) ^2) + ((Im x) ^2)) * |.x.| is complex real ext-real Element of REAL
0 * 0 is natural complex real ext-real V33() V34() V192() V193() V194() V195() V196() V197() Element of NAT
((((Re x) ^2) + ((Im x) ^2)) * |.x.|) + (0 * 0) is complex real ext-real Element of REAL
(((((Re x) ^2) + ((Im x) ^2)) * |.x.|) + (0 * 0)) / ((|.x.| ^2) + (0 ^2)) is complex real ext-real Element of REAL
x * x is complex Element of COMPLEX
|.(x * x).| is complex real ext-real Element of REAL
Re (x * x) is complex real ext-real Element of REAL
(Re (x * x)) ^2 is complex real ext-real Element of REAL
(Re (x * x)) * (Re (x * x)) is complex real ext-real set
Im (x * x) is complex real ext-real Element of REAL
(Im (x * x)) ^2 is complex real ext-real Element of REAL
(Im (x * x)) * (Im (x * x)) is complex real ext-real set
((Re (x * x)) ^2) + ((Im (x * x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (x * x)) ^2) + ((Im (x * x)) ^2)) is complex real ext-real Element of REAL
|.(x * x).| * |.x.| is complex real ext-real Element of REAL
|.x.| * |.x.| is complex real ext-real Element of REAL
(|.(x * x).| * |.x.|) / (|.x.| * |.x.|) is complex real ext-real Element of REAL
|.(x * x).| / |.x.| is complex real ext-real Element of REAL
(|.x.| * |.x.|) / |.x.| is complex real ext-real Element of REAL
x is complex real ext-real set
n is complex real ext-real set
n * <i> is complex set
x + (n * <i>) is complex set
1 * <i> is complex set
0 + (1 * <i>) is complex set
(0,1) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
() is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
() * () is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
the multF of F_Complex is V16() V19([: the carrier of F_Complex, the carrier of F_Complex:]) V20( the carrier of F_Complex) Function-like V30([: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex) Element of bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:]
[: the carrier of F_Complex, the carrier of F_Complex:] is set
[:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is set
bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is set
the multF of F_Complex . ((),()) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
[(),()] is set
{(),()} is non empty V192() set
{()} is non empty V192() set
{{(),()},{()}} is non empty set
the multF of F_Complex . [(),()] is set
K147((),()) is complex Element of COMPLEX
- (1_ F_Complex) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
- 1r is complex Element of COMPLEX
(- (1_ F_Complex)) * (- (1_ F_Complex)) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
the multF of F_Complex . ((- (1_ F_Complex)),(- (1_ F_Complex))) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
[(- (1_ F_Complex)),(- (1_ F_Complex))] is set
{(- (1_ F_Complex)),(- (1_ F_Complex))} is non empty V192() set
{(- (1_ F_Complex))} is non empty V192() set
{{(- (1_ F_Complex)),(- (1_ F_Complex))},{(- (1_ F_Complex))}} is non empty set
the multF of F_Complex . [(- (1_ F_Complex)),(- (1_ F_Complex))] is set
K147((- (1_ F_Complex)),(- (1_ F_Complex))) is complex Element of COMPLEX
- 1r is complex Element of COMPLEX
x is complex real ext-real Element of REAL
n is complex real ext-real Element of REAL
(x,n) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
n * <i> is complex set
x + (n * <i>) is complex set
p1 is complex real ext-real Element of REAL
M is complex real ext-real Element of REAL
(p1,M) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
M * <i> is complex set
p1 + (M * <i>) is complex set
(x,n) + (p1,M) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
the addF of F_Complex is V16() V19([: the carrier of F_Complex, the carrier of F_Complex:]) V20( the carrier of F_Complex) Function-like V30([: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex) Element of bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:]
the addF of F_Complex . ((x,n),(p1,M)) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
[(x,n),(p1,M)] is set
{(x,n),(p1,M)} is non empty V192() set
{(x,n)} is non empty V192() set
{{(x,n),(p1,M)},{(x,n)}} is non empty set
the addF of F_Complex . [(x,n),(p1,M)] is set
K145((x,n),(p1,M)) is complex Element of COMPLEX
x + p1 is complex real ext-real Element of REAL
n + M is complex real ext-real Element of REAL
((x + p1),(n + M)) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
(n + M) * <i> is complex set
(x + p1) + ((n + M) * <i>) is complex set
x is complex real ext-real set
n is complex real ext-real set
(x,n) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
n * <i> is complex set
x + (n * <i>) is complex set
p1 is complex real ext-real set
M is complex real ext-real set
(p1,M) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
M * <i> is complex set
p1 + (M * <i>) is complex set
(x,n) * (p1,M) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
the multF of F_Complex . ((x,n),(p1,M)) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
[(x,n),(p1,M)] is set
{(x,n),(p1,M)} is non empty V192() set
{(x,n)} is non empty V192() set
{{(x,n),(p1,M)},{(x,n)}} is non empty set
the multF of F_Complex . [(x,n),(p1,M)] is set
K147((x,n),(p1,M)) is complex Element of COMPLEX
x * p1 is complex real ext-real set
n * M is complex real ext-real set
(x * p1) - (n * M) is complex real ext-real set
x * M is complex real ext-real set
p1 * n is complex real ext-real set
(x * M) + (p1 * n) is complex real ext-real set
(((x * p1) - (n * M)),((x * M) + (p1 * n))) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
((x * M) + (p1 * n)) * <i> is complex set
((x * p1) - (n * M)) + (((x * M) + (p1 * n)) * <i>) is complex set
x is complex real ext-real Element of REAL
(x,0) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
x + (0 * <i>) is complex set
|.(x,0).| is complex real ext-real Element of REAL
Re (x,0) is complex real ext-real Element of REAL
(Re (x,0)) ^2 is complex real ext-real Element of REAL
(Re (x,0)) * (Re (x,0)) is complex real ext-real set
Im (x,0) is complex real ext-real Element of REAL
(Im (x,0)) ^2 is complex real ext-real Element of REAL
(Im (x,0)) * (Im (x,0)) is complex real ext-real set
((Re (x,0)) ^2) + ((Im (x,0)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (x,0)) ^2) + ((Im (x,0)) ^2)) is complex real ext-real Element of REAL
abs x is complex real ext-real Element of REAL
Re x is complex real ext-real Element of REAL
(Re x) ^2 is complex real ext-real Element of REAL
(Re x) * (Re x) is complex real ext-real set
Im x is complex real ext-real Element of REAL
(Im x) ^2 is complex real ext-real Element of REAL
(Im x) * (Im x) is complex real ext-real set
((Re x) ^2) + ((Im x) ^2) is complex real ext-real Element of REAL
sqrt (((Re x) ^2) + ((Im x) ^2)) is complex real ext-real Element of REAL
x is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
n is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
x + n is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
the addF of F_Complex is V16() V19([: the carrier of F_Complex, the carrier of F_Complex:]) V20( the carrier of F_Complex) Function-like V30([: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex) Element of bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:]
the addF of F_Complex . (x,n) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
[x,n] is set
{x,n} is non empty V192() set
{x} is non empty V192() set
{{x,n},{x}} is non empty set
the addF of F_Complex . [x,n] is set
K145(x,n) is complex Element of COMPLEX
Re (x + n) is complex real ext-real Element of REAL
Re x is complex real ext-real Element of REAL
Re n is complex real ext-real Element of REAL
(Re x) + (Re n) is complex real ext-real Element of REAL
p1 is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
M is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
p1 + M is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
the addF of F_Complex . (p1,M) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
[p1,M] is set
{p1,M} is non empty V192() set
{p1} is non empty V192() set
{{p1,M},{p1}} is non empty set
the addF of F_Complex . [p1,M] is set
K145(p1,M) is complex Element of COMPLEX
Im (p1 + M) is complex real ext-real Element of REAL
Im p1 is complex real ext-real Element of REAL
Im M is complex real ext-real Element of REAL
(Im p1) + (Im M) is complex real ext-real Element of REAL
x is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
n is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
x * n is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
the multF of F_Complex . (x,n) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
[x,n] is set
{x,n} is non empty V192() set
{x} is non empty V192() set
{{x,n},{x}} is non empty set
the multF of F_Complex . [x,n] is set
K147(x,n) is complex Element of COMPLEX
Re (x * n) is complex real ext-real Element of REAL
Re x is complex real ext-real Element of REAL
Re n is complex real ext-real Element of REAL
(Re x) * (Re n) is complex real ext-real Element of REAL
Im x is complex real ext-real Element of REAL
Im n is complex real ext-real Element of REAL
(Im x) * (Im n) is complex real ext-real Element of REAL
((Re x) * (Re n)) - ((Im x) * (Im n)) is complex real ext-real Element of REAL
p1 is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
M is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
p1 * M is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
the multF of F_Complex . (p1,M) is complex left_complementable right_complementable complementable Element of the carrier of F_Complex
[p1,M] is set
{p1,M} is non empty V192() set
{p1} is non empty V192() set
{{p1,M},{p1}} is non empty set
the multF of F_Complex . [p1,M] is set
K147(p1,M) is complex Element of COMPLEX
Im (p1 * M) is complex real ext-real Element of REAL
Re p1 is complex real ext-real Element of REAL
Im M is complex real ext-real Element of REAL
(Re p1) * (Im M) is complex real ext-real Element of REAL
Re M is complex real ext-real Element of REAL
Im p1 is complex real ext-real Element of REAL
(Re M) * (Im p1) is complex real ext-real Element of REAL
((Re p1) * (Im M)) + ((Re M) * (Im p1)) is complex real ext-real Element of REAL
x is 1-sorted
x is non empty addLoopStr
n is non empty VectSpStr over x
the carrier of n is non empty set
the carrier of x is non empty set
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
p1 is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
M is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
tcM is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
RVSM is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
l is Element of the carrier of n
RVSM . l is Element of the carrier of x
p1 . l is Element of the carrier of x
M . l is Element of the carrier of x
(p1 . l) + (M . l) is Element of the carrier of x
the addF of x is V16() V19([: the carrier of x, the carrier of x:]) V20( the carrier of x) Function-like V30([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the addF of x . ((p1 . l),(M . l)) is Element of the carrier of x
[(p1 . l),(M . l)] is set
{(p1 . l),(M . l)} is non empty set
{(p1 . l)} is non empty set
{{(p1 . l),(M . l)},{(p1 . l)}} is non empty set
the addF of x . [(p1 . l),(M . l)] is set
tcM is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
RVSM is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
l is Element of the carrier of n
tcM . l is Element of the carrier of x
p1 . l is Element of the carrier of x
M . l is Element of the carrier of x
(p1 . l) + (M . l) is Element of the carrier of x
the addF of x is V16() V19([: the carrier of x, the carrier of x:]) V20( the carrier of x) Function-like V30([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the addF of x . ((p1 . l),(M . l)) is Element of the carrier of x
[(p1 . l),(M . l)] is set
{(p1 . l),(M . l)} is non empty set
{(p1 . l)} is non empty set
{{(p1 . l),(M . l)},{(p1 . l)}} is non empty set
the addF of x . [(p1 . l),(M . l)] is set
RVSM . l is Element of the carrier of x
x is non empty addLoopStr
n is non empty VectSpStr over x
the carrier of n is non empty set
the carrier of x is non empty set
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
p1 is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
M is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
tcM is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
RVSM is Element of the carrier of n
tcM . RVSM is Element of the carrier of x
p1 . RVSM is Element of the carrier of x
- (p1 . RVSM) is Element of the carrier of x
M is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
tcM is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
RVSM is Element of the carrier of n
M . RVSM is Element of the carrier of x
p1 . RVSM is Element of the carrier of x
- (p1 . RVSM) is Element of the carrier of x
tcM . RVSM is Element of the carrier of x
x is non empty addLoopStr
n is non empty VectSpStr over x
the carrier of n is non empty set
the carrier of x is non empty set
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
p1 is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
M is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
(x,n,M) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
(x,n,p1,(x,n,M)) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
x is non empty multMagma
the carrier of x is non empty set
n is non empty VectSpStr over x
the carrier of n is non empty set
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
p1 is Element of the carrier of x
M is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
tcM is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
RVSM is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
l is Element of the carrier of n
RVSM . l is Element of the carrier of x
M . l is Element of the carrier of x
p1 * (M . l) is Element of the carrier of x
the multF of x is V16() V19([: the carrier of x, the carrier of x:]) V20( the carrier of x) Function-like V30([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the multF of x . (p1,(M . l)) is Element of the carrier of x
[p1,(M . l)] is set
{p1,(M . l)} is non empty set
{p1} is non empty set
{{p1,(M . l)},{p1}} is non empty set
the multF of x . [p1,(M . l)] is set
tcM is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
RVSM is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
l is Element of the carrier of n
tcM . l is Element of the carrier of x
M . l is Element of the carrier of x
p1 * (M . l) is Element of the carrier of x
the multF of x is V16() V19([: the carrier of x, the carrier of x:]) V20( the carrier of x) Function-like V30([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the multF of x . (p1,(M . l)) is Element of the carrier of x
[p1,(M . l)] is set
{p1,(M . l)} is non empty set
{p1} is non empty set
{{p1,(M . l)},{p1}} is non empty set
the multF of x . [p1,(M . l)] is set
RVSM . l is Element of the carrier of x
x is non empty ZeroStr
the carrier of x is non empty set
n is VectSpStr over x
[#] n is non proper Element of bool the carrier of n
the carrier of n is set
bool the carrier of n is set
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
([#] n) --> (0. x) is V16() V19( [#] n) V20( the carrier of x) Function-like V30( [#] n, the carrier of x) Element of bool [:([#] n), the carrier of x:]
[:([#] n), the carrier of x:] is set
bool [:([#] n), the carrier of x:] is set
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
x is non empty multMagma
n is non empty VectSpStr over x
the carrier of n is non empty set
the carrier of x is non empty set
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
x is non empty ZeroStr
n is non empty VectSpStr over x
the carrier of n is non empty set
the carrier of x is non empty set
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
x is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V105() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr
n is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V105() vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over x
the carrier of n is non empty set
the carrier of x is non empty set
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
p1 is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
0. n is zero left_complementable right_complementable complementable Element of the carrier of n
the ZeroF of n is left_complementable right_complementable complementable Element of the carrier of n
p1 . (0. n) is left_complementable right_complementable complementable Element of the carrier of x
0. x is zero left_complementable right_complementable complementable Element of the carrier of x
the ZeroF of x is left_complementable right_complementable complementable Element of the carrier of x
(0. x) * (0. n) is left_complementable right_complementable complementable Element of the carrier of n
the lmult of n is V16() V19([: the carrier of x, the carrier of n:]) V20( the carrier of n) Function-like V30([: the carrier of x, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of x, the carrier of n:], the carrier of n:]
[: the carrier of x, the carrier of n:] is set
[:[: the carrier of x, the carrier of n:], the carrier of n:] is set
bool [:[: the carrier of x, the carrier of n:], the carrier of n:] is set
the lmult of n . ((0. x),(0. n)) is left_complementable right_complementable complementable Element of the carrier of n
[(0. x),(0. n)] is set
{(0. x),(0. n)} is non empty set
{(0. x)} is non empty set
{{(0. x),(0. n)},{(0. x)}} is non empty set
the lmult of n . [(0. x),(0. n)] is set
p1 . ((0. x) * (0. n)) is left_complementable right_complementable complementable Element of the carrier of x
(0. x) * (p1 . (0. n)) is left_complementable right_complementable complementable Element of the carrier of x
the multF of x is V16() V19([: the carrier of x, the carrier of x:]) V20( the carrier of x) Function-like V30([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the multF of x . ((0. x),(p1 . (0. n))) is left_complementable right_complementable complementable Element of the carrier of x
[(0. x),(p1 . (0. n))] is set
{(0. x),(p1 . (0. n))} is non empty set
{{(0. x),(p1 . (0. n))},{(0. x)}} is non empty set
the multF of x . [(0. x),(p1 . (0. n))] is set
x is non empty right_zeroed addLoopStr
n is non empty VectSpStr over x
(x,n) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
the carrier of n is non empty set
the carrier of x is non empty set
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
[#] n is non empty non proper Element of bool the carrier of n
bool the carrier of n is set
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
([#] n) --> (0. x) is V16() V19( [#] n) V20( the carrier of x) Function-like V30( [#] n, the carrier of x) Element of bool [:([#] n), the carrier of x:]
[:([#] n), the carrier of x:] is set
bool [:([#] n), the carrier of x:] is set
p1 is Element of the carrier of n
M is Element of the carrier of n
p1 + M is Element of the carrier of n
the addF of n is V16() V19([: the carrier of n, the carrier of n:]) V20( the carrier of n) Function-like V30([: the carrier of n, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is set
the addF of n . (p1,M) is Element of the carrier of n
[p1,M] is set
{p1,M} is non empty set
{p1} is non empty set
{{p1,M},{p1}} is non empty set
the addF of n . [p1,M] is set
(x,n) . (p1 + M) is Element of the carrier of x
(x,n) . p1 is Element of the carrier of x
(x,n) . M is Element of the carrier of x
((x,n) . p1) + ((x,n) . M) is Element of the carrier of x
the addF of x is V16() V19([: the carrier of x, the carrier of x:]) V20( the carrier of x) Function-like V30([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the addF of x . (((x,n) . p1),((x,n) . M)) is Element of the carrier of x
[((x,n) . p1),((x,n) . M)] is set
{((x,n) . p1),((x,n) . M)} is non empty set
{((x,n) . p1)} is non empty set
{{((x,n) . p1),((x,n) . M)},{((x,n) . p1)}} is non empty set
the addF of x . [((x,n) . p1),((x,n) . M)] is set
x is non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
n is non empty VectSpStr over x
(x,n) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) additive Element of bool [: the carrier of n, the carrier of x:]
the carrier of n is non empty set
the carrier of x is non empty set
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
[#] n is non empty non proper Element of bool the carrier of n
bool the carrier of n is set
0. x is zero right_complementable Element of the carrier of x
the ZeroF of x is right_complementable Element of the carrier of x
([#] n) --> (0. x) is V16() V19( [#] n) V20( the carrier of x) Function-like V30( [#] n, the carrier of x) Element of bool [:([#] n), the carrier of x:]
[:([#] n), the carrier of x:] is set
bool [:([#] n), the carrier of x:] is set
p1 is Element of the carrier of n
(x,n) . p1 is right_complementable Element of the carrier of x
M is right_complementable Element of the carrier of x
M * p1 is Element of the carrier of n
the lmult of n is V16() V19([: the carrier of x, the carrier of n:]) V20( the carrier of n) Function-like V30([: the carrier of x, the carrier of n:], the carrier of n) Element of bool [:[: the carrier of x, the carrier of n:], the carrier of n:]
[: the carrier of x, the carrier of n:] is set
[:[: the carrier of x, the carrier of n:], the carrier of n:] is set
bool [:[: the carrier of x, the carrier of n:], the carrier of n:] is set
the lmult of n . (M,p1) is Element of the carrier of n
[M,p1] is set
{M,p1} is non empty set
{M} is non empty set
{{M,p1},{M}} is non empty set
the lmult of n . [M,p1] is set
(x,n) . (M * p1) is right_complementable Element of the carrier of x
M * ((x,n) . p1) is right_complementable Element of the carrier of x
the multF of x is V16() V19([: the carrier of x, the carrier of x:]) V20( the carrier of x) Function-like V30([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the multF of x . (M,((x,n) . p1)) is right_complementable Element of the carrier of x
[M,((x,n) . p1)] is set
{M,((x,n) . p1)} is non empty set
{{M,((x,n) . p1)},{M}} is non empty set
the multF of x . [M,((x,n) . p1)] is set
x is non empty ZeroStr
n is non empty VectSpStr over x
(x,n) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
the carrier of n is non empty set
the carrier of x is non empty set
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
[#] n is non empty non proper Element of bool the carrier of n
bool the carrier of n is set
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
([#] n) --> (0. x) is V16() V19( [#] n) V20( the carrier of x) Function-like V30( [#] n, the carrier of x) Element of bool [:([#] n), the carrier of x:]
[:([#] n), the carrier of x:] is set
bool [:([#] n), the carrier of x:] is set
0. n is zero Element of the carrier of n
the ZeroF of n is Element of the carrier of n
(x,n) . (0. n) is Element of the carrier of x
x is non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
n is non empty VectSpStr over x
the carrier of n is non empty set
the carrier of x is non empty set
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
(x,n) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) additive (x,n) (x,n) Element of bool [: the carrier of n, the carrier of x:]
[#] n is non empty non proper Element of bool the carrier of n
bool the carrier of n is set
0. x is zero right_complementable Element of the carrier of x
the ZeroF of x is right_complementable Element of the carrier of x
([#] n) --> (0. x) is V16() V19( [#] n) V20( the carrier of x) Function-like V30( [#] n, the carrier of x) Element of bool [:([#] n), the carrier of x:]
[:([#] n), the carrier of x:] is set
bool [:([#] n), the carrier of x:] is set
x is non empty Abelian addLoopStr
the carrier of x is non empty set
n is non empty VectSpStr over x
the carrier of n is non empty set
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
p1 is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
M is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
(x,n,p1,M) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
(x,n,M,p1) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
tcM is Element of the carrier of n
(x,n,p1,M) . tcM is Element of the carrier of x
p1 . tcM is Element of the carrier of x
M . tcM is Element of the carrier of x
(p1 . tcM) + (M . tcM) is Element of the carrier of x
the addF of x is V16() V19([: the carrier of x, the carrier of x:]) V20( the carrier of x) Function-like V30([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the addF of x . ((p1 . tcM),(M . tcM)) is Element of the carrier of x
[(p1 . tcM),(M . tcM)] is set
{(p1 . tcM),(M . tcM)} is non empty set
{(p1 . tcM)} is non empty set
{{(p1 . tcM),(M . tcM)},{(p1 . tcM)}} is non empty set
the addF of x . [(p1 . tcM),(M . tcM)] is set
(x,n,M,p1) . tcM is Element of the carrier of x
x is non empty add-associative addLoopStr
the carrier of x is non empty set
n is non empty VectSpStr over x
the carrier of n is non empty set
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
p1 is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
M is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
(x,n,p1,M) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
tcM is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
(x,n,(x,n,p1,M),tcM) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
(x,n,M,tcM) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
(x,n,p1,(x,n,M,tcM)) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
RVSM is Element of the carrier of n
(x,n,(x,n,p1,M),tcM) . RVSM is Element of the carrier of x
(x,n,p1,M) . RVSM is Element of the carrier of x
tcM . RVSM is Element of the carrier of x
((x,n,p1,M) . RVSM) + (tcM . RVSM) is Element of the carrier of x
the addF of x is V16() V19([: the carrier of x, the carrier of x:]) V20( the carrier of x) Function-like V30([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the addF of x . (((x,n,p1,M) . RVSM),(tcM . RVSM)) is Element of the carrier of x
[((x,n,p1,M) . RVSM),(tcM . RVSM)] is set
{((x,n,p1,M) . RVSM),(tcM . RVSM)} is non empty set
{((x,n,p1,M) . RVSM)} is non empty set
{{((x,n,p1,M) . RVSM),(tcM . RVSM)},{((x,n,p1,M) . RVSM)}} is non empty set
the addF of x . [((x,n,p1,M) . RVSM),(tcM . RVSM)] is set
p1 . RVSM is Element of the carrier of x
M . RVSM is Element of the carrier of x
(p1 . RVSM) + (M . RVSM) is Element of the carrier of x
the addF of x . ((p1 . RVSM),(M . RVSM)) is Element of the carrier of x
[(p1 . RVSM),(M . RVSM)] is set
{(p1 . RVSM),(M . RVSM)} is non empty set
{(p1 . RVSM)} is non empty set
{{(p1 . RVSM),(M . RVSM)},{(p1 . RVSM)}} is non empty set
the addF of x . [(p1 . RVSM),(M . RVSM)] is set
((p1 . RVSM) + (M . RVSM)) + (tcM . RVSM) is Element of the carrier of x
the addF of x . (((p1 . RVSM) + (M . RVSM)),(tcM . RVSM)) is Element of the carrier of x
[((p1 . RVSM) + (M . RVSM)),(tcM . RVSM)] is set
{((p1 . RVSM) + (M . RVSM)),(tcM . RVSM)} is non empty set
{((p1 . RVSM) + (M . RVSM))} is non empty set
{{((p1 . RVSM) + (M . RVSM)),(tcM . RVSM)},{((p1 . RVSM) + (M . RVSM))}} is non empty set
the addF of x . [((p1 . RVSM) + (M . RVSM)),(tcM . RVSM)] is set
(M . RVSM) + (tcM . RVSM) is Element of the carrier of x
the addF of x . ((M . RVSM),(tcM . RVSM)) is Element of the carrier of x
[(M . RVSM),(tcM . RVSM)] is set
{(M . RVSM),(tcM . RVSM)} is non empty set
{(M . RVSM)} is non empty set
{{(M . RVSM),(tcM . RVSM)},{(M . RVSM)}} is non empty set
the addF of x . [(M . RVSM),(tcM . RVSM)] is set
(p1 . RVSM) + ((M . RVSM) + (tcM . RVSM)) is Element of the carrier of x
the addF of x . ((p1 . RVSM),((M . RVSM) + (tcM . RVSM))) is Element of the carrier of x
[(p1 . RVSM),((M . RVSM) + (tcM . RVSM))] is set
{(p1 . RVSM),((M . RVSM) + (tcM . RVSM))} is non empty set
{{(p1 . RVSM),((M . RVSM) + (tcM . RVSM))},{(p1 . RVSM)}} is non empty set
the addF of x . [(p1 . RVSM),((M . RVSM) + (tcM . RVSM))] is set
(x,n,M,tcM) . RVSM is Element of the carrier of x
(p1 . RVSM) + ((x,n,M,tcM) . RVSM) is Element of the carrier of x
the addF of x . ((p1 . RVSM),((x,n,M,tcM) . RVSM)) is Element of the carrier of x
[(p1 . RVSM),((x,n,M,tcM) . RVSM)] is set
{(p1 . RVSM),((x,n,M,tcM) . RVSM)} is non empty set
{{(p1 . RVSM),((x,n,M,tcM) . RVSM)},{(p1 . RVSM)}} is non empty set
the addF of x . [(p1 . RVSM),((x,n,M,tcM) . RVSM)] is set
(x,n,p1,(x,n,M,tcM)) . RVSM is Element of the carrier of x
x is non empty ZeroStr
n is non empty VectSpStr over x
the carrier of n is non empty set
the carrier of x is non empty set
(x,n) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) (x,n) Element of bool [: the carrier of n, the carrier of x:]
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
[#] n is non empty non proper Element of bool the carrier of n
bool the carrier of n is set
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
([#] n) --> (0. x) is V16() V19( [#] n) V20( the carrier of x) Function-like V30( [#] n, the carrier of x) Element of bool [:([#] n), the carrier of x:]
[:([#] n), the carrier of x:] is set
bool [:([#] n), the carrier of x:] is set
p1 is Element of the carrier of n
(x,n) . p1 is Element of the carrier of x
x is non empty right_zeroed addLoopStr
the carrier of x is non empty set
n is non empty VectSpStr over x
the carrier of n is non empty set
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
(x,n) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) additive (x,n) Element of bool [: the carrier of n, the carrier of x:]
[#] n is non empty non proper Element of bool the carrier of n
bool the carrier of n is set
0. x is zero Element of the carrier of x
the ZeroF of x is Element of the carrier of x
([#] n) --> (0. x) is V16() V19( [#] n) V20( the carrier of x) Function-like V30( [#] n, the carrier of x) Element of bool [:([#] n), the carrier of x:]
[:([#] n), the carrier of x:] is set
bool [:([#] n), the carrier of x:] is set
p1 is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
(x,n,p1,(x,n)) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
M is Element of the carrier of n
(x,n,p1,(x,n)) . M is Element of the carrier of x
p1 . M is Element of the carrier of x
(x,n) . M is Element of the carrier of x
(p1 . M) + ((x,n) . M) is Element of the carrier of x
the addF of x is V16() V19([: the carrier of x, the carrier of x:]) V20( the carrier of x) Function-like V30([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the addF of x . ((p1 . M),((x,n) . M)) is Element of the carrier of x
[(p1 . M),((x,n) . M)] is set
{(p1 . M),((x,n) . M)} is non empty set
{(p1 . M)} is non empty set
{{(p1 . M),((x,n) . M)},{(p1 . M)}} is non empty set
the addF of x . [(p1 . M),((x,n) . M)] is set
(p1 . M) + (0. x) is Element of the carrier of x
the addF of x . ((p1 . M),(0. x)) is Element of the carrier of x
[(p1 . M),(0. x)] is set
{(p1 . M),(0. x)} is non empty set
{{(p1 . M),(0. x)},{(p1 . M)}} is non empty set
the addF of x . [(p1 . M),(0. x)] is set
x is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of x is non empty set
n is non empty VectSpStr over x
the carrier of n is non empty set
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
(x,n) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) additive (x,n) Element of bool [: the carrier of n, the carrier of x:]
[#] n is non empty non proper Element of bool the carrier of n
bool the carrier of n is set
0. x is zero right_complementable Element of the carrier of x
the ZeroF of x is right_complementable Element of the carrier of x
([#] n) --> (0. x) is V16() V19( [#] n) V20( the carrier of x) Function-like V30( [#] n, the carrier of x) Element of bool [:([#] n), the carrier of x:]
[:([#] n), the carrier of x:] is set
bool [:([#] n), the carrier of x:] is set
p1 is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
(x,n,p1,p1) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
(x,n,p1) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
(x,n,p1,(x,n,p1)) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
M is Element of the carrier of n
(x,n,p1,p1) . M is right_complementable Element of the carrier of x
p1 . M is right_complementable Element of the carrier of x
(x,n,p1) . M is right_complementable Element of the carrier of x
(p1 . M) + ((x,n,p1) . M) is right_complementable Element of the carrier of x
the addF of x is V16() V19([: the carrier of x, the carrier of x:]) V20( the carrier of x) Function-like V30([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the addF of x . ((p1 . M),((x,n,p1) . M)) is right_complementable Element of the carrier of x
[(p1 . M),((x,n,p1) . M)] is set
{(p1 . M),((x,n,p1) . M)} is non empty set
{(p1 . M)} is non empty set
{{(p1 . M),((x,n,p1) . M)},{(p1 . M)}} is non empty set
the addF of x . [(p1 . M),((x,n,p1) . M)] is set
- (p1 . M) is right_complementable Element of the carrier of x
(p1 . M) + (- (p1 . M)) is right_complementable Element of the carrier of x
the addF of x . ((p1 . M),(- (p1 . M))) is right_complementable Element of the carrier of x
[(p1 . M),(- (p1 . M))] is set
{(p1 . M),(- (p1 . M))} is non empty set
{{(p1 . M),(- (p1 . M))},{(p1 . M)}} is non empty set
the addF of x . [(p1 . M),(- (p1 . M))] is set
(x,n) . M is right_complementable Element of the carrier of x
x is non empty right-distributive doubleLoopStr
the carrier of x is non empty set
n is non empty VectSpStr over x
the carrier of n is non empty set
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
p1 is Element of the carrier of x
M is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
tcM is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
(x,n,M,tcM) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
(x,n,p1,(x,n,M,tcM)) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
(x,n,p1,M) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
(x,n,p1,tcM) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
(x,n,(x,n,p1,M),(x,n,p1,tcM)) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
RVSM is Element of the carrier of n
(x,n,p1,(x,n,M,tcM)) . RVSM is Element of the carrier of x
(x,n,M,tcM) . RVSM is Element of the carrier of x
p1 * ((x,n,M,tcM) . RVSM) is Element of the carrier of x
the multF of x is V16() V19([: the carrier of x, the carrier of x:]) V20( the carrier of x) Function-like V30([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the multF of x . (p1,((x,n,M,tcM) . RVSM)) is Element of the carrier of x
[p1,((x,n,M,tcM) . RVSM)] is set
{p1,((x,n,M,tcM) . RVSM)} is non empty set
{p1} is non empty set
{{p1,((x,n,M,tcM) . RVSM)},{p1}} is non empty set
the multF of x . [p1,((x,n,M,tcM) . RVSM)] is set
M . RVSM is Element of the carrier of x
tcM . RVSM is Element of the carrier of x
(M . RVSM) + (tcM . RVSM) is Element of the carrier of x
the addF of x is V16() V19([: the carrier of x, the carrier of x:]) V20( the carrier of x) Function-like V30([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
the addF of x . ((M . RVSM),(tcM . RVSM)) is Element of the carrier of x
[(M . RVSM),(tcM . RVSM)] is set
{(M . RVSM),(tcM . RVSM)} is non empty set
{(M . RVSM)} is non empty set
{{(M . RVSM),(tcM . RVSM)},{(M . RVSM)}} is non empty set
the addF of x . [(M . RVSM),(tcM . RVSM)] is set
p1 * ((M . RVSM) + (tcM . RVSM)) is Element of the carrier of x
the multF of x . (p1,((M . RVSM) + (tcM . RVSM))) is Element of the carrier of x
[p1,((M . RVSM) + (tcM . RVSM))] is set
{p1,((M . RVSM) + (tcM . RVSM))} is non empty set
{{p1,((M . RVSM) + (tcM . RVSM))},{p1}} is non empty set
the multF of x . [p1,((M . RVSM) + (tcM . RVSM))] is set
p1 * (M . RVSM) is Element of the carrier of x
the multF of x . (p1,(M . RVSM)) is Element of the carrier of x
[p1,(M . RVSM)] is set
{p1,(M . RVSM)} is non empty set
{{p1,(M . RVSM)},{p1}} is non empty set
the multF of x . [p1,(M . RVSM)] is set
p1 * (tcM . RVSM) is Element of the carrier of x
the multF of x . (p1,(tcM . RVSM)) is Element of the carrier of x
[p1,(tcM . RVSM)] is set
{p1,(tcM . RVSM)} is non empty set
{{p1,(tcM . RVSM)},{p1}} is non empty set
the multF of x . [p1,(tcM . RVSM)] is set
(p1 * (M . RVSM)) + (p1 * (tcM . RVSM)) is Element of the carrier of x
the addF of x . ((p1 * (M . RVSM)),(p1 * (tcM . RVSM))) is Element of the carrier of x
[(p1 * (M . RVSM)),(p1 * (tcM . RVSM))] is set
{(p1 * (M . RVSM)),(p1 * (tcM . RVSM))} is non empty set
{(p1 * (M . RVSM))} is non empty set
{{(p1 * (M . RVSM)),(p1 * (tcM . RVSM))},{(p1 * (M . RVSM))}} is non empty set
the addF of x . [(p1 * (M . RVSM)),(p1 * (tcM . RVSM))] is set
(x,n,p1,M) . RVSM is Element of the carrier of x
((x,n,p1,M) . RVSM) + (p1 * (tcM . RVSM)) is Element of the carrier of x
the addF of x . (((x,n,p1,M) . RVSM),(p1 * (tcM . RVSM))) is Element of the carrier of x
[((x,n,p1,M) . RVSM),(p1 * (tcM . RVSM))] is set
{((x,n,p1,M) . RVSM),(p1 * (tcM . RVSM))} is non empty set
{((x,n,p1,M) . RVSM)} is non empty set
{{((x,n,p1,M) . RVSM),(p1 * (tcM . RVSM))},{((x,n,p1,M) . RVSM)}} is non empty set
the addF of x . [((x,n,p1,M) . RVSM),(p1 * (tcM . RVSM))] is set
(x,n,p1,tcM) . RVSM is Element of the carrier of x
((x,n,p1,M) . RVSM) + ((x,n,p1,tcM) . RVSM) is Element of the carrier of x
the addF of x . (((x,n,p1,M) . RVSM),((x,n,p1,tcM) . RVSM)) is Element of the carrier of x
[((x,n,p1,M) . RVSM),((x,n,p1,tcM) . RVSM)] is set
{((x,n,p1,M) . RVSM),((x,n,p1,tcM) . RVSM)} is non empty set
{{((x,n,p1,M) . RVSM),((x,n,p1,tcM) . RVSM)},{((x,n,p1,M) . RVSM)}} is non empty set
the addF of x . [((x,n,p1,M) . RVSM),((x,n,p1,tcM) . RVSM)] is set
(x,n,(x,n,p1,M),(x,n,p1,tcM)) . RVSM is Element of the carrier of x
x is non empty left-distributive doubleLoopStr
the carrier of x is non empty set
n is non empty VectSpStr over x
the carrier of n is non empty set
[: the carrier of n, the carrier of x:] is set
bool [: the carrier of n, the carrier of x:] is set
p1 is Element of the carrier of x
M is Element of the carrier of x
p1 + M is Element of the carrier of x
the addF of x is V16() V19([: the carrier of x, the carrier of x:]) V20( the carrier of x) Function-like V30([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the addF of x . (p1,M) is Element of the carrier of x
[p1,M] is set
{p1,M} is non empty set
{p1} is non empty set
{{p1,M},{p1}} is non empty set
the addF of x . [p1,M] is set
tcM is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the carrier of x) Element of bool [: the carrier of n, the carrier of x:]
(x,n,(p1 + M),tcM) is V16() V19( the carrier of n) V20( the carrier of x) Function-like V30( the carrier of n, the