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