:: CIRCLED1 semantic presentation

REAL is non empty V39() V63() V64() V65() V69() set

NAT is V22() V39() cardinal limit_cardinal V63() V64() V65() V66() V67() V68() V69() Element of K10(REAL)

K10(REAL) is non empty V39() set

COMPLEX is non empty V39() V63() V69() set

RAT is non empty V39() V63() V64() V65() V66() V69() set

INT is non empty V39() V63() V64() V65() V66() V67() V69() set

K11(COMPLEX,COMPLEX) is non empty V39() V53() set

K10(K11(COMPLEX,COMPLEX)) is non empty V39() set

K11(K11(COMPLEX,COMPLEX),COMPLEX) is non empty V39() V53() set

K10(K11(K11(COMPLEX,COMPLEX),COMPLEX)) is non empty V39() set

K11(REAL,REAL) is non empty V39() V53() V54() V55() set

K10(K11(REAL,REAL)) is non empty V39() set

K11(K11(REAL,REAL),REAL) is non empty V39() V53() V54() V55() set

K10(K11(K11(REAL,REAL),REAL)) is non empty V39() set

K11(RAT,RAT) is non empty V14( RAT ) V39() V53() V54() V55() set

K10(K11(RAT,RAT)) is non empty V39() set

K11(K11(RAT,RAT),RAT) is non empty V14( RAT ) V39() V53() V54() V55() set

K10(K11(K11(RAT,RAT),RAT)) is non empty V39() set

K11(INT,INT) is non empty V14( RAT ) V14( INT ) V39() V53() V54() V55() set

K10(K11(INT,INT)) is non empty V39() set

K11(K11(INT,INT),INT) is non empty V14( RAT ) V14( INT ) V39() V53() V54() V55() set

K10(K11(K11(INT,INT),INT)) is non empty V39() set

K11(NAT,NAT) is V14( RAT ) V14( INT ) V53() V54() V55() V56() set

K11(K11(NAT,NAT),NAT) is V14( RAT ) V14( INT ) V53() V54() V55() V56() set

K10(K11(K11(NAT,NAT),NAT)) is non empty set

NAT is V22() V39() cardinal limit_cardinal V63() V64() V65() V66() V67() V68() V69() set

K10(NAT) is non empty V39() set

K10(NAT) is non empty V39() set

K232(NAT) is V38() set

K11(NAT,REAL) is V39() V53() V54() V55() set

K10(K11(NAT,REAL)) is non empty V39() set

{} is empty functional V22() cardinal {} -element FinSequence-membered V63() V64() V65() V66() V67() V68() V69() set

the empty functional V22() cardinal {} -element FinSequence-membered V63() V64() V65() V66() V67() V68() V69() set is empty functional V22() cardinal {} -element FinSequence-membered V63() V64() V65() V66() V67() V68() V69() set

2 is non empty V22() V26() V27() V28() V33() V34() V39() cardinal ext-real positive non negative V63() V64() V65() V66() V67() V68() Element of NAT

1 is non empty V22() V26() V27() V28() V33() V34() V39() cardinal ext-real positive non negative V63() V64() V65() V66() V67() V68() Element of NAT

3 is non empty V22() V26() V27() V28() V33() V34() V39() cardinal ext-real positive non negative V63() V64() V65() V66() V67() V68() Element of NAT

0 is empty functional V22() V26() V27() V28() V33() V34() V39() cardinal {} -element FinSequence-membered ext-real non positive non negative V63() V64() V65() V66() V67() V68() V69() Element of NAT

<*> REAL is empty V10() V13( NAT ) V14( REAL ) Function-like functional V22() V26() V27() V28() V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() FinSequence of REAL

Sum (<*> REAL) is V27() V28() ext-real Element of REAL

K187() is V10() V13(K11(REAL,REAL)) V14( REAL ) Function-like quasi_total V53() V54() V55() Element of K10(K11(K11(REAL,REAL),REAL))

K258(REAL,(<*> REAL),K187()) is V27() V28() ext-real Element of REAL

Seg 1 is non empty V2() V39() 1 -element V63() V64() V65() V66() V67() V68() Element of K10(NAT)

{1} is non empty V2() 1 -element V63() V64() V65() V66() V67() V68() set

Seg 2 is non empty V39() 2 -element V63() V64() V65() V66() V67() V68() Element of K10(NAT)

{1,2} is non empty V63() V64() V65() V66() V67() V68() set

card {} is empty functional V22() cardinal {} -element FinSequence-membered V63() V64() V65() V66() V67() V68() V69() set

V is non empty RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is Element of K10( the carrier of V)

v2 is Element of K10( the carrier of V)

v1 - v2 is Element of K10( the carrier of V)

L is Element of the carrier of V

L is Element of the carrier of V

L - L is Element of the carrier of V

{ (b

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is V179(V) circled Element of K10( the carrier of V)

v2 is V179(V) circled Element of K10( the carrier of V)

v1 - v2 is Element of K10( the carrier of V)

{ (b

L is V27() V28() ext-real Element of REAL

abs L is V27() V28() ext-real Element of REAL

L * (v1 - v2) is Element of K10( the carrier of V)

L * v1 is Element of K10( the carrier of V)

L * v2 is Element of K10( the carrier of V)

L is set

{ (L * b

F is Element of the carrier of V

L * F is Element of the carrier of V

f is Element of the carrier of V

r1 is Element of the carrier of V

f - r1 is Element of the carrier of V

L * f is Element of the carrier of V

L * r1 is Element of the carrier of V

(L * f) - (L * r1) is Element of the carrier of V

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is V179(V) circled Element of K10( the carrier of V)

v2 is V179(V) circled Element of K10( the carrier of V)

v1 - v2 is Element of K10( the carrier of V)

V is non empty RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is Element of K10( the carrier of V)

v2 is Element of the carrier of V

L is V27() V28() ext-real Element of REAL

abs L is V27() V28() ext-real Element of REAL

L * v2 is Element of the carrier of V

L * v1 is Element of K10( the carrier of V)

v2 is V27() V28() ext-real Element of REAL

abs v2 is V27() V28() ext-real Element of REAL

v2 * v1 is Element of K10( the carrier of V)

L is Element of the carrier of V

L is Element of the carrier of V

{ (v2 * b

F is Element of the carrier of V

v2 * F is Element of the carrier of V

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is Element of K10( the carrier of V)

v2 is V27() V28() ext-real Element of REAL

v2 * v1 is Element of K10( the carrier of V)

L is Element of the carrier of V

L is V27() V28() ext-real Element of REAL

abs L is V27() V28() ext-real Element of REAL

L * L is Element of the carrier of V

{ (v2 * b

F is Element of the carrier of V

v2 * F is Element of the carrier of V

v2 * L is V27() V28() ext-real Element of REAL

(v2 * L) * F is Element of the carrier of V

L * F is Element of the carrier of V

v2 * (L * F) is Element of the carrier of V

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is Element of K10( the carrier of V)

v2 is Element of K10( the carrier of V)

L is V27() V28() ext-real Element of REAL

L * v1 is Element of K10( the carrier of V)

L is V27() V28() ext-real Element of REAL

L * v2 is Element of K10( the carrier of V)

(L * v1) + (L * v2) is Element of K10( the carrier of V)

F is Element of the carrier of V

f is V27() V28() ext-real Element of REAL

abs f is V27() V28() ext-real Element of REAL

f * F is Element of the carrier of V

{ (b

r1 is Element of the carrier of V

r2 is Element of the carrier of V

r1 + r2 is Element of the carrier of V

{ (L * b

x1 is Element of the carrier of V

L * x1 is Element of the carrier of V

f * r1 is Element of the carrier of V

L * f is V27() V28() ext-real Element of REAL

(L * f) * x1 is Element of the carrier of V

f * x1 is Element of the carrier of V

L * (f * x1) is Element of the carrier of V

{ (L * b

x2 is Element of the carrier of V

L * x2 is Element of the carrier of V

f * r2 is Element of the carrier of V

L * f is V27() V28() ext-real Element of REAL

(L * f) * x2 is Element of the carrier of V

f * x2 is Element of the carrier of V

L * (f * x2) is Element of the carrier of V

f * (r1 + r2) is Element of the carrier of V

(f * r1) + (f * r2) is Element of the carrier of V

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is Element of K10( the carrier of V)

v2 is Element of K10( the carrier of V)

L is Element of K10( the carrier of V)

L is V27() V28() ext-real Element of REAL

L * v1 is Element of K10( the carrier of V)

F is V27() V28() ext-real Element of REAL

F * v2 is Element of K10( the carrier of V)

(L * v1) + (F * v2) is Element of K10( the carrier of V)

f is V27() V28() ext-real Element of REAL

f * L is Element of K10( the carrier of V)

((L * v1) + (F * v2)) + (f * L) is Element of K10( the carrier of V)

1 * ((L * v1) + (F * v2)) is Element of K10( the carrier of V)

(1 * ((L * v1) + (F * v2))) + (f * L) is Element of K10( the carrier of V)

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

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

Up ((0). V) is non empty Element of K10( the carrier of V)

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is Element of the carrier of V

v2 is V27() V28() ext-real Element of REAL

abs v2 is V27() V28() ext-real Element of REAL

v2 * v1 is Element of the carrier of V

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

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

{(0. V)} is non empty V2() 1 -element Element of K10( the carrier of V)

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

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

Up ((Omega). V) is non empty Element of K10( the carrier of V)

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is Element of the carrier of V

v2 is V27() V28() ext-real Element of REAL

abs v2 is V27() V28() ext-real Element of REAL

v2 * v1 is Element of the carrier of V

the ZeroF of V is Element of the carrier of V

the U6 of V is V10() V13(K11( the carrier of V, the carrier of V)) V14( the carrier of V) Function-like quasi_total Element of K10(K11(K11( the carrier of V, the carrier of V), the carrier of V))

K11( the carrier of V, the carrier of V) is non empty set

K11(K11( the carrier of V, the carrier of V), the carrier of V) is non empty set

K10(K11(K11( the carrier of V, the carrier of V), the carrier of V)) is non empty set

the Mult of V is V10() V13(K11(REAL, the carrier of V)) V14( the carrier of V) Function-like quasi_total Element of K10(K11(K11(REAL, the carrier of V), the carrier of V))

K11(REAL, the carrier of V) is non empty V39() set

K11(K11(REAL, the carrier of V), the carrier of V) is non empty V39() set

K10(K11(K11(REAL, the carrier of V), the carrier of V)) is non empty V39() set

RLSStruct(# the carrier of V, the ZeroF of V, the U6 of V, the Mult of V #) is non empty strict RLSStruct

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

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is V179(V) circled Element of K10( the carrier of V)

v2 is V179(V) circled Element of K10( the carrier of V)

v1 /\ v2 is Element of K10( the carrier of V)

L is Element of the carrier of V

L is V27() V28() ext-real Element of REAL

abs L is V27() V28() ext-real Element of REAL

L * L is Element of the carrier of V

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is V179(V) circled Element of K10( the carrier of V)

v2 is V179(V) circled Element of K10( the carrier of V)

v1 \/ v2 is Element of K10( the carrier of V)

L is Element of the carrier of V

L is V27() V28() ext-real Element of REAL

abs L is V27() V28() ext-real Element of REAL

L * L is Element of the carrier of V

V is non empty RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

K10(K10( the carrier of V)) is non empty set

v1 is Element of K10( the carrier of V)

v2 is Element of K10(K10( the carrier of V))

L is Element of K10(K10( the carrier of V))

L is Element of K10( the carrier of V)

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is Element of K10( the carrier of V)

(V,v1) is Element of K10(K10( the carrier of V))

K10(K10( the carrier of V)) is non empty set

meet (V,v1) is Element of K10( the carrier of V)

v2 is Element of K10( the carrier of V)

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is Element of K10( the carrier of V)

(V,v1) is Element of K10(K10( the carrier of V))

K10(K10( the carrier of V)) is non empty set

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

Up ((Omega). V) is non empty Element of K10( the carrier of V)

v2 is set

L is Element of the carrier of V

the ZeroF of V is Element of the carrier of V

the U6 of V is V10() V13(K11( the carrier of V, the carrier of V)) V14( the carrier of V) Function-like quasi_total Element of K10(K11(K11( the carrier of V, the carrier of V), the carrier of V))

K11( the carrier of V, the carrier of V) is non empty set

K11(K11( the carrier of V, the carrier of V), the carrier of V) is non empty set

K10(K11(K11( the carrier of V, the carrier of V), the carrier of V)) is non empty set

the Mult of V is V10() V13(K11(REAL, the carrier of V)) V14( the carrier of V) Function-like quasi_total Element of K10(K11(K11(REAL, the carrier of V), the carrier of V))

K11(REAL, the carrier of V) is non empty V39() set

K11(K11(REAL, the carrier of V), the carrier of V) is non empty V39() set

K10(K11(K11(REAL, the carrier of V), the carrier of V)) is non empty V39() set

RLSStruct(# the carrier of V, the ZeroF of V, the U6 of V, the Mult of V #) is non empty strict RLSStruct

the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the U6 of V, the Mult of V #) is non empty set

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

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is Element of K10( the carrier of V)

v2 is Element of K10( the carrier of V)

(V,v2) is non empty Element of K10(K10( the carrier of V))

K10(K10( the carrier of V)) is non empty set

(V,v1) is non empty Element of K10(K10( the carrier of V))

L is set

L is Element of K10( the carrier of V)

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is Element of K10( the carrier of V)

v2 is Element of K10( the carrier of V)

(V,v1) is V179(V) circled Element of K10( the carrier of V)

(V,v1) is non empty Element of K10(K10( the carrier of V))

K10(K10( the carrier of V)) is non empty set

meet (V,v1) is Element of K10( the carrier of V)

(V,v2) is V179(V) circled Element of K10( the carrier of V)

(V,v2) is non empty Element of K10(K10( the carrier of V))

meet (V,v2) is Element of K10( the carrier of V)

L is set

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is Element of K10( the carrier of V)

(V,v1) is V179(V) circled Element of K10( the carrier of V)

(V,v1) is non empty Element of K10(K10( the carrier of V))

K10(K10( the carrier of V)) is non empty set

meet (V,v1) is Element of K10( the carrier of V)

v2 is set

L is set

L is Element of K10( the carrier of V)

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is Element of K10( the carrier of V)

(V,v1) is V179(V) circled Element of K10( the carrier of V)

(V,v1) is non empty Element of K10(K10( the carrier of V))

K10(K10( the carrier of V)) is non empty set

meet (V,v1) is Element of K10( the carrier of V)

v2 is V179(V) circled Element of K10( the carrier of V)

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is V179(V) circled Element of K10( the carrier of V)

(V,v1) is V179(V) circled Element of K10( the carrier of V)

(V,v1) is non empty Element of K10(K10( the carrier of V))

K10(K10( the carrier of V)) is non empty set

meet (V,v1) is Element of K10( the carrier of V)

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

{} V is empty proper functional V22() cardinal {} -element FinSequence-membered V63() V64() V65() V66() V67() V68() V69() V179(V) circled Element of K10( the carrier of V)

the carrier of V is non empty set

K10( the carrier of V) is non empty set

(V,({} V)) is V179(V) circled Element of K10( the carrier of V)

(V,({} V)) is non empty Element of K10(K10( the carrier of V))

K10(K10( the carrier of V)) is non empty set

meet (V,({} V)) is Element of K10( the carrier of V)

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is Element of K10( the carrier of V)

(V,v1) is V179(V) circled Element of K10( the carrier of V)

(V,v1) is non empty Element of K10(K10( the carrier of V))

K10(K10( the carrier of V)) is non empty set

meet (V,v1) is Element of K10( the carrier of V)

v2 is V27() V28() ext-real Element of REAL

v2 * (V,v1) is Element of K10( the carrier of V)

v2 * v1 is Element of K10( the carrier of V)

(V,(v2 * v1)) is V179(V) circled Element of K10( the carrier of V)

(V,(v2 * v1)) is non empty Element of K10(K10( the carrier of V))

meet (V,(v2 * v1)) is Element of K10( the carrier of V)

L is set

{} V is empty proper functional V22() cardinal {} -element FinSequence-membered V63() V64() V65() V66() V67() V68() V69() V179(V) circled Element of K10( the carrier of V)

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

{(0. V)} is non empty V2() 1 -element Element of K10( the carrier of V)

{ (v2 * b

L is Element of the carrier of V

v2 * L is Element of the carrier of V

F is set

f is Element of K10( the carrier of V)

v2 " is V27() V28() ext-real Element of REAL

(v2 ") * (v2 * v1) is Element of K10( the carrier of V)

(v2 ") * f is Element of K10( the carrier of V)

(v2 ") * v2 is V27() V28() ext-real Element of REAL

((v2 ") * v2) * v1 is Element of K10( the carrier of V)

1 * v1 is Element of K10( the carrier of V)

{ ((v2 ") * b

r1 is Element of the carrier of V

(v2 ") * r1 is Element of the carrier of V

v2 * (v2 ") is V27() V28() ext-real Element of REAL

(v2 * (v2 ")) * r1 is Element of the carrier of V

1 * r1 is Element of the carrier of V

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

v1 is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() Linear_Combination of V

Carrier v1 is Element of K10( the carrier of V)

K10( the carrier of V) is non empty set

v2 is V10() V13( NAT ) V14( the carrier of V) Function-like V39() FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng v2 is set

len v2 is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

L is V10() V13( NAT ) V14( REAL ) Function-like V39() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL

len L is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

Sum L is V27() V28() ext-real Element of REAL

K258(REAL,L,K187()) is V27() V28() ext-real Element of REAL

dom L is V63() V64() V65() V66() V67() V68() Element of K10(NAT)

L is V10() V13( NAT ) V14( REAL ) Function-like V39() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL

len L is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

Sum L is V27() V28() ext-real Element of REAL

K258(REAL,L,K187()) is V27() V28() ext-real Element of REAL

dom L is V63() V64() V65() V66() V67() V68() Element of K10(NAT)

<*> the carrier of V is empty V10() V13( NAT ) V14( the carrier of V) Function-like functional V22() V26() V27() V28() V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() FinSequence of the carrier of V

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

v1 is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() Linear_Combination of V

Carrier v1 is Element of K10( the carrier of V)

K10( the carrier of V) is non empty set

v2 is Element of the carrier of V

v1 . v2 is V27() V28() ext-real Element of REAL

L is V10() V13( NAT ) V14( the carrier of V) Function-like V39() FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng L is set

len L is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

dom L is V63() V64() V65() V66() V67() V68() Element of K10(NAT)

L is set

L . L is set

f is V10() V13( NAT ) V14( REAL ) Function-like V39() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL

len f is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

Sum f is V27() V28() ext-real Element of REAL

K258(REAL,f,K187()) is V27() V28() ext-real Element of REAL

dom f is V63() V64() V65() V66() V67() V68() Element of K10(NAT)

f is V10() V13( NAT ) V14( REAL ) Function-like V39() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL

len f is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

Sum f is V27() V28() ext-real Element of REAL

K258(REAL,f,K187()) is V27() V28() ext-real Element of REAL

dom f is V63() V64() V65() V66() V67() V68() Element of K10(NAT)

F is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

Seg (len L) is V39() len L -element V63() V64() V65() V66() V67() V68() Element of K10(NAT)

f . F is V27() V28() ext-real set

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

ZeroLC V is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() Linear_Combination of V

v1 is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() Linear_Combination of V

Carrier v1 is Element of K10( the carrier of V)

K10( the carrier of V) is non empty set

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

the Element of the carrier of V is Element of the carrier of V

{ the Element of the carrier of V} is non empty V2() 1 -element Element of K10( the carrier of V)

K10( the carrier of V) is non empty set

v2 is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() Linear_Combination of { the Element of the carrier of V}

v2 . the Element of the carrier of V is V27() V28() ext-real Element of REAL

<* the Element of the carrier of V*> is non empty V2() V10() V13( NAT ) V14( the carrier of V) Function-like V39() 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng <* the Element of the carrier of V*> is set

Carrier v2 is Element of K10( the carrier of V)

len <* the Element of the carrier of V*> is non empty V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

<*1*> is non empty V2() V10() V13( NAT ) V14( REAL ) Function-like one-to-one V39() 1 -element FinSequence-like FinSubsequence-like V53() V54() V55() V57() V58() V59() V60() FinSequence of REAL

L is V10() V13( NAT ) V14( REAL ) Function-like V39() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL

len L is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

Sum L is V27() V28() ext-real Element of REAL

K258(REAL,L,K187()) is V27() V28() ext-real Element of REAL

dom L is V63() V64() V65() V66() V67() V68() Element of K10(NAT)

L is V22() V26() V27() V28() V39() cardinal ext-real set

L . L is V27() V28() ext-real set

<* the Element of the carrier of V*> . L is set

v2 . (<* the Element of the carrier of V*> . L) is V27() V28() ext-real set

{1} is non empty V2() 1 -element V63() V64() V65() V66() V67() V68() Element of K10(REAL)

len <*1*> is non empty V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

L is V22() V26() V27() V28() V39() cardinal ext-real set

L . L is V27() V28() ext-real set

<* the Element of the carrier of V*> . L is set

v2 . (<* the Element of the carrier of V*> . L) is V27() V28() ext-real set

{ b

L is V10() V13( NAT ) V14( REAL ) Function-like V39() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL

len L is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

Sum L is V27() V28() ext-real Element of REAL

K258(REAL,L,K187()) is V27() V28() ext-real Element of REAL

dom L is V63() V64() V65() V66() V67() V68() Element of K10(NAT)

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is non empty Element of K10( the carrier of V)

v2 is set

L is Element of the carrier of V

{L} is non empty V2() 1 -element Element of K10( the carrier of V)

L is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() Linear_Combination of {L}

L . L is V27() V28() ext-real Element of REAL

F is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() Linear_Combination of v1

<*L*> is non empty V2() V10() V13( NAT ) V14( the carrier of V) Function-like V39() 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng <*L*> is set

Carrier F is Element of K10( the carrier of V)

len <*L*> is non empty V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

<*1*> is non empty V2() V10() V13( NAT ) V14( REAL ) Function-like one-to-one V39() 1 -element FinSequence-like FinSubsequence-like V53() V54() V55() V57() V58() V59() V60() FinSequence of REAL

f is V10() V13( NAT ) V14( REAL ) Function-like V39() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL

len f is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

Sum f is V27() V28() ext-real Element of REAL

K258(REAL,f,K187()) is V27() V28() ext-real Element of REAL

dom f is V63() V64() V65() V66() V67() V68() Element of K10(NAT)

r1 is V22() V26() V27() V28() V39() cardinal ext-real set

f . r1 is V27() V28() ext-real set

<*L*> . r1 is set

F . (<*L*> . r1) is V27() V28() ext-real set

{1} is non empty V2() 1 -element V63() V64() V65() V66() V67() V68() Element of K10(REAL)

len <*1*> is non empty V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

r1 is V22() V26() V27() V28() V39() cardinal ext-real set

f . r1 is V27() V28() ext-real set

<*L*> . r1 is set

F . (<*L*> . r1) is V27() V28() ext-real set

{ b

f is V10() V13( NAT ) V14( REAL ) Function-like V39() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL

len f is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

Sum f is V27() V28() ext-real Element of REAL

K258(REAL,f,K187()) is V27() V28() ext-real Element of REAL

dom f is V63() V64() V65() V66() V67() V68() Element of K10(NAT)

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

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

v1 is set

v2 is set

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is non empty Element of K10( the carrier of V)

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

v2 is set

L is set

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is Element of the carrier of V

{v1} is non empty V2() 1 -element Element of K10( the carrier of V)

v2 is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() Linear_Combination of {v1}

v2 . v1 is V27() V28() ext-real Element of REAL

Carrier v2 is Element of K10( the carrier of V)

Sum v2 is Element of the carrier of V

L is V10() V13( NAT ) V14( the carrier of V) Function-like V39() FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng L is set

v2 (#) L is V10() V13( NAT ) V14( the carrier of V) Function-like V39() FinSequence-like FinSubsequence-like FinSequence of the carrier of V

Sum (v2 (#) L) is Element of the carrier of V

<*v1*> is non empty V2() V10() V13( NAT ) V14( the carrier of V) Function-like V39() 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V

L . 1 is set

len L is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

L is V10() V13( NAT ) Function-like V39() FinSequence-like FinSubsequence-like set

len L is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

dom L is V63() V64() V65() V66() V67() V68() Element of K10(NAT)

L . 1 is set

v2 . (L . 1) is V27() V28() ext-real set

<*1*> is non empty V2() V10() V13( NAT ) V14( REAL ) Function-like one-to-one V39() 1 -element FinSequence-like FinSubsequence-like V53() V54() V55() V57() V58() V59() V60() FinSequence of REAL

F is V10() V13( NAT ) V14( REAL ) Function-like V39() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL

dom F is V63() V64() V65() V66() V67() V68() Element of K10(NAT)

f is V22() V26() V27() V28() V39() cardinal ext-real set

F . f is V27() V28() ext-real set

L . f is set

v2 . (L . f) is V27() V28() ext-real set

len F is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

Seg (len F) is V39() len F -element V63() V64() V65() V66() V67() V68() Element of K10(NAT)

Sum F is V27() V28() ext-real Element of REAL

K258(REAL,F,K187()) is V27() V28() ext-real Element of REAL

f is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() (V) Linear_Combination of V

r1 is non empty Element of K10( the carrier of V)

Sum f is Element of the carrier of V

1 * v1 is Element of the carrier of V

r1 is non empty Element of K10( the carrier of V)

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v1 is Element of the carrier of V

v2 is Element of the carrier of V

{v1,v2} is non empty Element of K10( the carrier of V)

1 / 2 is V27() V28() ext-real non negative Element of REAL

L is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() Linear_Combination of {v1,v2}

L . v1 is V27() V28() ext-real Element of REAL

L . v2 is V27() V28() ext-real Element of REAL

Carrier L is Element of K10( the carrier of V)

Sum L is Element of the carrier of V

L is V10() V13( NAT ) V14( the carrier of V) Function-like V39() FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng L is set

L (#) L is V10() V13( NAT ) V14( the carrier of V) Function-like V39() FinSequence-like FinSubsequence-like FinSequence of the carrier of V

Sum (L (#) L) is Element of the carrier of V

len L is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

F is V10() V13( NAT ) Function-like V39() FinSequence-like FinSubsequence-like set

len F is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

dom F is V63() V64() V65() V66() V67() V68() Element of K10(NAT)

F . 2 is set

L . 2 is set

L . (L . 2) is V27() V28() ext-real set

F . 1 is set

L . 1 is set

L . (L . 1) is V27() V28() ext-real set

<*v1,v2*> is non empty V10() V13( NAT ) Function-like V39() 2 -element FinSequence-like FinSubsequence-like set

<*(1 / 2),(1 / 2)*> is non empty V10() V13( NAT ) Function-like V39() 2 -element FinSequence-like FinSubsequence-like set

<*(1 / 2)*> is non empty V2() V10() V13( NAT ) V14( REAL ) Function-like one-to-one V39() 1 -element FinSequence-like FinSubsequence-like V53() V54() V55() V57() V58() V59() V60() FinSequence of REAL

<*(1 / 2)*> ^ <*(1 / 2)*> is non empty V10() V13( NAT ) V14( REAL ) Function-like V39() K266(1,1) -element FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL

K266(1,1) is non empty V22() V26() V27() V28() V33() V34() V39() cardinal ext-real positive non negative V63() V64() V65() V66() V67() V68() Element of NAT

rng F is set

rng <*(1 / 2)*> is V63() V64() V65() Element of K10(REAL)

(rng <*(1 / 2)*>) \/ (rng <*(1 / 2)*>) is V63() V64() V65() Element of K10(REAL)

{(1 / 2)} is non empty V2() 1 -element V63() V64() V65() Element of K10(REAL)

f is V10() V13( NAT ) V14( REAL ) Function-like V39() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL

dom f is V63() V64() V65() V66() V67() V68() Element of K10(NAT)

r1 is V22() V26() V27() V28() V39() cardinal ext-real set

f . r1 is V27() V28() ext-real set

L . r1 is set

L . (L . r1) is V27() V28() ext-real set

len f is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

Seg (len f) is V39() len f -element V63() V64() V65() V66() V67() V68() Element of K10(NAT)

Sum f is V27() V28() ext-real Element of REAL

K258(REAL,f,K187()) is V27() V28() ext-real Element of REAL

(1 / 2) + (1 / 2) is V27() V28() ext-real non negative Element of REAL

r1 is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() (V) Linear_Combination of V

r2 is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() (V) Linear_Combination of V

x1 is non empty Element of K10( the carrier of V)

<*v2,v1*> is non empty V10() V13( NAT ) Function-like V39() 2 -element FinSequence-like FinSubsequence-like set

<*(1 / 2),(1 / 2)*> is non empty V10() V13( NAT ) Function-like V39() 2 -element FinSequence-like FinSubsequence-like set

<*(1 / 2)*> is non empty V2() V10() V13( NAT ) V14( REAL ) Function-like one-to-one V39() 1 -element FinSequence-like FinSubsequence-like V53() V54() V55() V57() V58() V59() V60() FinSequence of REAL

<*(1 / 2)*> ^ <*(1 / 2)*> is non empty V10() V13( NAT ) V14( REAL ) Function-like V39() K266(1,1) -element FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL

K266(1,1) is non empty V22() V26() V27() V28() V33() V34() V39() cardinal ext-real positive non negative V63() V64() V65() V66() V67() V68() Element of NAT

rng F is set

rng <*(1 / 2)*> is V63() V64() V65() Element of K10(REAL)

(rng <*(1 / 2)*>) \/ (rng <*(1 / 2)*>) is V63() V64() V65() Element of K10(REAL)

{(1 / 2)} is non empty V2() 1 -element V63() V64() V65() Element of K10(REAL)

f is V10() V13( NAT ) V14( REAL ) Function-like V39() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL

dom f is V63() V64() V65() V66() V67() V68() Element of K10(NAT)

r1 is V22() V26() V27() V28() V39() cardinal ext-real set

f . r1 is V27() V28() ext-real set

L . r1 is set

L . (L . r1) is V27() V28() ext-real set

len f is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

Seg (len f) is V39() len f -element V63() V64() V65() V66() V67() V68() Element of K10(NAT)

Sum f is V27() V28() ext-real Element of REAL

K258(REAL,f,K187()) is V27() V28() ext-real Element of REAL

(1 / 2) + (1 / 2) is V27() V28() ext-real non negative Element of REAL

r1 is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() (V) Linear_Combination of V

r2 is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() (V) Linear_Combination of V

x1 is non empty Element of K10( the carrier of V)

<*v1,v2*> is non empty V10() V13( NAT ) Function-like V39() 2 -element FinSequence-like FinSubsequence-like set

<*v2,v1*> is non empty V10() V13( NAT ) Function-like V39() 2 -element FinSequence-like FinSubsequence-like set

r1 is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() (V) Linear_Combination of V

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

v1 is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() (V) Linear_Combination of V

v2 is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() (V) Linear_Combination of V

L is V27() V28() ext-real Element of REAL

L is V27() V28() ext-real Element of REAL

L * L is V27() V28() ext-real Element of REAL

L * v1 is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() Linear_Combination of V

L * v2 is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() Linear_Combination of V

(L * v1) + (L * v2) is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() Linear_Combination of V

Carrier ((L * v1) + (L * v2)) is Element of K10( the carrier of V)

K10( the carrier of V) is non empty set

Carrier (L * v1) is Element of K10( the carrier of V)

Carrier (L * v2) is Element of K10( the carrier of V)

(Carrier (L * v1)) \/ (Carrier (L * v2)) is Element of K10( the carrier of V)

Carrier v2 is Element of K10( the carrier of V)

Carrier v1 is Element of K10( the carrier of V)

F is set

{ b

f is Element of the carrier of V

(L * v1) . f is V27() V28() ext-real Element of REAL

v1 . f is V27() V28() ext-real Element of REAL

v2 . f is V27() V28() ext-real Element of REAL

L * (v2 . f) is V27() V28() ext-real Element of REAL

(L * v2) . f is V27() V28() ext-real Element of REAL

((L * v1) . f) + ((L * v2) . f) is V27() V28() ext-real Element of REAL

L * (v1 . f) is V27() V28() ext-real Element of REAL

((L * v1) + (L * v2)) . f is V27() V28() ext-real Element of REAL

L * (v1 . f) is V27() V28() ext-real Element of REAL

(L * v2) . f is V27() V28() ext-real Element of REAL

((L * v1) . f) + ((L * v2) . f) is V27() V28() ext-real Element of REAL

L * (v2 . f) is V27() V28() ext-real Element of REAL

((L * v1) + (L * v2)) . f is V27() V28() ext-real Element of REAL

v2 . f is V27() V28() ext-real Element of REAL

L * (v2 . f) is V27() V28() ext-real Element of REAL

(L * v2) . f is V27() V28() ext-real Element of REAL

((L * v1) . f) + ((L * v2) . f) is V27() V28() ext-real Element of REAL

((L * v1) + (L * v2)) . f is V27() V28() ext-real Element of REAL

{ b

f is Element of the carrier of V

(L * v2) . f is V27() V28() ext-real Element of REAL

v2 . f is V27() V28() ext-real Element of REAL

v1 . f is V27() V28() ext-real Element of REAL

L * (v2 . f) is V27() V28() ext-real Element of REAL

(L * v1) . f is V27() V28() ext-real Element of REAL

((L * v1) . f) + ((L * v2) . f) is V27() V28() ext-real Element of REAL

L * (v1 . f) is V27() V28() ext-real Element of REAL

((L * v1) + (L * v2)) . f is V27() V28() ext-real Element of REAL

L * (v1 . f) is V27() V28() ext-real Element of REAL

(L * v1) . f is V27() V28() ext-real Element of REAL

((L * v1) . f) + ((L * v2) . f) is V27() V28() ext-real Element of REAL

L * (v2 . f) is V27() V28() ext-real Element of REAL

((L * v1) + (L * v2)) . f is V27() V28() ext-real Element of REAL

v1 . f is V27() V28() ext-real Element of REAL

L * (v1 . f) is V27() V28() ext-real Element of REAL

(L * v1) . f is V27() V28() ext-real Element of REAL

((L * v1) . f) + ((L * v2) . f) is V27() V28() ext-real Element of REAL

((L * v1) + (L * v2)) . f is V27() V28() ext-real Element of REAL

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

v1 is Element of the carrier of V

{v1} is non empty V2() 1 -element Element of K10( the carrier of V)

K10( the carrier of V) is non empty set

v2 is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() Linear_Combination of V

Carrier v2 is Element of K10( the carrier of V)

v2 . v1 is V27() V28() ext-real Element of REAL

Sum v2 is Element of the carrier of V

(v2 . v1) * v1 is Element of the carrier of V

L is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() Linear_Combination of {v1}

Carrier L is Element of K10( the carrier of V)

L is V10() V13( NAT ) V14( the carrier of V) Function-like V39() FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng L is set

len L is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

<*v1*> is non empty V2() V10() V13( NAT ) V14( the carrier of V) Function-like V39() 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V

F is V10() V13( NAT ) V14( REAL ) Function-like V39() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL

len F is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

Sum F is V27() V28() ext-real Element of REAL

K258(REAL,F,K187()) is V27() V28() ext-real Element of REAL

dom F is V63() V64() V65() V66() V67() V68() Element of K10(NAT)

F is V10() V13( NAT ) V14( REAL ) Function-like V39() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL

len F is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

Sum F is V27() V28() ext-real Element of REAL

K258(REAL,F,K187()) is V27() V28() ext-real Element of REAL

dom F is V63() V64() V65() V66() V67() V68() Element of K10(NAT)

F /. 1 is V27() V28() ext-real Element of REAL

card (Carrier L) is V22() cardinal set

F . 1 is V27() V28() ext-real set

f is V27() V28() ext-real Element of REAL

<*f*> is non empty V2() V10() V13( NAT ) V14( REAL ) Function-like one-to-one V39() 1 -element FinSequence-like FinSubsequence-like V53() V54() V55() V57() V58() V59() V60() FinSequence of REAL

L . 1 is set

L . (L . 1) is V27() V28() ext-real set

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

v1 is Element of the carrier of V

v2 is Element of the carrier of V

{v1,v2} is non empty Element of K10( the carrier of V)

K10( the carrier of V) is non empty set

L is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() Linear_Combination of V

Carrier L is Element of K10( the carrier of V)

L . v1 is V27() V28() ext-real Element of REAL

L . v2 is V27() V28() ext-real Element of REAL

(L . v1) + (L . v2) is V27() V28() ext-real Element of REAL

Sum L is Element of the carrier of V

(L . v1) * v1 is Element of the carrier of V

(L . v2) * v2 is Element of the carrier of V

((L . v1) * v1) + ((L . v2) * v2) is Element of the carrier of V

L is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() Linear_Combination of {v1,v2}

Carrier L is Element of K10( the carrier of V)

F is V10() V13( NAT ) V14( the carrier of V) Function-like V39() FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng F is set

len F is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

f is V10() V13( NAT ) V14( REAL ) Function-like V39() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL

len f is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

Sum f is V27() V28() ext-real Element of REAL

K258(REAL,f,K187()) is V27() V28() ext-real Element of REAL

dom f is V63() V64() V65() V66() V67() V68() Element of K10(NAT)

f is V10() V13( NAT ) V14( REAL ) Function-like V39() FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL

len f is V22() V26() V27() V28() V33() V34() V39() cardinal ext-real V63() V64() V65() V66() V67() V68() Element of NAT

Sum f is V27() V28() ext-real Element of REAL

K258(REAL,f,K187()) is V27() V28() ext-real Element of REAL

dom f is V63() V64() V65() V66() V67() V68() Element of K10(NAT)

card {v1,v2} is non empty V22() cardinal set

{1,2} is non empty V63() V64() V65() V66() V67() V68() Element of K10(REAL)

f . 1 is V27() V28() ext-real set

F . 1 is set

L . (F . 1) is V27() V28() ext-real set

f /. 1 is V27() V28() ext-real Element of REAL

f . 2 is V27() V28() ext-real set

F . 2 is set

L . (F . 2) is V27() V28() ext-real set

f /. 2 is V27() V28() ext-real Element of REAL

r1 is V27() V28() ext-real Element of REAL

r2 is V27() V28() ext-real Element of REAL

<*r1,r2*> is non empty V10() V13( NAT ) Function-like V39() 2 -element FinSequence-like FinSubsequence-like set

<*v1,v2*> is non empty V10() V13( NAT ) Function-like V39() 2 -element FinSequence-like FinSubsequence-like set

L . v1 is V27() V28() ext-real Element of REAL

L . v2 is V27() V28() ext-real Element of REAL

(L . v1) + (L . v2) is V27() V28() ext-real Element of REAL

<*v2,v1*> is non empty V10() V13( NAT ) Function-like V39() 2 -element FinSequence-like FinSubsequence-like set

L . v1 is V27() V28() ext-real Element of REAL

L . v2 is V27() V28() ext-real Element of REAL

(L . v1) + (L . v2) is V27() V28() ext-real Element of REAL

<*v1,v2*> is non empty V10() V13( NAT ) Function-like V39() 2 -element FinSequence-like FinSubsequence-like set

<*v2,v1*> is non empty V10() V13( NAT ) Function-like V39() 2 -element FinSequence-like FinSubsequence-like set

L . v1 is V27() V28() ext-real Element of REAL

L . v2 is V27() V28() ext-real Element of REAL

(L . v1) + (L . v2) is V27() V28() ext-real Element of REAL

L . v1 is V27() V28() ext-real Element of REAL

L . v2 is V27() V28() ext-real Element of REAL

(L . v1) + (L . v2) is V27() V28() ext-real Element of REAL

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

v1 is Element of the carrier of V

{v1} is non empty V2() 1 -element Element of K10( the carrier of V)

K10( the carrier of V) is non empty set

v2 is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() Linear_Combination of {v1}

v2 . v1 is V27() V28() ext-real Element of REAL

Sum v2 is Element of the carrier of V

(v2 . v1) * v1 is Element of the carrier of V

Carrier v2 is Element of K10( the carrier of V)

V is non empty V112() V113() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V145() RLSStruct

the carrier of V is non empty set

v1 is Element of the carrier of V

v2 is Element of the carrier of V

{v1,v2} is non empty Element of K10( the carrier of V)

K10( the carrier of V) is non empty set

L is V10() V13( the carrier of V) V14( REAL ) Function-like quasi_total V53() V54() V55() Linear_Combination of {v1,v2}

L . v1 is V27() V28() ext-real Element of REAL

L . v2 is V27() V28() ext-real Element of REAL

(L . v1) + (L . v2) is V27() V28() ext-real Element of REAL

Sum L is Element of the carrier of V

(L . v1) * v1 is Element of the carrier of V

(L . v2) * v2 is Element of the carrier of V

((L . v1) * v1) + ((L . v2) * v2) is Element of the carrier of V

Carrier L is Element of K10( the carrier of V)

{v1} is non empty V2() 1 -element Element of K10( the carrier of V)

{ b

{v2} is non empty V2() 1 -element Element of K10( the carrier of V)

{ b

{v1} is non empty V2() 1 -element Element of K10( the carrier of V)

{v2} is non empty V2() 1 -element Element of K10( the carrier of V)