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

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

(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

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

c

rng c

(V * B) (#) c

Sum ((V * B) (#) c

Carrier B is finite Element of bool the carrier of A

{ b

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

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

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

dom c

f is set

dom l is set

x . f is set

dom c

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

c

c

l . f is set

x . f is set

c

x (#) c

c

l (#) (c

f is set

dom (c

rng (l (#) (c

rng (c

c

x (#) (c

id (dom c

[:(dom c

bool [:(dom c

x (#) (id (dom c

[:(Seg (len c

bool [:(Seg (len c

f is Relation-like Seg (len c

len ((V * B) (#) c

dom ((V * B) (#) c

f is Relation-like Seg (len c

((V * B) (#) c

[:(Seg (len c

bool [:(Seg (len c

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

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

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

c

c

f . g is set

((V * B) (#) c

((V * B) (#) c

(V * B) . (c

((V * B) . (c

B . (c

V * (B . (c

(V * (B . (c

(B . (c

V * ((B . (c

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

c

Carrier c

{ b

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

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

Carrier c

{ b

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

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

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

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

c

c

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

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

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

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

c

(B * A) + (c

B " is V22() V23() V24() Element of REAL

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

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

(B ") * (c

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

(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 ") * c

((B ") * c

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

1 * A is Element of the carrier of V

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

A + (((B ") * c

- (((B ") * c

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

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

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

c

(c

(c

(c

((c

(c

((c

(((c

(c

((c

(((c

1 * B is Element of the carrier of V

(((c

(((c

- (((c

(- 1) * (((c

(- 1) * ((c

((- 1) * ((c

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

B is set

c

Sum c

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

Sum c

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

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

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

c

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

{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

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

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

Sum c

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

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

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

Sum c

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

Sum c

Carrier c

{ b

(Carrier c

(Carrier c

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

c

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

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

c

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

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

(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

(c

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