:: 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₁ where b₁ is Element of the carrier of V : not A . b₁ = 0. R } is set
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₆ is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng c₆ is finite set
A (#) c₆ is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (A (#) c₆) is Element of the carrier of V
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₆ ^ 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 (c₆ ^ l) is finite set
A (#) (c₆ ^ l) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (A (#) (c₆ ^ l)) is Element of the carrier of V
(A (#) c₆) ^ (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
Sum ((A (#) c₆) ^ (A (#) l)) is Element of the carrier of V
(Sum (A (#) c₆)) + (0. V) is Element of the carrier of V
(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₁ where b₁ is Element of the carrier of V : not (B * A) . b₁ = 0. R } is set
Carrier A is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not A . b₁ = 0. R } is set
c₆ is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng c₆ is finite set
(B * A) (#) c₆ is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum ((B * A) (#) c₆) is Element of the carrier of V
A (#) c₆ is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len ((B * A) (#) c₆) is epsilon-transitive epsilon-connected ordinal natural Element of NAT
len c₆ is epsilon-transitive epsilon-connected ordinal natural Element of NAT
len (A (#) c₆) is epsilon-transitive epsilon-connected ordinal natural Element of NAT
dom c₆ is finite set
Seg (len ((B * A) (#) c₆)) is finite V38( len ((B * A) (#) c₆)) Element of bool NAT
x is epsilon-transitive epsilon-connected ordinal natural Element of NAT
dom ((B * A) (#) c₆) is finite set
f is Element of the carrier of V
(A (#) c₆) . x is set
c₆ /. x is Element of the carrier of V
c₆ . x is set
((B * A) (#) c₆) . x is set
(B * A) . (c₆ /. x) is Element of the carrier of R
((B * A) . (c₆ /. x)) * (c₆ /. x) is Element of the carrier of V
A . (c₆ /. x) is Element of the carrier of R
B * (A . (c₆ /. x)) is Element of the carrier of R
(B * (A . (c₆ /. x))) * (c₆ /. x) is Element of the carrier of V
(A . (c₆ /. x)) * (c₆ /. x) is Element of the carrier of V
B * ((A . (c₆ /. x)) * (c₆ /. x)) is Element of the carrier of V
B * f is Element of the carrier of V
Sum (A (#) c₆) 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
the carrier of R is non empty set
A is Element of bool the carrier of V
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A : verum } is set
B is set
c₆ is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A
Sum c₆ is Element of the carrier of V
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₆ is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A
Sum c₆ is Element of the carrier of V
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₁) where b₁ is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of B : verum } is set
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₁) where b₁ is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of B : verum } is set
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₆ is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Element of bool [: the carrier of A, the carrier of V:]
c₆ . B is Element of the carrier of V
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₁ where b₁ is Element of the carrier of A : not l . b₁ = 0. V } is set
{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₁ where b₁ is Element of the carrier of A : not x . b₁ = 0. V } is set
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₁) where 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 : verum } is set
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₆ is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A
Sum c₆ 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
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₆ is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A
Sum c₆ 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 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₆ is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A \/ B
Sum c₆ is Element of the carrier of V
Carrier c₆ is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not c₆ . b₁ = 0. R } is set
(Carrier c₆) \ A is finite Element of bool the carrier of V
(Carrier c₆) /\ A is finite Element of bool the carrier of V
x is set
c₆ . x is set
[: 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₆ . f is set
[: 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₁ where b₁ is Element of the carrier of V : not g . b₁ = 0. R } is set
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₁ where b₁ is Element of the carrier of V : not u . b₁ = 0. R } is set
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₆ . v is Element of the carrier of R
(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₆ . v) + (g . v) is Element of the carrier of R
(c₆ . v) + (0. R) 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
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₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. R } is set
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₆ 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:]
c₆ . A is Element of the carrier of R
c₆ . B 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
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₁ where b₁ is Element of the carrier of V : not l . b₁ = 0. R } is set
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₁ where b₁ is Element of the carrier of V : not x . b₁ = 0. R } is set
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₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. R } is set
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₆ is Element of the carrier of R
c₆ * B is Element of the carrier of V
(B * A) + (c₆ * B) is Element of the carrier of V
B " is Element of the carrier of R
(B ") * ((B * A) + (c₆ * B)) is Element of the carrier of V
(B ") * (B * A) is Element of the carrier of V
(B ") * (c₆ * B) is Element of the carrier of V
((B ") * (B * A)) + ((B ") * (c₆ * B)) is Element of the carrier of V
(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)) is Element of the carrier of V
(B ") * c₆ is Element of the carrier of R
((B ") * c₆) * B is Element of the carrier of V
(((B ") * B) * A) + (((B ") * c₆) * 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 ") * c₆) * B) is Element of the carrier of V
A + (((B ") * c₆) * B) is Element of the carrier of V
- (((B ") * c₆) * B) is Element of the carrier of V
- (1. R) is Element of the carrier of R
(- (1. R)) * (((B ") * c₆) * B) is Element of the carrier of V
(- (1. R)) * ((B ") * c₆) is Element of the carrier of R
((- (1. R)) * ((B ") * c₆)) * B is Element of the carrier of V
c₆ " is Element of the carrier of R
(c₆ ") * ((B * A) + (c₆ * B)) is Element of the carrier of V
(c₆ ") * (B * A) is Element of the carrier of V
(c₆ ") * (c₆ * B) is Element of the carrier of V
((c₆ ") * (B * A)) + ((c₆ ") * (c₆ * B)) is Element of the carrier of V
(c₆ ") * B is Element of the carrier of R
((c₆ ") * B) * A is Element of the carrier of V
(((c₆ ") * B) * A) + ((c₆ ") * (c₆ * B)) is Element of the carrier of V
1. R is V47(R) Element of the carrier of R
(1. R) * B is Element of the carrier of V
(((c₆ ") * B) * A) + ((1. R) * B) is Element of the carrier of V
(((c₆ ") * B) * A) + B is Element of the carrier of V
- (((c₆ ") * B) * A) is Element of the carrier of V
- (1. R) is Element of the carrier of R
(- (1. R)) * (((c₆ ") * B) * A) is Element of the carrier of V
(- (1. R)) * ((c₆ ") * B) is Element of the carrier of R
((- (1. R)) * ((c₆ ") * B)) * A is Element of the carrier of V
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₁ where b₁ is Element of bool the carrier of V : ( a₁ in b₁ & b₁ in B ) } is set
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₁ where b₁ is Element of the carrier of V : not l . b₁ = 0. R } is set
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₁ where b₁ is Element of bool the carrier of V : ( g in b₁ & b₁ in B ) } is set
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₁ where b₁ is Element of bool the carrier of V : ( g in b₁ & b₁ in B ) } is set
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₁ where b₁ is Element of bool the carrier of V : ( g in b₁ & b₁ in B ) } is set
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₆ is Element of bool the carrier of V
(R,V,c₆) 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 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₆ \/ {v} is Element of bool the carrier of V
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of c₆ \/ {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₁ where b₁ is Element of the carrier of V : not l . b₁ = 0. R } is set
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₁ where b₁ is Element of the carrier of V : not f . b₁ = 0. R } is set
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₁ where b₁ is Element of the carrier of V : not g . b₁ = 0. R } is set
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₁ where b₁ is Element of bool the carrier of V : ( a₁ in b₁ & b₁ in B ) } is 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
{ b₁ where b₁ is Element of the carrier of V : not l . b₁ = 0. R } is set
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₁ where b₁ is Element of bool the carrier of V : ( g in b₁ & b₁ in B ) } is set
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₁ where b₁ is Element of bool the carrier of V : ( g in b₁ & b₁ in B ) } is set
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₁ where b₁ is Element of bool the carrier of V : ( g in b₁ & b₁ in B ) } is set
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₆ is Element of bool the carrier of V
(R,V,c₆) 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 (R,V,c₆) is non empty set
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₁ where b₁ is Element of the carrier of V : not x . b₁ = 0. R } is set
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₆ \/ {v} is Element of bool the carrier of V
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of c₆ \/ {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₁ where b₁ is Element of the carrier of V : not l . b₁ = 0. R } is set
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₁ where b₁ is Element of the carrier of V : not f . b₁ = 0. R } is set
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₁ where b₁ is Element of the carrier of V : not g . b₁ = 0. R } is set
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)