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

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

omega is V192() V193() V194() V195() V196() V197() V198() 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

the carrier of x is non empty set

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

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

the ZeroF of 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 + (n * <i>) is complex set

p1 + (M * <i>) is complex set
(x + (n * <i>)) * (p1 + (M * <i>)) is complex set

(x * p1) - (n * M) 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

(Re x) * (Re x) is complex real ext-real set

(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 set

(Im x) * <i> is complex set
(Re x) - ((Im x) * <i>) is complex set
(x *') / (|.x.| + ()) is complex Element of COMPLEX
((x *') / (|.x.| + ())) * x is complex Element of COMPLEX
x * (x *') is complex Element of COMPLEX
Im (x * (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

(((Re x) ^2) + ((Im x) ^2)) * 0 is complex real ext-real Element of REAL
() - ((((Re x) ^2) + ((Im x) ^2)) * 0) is complex real ext-real Element of REAL

() + () is complex real ext-real Element of REAL
(() - ((((Re x) ^2) + ((Im x) ^2)) * 0)) / (() + ()) 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.|) + () is complex real ext-real Element of REAL
(((((Re x) ^2) + ((Im x) ^2)) * |.x.|) + ()) / (() + ()) 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).| * |.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 Element of REAL

x + (n * <i>) is complex set

0 + (1 * <i>) is complex set

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

[(),()] 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

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

x + (n * <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),(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 + (n * <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) - (n * M) 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 set

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

(Re x) * (Re x) is complex real ext-real set

(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

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

[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) + (Re n) is complex real ext-real Element of REAL

[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) + (Im M) is complex real ext-real Element of REAL

[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) * (Re 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,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) * (Im M) 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
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
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
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

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

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

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

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

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

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