:: RLAFFIN1 semantic presentation

REAL is non empty non trivial non finite V65() V66() V67() V71() set

NAT is non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() Element of K19(REAL)

K19(REAL) is non empty non trivial non finite set

COMPLEX is non empty non trivial non finite V65() V71() set

RAT is non empty non trivial non finite V65() V66() V67() V68() V71() set

INT is non empty non trivial non finite V65() V66() V67() V68() V69() V71() set

K20(COMPLEX,COMPLEX) is Relation-like non empty non trivial non finite V55() set

K19(K20(COMPLEX,COMPLEX)) is non empty non trivial non finite set

K20(K20(COMPLEX,COMPLEX),COMPLEX) is Relation-like non empty non trivial non finite V55() set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is non empty non trivial non finite set

K20(REAL,REAL) is Relation-like non empty non trivial non finite V55() V56() V57() set

K19(K20(REAL,REAL)) is non empty non trivial non finite set

K20(K20(REAL,REAL),REAL) is Relation-like non empty non trivial non finite V55() V56() V57() set

K19(K20(K20(REAL,REAL),REAL)) is non empty non trivial non finite set

K20(RAT,RAT) is Relation-like RAT -valued non empty non trivial non finite V55() V56() V57() set

K19(K20(RAT,RAT)) is non empty non trivial non finite set

K20(K20(RAT,RAT),RAT) is Relation-like RAT -valued non empty non trivial non finite V55() V56() V57() set

K19(K20(K20(RAT,RAT),RAT)) is non empty non trivial non finite set

K20(INT,INT) is Relation-like RAT -valued INT -valued non empty non trivial non finite V55() V56() V57() set

K19(K20(INT,INT)) is non empty non trivial non finite set

K20(K20(INT,INT),INT) is Relation-like RAT -valued INT -valued non empty non trivial non finite V55() V56() V57() set

K19(K20(K20(INT,INT),INT)) is non empty non trivial non finite set

K20(NAT,NAT) is Relation-like RAT -valued INT -valued V55() V56() V57() V58() set

K20(K20(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued V55() V56() V57() V58() set

K19(K20(K20(NAT,NAT),NAT)) is non empty set

omega is non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() set

K19(omega) is non empty non trivial non finite set

K19(NAT) is non empty non trivial non finite set

{} is set

the Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() set is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() set

2 is non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT

K204(NAT) is V54() set

1 is non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT

K20(NAT,REAL) is Relation-like non trivial non finite V55() V56() V57() set

K19(K20(NAT,REAL)) is non empty non trivial non finite set

0 is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT

- 1 is non empty V24() V32() ext-real non positive negative Element of REAL

<*> REAL is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL

Sum (<*> REAL) is V24() V32() ext-real Element of REAL

K148() is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like non empty total quasi_total V21( REAL ) V22( REAL ) V55() V56() V57() V215( REAL ) Element of K19(K20(K20(REAL,REAL),REAL))

K406(REAL,(<*> REAL),K148()) is V24() V32() ext-real Element of REAL

r is non empty RLSStruct

the carrier of r is non empty set

K19( the carrier of r) is non empty set

V is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() Element of K19( the carrier of r)

conv V is convex Element of K19( the carrier of r)

Convex-Family V is Element of K19(K19( the carrier of r))

K19(K19( the carrier of r)) is non empty set

meet (Convex-Family V) is Element of K19( the carrier of r)

the Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() convex Element of K19( the carrier of r) is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() convex Element of K19( the carrier of r)

r is non empty RLSStruct

the carrier of r is non empty set

K19( the carrier of r) is non empty set

V is Element of K19( the carrier of r)

conv V is convex Element of K19( the carrier of r)

Convex-Family V is Element of K19(K19( the carrier of r))

K19(K19( the carrier of r)) is non empty set

meet (Convex-Family V) is Element of K19( the carrier of r)

v is set

w is set

[#] r is non empty non proper Element of K19( the carrier of r)

r is non empty RLSStruct

the carrier of r is non empty set

K19( the carrier of r) is non empty set

V is non empty Element of K19( the carrier of r)

conv V is convex Element of K19( the carrier of r)

Convex-Family V is Element of K19(K19( the carrier of r))

K19(K19( the carrier of r)) is non empty set

meet (Convex-Family V) is Element of K19( the carrier of r)

r is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of r is non empty set

V is Element of the carrier of r

{V} is non empty trivial finite 1 -element Element of K19( the carrier of r)

K19( the carrier of r) is non empty set

conv {V} is non empty convex Element of K19( the carrier of r)

Convex-Family {V} is Element of K19(K19( the carrier of r))

K19(K19( the carrier of r)) is non empty set

meet (Convex-Family {V}) is Element of K19( the carrier of r)

v is Element of the carrier of r

w is Element of the carrier of r

p is V24() V32() ext-real Element of REAL

p * v is Element of the carrier of r

1 - p is V24() V32() ext-real Element of REAL

(1 - p) * w is Element of the carrier of r

(p * v) + ((1 - p) * w) is Element of the carrier of r

p + (1 - p) is V24() V32() ext-real Element of REAL

(p + (1 - p)) * v is Element of the carrier of r

r is non empty RLSStruct

the carrier of r is non empty set

K19( the carrier of r) is non empty set

V is Element of K19( the carrier of r)

conv V is convex Element of K19( the carrier of r)

Convex-Family V is Element of K19(K19( the carrier of r))

K19(K19( the carrier of r)) is non empty set

meet (Convex-Family V) is Element of K19( the carrier of r)

r is non empty RLSStruct

the carrier of r is non empty set

K19( the carrier of r) is non empty set

V is Element of K19( the carrier of r)

v is Element of K19( the carrier of r)

conv V is convex Element of K19( the carrier of r)

Convex-Family V is Element of K19(K19( the carrier of r))

K19(K19( the carrier of r)) is non empty set

meet (Convex-Family V) is Element of K19( the carrier of r)

conv v is convex Element of K19( the carrier of r)

Convex-Family v is Element of K19(K19( the carrier of r))

meet (Convex-Family v) is Element of K19( the carrier of r)

w is set

p is Element of K19( the carrier of r)

[#] r is non empty non proper Element of K19( the carrier of r)

w is set

r is non empty RLSStruct

the carrier of r is non empty set

K19( the carrier of r) is non empty set

v is Element of K19( the carrier of r)

V is Element of K19( the carrier of r)

conv V is convex Element of K19( the carrier of r)

Convex-Family V is Element of K19(K19( the carrier of r))

K19(K19( the carrier of r)) is non empty set

meet (Convex-Family V) is Element of K19( the carrier of r)

V \/ v is Element of K19( the carrier of r)

conv (V \/ v) is convex Element of K19( the carrier of r)

Convex-Family (V \/ v) is Element of K19(K19( the carrier of r))

meet (Convex-Family (V \/ v)) is Element of K19( the carrier of r)

r is non empty right_complementable add-associative right_zeroed addLoopStr

the carrier of r is non empty set

K19( the carrier of r) is non empty set

V is Element of K19( the carrier of r)

v is Element of K19( the carrier of r)

V \ v is Element of K19( the carrier of r)

w is Element of the carrier of r

w + V is Element of K19( the carrier of r)

{ (w + b

w + v is Element of K19( the carrier of r)

{ (w + b

(w + V) \ (w + v) is Element of K19( the carrier of r)

w + (V \ v) is Element of K19( the carrier of r)

{ (w + b

p is set

I is Element of the carrier of r

w + I is Element of the carrier of r

p is set

I is Element of the carrier of r

w + I is Element of the carrier of r

A is Element of the carrier of r

w + A is Element of the carrier of r

r is non empty addLoopStr

the carrier of r is non empty set

V is Element of the carrier of r

v is Element of the carrier of r

V + v is Element of the carrier of r

{(V + v)} is non empty trivial finite 1 -element Element of K19( the carrier of r)

K19( the carrier of r) is non empty set

{v} is non empty trivial finite 1 -element Element of K19( the carrier of r)

V + {v} is Element of K19( the carrier of r)

{ (V + b

w is set

w is set

p is Element of the carrier of r

V + p is Element of the carrier of r

r is non empty add-associative addLoopStr

the carrier of r is non empty set

K19( the carrier of r) is non empty set

V is Element of K19( the carrier of r)

v is Element of the carrier of r

w is Element of the carrier of r

v + w is Element of the carrier of r

(v + w) + V is Element of K19( the carrier of r)

{ ((v + w) + b

w + V is Element of K19( the carrier of r)

{ (w + b

v + (w + V) is Element of K19( the carrier of r)

{ (v + b

I is set

A is Element of the carrier of r

(v + w) + A is Element of the carrier of r

w + A is Element of the carrier of r

v + (w + A) is Element of the carrier of r

I is set

A is Element of the carrier of r

v + A is Element of the carrier of r

u2 is Element of the carrier of r

w + u2 is Element of the carrier of r

(v + w) + u2 is Element of the carrier of r

r is non empty Abelian right_zeroed V135() addLoopStr

the carrier of r is non empty set

K19( the carrier of r) is non empty set

0. r is V84(r) Element of the carrier of r

the ZeroF of r is Element of the carrier of r

V is Element of K19( the carrier of r)

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

{ ((0. r) + b

v is set

w is Element of the carrier of r

(0. r) + w is Element of the carrier of r

v is set

w is Element of the carrier of r

(0. r) + w is Element of the carrier of r

r is non empty addLoopStr

the carrier of r is non empty set

K19( the carrier of r) is non empty set

V is Element of K19( the carrier of r)

card V is ordinal cardinal set

v is Element of the carrier of r

v + V is Element of K19( the carrier of r)

{ (v + b

card (v + V) is ordinal cardinal set

{ H

card { H

r is non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() addLoopStr

the carrier of r is non empty set

K19( the carrier of r) is non empty set

V is Element of the carrier of r

v is Element of K19( the carrier of r)

card v is ordinal cardinal set

V + v is Element of K19( the carrier of r)

{ (V + b

card (V + v) is ordinal cardinal set

- V is Element of the carrier of r

(- V) + (V + v) is Element of K19( the carrier of r)

{ ((- V) + b

(- V) + V is Element of the carrier of r

((- V) + V) + v is Element of K19( the carrier of r)

{ (((- V) + V) + b

0. r is V84(r) Element of the carrier of r

the ZeroF of r is Element of the carrier of r

(0. r) + v is Element of K19( the carrier of r)

{ ((0. r) + b

r is non empty addLoopStr

the carrier of r is non empty set

{} r is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() Element of K19( the carrier of r)

K19( the carrier of r) is non empty set

V is Element of the carrier of r

V + ({} r) is Element of K19( the carrier of r)

{ (V + b

v is set

w is Element of the carrier of r

V + w is Element of the carrier of r

r is V24() V32() ext-real Element of REAL

V is non empty RLSStruct

the carrier of V is non empty set

K19( the carrier of V) is non empty set

v is Element of K19( the carrier of V)

w is Element of K19( the carrier of V)

r * v is Element of K19( the carrier of V)

{ (r * b

r * w is Element of K19( the carrier of V)

{ (r * b

p is set

I is Element of the carrier of V

r * I is Element of the carrier of V

r is V24() V32() ext-real Element of REAL

V is V24() V32() ext-real Element of REAL

r * V is V24() V32() ext-real Element of REAL

v is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of v is non empty set

K19( the carrier of v) is non empty set

w is Element of K19( the carrier of v)

(r * V) * w is Element of K19( the carrier of v)

{ ((r * V) * b

V * w is Element of K19( the carrier of v)

{ (V * b

r * (V * w) is Element of K19( the carrier of v)

{ (r * b

I is set

A is Element of the carrier of v

(r * V) * A is Element of the carrier of v

V * A is Element of the carrier of v

r * (V * A) is Element of the carrier of v

I is set

A is Element of the carrier of v

r * A is Element of the carrier of v

u2 is Element of the carrier of v

V * u2 is Element of the carrier of v

(r * V) * u2 is Element of the carrier of v

r is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of r is non empty set

K19( the carrier of r) is non empty set

V is Element of K19( the carrier of r)

1 * V is Element of K19( the carrier of r)

{ (1 * b

v is set

w is Element of the carrier of r

1 * w is Element of the carrier of r

v is set

w is Element of the carrier of r

1 * w is Element of the carrier of r

r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct

the carrier of r is non empty set

K19( the carrier of r) is non empty set

0. r is V84(r) Element of the carrier of r

the ZeroF of r is Element of the carrier of r

{(0. r)} is non empty trivial finite 1 -element Element of K19( the carrier of r)

V is Element of K19( the carrier of r)

0 * V is Element of K19( the carrier of r)

{ (0 * b

v is set

w is Element of the carrier of r

0 * w is Element of the carrier of r

r is non empty addLoopStr

the carrier of r is non empty set

V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

V + v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

w is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r

(V + v) * w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL

V * w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL

v * w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL

(V * w) + (v * w) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL

K376(K148(),(V * w),(v * w)) is set

len (V * w) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT

len w is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT

len (v * w) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT

(len w) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL

len ((V + v) * w) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT

A is V24() ordinal natural V32() ext-real non negative finite cardinal set

dom ((V + v) * w) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)

((V + v) * w) . A is V24() V32() ext-real Element of REAL

w . A is set

(V + v) . (w . A) is V24() V32() ext-real Element of REAL

p is Relation-like NAT -defined REAL -valued Function-like len w -element FinSequence-like V55() V56() V57() Element of (len w) -tuples_on REAL

dom p is len w -element V65() V66() V67() V68() V69() V70() Element of K19(NAT)

dom V is set

p . A is V24() V32() ext-real Element of REAL

V . (w . A) is V24() V32() ext-real Element of REAL

I is Relation-like NAT -defined REAL -valued Function-like len w -element FinSequence-like V55() V56() V57() Element of (len w) -tuples_on REAL

dom I is len w -element V65() V66() V67() V68() V69() V70() Element of K19(NAT)

I . A is V24() V32() ext-real Element of REAL

v . (w . A) is V24() V32() ext-real Element of REAL

(p . A) + (I . A) is V24() V32() ext-real Element of REAL

p + I is Relation-like NAT -defined REAL -valued Function-like len w -element FinSequence-like V55() V56() V57() Element of (len w) -tuples_on REAL

K376(K148(),p,I) is set

(p + I) . A is V24() V32() ext-real Element of REAL

len (p + I) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT

r is V24() V32() ext-real Element of REAL

V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct

the carrier of V is non empty set

v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

r * v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

w is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

(r * v) * w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL

v * w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL

r * (v * w) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL

K518(r) is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total V55() V56() V57() Element of K19(K20(REAL,REAL))

K150() is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like non empty total quasi_total V21( REAL ) V22( REAL ) V55() V56() V57() V215( REAL ) Element of K19(K20(K20(REAL,REAL),REAL))

id REAL is Relation-like REAL -defined REAL -valued Function-like one-to-one non empty total quasi_total V55() V56() V57() V59() V61() Element of K19(K20(REAL,REAL))

K378(K150(),r,(id REAL)) is set

(v * w) * K518(r) is Relation-like NAT -defined REAL -valued Function-like V55() V56() V57() set

len ((r * v) * w) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT

len w is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT

len (v * w) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT

(len w) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL

A is V24() ordinal natural V32() ext-real non negative finite cardinal set

I is Relation-like NAT -defined REAL -valued Function-like len w -element FinSequence-like V55() V56() V57() Element of (len w) -tuples_on REAL

dom I is len w -element V65() V66() V67() V68() V69() V70() Element of K19(NAT)

I . A is V24() V32() ext-real Element of REAL

w . A is set

v . (w . A) is V24() V32() ext-real Element of REAL

dom v is set

p is Relation-like NAT -defined REAL -valued Function-like len w -element FinSequence-like V55() V56() V57() Element of (len w) -tuples_on REAL

dom p is len w -element V65() V66() V67() V68() V69() V70() Element of K19(NAT)

p . A is V24() V32() ext-real Element of REAL

(r * v) . (w . A) is V24() V32() ext-real Element of REAL

r * I is Relation-like NAT -defined REAL -valued Function-like len w -element FinSequence-like V55() V56() V57() Element of (len w) -tuples_on REAL

I * K518(r) is Relation-like NAT -defined REAL -valued Function-like V55() V56() V57() set

(r * I) . A is V24() V32() ext-real Element of REAL

r * (I . A) is V24() V32() ext-real Element of REAL

len (r * I) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT

r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct

the carrier of r is non empty set

K19( the carrier of r) is non empty set

V is Element of K19( the carrier of r)

v is Element of K19( the carrier of r)

Lin v is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r

bool the carrier of r is non empty Element of K19(K19( the carrier of r))

K19(K19( the carrier of r)) is non empty set

w is set

p is set

union p is set

A is set

u2 is set

the Element of p is Element of p

A is Element of K19( the carrier of r)

{ b

q is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of A

Sum q is Element of the carrier of r

0. r is V84(r) Element of the carrier of r

the ZeroF of r is Element of the carrier of r

Carrier q is finite Element of K19( the carrier of r)

{ b

LI is Relation-like Function-like set

dom LI is set

rng LI is set

qI is non empty set

LI is set

LI . LI is set

LA is set

pA is Element of K19( the carrier of r)

{ b

union qI is set

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

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

the Element of qI is Element of qI

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

pA is set

u is set

the Relation-like qI -defined union qI -valued Function-like quasi_total Choice_Function of qI . u is set

v is set

LI . v is set

{ b

x is Element of K19( the carrier of r)

pA is set

u is set

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

pA is Element of K19( the carrier of r)

u is set

LI . u is set

{ b

the Relation-like qI -defined union qI -valued Function-like quasi_total Choice_Function of qI . (LI . u) is set

v is Element of K19( the carrier of r)

q is set

LI is set

qI is Element of K19( the carrier of r)

q is Element of K19( the carrier of r)

p is set

I is Element of K19( the carrier of r)

A is linearly-independent Element of K19( the carrier of r)

Lin A is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r

u2 is Element of the carrier of r

q is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v

Sum q is Element of the carrier of r

Carrier q is finite Element of K19( the carrier of r)

{ b

the carrier of (Lin A) is non empty set

LI is set

qI is Element of the carrier of r

Up (Lin A) is non empty Element of K19( the carrier of r)

LI is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of Up (Lin A)

Sum LI is Element of the carrier of r

Lin (Up (Lin A)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r

u2 is Element of the carrier of r

u2 is Element of the carrier of r

{u2} is non empty trivial finite 1 -element Element of K19( the carrier of r)

A \/ {u2} is Element of K19( the carrier of r)

q is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of A \/ {u2}

Sum q is Element of the carrier of r

0. r is V84(r) Element of the carrier of r

the ZeroF of r is Element of the carrier of r

Carrier q is finite Element of K19( the carrier of r)

{ b

q . u2 is V24() V32() ext-real Element of REAL

- (q . u2) is V24() V32() ext-real Element of REAL

K20( the carrier of r,REAL) is Relation-like non empty non trivial non finite V55() V56() V57() set

K19(K20( the carrier of r,REAL)) is non empty non trivial non finite set

LI is Relation-like the carrier of r -defined REAL -valued Function-like non empty total quasi_total V55() V56() V57() Element of K19(K20( the carrier of r,REAL))

LI . u2 is V24() V32() ext-real Element of REAL

Funcs ( the carrier of r,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of r, REAL

LI is Element of the carrier of r

(Carrier q) \ {u2} is finite Element of K19( the carrier of r)

q . LI is V24() V32() ext-real Element of REAL

qI is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Element of Funcs ( the carrier of r,REAL)

qI . LI is V24() V32() ext-real Element of REAL

LI is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

Carrier LI is finite Element of K19( the carrier of r)

{ b

LA is set

pA is Element of the carrier of r

LI . pA is V24() V32() ext-real Element of REAL

q . pA is V24() V32() ext-real Element of REAL

pA is Relation-like the carrier of r -defined REAL -valued Function-like non empty total quasi_total V55() V56() V57() Element of K19(K20( the carrier of r,REAL))

pA . u2 is V24() V32() ext-real Element of REAL

v is Element of the carrier of r

u is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Element of Funcs ( the carrier of r,REAL)

u . v is V24() V32() ext-real Element of REAL

v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

Carrier v is finite Element of K19( the carrier of r)

{ b

x is set

u is Element of the carrier of r

v . u is V24() V32() ext-real Element of REAL

x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of {u2}

Sum x is Element of the carrier of r

(- (q . u2)) * u2 is Element of the carrier of r

u is Element of the carrier of r

LA is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of A

LA - x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

- x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

(- 1) * x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

LA + (- x) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

(LA - x) . u is V24() V32() ext-real Element of REAL

LA . u is V24() V32() ext-real Element of REAL

x . u is V24() V32() ext-real Element of REAL

(LA . u) - (x . u) is V24() V32() ext-real Element of REAL

q . u is V24() V32() ext-real Element of REAL

u is Element of the carrier of r

LA is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of A

LA - x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

- x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

(- 1) * x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

LA + (- x) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

(LA - x) . u is V24() V32() ext-real Element of REAL

LA . u is V24() V32() ext-real Element of REAL

x . u is V24() V32() ext-real Element of REAL

(LA . u) - (x . u) is V24() V32() ext-real Element of REAL

q . u is V24() V32() ext-real Element of REAL

(q . u) - (x . u) is V24() V32() ext-real Element of REAL

(q . u) - 0 is V24() V32() ext-real Element of REAL

u is Element of the carrier of r

LA is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of A

LA - x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

- x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

(- 1) * x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

LA + (- x) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

(LA - x) . u is V24() V32() ext-real Element of REAL

q . u is V24() V32() ext-real Element of REAL

LA is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of A

LA - x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

- x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

(- 1) * x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

LA + (- x) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

u is Element of the carrier of r

(LA - x) . u is V24() V32() ext-real Element of REAL

q . u is V24() V32() ext-real Element of REAL

Sum LA is Element of the carrier of r

(Sum LA) - (Sum x) is Element of the carrier of r

(0. r) + (Sum x) is Element of the carrier of r

(- (q . u2)) " is V24() V32() ext-real Element of REAL

((- (q . u2)) ") * ((- (q . u2)) * u2) is Element of the carrier of r

((- (q . u2)) ") * (- (q . u2)) is V24() V32() ext-real Element of REAL

(((- (q . u2)) ") * (- (q . u2))) * u2 is Element of the carrier of r

1 * u2 is Element of the carrier of r

LI is set

r is non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() addLoopStr

the carrier of r is non empty set

V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

v is Element of the carrier of r

Carrier V is finite Element of K19( the carrier of r)

K19( the carrier of r) is non empty set

{ b

{ H

p is set

I is Element of the carrier of r

v + I is Element of the carrier of r

K20( the carrier of r,REAL) is Relation-like non empty non trivial non finite V55() V56() V57() set

K19(K20( the carrier of r,REAL)) is non empty non trivial non finite set

I is Relation-like the carrier of r -defined REAL -valued Function-like non empty total quasi_total V55() V56() V57() Element of K19(K20( the carrier of r,REAL))

Funcs ( the carrier of r,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of r, REAL

u2 is Element of the carrier of r

p is finite Element of K19( the carrier of r)

A is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Element of Funcs ( the carrier of r,REAL)

A . u2 is V24() V32() ext-real Element of REAL

u2 - v is Element of the carrier of r

V . (u2 - v) is V24() V32() ext-real Element of REAL

v + (u2 - v) is Element of the carrier of r

- v is Element of the carrier of r

u2 + (- v) is Element of the carrier of r

(u2 + (- v)) + v is Element of the carrier of r

v + (- v) is Element of the carrier of r

u2 + (v + (- v)) is Element of the carrier of r

0. r is V84(r) Element of the carrier of r

the ZeroF of r is Element of the carrier of r

u2 + (0. r) is Element of the carrier of r

u2 is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

q is Element of the carrier of r

u2 . q is V24() V32() ext-real Element of REAL

q - v is Element of the carrier of r

V . (q - v) is V24() V32() ext-real Element of REAL

w is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

I is Element of the carrier of r

w . I is V24() V32() ext-real Element of REAL

I - v is Element of the carrier of r

V . (I - v) is V24() V32() ext-real Element of REAL

p . I is V24() V32() ext-real Element of REAL

r is non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() addLoopStr

the carrier of r is non empty set

V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

Carrier V is finite Element of K19( the carrier of r)

K19( the carrier of r) is non empty set

{ b

v is Element of the carrier of r

(r,V,v) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

Carrier (r,V,v) is finite Element of K19( the carrier of r)

{ b

v + (Carrier V) is Element of K19( the carrier of r)

{ (v + b

w is set

p is Element of the carrier of r

(r,V,v) . p is V24() V32() ext-real Element of REAL

p - v is Element of the carrier of r

v + (p - v) is Element of the carrier of r

- v is Element of the carrier of r

p + (- v) is Element of the carrier of r

(p + (- v)) + v is Element of the carrier of r

v + (- v) is Element of the carrier of r

p + (v + (- v)) is Element of the carrier of r

0. r is V84(r) Element of the carrier of r

the ZeroF of r is Element of the carrier of r

p + (0. r) is Element of the carrier of r

V . (p - v) is V24() V32() ext-real Element of REAL

w is set

p is Element of the carrier of r

v + p is Element of the carrier of r

(v + p) - v is Element of the carrier of r

- v is Element of the carrier of r

(v + p) + (- v) is Element of the carrier of r

(- v) + v is Element of the carrier of r

((- v) + v) + p is Element of the carrier of r

0. r is V84(r) Element of the carrier of r

the ZeroF of r is Element of the carrier of r

(0. r) + p is Element of the carrier of r

(r,V,v) . (v + p) is V24() V32() ext-real Element of REAL

V . p is V24() V32() ext-real Element of REAL

r is non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() addLoopStr

the carrier of r is non empty set

V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

V + v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

w is Element of the carrier of r

(r,(V + v),w) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

(r,V,w) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

(r,v,w) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

(r,V,w) + (r,v,w) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

p is Element of the carrier of r

(r,(V + v),w) . p is V24() V32() ext-real Element of REAL

p - w is Element of the carrier of r

(V + v) . (p - w) is V24() V32() ext-real Element of REAL

V . (p - w) is V24() V32() ext-real Element of REAL

v . (p - w) is V24() V32() ext-real Element of REAL

(V . (p - w)) + (v . (p - w)) is V24() V32() ext-real Element of REAL

(r,V,w) . p is V24() V32() ext-real Element of REAL

((r,V,w) . p) + (v . (p - w)) is V24() V32() ext-real Element of REAL

(r,v,w) . p is V24() V32() ext-real Element of REAL

((r,V,w) . p) + ((r,v,w) . p) is V24() V32() ext-real Element of REAL

((r,V,w) + (r,v,w)) . p is V24() V32() ext-real Element of REAL

r is V24() V32() ext-real Element of REAL

V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct

the carrier of V is non empty set

v is Element of the carrier of V

w is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

r * w is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

(V,(r * w),v) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

(V,w,v) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

r * (V,w,v) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

p is Element of the carrier of V

(V,(r * w),v) . p is V24() V32() ext-real Element of REAL

p - v is Element of the carrier of V

(r * w) . (p - v) is V24() V32() ext-real Element of REAL

w . (p - v) is V24() V32() ext-real Element of REAL

r * (w . (p - v)) is V24() V32() ext-real Element of REAL

(V,w,v) . p is V24() V32() ext-real Element of REAL

r * ((V,w,v) . p) is V24() V32() ext-real Element of REAL

(r * (V,w,v)) . p is V24() V32() ext-real Element of REAL

r is non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() addLoopStr

the carrier of r is non empty set

V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

v is Element of the carrier of r

w is Element of the carrier of r

(r,V,w) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

(r,(r,V,w),v) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

v + w is Element of the carrier of r

(r,V,(v + w)) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

p is Element of the carrier of r

(r,(r,V,w),v) . p is V24() V32() ext-real Element of REAL

p - v is Element of the carrier of r

(r,V,w) . (p - v) is V24() V32() ext-real Element of REAL

(p - v) - w is Element of the carrier of r

V . ((p - v) - w) is V24() V32() ext-real Element of REAL

p - (v + w) is Element of the carrier of r

V . (p - (v + w)) is V24() V32() ext-real Element of REAL

(r,V,(v + w)) . p is V24() V32() ext-real Element of REAL

r is non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() addLoopStr

the carrier of r is non empty set

ZeroLC r is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

V is Element of the carrier of r

(r,(ZeroLC r),V) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

Carrier (ZeroLC r) is finite Element of K19( the carrier of r)

K19( the carrier of r) is non empty set

{ b

{} r is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() Element of K19( the carrier of r)

V + (Carrier (ZeroLC r)) is Element of K19( the carrier of r)

{ (V + b

Carrier (r,(ZeroLC r),V) is finite Element of K19( the carrier of r)

{ b

r is non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() addLoopStr

the carrier of r is non empty set

0. r is V84(r) Element of the carrier of r

the ZeroF of r is Element of the carrier of r

V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

(r,V,(0. r)) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

v is Element of the carrier of r

(r,V,(0. r)) . v is V24() V32() ext-real Element of REAL

v - (0. r) is Element of the carrier of r

V . (v - (0. r)) is V24() V32() ext-real Element of REAL

V . v is V24() V32() ext-real Element of REAL

r is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of r is non empty set

v is V24() V32() ext-real Element of REAL

V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

v " is V24() V32() ext-real Element of REAL

ZeroLC r is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

K20( the carrier of r,REAL) is Relation-like non empty non trivial non finite V55() V56() V57() set

K19(K20( the carrier of r,REAL)) is non empty non trivial non finite set

w is Relation-like the carrier of r -defined REAL -valued Function-like non empty total quasi_total V55() V56() V57() Element of K19(K20( the carrier of r,REAL))

Funcs ( the carrier of r,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of r, REAL

I is Element of the carrier of r

Carrier V is finite Element of K19( the carrier of r)

K19( the carrier of r) is non empty set

{ b

v * (Carrier V) is Element of K19( the carrier of r)

{ (v * b

p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Element of Funcs ( the carrier of r,REAL)

p . I is V24() V32() ext-real Element of REAL

(v ") * I is Element of the carrier of r

V . ((v ") * I) is V24() V32() ext-real Element of REAL

v * ((v ") * I) is Element of the carrier of r

v * (v ") is V24() V32() ext-real Element of REAL

(v * (v ")) * I is Element of the carrier of r

1 * I is Element of the carrier of r

{ H

I is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

A is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

u2 is Element of the carrier of r

A . u2 is V24() V32() ext-real Element of REAL

(v ") * u2 is Element of the carrier of r

V . ((v ") * u2) is V24() V32() ext-real Element of REAL

p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

I is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

w is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

I is Element of the carrier of r

w . I is V24() V32() ext-real Element of REAL

(v ") * I is Element of the carrier of r

V . ((v ") * I) is V24() V32() ext-real Element of REAL

p . I is V24() V32() ext-real Element of REAL

w is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

I is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

A is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

r is V24() V32() ext-real Element of REAL

V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

(V,v,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

Carrier (V,v,r) is finite Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

{ b

Carrier v is finite Element of K19( the carrier of V)

{ b

r * (Carrier v) is Element of K19( the carrier of V)

{ (r * b

w is set

p is Element of the carrier of V

(V,v,r) . p is V24() V32() ext-real Element of REAL

(V,v,0) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

r " is V24() V32() ext-real Element of REAL

(r ") * p is Element of the carrier of V

v . ((r ") * p) is V24() V32() ext-real Element of REAL

r * ((r ") * p) is Element of the carrier of V

r * (r ") is V24() V32() ext-real Element of REAL

(r * (r ")) * p is Element of the carrier of V

1 * p is Element of the carrier of V

r is V24() V32() ext-real Element of REAL

V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

(V,v,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

Carrier (V,v,r) is finite Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

{ b

Carrier v is finite Element of K19( the carrier of V)

{ b

r * (Carrier v) is Element of K19( the carrier of V)

{ (r * b

w is set

p is Element of the carrier of V

r * p is Element of the carrier of V

r " is V24() V32() ext-real Element of REAL

(r ") * (r * p) is Element of the carrier of V

(r ") * r is V24() V32() ext-real Element of REAL

((r ") * r) * p is Element of the carrier of V

1 * p is Element of the carrier of V

v . p is V24() V32() ext-real Element of REAL

(V,v,r) . w is V24() V32() ext-real Element of REAL

r is V24() V32() ext-real Element of REAL

V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

(V,v,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

w is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

v + w is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

(V,(v + w),r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

(V,w,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

(V,v,r) + (V,w,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

(ZeroLC V) + (ZeroLC V) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

I is Element of the carrier of V

((ZeroLC V) + (ZeroLC V)) . I is V24() V32() ext-real Element of REAL

(ZeroLC V) . I is V24() V32() ext-real Element of REAL

((ZeroLC V) . I) + ((ZeroLC V) . I) is V24() V32() ext-real Element of REAL

((ZeroLC V) . I) + 0 is V24() V32() ext-real Element of REAL

(V,v,r) + (ZeroLC V) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

p is Element of the carrier of V

(V,(v + w),r) . p is V24() V32() ext-real Element of REAL

r " is V24() V32() ext-real Element of REAL

(r ") * p is Element of the carrier of V

(v + w) . ((r ") * p) is V24() V32() ext-real Element of REAL

v . ((r ") * p) is V24() V32() ext-real Element of REAL

w . ((r ") * p) is V24() V32() ext-real Element of REAL

(v . ((r ") * p)) + (w . ((r ") * p)) is V24() V32() ext-real Element of REAL

(V,v,r) . p is V24() V32() ext-real Element of REAL

((V,v,r) . p) + (w . ((r ") * p)) is V24() V32() ext-real Element of REAL

(V,w,r) . p is V24() V32() ext-real Element of REAL

((V,v,r) . p) + ((V,w,r) . p) is V24() V32() ext-real Element of REAL

((V,v,r) + (V,w,r)) . p is V24() V32() ext-real Element of REAL

r is V24() V32() ext-real Element of REAL

V is V24() V32() ext-real Element of REAL

v is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct

the carrier of v is non empty set

w is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v

(v,w,V) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v

r * (v,w,V) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v

r * w is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v

(v,(r * w),V) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v

ZeroLC v is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v

r * (ZeroLC v) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v

0 * w is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v

r * (0 * w) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v

r * 0 is V24() V32() ext-real Element of REAL

(r * 0) * w is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v

p is Element of the carrier of v

(r * (v,w,V)) . p is V24() V32() ext-real Element of REAL

(v,w,V) . p is V24() V32() ext-real Element of REAL

r * ((v,w,V) . p) is V24() V32() ext-real Element of REAL

V " is V24() V32() ext-real Element of REAL

(V ") * p is Element of the carrier of v

w . ((V ") * p) is V24() V32() ext-real Element of REAL

r * (w . ((V ") * p)) is V24() V32() ext-real Element of REAL

(r * w) . ((V ") * p) is V24() V32() ext-real Element of REAL

(v,(r * w),V) . p is V24() V32() ext-real Element of REAL

r is V24() V32() ext-real Element of REAL

V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

the carrier of V is non empty set

(V,(ZeroLC V),r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V

v is Element of the carrier of V

(V,(ZeroLC V),r) . v is V24() V32() ext-real Element of REAL

r " is V24() V32() ext-real Element of REAL

(r ") * v is Element of the carrier of V

(ZeroLC V) . ((r ") * v) is V24() V32() ext-real Element of REAL

(ZeroLC V) . v is V24() V32() ext-real Element of REAL

r is V24() V32() ext-real Element of REAL

V is V24() V32() ext-real Element of REAL

r * V is V24() V32() ext-real Element of REAL

v is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of v is non empty set

w is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v

(v,w,V) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v

(v,(v,w,V),r) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v

(v,w,(r * V)) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v

ZeroLC v is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v

p is Element of the carrier of v

(v,(v,w,V),r) . p is V24() V32() ext-real Element of REAL

r " is V24() V32() ext-real Element of REAL

(r ") * p is Element of the carrier of v

(v,w,V) . ((r ") * p) is V24() V32() ext-real Element of REAL

V " is V24() V32() ext-real Element of REAL

(V ") * ((r ") * p) is Element of the carrier of v

w . ((V ") * ((r ") * p)) is V24() V32() ext-real Element of REAL

(V ") * (r ") is V24() V32() ext-real Element of REAL

((V ") * (r ")) * p is Element of the carrier of v

w . (((V ") * (r ")) * p) is V24() V32() ext-real Element of REAL

(r * V) " is V24() V32() ext-real Element of REAL

((r * V) ") * p is Element of the carrier of v

w . (((r * V) ") * p) is V24() V32() ext-real Element of REAL

(v,w,(r * V)) . p is V24() V32() ext-real Element of REAL

r is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of r is non empty set

V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

(r,V,1) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

v is Element of the carrier of r

(r,V,1) . v is V24() V32() ext-real Element of REAL

1 " is non empty V24() V32() ext-real positive non negative Element of REAL

(1 ") * v is Element of the carrier of r

V . ((1 ") * v) is V24() V32() ext-real Element of REAL

V . v is V24() V32() ext-real Element of REAL

r is non empty addLoopStr

the carrier of r is non empty set

V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

Carrier V is finite Element of K19( the carrier of r)

K19( the carrier of r) is non empty set

{ b

v is Relation-like Function-like FinSequence-like set

rng v is set

w is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r

V * w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL

Sum (V * w) is V24() V32() ext-real Element of REAL

K406(REAL,(V * w),K148()) is V24() V32() ext-real Element of REAL

v is V24() V32() ext-real Element of REAL

w is V24() V32() ext-real Element of REAL

p is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r

rng p is set

V * p is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL

Sum (V * p) is V24() V32() ext-real Element of REAL

K406(REAL,(V * p),K148()) is V24() V32() ext-real Element of REAL

p " is Relation-like Function-like set

dom (p ") is set

len p is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT

card (Carrier V) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega

I is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r

rng I is set

V * I is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL

Sum (V * I) is V24() V32() ext-real Element of REAL

K406(REAL,(V * I),K148()) is V24() V32() ext-real Element of REAL

I * (p ") is Relation-like NAT -defined Function-like set

dom I is V65() V66() V67() V68() V69() V70() Element of K19(NAT)

len I is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT

Seg (len I) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)

{ b

dom (I * (p ")) is set

Seg (len p) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)

{ b

dom p is V65() V66() V67() V68() V69() V70() Element of K19(NAT)

rng (p ") is set

rng (I * (p ")) is set

K20((Seg (len p)),(Seg (len p))) is Relation-like RAT -valued INT -valued V55() V56() V57() V58() set

K19(K20((Seg (len p)),(Seg (len p)))) is non empty set

u2 is Relation-like Seg (len p) -defined Seg (len p) -valued Function-like total quasi_total V55() V56() V57() V58() Element of K19(K20((Seg (len p)),(Seg (len p))))

len (V * p) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT

dom (V * p) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)

K20((dom (V * p)),(dom (V * p))) is Relation-like RAT -valued INT -valued V55() V56() V57() V58() set

K19(K20((dom (V * p)),(dom (V * p)))) is non empty set

q is Relation-like dom (V * p) -defined dom (V * p) -valued Function-like one-to-one total quasi_total onto bijective V55() V56() V57() V58() Element of K19(K20((dom (V * p)),(dom (V * p))))

(V * p) * q is Relation-like dom (V * p) -defined REAL -valued Function-like V55() V56() V57() Element of K19(K20((dom (V * p)),REAL))

K20((dom (V * p)),REAL) is Relation-like V55() V56() V57() set

K19(K20((dom (V * p)),REAL)) is non empty set

p * q is Relation-like dom (V * p) -defined the carrier of r -valued Function-like Element of K19(K20((dom (V * p)), the carrier of r))

K20((dom (V * p)), the carrier of r) is Relation-like set

K19(K20((dom (V * p)), the carrier of r)) is non empty set

V * (p * q) is Relation-like dom (V * p) -defined REAL -valued Function-like V55() V56() V57() Element of K19(K20((dom (V * p)),REAL))

(p ") * p is Relation-like the carrier of r -valued Function-like set

I * ((p ") * p) is Relation-like NAT -defined the carrier of r -valued Function-like set

(I * ((p ") * p)) * V is Relation-like NAT -defined REAL -valued Function-like V55() V56() V57() set

id (Carrier V) is Relation-like Carrier V -defined Carrier V -valued Function-like one-to-one total quasi_total finite Element of K19(K20((Carrier V),(Carrier V)))

K20((Carrier V),(Carrier V)) is Relation-like finite set

K19(K20((Carrier V),(Carrier V))) is non empty finite V44() set

(id (Carrier V)) * I is Relation-like NAT -defined Carrier V -valued Function-like Element of K19(K20(NAT,(Carrier V)))

K20(NAT,(Carrier V)) is Relation-like set

K19(K20(NAT,(Carrier V))) is non empty set

V * ((id (Carrier V)) * I) is Relation-like NAT -defined REAL -valued Function-like V55() V56() V57() Element of K19(K20(NAT,REAL))

r is non empty addLoopStr

the carrier of r is non empty set

V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

Carrier V is finite Element of K19( the carrier of r)

K19( the carrier of r) is non empty set

{ b

v is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r

rng v is set

V * v is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL

Sum (V * v) is V24() V32() ext-real Element of REAL

K406(REAL,(V * v),K148()) is V24() V32() ext-real Element of REAL

len (V * v) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT

(len (V * v)) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like len (V * v) -element FinSequence-like V55() V56() V57() Element of (len (V * v)) -tuples_on REAL

(len (V * v)) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL

I is V24() ordinal natural V32() ext-real non negative finite cardinal set

dom (V * v) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)

dom v is V65() V66() V67() V68() V69() V70() Element of K19(NAT)

v . I is set

dom V is set

(V * v) . I is V24() V32() ext-real Element of REAL

V . (v . I) is V24() V32() ext-real Element of REAL

((len (V * v)) |-> 0) . I is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() Element of REAL

len ((len (V * v)) |-> 0) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT

r is non empty addLoopStr

the carrier of r is non empty set

V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r

Carrier V is finite Element of K19( the carrier of r)

K19( the carrier of r) is non empty set

{ b

(r,V) is V24() V32() ext-real Element of REAL

v is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r

rng v is set

V * v is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL

Sum (V * v) is V24() V32() ext-real Element of REAL

K406(REAL,(V * v),K148()) is V24() V32() ext-real Element of REAL

w is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r

rng w is set

V * w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL

Sum (V * w) is V24() V32() ext-real Element of REAL

K406(REAL,(V * w),K148()) is V24() V32() ext-real Element of REAL

K19((rng v)) is non empty set

p is Element of K19((rng v))

v - p is Relation-like Function-like FinSequence-like set

p ` is Element of K19((rng v))

(rng v) \ p is set

v - (p `) is Relation-like Function-like FinSequence-like set

dom v is V65() V66() V67() V68(