:: MOD_3 semantic presentation

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL

REAL is set

bool REAL is non empty set

NAT is non empty epsilon-transitive epsilon-connected ordinal set

bool NAT is non empty set

bool NAT is non empty set

{} is set

the empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V35() FinSequence-membered set is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V35() FinSequence-membered set

1 is non empty set

2 is non empty set

3 is non empty set

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of R is non empty set

0. R is V47(R) Element of the carrier of R

V is Element of the carrier of R

- V is Element of the carrier of R

- (- V) is Element of the carrier of R

R is non empty non degenerated non trivial right_complementable add-associative right_zeroed doubleLoopStr

0. R is V47(R) Element of the carrier of R

the carrier of R is non empty non trivial set

1. R is V47(R) Element of the carrier of R

- (1. R) is Element of the carrier of R

- (- (1. R)) is Element of the carrier of R

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of R is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

bool the carrier of V is non empty set

A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

Carrier A is finite Element of bool the carrier of V

0. R is V47(R) Element of the carrier of R

{ b

Sum A is Element of the carrier of V

B is finite Element of bool the carrier of V

B \ (Carrier A) is finite Element of bool the carrier of V

c

rng c

A (#) c

Sum (A (#) c

v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng v is finite set

l is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng l is finite set

x is set

len l is epsilon-transitive epsilon-connected ordinal natural Element of NAT

A (#) l is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

len (A (#) l) is epsilon-transitive epsilon-connected ordinal natural Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural Element of NAT

dom l is finite set

l /. x is Element of the carrier of V

l . x is set

dom (A (#) l) is finite set

(A (#) l) . x is set

A . (l /. x) is Element of the carrier of R

(A . (l /. x)) * (l /. x) is Element of the carrier of V

(0. R) * (l /. x) is Element of the carrier of V

Sum (A (#) l) is Element of the carrier of V

Sum l is Element of the carrier of V

(0. R) * (Sum l) is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

c

rng (c

A (#) (c

Sum (A (#) (c

(A (#) c

Sum ((A (#) c

(Sum (A (#) c

(Carrier A) \/ (B \ (Carrier A)) is finite Element of bool the carrier of V

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of R is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

Sum A is Element of the carrier of V

B is Element of the carrier of R

B * A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

Sum (B * A) is Element of the carrier of V

B * (Sum A) is Element of the carrier of V

Carrier (B * A) is finite Element of bool the carrier of V

bool the carrier of V is non empty set

0. R is V47(R) Element of the carrier of R

{ b

Carrier A is finite Element of bool the carrier of V

{ b

c

rng c

(B * A) (#) c

Sum ((B * A) (#) c

A (#) c

len ((B * A) (#) c

len c

len (A (#) c

dom c

Seg (len ((B * A) (#) c

x is epsilon-transitive epsilon-connected ordinal natural Element of NAT

dom ((B * A) (#) c

f is Element of the carrier of V

(A (#) c

c

c

((B * A) (#) c

(B * A) . (c

((B * A) . (c

A . (c

B * (A . (c

(B * (A . (c

(A . (c

B * ((A . (c

B * f is Element of the carrier of V

Sum (A (#) c

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

bool the carrier of V is non empty set

the carrier of R is non empty set

A is Element of bool the carrier of V

{ (Sum b

B is set

c

Sum c

ZeroLC V is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

B is Element of bool the carrier of V

v is Element of the carrier of V

l is Element of the carrier of V

v + l is Element of the carrier of V

x is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

Sum x is Element of the carrier of V

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

Sum f is Element of the carrier of V

x + f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

Sum f is Element of the carrier of V

v is Element of the carrier of R

l is Element of the carrier of V

v * l is Element of the carrier of V

x is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

Sum x is Element of the carrier of V

v * x is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

Sum f is Element of the carrier of V

c

Sum c

0. V is V47(V) Element of the carrier of V

B is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of B is non empty set

B is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of B is non empty set

R is set

V is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of V is non empty set

A is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over V

the carrier of A is non empty set

bool the carrier of A is non empty set

B is Element of bool the carrier of A

(V,A,B) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of A

the carrier of (V,A,B) is non empty set

{ (Sum b

B is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of B

Sum B is Element of the carrier of A

{ (Sum b

the carrier of (V,A,B) is non empty set

R is set

V is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

A is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over V

the carrier of A is non empty set

bool the carrier of A is non empty set

B is Element of bool the carrier of A

(V,A,B) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of A

0. V is V47(V) Element of the carrier of V

the carrier of V is non empty set

[: the carrier of A, the carrier of V:] is non empty set

bool [: the carrier of A, the carrier of V:] is non empty set

B is Element of the carrier of A

1. V is Element of the carrier of V

c

c

Funcs ( the carrier of A, the carrier of V) is non empty FUNCTION_DOMAIN of the carrier of A, the carrier of V

v is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Element of Funcs ( the carrier of A, the carrier of V)

{B} is finite Element of bool the carrier of A

l is finite Element of bool the carrier of A

x is Element of the carrier of A

v . x is Element of the carrier of V

x is finite Element of bool the carrier of A

l is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of A

Carrier l is finite Element of bool the carrier of A

{ b

{B} is finite Element of bool the carrier of A

x is set

f is Element of the carrier of A

l . f is Element of the carrier of V

x is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of {B}

Sum x is Element of the carrier of A

(1. V) * B is Element of the carrier of A

Carrier x is finite Element of bool the carrier of A

{ b

f is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of B

Sum f is Element of the carrier of A

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

{} the carrier of V is empty proper functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V35() FinSequence-membered Element of bool the carrier of V

bool the carrier of V is non empty set

(R,V,({} the carrier of V)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(0). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

B is Element of the carrier of V

the carrier of (R,V,({} the carrier of V)) is non empty set

the carrier of R is non empty set

{ (Sum b

0. V is V47(V) Element of the carrier of V

B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of {} the carrier of V

Sum B is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

bool the carrier of V is non empty set

(0). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

0. V is V47(V) Element of the carrier of V

{(0. V)} is finite Element of bool the carrier of V

A is Element of bool the carrier of V

(R,V,A) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

B is set

the Element of A is Element of A

B is set

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

0. R is V47(R) Element of the carrier of R

the carrier of R is non empty set

1. R is Element of the carrier of R

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

bool the carrier of V is non empty set

A is Element of bool the carrier of V

(R,V,A) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

B is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of B is non empty set

B is Element of the carrier of V

c

Sum c

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

0. R is V47(R) Element of the carrier of R

the carrier of R is non empty set

1. R is Element of the carrier of R

V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

bool the carrier of V is non empty set

A is Element of bool the carrier of V

(R,V,A) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(Omega). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

the ZeroF of V is Element of the carrier of V

the lmult of V is Relation-like [: the carrier of R, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of V:], the carrier of V:]

[: the carrier of R, the carrier of V:] is non empty set

[:[: the carrier of R, the carrier of V:], the carrier of V:] is non empty set

bool [:[: the carrier of R, the carrier of V:], the carrier of V:] is non empty set

VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over R

the carrier of ((Omega). V) is non empty set

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

bool the carrier of V is non empty set

A is Element of bool the carrier of V

(R,V,A) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

B is Element of bool the carrier of V

(R,V,B) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

B is Element of the carrier of V

the carrier of R is non empty set

c

Sum c

v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of B

Sum v is Element of the carrier of V

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

bool the carrier of V is non empty set

A is Element of bool the carrier of V

(R,V,A) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

B is Element of bool the carrier of V

(R,V,B) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

bool the carrier of V is non empty set

A is Element of bool the carrier of V

(R,V,A) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

B is Element of bool the carrier of V

A \/ B is Element of bool the carrier of V

(R,V,(A \/ B)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(R,V,B) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(R,V,A) + (R,V,B) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

0. R is V47(R) Element of the carrier of R

the carrier of R is non empty set

B is Element of the carrier of V

c

Sum c

Carrier c

{ b

(Carrier c

(Carrier c

x is set

c

[: the carrier of V, the carrier of R:] is non empty set

bool [: the carrier of V, the carrier of R:] is non empty set

f is Element of the carrier of V

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of R:]

f . f is Element of the carrier of R

f is set

c

[: the carrier of V, the carrier of R:] is non empty set

bool [: the carrier of V, the carrier of R:] is non empty set

f is Element of the carrier of V

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of R:]

f . f is Element of the carrier of R

[: the carrier of V, the carrier of R:] is non empty set

bool [: the carrier of V, the carrier of R:] is non empty set

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of R:]

f is finite Element of bool the carrier of V

f is set

Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)

g is Element of the carrier of V

f . g is Element of the carrier of R

g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

Carrier g is finite Element of bool the carrier of V

{ b

g is set

g is Element of the carrier of V

g . g is Element of the carrier of R

g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of R:]

x is finite Element of bool the carrier of V

g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)

u is Element of the carrier of V

g . u is Element of the carrier of R

u is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

Carrier u is finite Element of bool the carrier of V

{ b

f is set

v is Element of the carrier of V

u . v is Element of the carrier of R

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of B

f + g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

v is Element of the carrier of V

c

(f + g) . v is Element of the carrier of R

f . v is Element of the carrier of R

g . v is Element of the carrier of R

(f . v) + (g . v) is Element of the carrier of R

(c

(c

f . v is Element of the carrier of R

g . v is Element of the carrier of R

(f . v) + (g . v) is Element of the carrier of R

(0. R) + (g . v) is Element of the carrier of R

f . v is Element of the carrier of R

g . v is Element of the carrier of R

(f . v) + (g . v) is Element of the carrier of R

(0. R) + (g . v) is Element of the carrier of R

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

Sum f is Element of the carrier of V

Sum g is Element of the carrier of V

(Sum f) + (Sum g) is Element of the carrier of V

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

bool the carrier of V is non empty set

A is Element of bool the carrier of V

(R,V,A) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

B is Element of bool the carrier of V

A /\ B is Element of bool the carrier of V

(R,V,(A /\ B)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(R,V,B) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(R,V,A) /\ (R,V,B) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

bool the carrier of V is non empty set

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

(0). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of ((0). V) is non empty set

bool the carrier of ((0). V) is non empty set

the carrier of V is non empty set

{} the carrier of V is empty proper functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V35() FinSequence-membered Element of bool the carrier of V

bool the carrier of V is non empty set

B is Element of bool the carrier of ((0). V)

{} the carrier of ((0). V) is empty proper functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V35() FinSequence-membered Element of bool the carrier of ((0). V)

B is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(0). B is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of B

(0). ((0). V) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of (0). V

(R,((0). V),B) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of (0). V

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

LeftModule R is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

(0). (LeftModule R) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of LeftModule R

R is non empty non degenerated non trivial right_complementable almost_left_invertible V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of R is non empty non trivial set

0. R is V47(R) Element of the carrier of R

1. R is V47(R) Element of the carrier of R

V is Element of the carrier of R

V " is Element of the carrier of R

(V ") * V is Element of the carrier of R

A is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of A is non empty set

B is Element of the carrier of A

V * B is Element of the carrier of A

(V ") * (V * B) is Element of the carrier of A

(1. R) * B is Element of the carrier of A

((V ") * V) * B is Element of the carrier of A

R is non empty non degenerated non trivial right_complementable almost_left_invertible V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

0. V is V47(V) Element of the carrier of V

A is Element of the carrier of V

{A} is finite Element of bool the carrier of V

bool the carrier of V is non empty set

0. R is V47(R) Element of the carrier of R

the carrier of R is non empty non trivial set

1. R is V47(R) Element of the carrier of R

B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of {A}

Sum B is Element of the carrier of V

Carrier B is finite Element of bool the carrier of V

{ b

B . A is Element of the carrier of R

(B . A) * A is Element of the carrier of V

R is non empty non degenerated non trivial right_complementable almost_left_invertible V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of R is non empty non trivial set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

0. V is V47(V) Element of the carrier of V

A is Element of the carrier of V

B is Element of the carrier of V

{A,B} is finite Element of bool the carrier of V

bool the carrier of V is non empty set

0. R is V47(R) Element of the carrier of R

1. R is V47(R) Element of the carrier of R

B is Element of the carrier of R

B * B is Element of the carrier of V

[: the carrier of V, the carrier of R:] is non empty set

bool [: the carrier of V, the carrier of R:] is non empty set

- (1. R) is Element of the carrier of R

c

c

c

Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R

l is Element of the carrier of V

v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)

v . l is Element of the carrier of R

l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

Carrier l is finite Element of bool the carrier of V

{ b

x is set

f is Element of the carrier of V

l . f is Element of the carrier of R

x is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of {A,B}

Carrier x is finite Element of bool the carrier of V

{ b

Sum x is Element of the carrier of V

(- (1. R)) * (B * B) is Element of the carrier of V

((- (1. R)) * (B * B)) + (B * B) is Element of the carrier of V

- (B * B) is Element of the carrier of V

(- (B * B)) + (B * B) is Element of the carrier of V

(1. R) * B is Element of the carrier of V

B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of {A,B}

Sum B is Element of the carrier of V

Carrier B is finite Element of bool the carrier of V

{ b

B . A is Element of the carrier of R

(B . A) * A is Element of the carrier of V

B . B is Element of the carrier of R

(B . B) * B is Element of the carrier of V

((B . A) * A) + ((B . B) * B) is Element of the carrier of V

the Element of Carrier B is Element of Carrier B

(B . A) " is Element of the carrier of R

((B . A) ") * (((B . A) * A) + ((B . B) * B)) is Element of the carrier of V

((B . A) ") * ((B . A) * A) is Element of the carrier of V

((B . A) ") * ((B . B) * B) is Element of the carrier of V

(((B . A) ") * ((B . A) * A)) + (((B . A) ") * ((B . B) * B)) is Element of the carrier of V

((B . A) ") * (B . A) is Element of the carrier of R

(((B . A) ") * (B . A)) * A is Element of the carrier of V

((((B . A) ") * (B . A)) * A) + (((B . A) ") * ((B . B) * B)) is Element of the carrier of V

((B . A) ") * (B . B) is Element of the carrier of R

(((B . A) ") * (B . B)) * B is Element of the carrier of V

((((B . A) ") * (B . A)) * A) + ((((B . A) ") * (B . B)) * B) is Element of the carrier of V

(1. R) * A is Element of the carrier of V

((1. R) * A) + ((((B . A) ") * (B . B)) * B) is Element of the carrier of V

A + ((((B . A) ") * (B . B)) * B) is Element of the carrier of V

- ((((B . A) ") * (B . B)) * B) is Element of the carrier of V

- (1. R) is Element of the carrier of R

(- (1. R)) * ((((B . A) ") * (B . B)) * B) is Element of the carrier of V

(- (1. R)) * (((B . A) ") * (B . B)) is Element of the carrier of R

((- (1. R)) * (((B . A) ") * (B . B))) * B is Element of the carrier of V

(B . B) " is Element of the carrier of R

((B . B) ") * (((B . A) * A) + ((B . B) * B)) is Element of the carrier of V

((B . B) ") * ((B . A) * A) is Element of the carrier of V

((B . B) ") * ((B . B) * B) is Element of the carrier of V

(((B . B) ") * ((B . A) * A)) + (((B . B) ") * ((B . B) * B)) is Element of the carrier of V

((B . B) ") * (B . A) is Element of the carrier of R

(((B . B) ") * (B . A)) * A is Element of the carrier of V

((((B . B) ") * (B . A)) * A) + (((B . B) ") * ((B . B) * B)) is Element of the carrier of V

((((B . B) ") * (B . A)) * A) + ((1. R) * B) is Element of the carrier of V

((((B . B) ") * (B . A)) * A) + B is Element of the carrier of V

(0. R) * A is Element of the carrier of V

((0. R) * A) + B is Element of the carrier of V

(0. V) + B is Element of the carrier of V

v is Element of the carrier of V

B . v is Element of the carrier of R

R is non empty non degenerated non trivial right_complementable almost_left_invertible V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of R is non empty non trivial set

0. R is V47(R) Element of the carrier of R

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

0. V is V47(V) Element of the carrier of V

A is Element of the carrier of V

B is Element of the carrier of V

{A,B} is finite Element of bool the carrier of V

bool the carrier of V is non empty set

B is Element of the carrier of R

B * A is Element of the carrier of V

c

c

(B * A) + (c

B " is Element of the carrier of R

(B ") * ((B * A) + (c

(B ") * (B * A) is Element of the carrier of V

(B ") * (c

((B ") * (B * A)) + ((B ") * (c

(B ") * B is Element of the carrier of R

((B ") * B) * A is Element of the carrier of V

(((B ") * B) * A) + ((B ") * (c

(B ") * c

((B ") * c

(((B ") * B) * A) + (((B ") * c

1. R is V47(R) Element of the carrier of R

(1. R) * A is Element of the carrier of V

((1. R) * A) + (((B ") * c

A + (((B ") * c

- (((B ") * c

- (1. R) is Element of the carrier of R

(- (1. R)) * (((B ") * c

(- (1. R)) * ((B ") * c

((- (1. R)) * ((B ") * c

c

(c

(c

(c

((c

(c

((c

(((c

1. R is V47(R) Element of the carrier of R

(1. R) * B is Element of the carrier of V

(((c

(((c

- (((c

- (1. R) is Element of the carrier of R

(- (1. R)) * (((c

(- (1. R)) * ((c

((- (1. R)) * ((c

B is Element of the carrier of R

B * B is Element of the carrier of V

(0. V) + (B * B) is Element of the carrier of V

A - (B * B) is Element of the carrier of V

- B is Element of the carrier of R

(- B) * B is Element of the carrier of V

A + ((- B) * B) is Element of the carrier of V

1. R is V47(R) Element of the carrier of R

(1. R) * A is Element of the carrier of V

((1. R) * A) + ((- B) * B) is Element of the carrier of V

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

(0. R) * A is Element of the carrier of V

((0. R) * A) + (0. V) is Element of the carrier of V

(1. R) * B is Element of the carrier of V

((0. R) * A) + ((1. R) * B) is Element of the carrier of V

R is non empty non degenerated non trivial right_complementable almost_left_invertible V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

bool the carrier of V is non empty set

A is Element of bool the carrier of V

B is set

B is set

union B is set

v is set

l is set

v is Element of bool the carrier of V

{ b

the carrier of R is non empty non trivial set

l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of v

Sum l is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

Carrier l is finite Element of bool the carrier of V

0. R is V47(R) Element of the carrier of R

{ b

x is Relation-like Function-like set

dom x is set

rng x is set

f is non empty set

union f is set

the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f is Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f

rng the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f is set

g is set

x . g is set

g is set

g is Element of bool the carrier of V

{ b

dom the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f is set

g is set

g is set

the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f . g is set

g is set

x . g is set

{ b

g is Element of bool the carrier of V

g is set

g is set

union (rng the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f) is set

g is Element of bool the carrier of V

g is set

x . g is set

{ b

the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f . (x . g) is set

g is Element of bool the carrier of V

the Element of B is Element of B

x is Element of bool the carrier of V

B is set

c

(R,V,c

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

the ZeroF of V is Element of the carrier of V

the lmult of V is Relation-like [: the carrier of R, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of V:], the carrier of V:]

the carrier of R is non empty non trivial set

[: the carrier of R, the carrier of V:] is non empty set

[:[: the carrier of R, the carrier of V:], the carrier of V:] is non empty set

bool [:[: the carrier of R, the carrier of V:], the carrier of V:] is non empty set

VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over R

(Omega). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

v is Element of the carrier of V

{v} is finite Element of bool the carrier of V

c

l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of c

Sum l is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

Carrier l is finite Element of bool the carrier of V

0. R is V47(R) Element of the carrier of R

{ b

l . v is Element of the carrier of R

- (l . v) is Element of the carrier of R

(- (l . v)) " is Element of the carrier of R

(- (l . v)) * v is Element of the carrier of V

((- (l . v)) ") * ((- (l . v)) * v) is Element of the carrier of V

1. R is V47(R) Element of the carrier of R

(1. R) * v is Element of the carrier of V

[: the carrier of V, the carrier of R:] is non empty set

bool [: the carrier of V, the carrier of R:] is non empty set

x is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of R:]

x . v is Element of the carrier of R

Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R

f is Element of the carrier of V

(Carrier l) \ {v} is finite Element of bool the carrier of V

l . f is Element of the carrier of R

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)

f . f is Element of the carrier of R

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

Carrier f is finite Element of bool the carrier of V

{ b

f is set

g is Element of the carrier of V

f . g is Element of the carrier of R

l . g is Element of the carrier of R

g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of R:]

g . v is Element of the carrier of R

g is Element of the carrier of V

g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)

g . g is Element of the carrier of R

g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

Carrier g is finite Element of bool the carrier of V

{ b

g is set

u is Element of the carrier of V

g . u is Element of the carrier of R

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of c

g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of {v}

f - g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

- g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

- (1. R) is Element of the carrier of R

(- (1. R)) * g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

f + (- g) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

u is Element of the carrier of V

(f - g) . u is Element of the carrier of R

l . u is Element of the carrier of R

f . u is Element of the carrier of R

g . u is Element of the carrier of R

(f . u) - (g . u) is Element of the carrier of R

- (- (l . v)) is Element of the carrier of R

(0. R) + (- (- (l . v))) is Element of the carrier of R

(l . v) + (0. R) is Element of the carrier of R

f . u is Element of the carrier of R

g . u is Element of the carrier of R

(f . u) - (g . u) is Element of the carrier of R

(l . u) - (g . u) is Element of the carrier of R

(l . u) - (0. R) is Element of the carrier of R

Sum f is Element of the carrier of V

Sum g is Element of the carrier of V

(Sum f) - (Sum g) is Element of the carrier of V

x is set

R is non empty non degenerated non trivial right_complementable almost_left_invertible V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

bool the carrier of V is non empty set

A is Element of bool the carrier of V

(R,V,A) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

0. R is V47(R) Element of the carrier of R

the carrier of R is non empty non trivial set

1. R is V47(R) Element of the carrier of R

B is set

B is set

union B is set

v is set

l is set

v is Element of bool the carrier of V

{ b

l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of v

Sum l is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

Carrier l is finite Element of bool the carrier of V

{ b

x is Relation-like Function-like set

dom x is set

rng x is set

f is non empty set

union f is set

the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f is Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f

rng the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f is set

g is set

x . g is set

g is set

g is Element of bool the carrier of V

{ b

dom the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f is set

g is set

g is set

the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f . g is set

g is set

x . g is set

{ b

g is Element of bool the carrier of V

g is set

g is set

union (rng the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f) is set

g is Element of bool the carrier of V

g is set

x . g is set

{ b

the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f . (x . g) is set

g is Element of bool the carrier of V

l is set

x is set

f is Element of bool the carrier of V

{} the carrier of V is empty proper functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V35() FinSequence-membered Element of bool the carrier of V

B is set

c

(R,V,c

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

the ZeroF of V is Element of the carrier of V

the lmult of V is Relation-like [: the carrier of R, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of V:], the carrier of V:]

[: the carrier of R, the carrier of V:] is non empty set

[:[: the carrier of R, the carrier of V:], the carrier of V:] is non empty set

bool [:[: the carrier of R, the carrier of V:], the carrier of V:] is non empty set

VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over R

the carrier of (R,V,c

l is Element of the carrier of V

x is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

Sum x is Element of the carrier of V

Carrier x is finite Element of bool the carrier of V

{ b

f is set

f is Element of the carrier of V

v is Element of bool the carrier of V

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of v

Sum f is Element of the carrier of V

(R,V,v) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

v is Element of the carrier of V

v is Element of the carrier of V

{v} is finite Element of bool the carrier of V

c

l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of c

Sum l is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

Carrier l is finite Element of bool the carrier of V

{ b

l . v is Element of the carrier of R

- (l . v) is Element of the carrier of R

(- (l . v)) " is Element of the carrier of R

(- (l . v)) * v is Element of the carrier of V

((- (l . v)) ") * ((- (l . v)) * v) is Element of the carrier of V

(1. R) * v is Element of the carrier of V

[: the carrier of V, the carrier of R:] is non empty set

bool [: the carrier of V, the carrier of R:] is non empty set

x is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of R:]

x . v is Element of the carrier of R

Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R

f is Element of the carrier of V

(Carrier l) \ {v} is finite Element of bool the carrier of V

l . f is Element of the carrier of R

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)

f . f is Element of the carrier of R

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

Carrier f is finite Element of bool the carrier of V

{ b

f is set

g is Element of the carrier of V

f . g is Element of the carrier of R

l . g is Element of the carrier of R

g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of R:]

g . v is Element of the carrier of R

g is Element of the carrier of V

g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)

g . g is Element of the carrier of R

g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

Carrier g is finite Element of bool the carrier of V

{ b

g is set

u is Element of the carrier of V

g . u is Element of the carrier of R

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of c

g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of {v}

f - g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

- g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

- (1. R) is Element of the carrier of R

(- (1. R)) * g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

f + (- g) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

u is Element of the carrier of V

(f - g) . u is Element of the carrier of R

l . u is Element of the carrier of R

f . u is Element of the carrier of R

g . u is Element of the carrier of R

(f . u) - (g . u) is Element of the carrier of R

- (- (l . v)) is Element of the carrier of R

(0. R) + (- (- (l . v))) is Element of the carrier of R

(l . v) + (0. R) is Element of the carrier of R

f . u is Element of the carrier of R

g . u is Element of the carrier of R

(f . u) - (g . u) is Element of the carrier of R

(l . u) - (g . u) is Element of the carrier of R

(l . u) - (0. R) is Element of the carrier of R

Sum f is Element of the carrier of V

Sum g is Element of the carrier of V

(Sum f) - (Sum g) is Element of the carrier of V

x is set

R is non empty non degenerated non trivial right_complementable almost_left_invertible V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

bool the carrier of V is non empty set

{} the carrier of V is empty proper functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V35() FinSequence-membered Element of bool the carrier of V

A is Element of bool the carrier of V

R is non empty non degenerated non trivial right_complementable almost_left_invertible V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

bool the carrier of V is non empty set

A is Element of bool the carrier of V

R is non empty non degenerated non trivial right_complementable almost_left_invertible V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

bool the carrier of V is non empty set

R is non empty non degenerated non trivial right_complementable almost_left_invertible V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

bool the carrier of V is non empty set

A is Element of bool the carrier of V

B is Element of bool the carrier of V

B is (R,V)

R is non empty non degenerated non trivial right_complementable almost_left_invertible V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over R

the carrier of V is non empty set

bool the carrier of V is non empty set

A is Element of bool the carrier of V

(R,V,A) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

B is Element of bool the carrier of V

B is (R,V)