:: RLVECT_3 semantic presentation

REAL is non empty non trivial non finite set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL
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
COMPLEX is non empty non trivial non finite set
RAT is non empty non trivial non finite set
INT is non empty non trivial non finite set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
{} is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() V24() finite V40() set
the Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() V24() finite V40() set is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() V24() finite V40() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
0 is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() V24() finite V40() Element of NAT
- 1 is V22() V23() V24() Element of REAL
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
[: the carrier of V,REAL:] is non empty set
bool [: the carrier of V,REAL:] is non empty set
A is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
B is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
A ^ B is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
B is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of bool [: the carrier of V,REAL:]
B (#) (A ^ B) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
B (#) A is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
B (#) B is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
(B (#) A) ^ (B (#) B) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
len ((B (#) A) ^ (B (#) B)) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
len (B (#) A) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
len (B (#) B) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
(len (B (#) A)) + (len (B (#) B)) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
len A is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
(len A) + (len (B (#) B)) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
len B is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
(len A) + (len B) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
len (A ^ B) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom ((B (#) A) ^ (B (#) B)) is set
dom (B (#) A) is set
dom A is set
dom (A ^ B) is set
A /. l is Element of the carrier of V
A . l is set
(A ^ B) . l is set
(A ^ B) /. l is Element of the carrier of V
((B (#) A) ^ (B (#) B)) . l is set
(B (#) A) . l is set
B . ((A ^ B) /. l) is V22() V23() V24() Element of REAL
(B . ((A ^ B) /. l)) * ((A ^ B) /. l) is Element of the carrier of V
dom (B (#) B) is set
dom (A ^ B) is set
x is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() set
(len (B (#) A)) + x is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() set
(len (B (#) A)) + x is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom B is set
B /. x is Element of the carrier of V
B . x is set
(A ^ B) . l is set
(A ^ B) /. l is Element of the carrier of V
((B (#) A) ^ (B (#) B)) . l is set
(B (#) B) . x is set
B . ((A ^ B) /. l) is V22() V23() V24() Element of REAL
(B . ((A ^ B) /. l)) * ((A ^ B) /. l) is Element of the carrier of V
dom (B (#) A) is set
dom (B (#) B) is set
((B (#) A) ^ (B (#) B)) . l is set
(A ^ B) /. l is Element of the carrier of V
B . ((A ^ B) /. l) is V22() V23() V24() Element of REAL
(B . ((A ^ B) /. l)) * ((A ^ B) /. l) is Element of the carrier of V
((B (#) A) ^ (B (#) B)) . l is set
(A ^ B) /. l is Element of the carrier of V
B . ((A ^ B) /. l) is V22() V23() V24() Element of REAL
(B . ((A ^ B) /. l)) * ((A ^ B) /. l) is Element of the carrier of V
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
A is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
Sum A is Element of the carrier of V
B is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
A + B is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
Sum (A + B) is Element of the carrier of V
Sum B is Element of the carrier of V
(Sum A) + (Sum B) is Element of the carrier of V
Carrier (A + B) is finite Element of bool the carrier of V
bool the carrier of V is non empty set
{ b₁ where b₁ is Element of the carrier of V : not (A + B) . b₁ = 0 } is set
B is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
rng B is set
(A + B) (#) B is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
Sum ((A + B) (#) B) is Element of the carrier of V
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 } is set
(Carrier (A + B)) \/ (Carrier A) is finite Element of bool 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 } is set
((Carrier (A + B)) \/ (Carrier A)) \/ (Carrier B) is finite Element of bool the carrier of V
(((Carrier (A + B)) \/ (Carrier A)) \/ (Carrier B)) \ (Carrier (A + B)) is finite Element of bool the carrier of V
l is Relation-like Function-like FinSequence-like set
rng l is set
x is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
B ^ x is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
(Carrier A) \/ (Carrier B) is finite Element of bool the carrier of V
(Carrier (A + B)) \/ ((Carrier A) \/ (Carrier B)) is finite Element of bool the carrier of V
rng x is set
(rng B) /\ (rng x) is set
the Element of (rng B) /\ (rng x) is Element of (rng B) /\ (rng x)
len x is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
(A + B) (#) x is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
len ((A + B) (#) x) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom x is set
x /. f is Element of the carrier of V
x . f is set
dom ((A + B) (#) x) is set
((A + B) (#) x) . f is set
(A + B) . (x /. f) is V22() V23() V24() Element of REAL
((A + B) . (x /. f)) * (x /. f) is Element of the carrier of V
0 * (x /. f) is Element of the carrier of V
Sum ((A + B) (#) x) is Element of the carrier of V
Sum x is Element of the carrier of V
0 * (Sum x) is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
(A + B) (#) (B ^ x) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
(((Carrier (A + B)) \/ (Carrier A)) \/ (Carrier B)) \ (Carrier A) is finite Element of bool the carrier of V
g is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
rng g is set
A (#) g is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
Sum (A (#) g) is Element of the carrier of V
g is Relation-like Function-like FinSequence-like set
rng g is set
g is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
g ^ g is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
Sum ((A + B) (#) (B ^ x)) is Element of the carrier of V
((A + B) (#) B) ^ ((A + B) (#) x) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
Sum (((A + B) (#) B) ^ ((A + B) (#) x)) is Element of the carrier of V
(Sum ((A + B) (#) B)) + (0. V) is Element of the carrier of V
(((Carrier (A + B)) \/ (Carrier A)) \/ (Carrier B)) \ (Carrier B) is finite Element of bool the carrier of V
g is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
rng g is set
B (#) g is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
Sum (B (#) g) is Element of the carrier of V
v is Relation-like Function-like FinSequence-like set
rng v is set
q is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
g ^ q is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
rng q is set
(rng g) /\ (rng q) is set
the Element of (rng g) /\ (rng q) is Element of (rng g) /\ (rng q)
B (#) (g ^ q) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
(Carrier (A + B)) \/ (Carrier B) is finite Element of bool the carrier of V
(Carrier A) \/ ((Carrier (A + B)) \/ (Carrier B)) is finite Element of bool the carrier of V
rng (g ^ g) is set
rng g is set
(rng g) \/ (rng g) is set
(Carrier A) \/ (((Carrier (A + B)) \/ (Carrier A)) \/ (Carrier B)) is finite Element of bool the carrier of V
len q is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
B (#) q is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
len (B (#) q) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom q is set
q /. g is Element of the carrier of V
q . g is set
dom (B (#) q) is set
(B (#) q) . g is set
B . (q /. g) is V22() V23() V24() Element of REAL
(B . (q /. g)) * (q /. g) is Element of the carrier of V
0 * (q /. g) is Element of the carrier of V
Sum (B (#) q) is Element of the carrier of V
Sum q is Element of the carrier of V
0 * (Sum q) is Element of the carrier of V
Sum (B (#) (g ^ q)) is Element of the carrier of V
(B (#) g) ^ (B (#) q) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
Sum ((B (#) g) ^ (B (#) q)) is Element of the carrier of V
(Sum (B (#) g)) + (0. V) is Element of the carrier of V
A (#) (g ^ g) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
len (B ^ x) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
P is Relation-like Function-like FinSequence-like set
len P is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom P is set
Seg (len (B ^ x)) is Element of bool NAT
len g is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
A (#) g is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
len (A (#) g) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
P is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom g is set
g /. P is Element of the carrier of V
g . P is set
dom (A (#) g) is set
(A (#) g) . P is set
A . (g /. P) is V22() V23() V24() Element of REAL
(A . (g /. P)) * (g /. P) is Element of the carrier of V
0 * (g /. P) is Element of the carrier of V
Sum (A (#) g) is Element of the carrier of V
Sum g is Element of the carrier of V
0 * (Sum g) is Element of the carrier of V
Sum (A (#) (g ^ g)) is Element of the carrier of V
(A (#) g) ^ (A (#) g) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
Sum ((A (#) g) ^ (A (#) g)) is Element of the carrier of V
(Sum (A (#) g)) + (0. V) is Element of the carrier of V
rng (B ^ x) is set
(rng B) \/ (rng x) is set
(Carrier (A + B)) \/ (((Carrier (A + B)) \/ (Carrier A)) \/ (Carrier B)) is finite Element of bool the carrier of V
(rng g) /\ (rng g) is set
the Element of (rng g) /\ (rng g) is Element of (rng g) /\ (rng g)
len (g ^ g) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
P is set
dom (g ^ g) is set
P is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
(g ^ g) . P is set
P . P is set
(B ^ x) . (P . P) is set
(B ^ x) <- ((g ^ g) . P) is set
(B ^ x) . ((B ^ x) <- ((g ^ g) . P)) is set
(g ^ g) . P is set
P . P is set
(B ^ x) . (P . P) is set
rng P is set
P is set
P is set
P . P is set
Fp is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
(g ^ g) . Fp is set
P . Fp is set
(B ^ x) <- ((g ^ g) . Fp) is set
dom (B ^ x) is set
P is set
P . P is set
dom (B ^ x) is set
Seg (len P) is Element of bool NAT
Seg (len P) is Element of bool NAT
P (#) (B ^ x) is Relation-like Function-like set
(B ^ x) " is Relation-like Function-like set
(g ^ g) (#) ((B ^ x) ") is Relation-like Function-like set
P is set
dom ((B ^ x) ") is set
rng ((g ^ g) (#) ((B ^ x) ")) is set
rng ((B ^ x) ") is set
(B ^ x) (#) ((B ^ x) ") is Relation-like Function-like set
P (#) ((B ^ x) (#) ((B ^ x) ")) is Relation-like Function-like set
id (dom (B ^ x)) is Relation-like dom (B ^ x) -defined dom (B ^ x) -valued Function-like one-to-one total Element of bool [:(dom (B ^ x)),(dom (B ^ x)):]
[:(dom (B ^ x)),(dom (B ^ x)):] is set
bool [:(dom (B ^ x)),(dom (B ^ x)):] is non empty set
P (#) (id (dom (B ^ x))) is Relation-like Function-like set
[:(Seg (len (B ^ x))),(Seg (len (B ^ x))):] is set
bool [:(Seg (len (B ^ x))),(Seg (len (B ^ x))):] is non empty set
P is Relation-like Seg (len (B ^ x)) -defined Seg (len (B ^ x)) -valued Function-like quasi_total Element of bool [:(Seg (len (B ^ x))),(Seg (len (B ^ x))):]
len ((A + B) (#) (B ^ x)) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom ((A + B) (#) (B ^ x)) is set
P is Relation-like Seg (len (B ^ x)) -defined Seg (len (B ^ x)) -valued Function-like quasi_total bijective Element of bool [:(Seg (len (B ^ x))),(Seg (len (B ^ x))):]
((A + B) (#) (B ^ x)) * P is Relation-like Seg (len (B ^ x)) -defined the carrier of V -valued Function-like Element of bool [:(Seg (len (B ^ x))), the carrier of V:]
[:(Seg (len (B ^ x))), the carrier of V:] is set
bool [:(Seg (len (B ^ x))), the carrier of V:] is non empty set
len (A (#) (g ^ g)) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
len (g ^ q) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
R is Relation-like Function-like FinSequence-like set
len R is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom R is set
Seg (len (g ^ q)) is Element of bool NAT
rng (g ^ q) is set
(rng g) \/ (rng q) is set
(Carrier B) \/ (((Carrier (A + B)) \/ (Carrier A)) \/ (Carrier B)) is finite Element of bool the carrier of V
R is set
R is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
(g ^ g) . R is set
R . R is set
(g ^ q) . (R . R) is set
(g ^ q) <- ((g ^ g) . R) is set
(g ^ q) . ((g ^ q) <- ((g ^ g) . R)) is set
(g ^ g) . R is set
R . R is set
(g ^ q) . (R . R) is set
rng R is set
R is set
R is set
R . R is set
Hp is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
(g ^ g) . Hp is set
R . Hp is set
(g ^ q) <- ((g ^ g) . Hp) is set
dom (g ^ q) is set
R is set
R . R is set
dom (g ^ q) is set
Seg (len R) is Element of bool NAT
Seg (len R) is Element of bool NAT
R (#) (g ^ q) is Relation-like Function-like set
(g ^ q) " is Relation-like Function-like set
(g ^ g) (#) ((g ^ q) ") is Relation-like Function-like set
R is set
dom ((g ^ q) ") is set
rng ((g ^ g) (#) ((g ^ q) ")) is set
rng ((g ^ q) ") is set
(g ^ q) (#) ((g ^ q) ") is Relation-like Function-like set
R (#) ((g ^ q) (#) ((g ^ q) ")) is Relation-like Function-like set
id (dom (g ^ q)) is Relation-like dom (g ^ q) -defined dom (g ^ q) -valued Function-like one-to-one total Element of bool [:(dom (g ^ q)),(dom (g ^ q)):]
[:(dom (g ^ q)),(dom (g ^ q)):] is set
bool [:(dom (g ^ q)),(dom (g ^ q)):] is non empty set
R (#) (id (dom (g ^ q))) is Relation-like Function-like set
[:(Seg (len (g ^ q))),(Seg (len (g ^ q))):] is set
bool [:(Seg (len (g ^ q))),(Seg (len (g ^ q))):] is non empty set
R is Relation-like Seg (len (g ^ q)) -defined Seg (len (g ^ q)) -valued Function-like quasi_total Element of bool [:(Seg (len (g ^ q))),(Seg (len (g ^ q))):]
len (B (#) (g ^ q)) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom (B (#) (g ^ q)) is set
R is Relation-like Seg (len (g ^ q)) -defined Seg (len (g ^ q)) -valued Function-like quasi_total bijective Element of bool [:(Seg (len (g ^ q))),(Seg (len (g ^ q))):]
(B (#) (g ^ q)) * R is Relation-like Seg (len (g ^ q)) -defined the carrier of V -valued Function-like Element of bool [:(Seg (len (g ^ q))), the carrier of V:]
[:(Seg (len (g ^ q))), the carrier of V:] is set
bool [:(Seg (len (g ^ q))), the carrier of V:] is non empty set
Hp is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
len Hp is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
I is Relation-like Function-like FinSequence-like set
len I is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom I is set
Seg (len (g ^ g)) is Element of bool NAT
I is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
I . I is set
(A (#) (g ^ g)) /. I is Element of the carrier of V
Hp /. I is Element of the carrier of V
((A (#) (g ^ g)) /. I) + (Hp /. I) is Element of the carrier of V
rng I is set
I is set
x is set
I . x is set
k is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
I . k is set
(A (#) (g ^ g)) /. k is Element of the carrier of V
Hp /. k is Element of the carrier of V
((A (#) (g ^ g)) /. k) + (Hp /. k) is Element of the carrier of V
Fp is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
len Fp is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
I is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
len I is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
x is set
dom I is set
dom Hp is set
k is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom R is set
R . k is set
(g ^ g) /. k is Element of the carrier of V
j is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
(g ^ q) . j is set
(g ^ g) . k is set
(B (#) (g ^ q)) . j is set
B . ((g ^ g) /. k) is V22() V23() V24() Element of REAL
(B . ((g ^ g) /. k)) * ((g ^ g) /. k) is Element of the carrier of V
dom P is set
P . k is set
dom Fp is set
Fp . k is set
((A + B) (#) (B ^ x)) . (P . k) is set
Hp /. k is Element of the carrier of V
((B (#) (g ^ q)) * R) . k is set
(B (#) (g ^ q)) . (R . k) is set
dom (A (#) (g ^ g)) is set
l is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
(B ^ x) . l is set
((A + B) (#) (B ^ x)) . l is set
(A + B) . ((g ^ g) /. k) is V22() V23() V24() Element of REAL
((A + B) . ((g ^ g) /. k)) * ((g ^ g) /. k) is Element of the carrier of V
A . ((g ^ g) /. k) is V22() V23() V24() Element of REAL
(A . ((g ^ g) /. k)) + (B . ((g ^ g) /. k)) is V22() V23() V24() Element of REAL
((A . ((g ^ g) /. k)) + (B . ((g ^ g) /. k))) * ((g ^ g) /. k) is Element of the carrier of V
(A . ((g ^ g) /. k)) * ((g ^ g) /. k) is Element of the carrier of V
((A . ((g ^ g) /. k)) * ((g ^ g) /. k)) + ((B . ((g ^ g) /. k)) * ((g ^ g) /. k)) is Element of the carrier of V
(A (#) (g ^ g)) /. k is Element of the carrier of V
(A (#) (g ^ g)) . k is set
I . x is set
Fp . x is set
Seg (len (B (#) (g ^ q))) is Element of bool NAT
Sum Hp is Element of the carrier of V
Seg (len ((A + B) (#) (B ^ x))) is Element of bool NAT
Sum Fp is Element of the carrier of V
Seg (len I) is Element of bool NAT
V is V22() V23() V24() Element of REAL
A is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of A is non empty set
B is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total Linear_Combination of A
V * B is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total Linear_Combination of A
Sum (V * B) is Element of the carrier of A
Sum B is Element of the carrier of A
V * (Sum B) is Element of the carrier of A
Carrier (V * B) is finite Element of bool the carrier of A
bool the carrier of A is non empty set
{ b₁ where b₁ is Element of the carrier of A : not (V * B) . b₁ = 0 } is set
c₅ is Relation-like NAT -defined the carrier of A -valued Function-like FinSequence-like FinSequence of the carrier of A
rng c₅ is set
(V * B) (#) c₅ is Relation-like NAT -defined the carrier of A -valued Function-like FinSequence-like FinSequence of the carrier of A
Sum ((V * B) (#) c₅) is Element of the carrier of A
Carrier B is finite Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not B . b₁ = 0 } is set
l is Relation-like NAT -defined the carrier of A -valued Function-like FinSequence-like FinSequence of the carrier of A
rng l is set
B (#) l is Relation-like NAT -defined the carrier of A -valued Function-like FinSequence-like FinSequence of the carrier of A
Sum (B (#) l) is Element of the carrier of A
len l is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
len c₅ is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
x is Relation-like Function-like FinSequence-like set
len x is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom x is set
rng x is set
Seg (len c₅) is Element of bool NAT
f is set
f is set
x . f is set
f is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom l is set
l . f is set
x . f is set
c₅ <- (l . f) is set
dom c₅ is set
f is set
dom l is set
x . f is set
dom c₅ is set
Seg (len x) is Element of bool NAT
Seg (len x) is Element of bool NAT
f is set
f is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
l . f is set
x . f is set
c₅ . (x . f) is set
c₅ <- (l . f) is set
c₅ . (c₅ <- (l . f)) is set
l . f is set
x . f is set
c₅ . (x . f) is set
x (#) c₅ is Relation-like Function-like set
c₅ " is Relation-like Function-like set
l (#) (c₅ ") is Relation-like Function-like set
f is set
dom (c₅ ") is set
rng (l (#) (c₅ ")) is set
rng (c₅ ") is set
c₅ (#) (c₅ ") is Relation-like Function-like set
x (#) (c₅ (#) (c₅ ")) is Relation-like Function-like set
id (dom c₅) is Relation-like dom c₅ -defined dom c₅ -valued Function-like one-to-one total Element of bool [:(dom c₅),(dom c₅):]
[:(dom c₅),(dom c₅):] is set
bool [:(dom c₅),(dom c₅):] is non empty set
x (#) (id (dom c₅)) is Relation-like Function-like set
[:(Seg (len c₅)),(Seg (len c₅)):] is set
bool [:(Seg (len c₅)),(Seg (len c₅)):] is non empty set
f is Relation-like Seg (len c₅) -defined Seg (len c₅) -valued Function-like quasi_total Element of bool [:(Seg (len c₅)),(Seg (len c₅)):]
len ((V * B) (#) c₅) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom ((V * B) (#) c₅) is set
f is Relation-like Seg (len c₅) -defined Seg (len c₅) -valued Function-like quasi_total bijective Element of bool [:(Seg (len c₅)),(Seg (len c₅)):]
((V * B) (#) c₅) * f is Relation-like Seg (len c₅) -defined the carrier of A -valued Function-like Element of bool [:(Seg (len c₅)), the carrier of A:]
[:(Seg (len c₅)), the carrier of A:] is set
bool [:(Seg (len c₅)), the carrier of A:] is non empty set
Seg (len ((V * B) (#) c₅)) is Element of bool NAT
f is Relation-like NAT -defined the carrier of A -valued Function-like FinSequence-like FinSequence of the carrier of A
Sum f is Element of the carrier of A
len f is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
len (B (#) l) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom (B (#) l) is set
g is Element of the carrier of A
(B (#) l) . g is set
l . g is set
c₅ <- (l . g) is set
g is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom f is set
l /. g is Element of the carrier of A
f . g is set
c₅ . (f . g) is set
c₅ . g is set
c₅ /. g is Element of the carrier of A
f . g is set
((V * B) (#) c₅) . (f . g) is set
((V * B) (#) c₅) . (c₅ <- (l . g)) is set
(V * B) . (c₅ /. g) is V22() V23() V24() Element of REAL
((V * B) . (c₅ /. g)) * (c₅ /. g) is Element of the carrier of A
B . (c₅ /. g) is V22() V23() V24() Element of REAL
V * (B . (c₅ /. g)) is V22() V23() V24() Element of REAL
(V * (B . (c₅ /. g))) * (c₅ /. g) is Element of the carrier of A
(B . (c₅ /. g)) * (c₅ /. g) is Element of the carrier of A
V * ((B . (c₅ /. g)) * (c₅ /. g)) is Element of the carrier of A
V * g is Element of the carrier of A
dom f is set
ZeroLC A is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total Linear_Combination of A
Sum (ZeroLC A) is Element of the carrier of A
0. A is V55(A) Element of the carrier of A
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
A is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
- A is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
(- 1) * A is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
Sum (- A) is Element of the carrier of V
Sum A is Element of the carrier of V
- (Sum A) is Element of the carrier of V
(- 1) * (Sum A) is Element of the carrier of V
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
A is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
Sum A is Element of the carrier of V
B is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
A - B is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
- B is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
(- 1) * B is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
A + (- B) is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
Sum (A - B) is Element of the carrier of V
Sum B is Element of the carrier of V
(Sum A) - (Sum B) is Element of the carrier of V
Sum (- B) is Element of the carrier of V
(Sum A) + (Sum (- B)) is Element of the carrier of V
- (Sum B) is Element of the carrier of V
(Sum A) + (- (Sum B)) is Element of the carrier of V
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty set
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty set
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
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 Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of A
Sum B is Element of the carrier of V
0. V is V55(V) 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 } is set
c₅ is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of B
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 } is set
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty set
0. V is V55(V) Element of the carrier of V
A is Element of bool the carrier of V
[: the carrier of V,REAL:] is non empty set
bool [: the carrier of V,REAL:] is non empty set
B is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of bool [: the carrier of V,REAL:]
B . (0. V) is V22() V23() V24() Element of REAL
Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL
B is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of Funcs ( the carrier of V,REAL)
{(0. V)} is non empty finite Element of bool the carrier of V
c₅ is non empty finite Element of bool the carrier of V
v is Element of the carrier of V
B . v is V22() V23() V24() Element of REAL
v is finite Element of bool the carrier of V
c₅ is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination 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 } is set
{(0. V)} is non empty finite Element of bool the carrier of V
v is set
l is Element of the carrier of V
c₅ . l is V22() V23() V24() Element of REAL
v is set
v is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of A
Sum v is Element of the carrier of V
v . (0. V) is V22() V23() V24() Element of REAL
(v . (0. V)) * (0. V) is Element of the carrier of V
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
{} the carrier of V is Function-like functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() V24() finite V40() Element of bool the carrier of V
bool the carrier of V is non empty set
A is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of {} the carrier of V
Sum A is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
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 } is set
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty set
{} the carrier of V is Function-like functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() V24() finite V40() Element of bool the carrier of V
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
0. V is V55(V) Element of the carrier of V
A is Element of the carrier of V
{A} is non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set
B is Relation-like the carrier of V -defined REAL -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 } is set
B . A is V22() V23() V24() Element of REAL
(B . A) * A is Element of the carrier of V
B is Element of the carrier of V
B . B is V22() V23() V24() Element of REAL
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
0. V is V55(V) Element of the carrier of V
{(0. V)} is non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
0. V is V55(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 non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
B is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of B is non empty set
A is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
{A,(0. V)} is non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set
0. B is V55(B) Element of the carrier of B
B is Element of the carrier of B
{(0. B),B} is non empty finite Element of bool the carrier of B
bool the carrier of B is non empty set
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
0. V is V55(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 non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set
B is V22() V23() V24() Element of REAL
B * B is Element of the carrier of V
[: the carrier of V,REAL:] is non empty set
bool [: the carrier of V,REAL:] is non empty set
c₅ is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of bool [: the carrier of V,REAL:]
c₅ . A is V22() V23() V24() Element of REAL
c₅ . B is V22() V23() V24() Element of REAL
Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL
l is Element of the carrier of V
v is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of Funcs ( the carrier of V,REAL)
v . l is V22() V23() V24() Element of REAL
l is Relation-like the carrier of V -defined REAL -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 } is set
x is set
f is Element of the carrier of V
l . f is V22() V23() V24() Element of REAL
x is Relation-like the carrier of V -defined REAL -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 } is set
Sum x is Element of the carrier of V
(- 1) * (B * B) is Element of the carrier of V
((- 1) * (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
(B * B) - (B * B) is Element of the carrier of V
- ((B * B) - (B * B)) is Element of the carrier of V
- (0. V) is Element of the carrier of V
1 * B is Element of the carrier of V
B is Relation-like the carrier of V -defined REAL -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 } is set
B . A is V22() V23() V24() Element of REAL
(B . A) * A is Element of the carrier of V
B . B is V22() V23() V24() Element of REAL
(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 V22() V23() V24() Element of REAL
((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 V22() V23() V24() Element of REAL
(((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 V22() V23() V24() Element of REAL
(((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 * A is Element of the carrier of V
(1 * 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) * ((((B . A) ") * (B . B)) * B) is Element of the carrier of V
(- 1) * (((B . A) ") * (B . B)) is V22() V23() V24() Element of REAL
((- 1) * (((B . A) ") * (B . B))) * B is Element of the carrier of V
(B . B) " is V22() V23() V24() Element of REAL
((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 V22() V23() V24() Element of REAL
(((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 . B) is V22() V23() V24() Element of REAL
(((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)) * A) + (1 * B) is Element of the carrier of V
0 * A is Element of the carrier of V
(0 * 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 V22() V23() V24() Element of REAL
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
0. V is V55(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 non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set
B is V22() V23() V24() Element of REAL
B * A is Element of the carrier of V
c₅ is V22() V23() V24() Element of REAL
c₅ * B is Element of the carrier of V
(B * A) + (c₅ * B) is Element of the carrier of V
B " is V22() V23() V24() Element of REAL
(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 V22() V23() V24() Element of REAL
((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 V22() V23() V24() Element of REAL
((B ") * c₅) * B is Element of the carrier of V
(((B ") * B) * A) + (((B ") * c₅) * B) is Element of the carrier of V
1 * A is Element of the carrier of V
(1 * 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) * (((B ") * c₅) * B) is Element of the carrier of V
(- 1) * ((B ") * c₅) is V22() V23() V24() Element of REAL
((- 1) * ((B ") * c₅)) * B is Element of the carrier of V
c₅ " is V22() V23() V24() Element of REAL
(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 V22() V23() V24() Element of REAL
((c₅ ") * B) * A is Element of the carrier of V
(((c₅ ") * B) * A) + ((c₅ ") * (c₅ * B)) is Element of the carrier of V
(c₅ ") * c₅ is V22() V23() V24() Element of REAL
((c₅ ") * c₅) * B is Element of the carrier of V
(((c₅ ") * B) * A) + (((c₅ ") * c₅) * B) is Element of the carrier of V
1 * B is Element of the carrier of V
(((c₅ ") * B) * A) + (1 * 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) * (((c₅ ") * B) * A) is Element of the carrier of V
(- 1) * ((c₅ ") * B) is V22() V23() V24() Element of REAL
((- 1) * ((c₅ ") * B)) * A is Element of the carrier of V
B is V22() V23() V24() Element of REAL
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 * 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 V
B * (- B) is Element of the carrier of V
A + (B * (- B)) is Element of the carrier of V
- B is V22() V23() V24() Element of REAL
(- B) * B is Element of the carrier of V
A + ((- B) * B) is Element of the carrier of V
1 * A is Element of the carrier of V
(1 * A) + ((- B) * B) is Element of the carrier of V
(0. V) + (0. V) is Element of the carrier of V
0 * A is Element of the carrier of V
(0 * A) + (0. V) is Element of the carrier of V
1 * B is Element of the carrier of V
(0 * A) + (1 * B) is Element of the carrier of V
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
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
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of A : verum } is set
B is set
c₅ is Relation-like the carrier of V -defined REAL -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 REAL -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 REAL -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 REAL -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 REAL -valued Function-like quasi_total Linear_Combination of V
f is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of A
Sum f is Element of the carrier of V
v is V22() V23() V24() Element of REAL
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 REAL -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 REAL -valued Function-like quasi_total Linear_Combination of V
f is Relation-like the carrier of V -defined REAL -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 REAL -valued Function-like quasi_total Linear_Combination of A
Sum c₅ is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
B is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
the carrier of B is non empty set
B is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
the carrier of B is non empty set
V is set
A is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
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
(A,B) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of A
the carrier of (A,B) is non empty set
{ (Sum b₁) where b₁ is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total Linear_Combination of B : verum } is set
B is Relation-like the carrier of A -defined REAL -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 REAL -valued Function-like quasi_total Linear_Combination of B : verum } is set
the carrier of (A,B) is non empty set
V is set
A is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
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
(A,B) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of A
[: the carrier of A,REAL:] is non empty set
bool [: the carrier of A,REAL:] is non empty set
B is Element of the carrier of A
c₅ is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total Element of bool [: the carrier of A,REAL:]
c₅ . B is V22() V23() V24() Element of REAL
Funcs ( the carrier of A,REAL) is non empty FUNCTION_DOMAIN of the carrier of A, REAL
v is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total Element of Funcs ( the carrier of A,REAL)
{B} is non empty finite Element of bool the carrier of A
l is non empty finite Element of bool the carrier of A
x is Element of the carrier of A
v . x is V22() V23() V24() Element of REAL
x is finite Element of bool the carrier of A
l is Relation-like the carrier of A -defined REAL -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 } is set
{B} is non empty finite Element of bool the carrier of A
x is set
f is Element of the carrier of A
l . f is V22() V23() V24() Element of REAL
x is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total Linear_Combination of {B}
Sum x is Element of the carrier of A
1 * 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 } is set
f is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total Linear_Combination of B
Sum f is Element of the carrier of A
V is set
A is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
(0). A is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of A
0. A is V55(A) Element of the carrier of A
the carrier of A is non empty set
the carrier of ((0). A) is non empty set
{(0. A)} is non empty finite Element of bool the carrier of A
bool the carrier of A is non empty set
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
{} the carrier of V is Function-like functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() V24() finite V40() Element of bool the carrier of V
bool the carrier of V is non empty set
(V,({} the carrier of V)) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
(0). V is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is Element of the carrier of V
the carrier of (V,({} the carrier of V)) is non empty set
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of {} the carrier of V : verum } is set
0. V is V55(V) Element of the carrier of V
B is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of {} the carrier of V
Sum B is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty set
(0). V is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
0. V is V55(V) Element of the carrier of V
{(0. V)} is non empty finite Element of bool the carrier of V
A is Element of bool the carrier of V
(V,A) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is set
the Element of A is Element of A
B is set
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
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
(V,A) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() 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 REAL -valued Function-like quasi_total Linear_Combination of A
Sum c₅ is Element of the carrier of V
V is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
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
(V,A) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
(Omega). V is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
the ZeroF of V is Element of the carrier of V
the U5 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 Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) is non empty strict RLSStruct
the carrier of ((Omega). V) is non empty set
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
A is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
A /\ B is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
A is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B /\ B is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
the carrier of V is non empty set
c₅ is Element of the carrier of V
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
A is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B + B is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
A is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
A + B is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
the carrier of V is non empty set
c₅ is Element of 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
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
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
(V,A) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is Element of bool the carrier of V
(V,B) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is Element of the carrier of V
c₅ is Relation-like the carrier of V -defined REAL -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 REAL -valued Function-like quasi_total Linear_Combination of B
Sum v is Element of the carrier of V
V is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
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
(V,A) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is Element of bool the carrier of V
(V,B) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
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
(V,A) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is Element of bool the carrier of V
A \/ B is Element of bool the carrier of V
(V,(A \/ B)) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
(V,B) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
(V,A) + (V,B) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is Element of the carrier of V
c₅ is Relation-like the carrier of V -defined REAL -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 } 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
[: the carrier of V,REAL:] is non empty set
bool [: the carrier of V,REAL:] is non empty set
f is Element of the carrier of V
f is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of bool [: the carrier of V,REAL:]
f . f is V22() V23() V24() Element of REAL
c₅ . x is set
x is set
c₅ . x is set
x is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of bool [: the carrier of V,REAL:]
Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL
f is finite Element of bool the carrier of V
f is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of Funcs ( the carrier of V,REAL)
f is Element of the carrier of V
f . f is V22() V23() V24() Element of REAL
f is Relation-like the carrier of V -defined REAL -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 } is set
g is set
g is Element of the carrier of V
f . g is V22() V23() V24() Element of REAL
g is set
g is Element of the carrier of V
g is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of bool [: the carrier of V,REAL:]
g . g is V22() V23() V24() Element of REAL
c₅ . g is set
g is set
c₅ . g is set
g is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of bool [: the carrier of V,REAL:]
g is finite Element of bool the carrier of V
g is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of Funcs ( the carrier of V,REAL)
u is Element of the carrier of V
g . u is V22() V23() V24() Element of REAL
g is set
u is Relation-like the carrier of V -defined REAL -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 } is set
g is set
v is Element of the carrier of V
u . v is V22() V23() V24() Element of REAL
g is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of A
g is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of B
g + g is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
v is Element of the carrier of V
c₅ . v is V22() V23() V24() Element of REAL
(g + g) . v is V22() V23() V24() Element of REAL
g . v is V22() V23() V24() Element of REAL
g . v is V22() V23() V24() Element of REAL
(g . v) + (g . v) is V22() V23() V24() Element of REAL
(c₅ . v) + (g . v) is V22() V23() V24() Element of REAL
(c₅ . v) + 0 is V22() V23() V24() Element of REAL
g . v is V22() V23() V24() Element of REAL
g . v is V22() V23() V24() Element of REAL
(g . v) + (g . v) is V22() V23() V24() Element of REAL
0 + (g . v) is V22() V23() V24() Element of REAL
g . v is V22() V23() V24() Element of REAL
g . v is V22() V23() V24() Element of REAL
(g . v) + (g . v) is V22() V23() V24() Element of REAL
0 + (g . v) is V22() V23() V24() Element of REAL
0 + 0 is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
Sum g is Element of the carrier of V
Sum g is Element of the carrier of V
(Sum g) + (Sum g) is Element of the carrier of V
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
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
(V,A) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is Element of bool the carrier of V
A /\ B is Element of bool the carrier of V
(V,(A /\ B)) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
(V,B) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
(V,A) /\ (V,B) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
V is non empty set
union V is set
A is Relation-like V -defined union V -valued Function-like quasi_total Choice_Function of V
dom A is set
the Element of V is Element of V
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
the U5 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 Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) is non empty strict RLSStruct
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
l is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of v
Sum l is Element of the carrier of V
0. V is V55(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 } 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
(Omega). V is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is set
c₅ is Element of bool the carrier of V
(V,c₅) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
v is Element of the carrier of V
{v} is non empty finite Element of bool the carrier of V
c₅ \/ {v} is non empty Element of bool the carrier of V
l is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of c₅ \/ {v}
Sum l is Element of the carrier of V
0. V is V55(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 } is set
l . v is V22() V23() V24() Element of REAL
- (l . v) is V22() V23() V24() Element of REAL
[: the carrier of V,REAL:] is non empty set
bool [: the carrier of V,REAL:] is non empty set
x is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of bool [: the carrier of V,REAL:]
x . v is V22() V23() V24() Element of REAL
Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL
f is Element of the carrier of V
(Carrier l) \ {v} is finite Element of bool the carrier of V
l . f is V22() V23() V24() Element of REAL
f is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of Funcs ( the carrier of V,REAL)
f . f is V22() V23() V24() Element of REAL
f is Relation-like the carrier of V -defined REAL -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 } is set
f is set
g is Element of the carrier of V
f . g is V22() V23() V24() Element of REAL
l . g is V22() V23() V24() Element of REAL
g is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of bool [: the carrier of V,REAL:]
g . v is V22() V23() V24() Element of REAL
g is Element of the carrier of V
g is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of Funcs ( the carrier of V,REAL)
g . g is V22() V23() V24() Element of REAL
g is Relation-like the carrier of V -defined REAL -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 } is set
g is set
u is Element of the carrier of V
g . u is V22() V23() V24() Element of REAL
g is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of {v}
Sum g is Element of the carrier of V
(- (l . v)) * v is Element of the carrier of V
f is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of c₅
f - g is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
- g is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
(- 1) * g is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
f + (- g) is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
u is Element of the carrier of V
(f - g) . u is V22() V23() V24() Element of REAL
l . u is V22() V23() V24() Element of REAL
f . u is V22() V23() V24() Element of REAL
g . u is V22() V23() V24() Element of REAL
(f . u) - (g . u) is V22() V23() V24() Element of REAL
f . u is V22() V23() V24() Element of REAL
g . u is V22() V23() V24() Element of REAL
(f . u) - (g . u) is V22() V23() V24() Element of REAL
(l . u) - (g . u) is V22() V23() V24() Element of REAL
(l . u) - 0 is V22() V23() V24() Element of REAL
Sum f is Element of the carrier of V
(Sum f) - (Sum g) is Element of the carrier of V
(0. V) + (Sum g) is Element of the carrier of V
(- (l . v)) " is V22() V23() V24() Element of REAL
((- (l . v)) ") * ((- (l . v)) * v) is Element of the carrier of V
((- (l . v)) ") * (- (l . v)) is V22() V23() V24() Element of REAL
(((- (l . v)) ") * (- (l . v))) * v is Element of the carrier of V
1 * v is Element of the carrier of V
x is set
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
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
(V,A) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace 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
l is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of v
Sum l is Element of the carrier of V
0. V is V55(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 } 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 Function-like functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() V24() finite V40() Element of bool the carrier of V
B is set
c₅ is Element of bool the carrier of V
(V,c₅) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
the carrier of (V,c₅) is non empty set
l is Element of the carrier of V
x is Relation-like the carrier of V -defined REAL -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 } 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 REAL -valued Function-like quasi_total Linear_Combination of v
Sum f is Element of the carrier of V
(V,v) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
v is Element of the carrier of V
v is Element of the carrier of V
{v} is non empty finite Element of bool the carrier of V
c₅ \/ {v} is non empty Element of bool the carrier of V
l is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of c₅ \/ {v}
Sum l is Element of the carrier of V
0. V is V55(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 } is set
l . v is V22() V23() V24() Element of REAL
- (l . v) is V22() V23() V24() Element of REAL
[: the carrier of V,REAL:] is non empty set
bool [: the carrier of V,REAL:] is non empty set
x is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of bool [: the carrier of V,REAL:]
x . v is V22() V23() V24() Element of REAL
Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL
f is Element of the carrier of V
(Carrier l) \ {v} is finite Element of bool the carrier of V
l . f is V22() V23() V24() Element of REAL
f is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of Funcs ( the carrier of V,REAL)
f . f is V22() V23() V24() Element of REAL
f is Relation-like the carrier of V -defined REAL -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 } is set
f is set
g is Element of the carrier of V
f . g is V22() V23() V24() Element of REAL
l . g is V22() V23() V24() Element of REAL
g is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of bool [: the carrier of V,REAL:]
g . v is V22() V23() V24() Element of REAL
g is Element of the carrier of V
g is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of Funcs ( the carrier of V,REAL)
g . g is V22() V23() V24() Element of REAL
g is Relation-like the carrier of V -defined REAL -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 } is set
g is set
u is Element of the carrier of V
g . u is V22() V23() V24() Element of REAL
g is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of {v}
Sum g is Element of the carrier of V
(- (l . v)) * v is Element of the carrier of V
f is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of c₅
f - g is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
- g is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
(- 1) * g is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
f + (- g) is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of V
u is Element of the carrier of V
(f - g) . u is V22() V23() V24() Element of REAL
l . u is V22() V23() V24() Element of REAL
f . u is V22() V23() V24() Element of REAL
g . u is V22() V23() V24() Element of REAL
(f . u) - (g . u) is V22() V23() V24() Element of REAL
f . u is V22() V23() V24() Element of REAL
g . u is V22() V23() V24() Element of REAL
(f . u) - (g . u) is V22() V23() V24() Element of REAL
(l . u) - (g . u) is V22() V23() V24() Element of REAL
(l . u) - 0 is V22() V23() V24() Element of REAL
Sum f is Element of the carrier of V
(Sum f) - (Sum g) is Element of the carrier of V
(0. V) + (Sum g) is Element of the carrier of V
(- (l . v)) " is V22() V23() V24() Element of REAL
((- (l . v)) ") * ((- (l . v)) * v) is Element of the carrier of V
((- (l . v)) ") * (- (l . v)) is V22() V23() V24() Element of REAL
(((- (l . v)) ") * (- (l . v))) * v is Element of the carrier of V
1 * v is Element of the carrier of V
x is set
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
the U5 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 Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) is non empty strict RLSStruct
{} the carrier of V is Function-like functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() V24() finite V40() Element of bool the carrier of V
A is Element of bool the carrier of V
(V,A) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
V is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
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
(V,B) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is (V)
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
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
(V,A) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is Element of bool the carrier of V
(V,B) is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is (V)
V is non empty set
union V is set
A is Relation-like V -defined union V -valued Function-like quasi_total Choice_Function of V
dom A is set
A is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
(0). A is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of A
V is set
0. A is V55(A) Element of the carrier of A
the carrier of A is non empty set
B is set
B is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
0. B is V55(B) Element of the carrier of B
the carrier of B is non empty set
(0). B is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of B
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
A is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
A /\ B is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
A is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B /\ B is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
A is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
A + B is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
A is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
B + B is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
the carrier of V is non empty set
[: the carrier of V,REAL:] is non empty set
bool [: the carrier of V,REAL:] is non empty set
A is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
B is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
A ^ B is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
B is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of bool [: the carrier of V,REAL:]
B (#) (A ^ B) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
B (#) A is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
B (#) B is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
(B (#) A) ^ (B (#) B) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V