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
{ (b1 - b2) where b1, b2 is Element of the carrier of V : ( b1 in v1 & b2 in 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 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)
{ (b1 - b2) where b1, b2 is Element of the carrier of V : ( b1 in v1 & b2 in v2 ) } is set
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 * b1) where b1 is Element of the carrier of V : b1 in v1 - v2 } is set
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 * b1) where b1 is Element of the carrier of V : b1 in v1 } is set
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 * b1) where b1 is Element of the carrier of V : b1 in v1 } is set
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
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in L * v1 & b2 in L * v2 ) } is set
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 * b1) where b1 is Element of the carrier of V : b1 in v1 } is set
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 * b1) where b1 is Element of the carrier of V : b1 in v2 } is set
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 * b1) where b1 is Element of the carrier of V : b1 in (V,v1) } is set
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 ") * b1) where b1 is Element of the carrier of V : b1 in f } is set
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
{ b1 where b1 is Element of the carrier of V : not v2 . b1 = 0 } is set
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
{ b1 where b1 is Element of the carrier of V : not F . b1 = 0 } 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)
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
{ b1 where b1 is Element of the carrier of V : not (L * v1) . b1 = 0 } is set
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
{ b1 where b1 is Element of the carrier of V : not (L * v2) . b1 = 0 } is set
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)
{ b1 where b1 is Element of the carrier of V : not L . b1 = 0 } is set
{v2} is non empty V2() 1 -element Element of K10( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not L . b1 = 0 } is set
{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)