REAL is non empty V12() non finite set
NAT is non empty V12() V24() V25() V26() non finite cardinal limit_cardinal Element of K19(REAL)
K19(REAL) is V12() non finite set
NAT is non empty V12() V24() V25() V26() non finite cardinal limit_cardinal set
K19(NAT) is V12() non finite set
K19(NAT) is V12() non finite set
COMPLEX is non empty V12() non finite set
RAT is non empty V12() non finite set
INT is non empty V12() non finite set
{} is Function-like functional empty ext-real V24() V25() V26() V28() V29() V30() V31() V32() finite V37() cardinal {} -element FinSequence-membered integer set
2 is non empty ext-real positive V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
K20(NAT,REAL) is V12() non finite set
K19(K20(NAT,REAL)) is V12() non finite set
K20(COMPLEX,COMPLEX) is V12() non finite set
K19(K20(COMPLEX,COMPLEX)) is V12() non finite set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is V12() non finite set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is V12() non finite set
K20(REAL,REAL) is V12() non finite set
K19(K20(REAL,REAL)) is V12() non finite set
K20(K20(REAL,REAL),REAL) is V12() non finite set
K19(K20(K20(REAL,REAL),REAL)) is V12() non finite set
K20(RAT,RAT) is V12() non finite set
K19(K20(RAT,RAT)) is V12() non finite set
K20(K20(RAT,RAT),RAT) is V12() non finite set
K19(K20(K20(RAT,RAT),RAT)) is V12() non finite set
K20(INT,INT) is V12() non finite set
K19(K20(INT,INT)) is V12() non finite set
K20(K20(INT,INT),INT) is V12() non finite set
K19(K20(K20(INT,INT),INT)) is V12() non finite set
K20(NAT,NAT) is V12() non finite set
K20(K20(NAT,NAT),NAT) is V12() non finite set
K19(K20(K20(NAT,NAT),NAT)) is V12() non finite set
1 is non empty ext-real positive V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
K20(1,1) is finite set
K19(K20(1,1)) is finite V37() set
K20(K20(1,1),1) is finite set
K19(K20(K20(1,1),1)) is finite V37() set
K20(K20(1,1),REAL) is set
K19(K20(K20(1,1),REAL)) is set
K20(2,2) is finite set
K20(K20(2,2),REAL) is set
K19(K20(K20(2,2),REAL)) is set
K534(2) is V206() L20()
the carrier of K534(2) is set
K580() is L18()
the carrier of K580() is set
K508() is V190() L19()
K585() is V173() L18()
K587() is M24(K585())
K565(K587(),K587()) is V172() V173() L18()
the carrier of K565(K587(),K587()) is set
K589() is V221() M24(K585())
the carrier of K589() is set
K19( the carrier of K589()) is set
K19(K19( the carrier of K589())) is set
K598(2) is M24(K534(2))
the carrier of K598(2) is set
K20( the carrier of K589(), the carrier of K598(2)) is set
K19(K20( the carrier of K589(), the carrier of K598(2))) is set
K602() is Relation-like the carrier of K589() -defined the carrier of K598(2) -valued Function-like quasi_total Element of K19(K20( the carrier of K589(), the carrier of K598(2)))
K599() is Element of the carrier of K598(2)
K601(K599()) is V172() M24(K598(2))
the carrier of K601(K599()) is set
0 is Function-like functional empty ext-real V24() V25() V26() V28() V29() V30() V31() V32() finite V37() cardinal {} -element FinSequence-membered integer Element of NAT
K472(0,1) is Element of K19(REAL)
K595(K472(0,1)) is Element of K19( the carrier of K589())
K475(K589(),K595(K472(0,1))) is V172() M24(K589())
the carrier of K475(K589(),K595(K472(0,1))) is set
K20( the carrier of K601(K599()), the carrier of K475(K589(),K595(K472(0,1)))) is set
K19(K20( the carrier of K601(K599()), the carrier of K475(K589(),K595(K472(0,1))))) is set
K600() is Element of the carrier of K598(2)
K601(K600()) is V172() M24(K598(2))
the carrier of K601(K600()) is set
1 / 2 is ext-real V31() V32() Element of REAL
3 is non empty ext-real positive V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
3 / 2 is ext-real V31() V32() Element of REAL
K472((1 / 2),(3 / 2)) is Element of K19(REAL)
K595(K472((1 / 2),(3 / 2))) is Element of K19( the carrier of K589())
K475(K589(),K595(K472((1 / 2),(3 / 2)))) is V172() M24(K589())
the carrier of K475(K589(),K595(K472((1 / 2),(3 / 2)))) is set
K20( the carrier of K601(K600()), the carrier of K475(K589(),K595(K472((1 / 2),(3 / 2))))) is set
K19(K20( the carrier of K601(K600()), the carrier of K475(K589(),K595(K472((1 / 2),(3 / 2)))))) is set
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
A is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len A is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
B is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len B is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
A + B is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (A + B) is Element of the carrier of V
Sum A is Element of the carrier of V
Sum B is Element of the carrier of V
(Sum A) + (Sum B) is Element of the carrier of V
dom A is finite Element of K19(NAT)
dom B is finite Element of K19(NAT)
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
A is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len A is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
B is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len B is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
g1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
A - B is Relation-like NAT -defined the carrier of V -valued Function-like Element of K19(K20(NAT, the carrier of V))
K20(NAT, the carrier of V) is V12() non finite set
K19(K20(NAT, the carrier of V)) is V12() non finite set
Sum g1 is Element of the carrier of V
Sum A is Element of the carrier of V
Sum B is Element of the carrier of V
(Sum A) - (Sum B) is Element of the carrier of V
dom A is finite Element of K19(NAT)
dom B is finite Element of K19(NAT)
dom g1 is finite Element of K19(NAT)
(dom A) /\ (dom B) is finite Element of K19(NAT)
len g1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
h1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
g1 . h1 is set
A /. h1 is Element of the carrier of V
B /. h1 is Element of the carrier of V
(A /. h1) - (B /. h1) is Element of the carrier of V
g1 /. h1 is Element of the carrier of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
B is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
A is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum B is Element of the carrier of V
Sum A is Element of the carrier of V
g1 is ext-real V31() V32() Element of REAL
g1 (#) A is Relation-like NAT -defined the carrier of V -valued Function-like Element of K19(K20(NAT, the carrier of V))
K20(NAT, the carrier of V) is V12() non finite set
K19(K20(NAT, the carrier of V)) is V12() non finite set
g1 * (Sum A) is Element of the carrier of V
dom B is finite Element of K19(NAT)
dom A is finite Element of K19(NAT)
len B is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
len A is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
h1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
B . h1 is set
A /. h1 is Element of the carrier of V
g1 * (A /. h1) is Element of the carrier of V
B /. h1 is Element of the carrier of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
A is ext-real V31() V32() integer set
B is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of V
K20( the carrier of V,REAL) is V12() non finite set
K19(K20( the carrier of V,REAL)) is V12() non finite set
g1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20( the carrier of V,REAL))
Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL
a1 is Element of the carrier of V
Carrier B is finite Element of K19( the carrier of V)
K19( the carrier of V) is set
{ b1 where b1 is Element of the carrier of V : not B . b1 = 0 } is set
B . a1 is ext-real V31() V32() Element of REAL
h1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of V,REAL)
h1 . a1 is ext-real V31() V32() Element of REAL
A * 0 is ext-real V31() V32() integer Element of INT
a1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of V
g1 is Element of the carrier of V
a1 . g1 is ext-real V31() V32() Element of REAL
B . g1 is ext-real V31() V32() Element of REAL
A * (B . g1) is ext-real V31() V32() Element of REAL
g1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of V
h1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of V
a1 is Element of the carrier of V
g1 . a1 is ext-real V31() V32() Element of REAL
h1 . a1 is ext-real V31() V32() Element of REAL
g1 . a1 is ext-real V31() V32() Element of REAL
B . a1 is ext-real V31() V32() Element of REAL
A * (B . a1) is ext-real V31() V32() Element of REAL
h1 . a1 is ext-real V31() V32() Element of REAL
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is set
A is Element of K19( the carrier of V)
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A : rng b1 c= INT } is set
g1 is set
h1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A
Sum h1 is Element of the carrier of V
rng h1 is V117() V118() V119() Element of K19(REAL)
V is ext-real V31() V32() Element of REAL
A is ext-real V31() V32() integer set
B is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of B is non empty set
K19( the carrier of B) is set
g1 is Element of K19( the carrier of B)
h1 is Relation-like the carrier of B -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of g1
V * h1 is Relation-like the carrier of B -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of B
(B,A,h1) is Relation-like the carrier of B -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of B
a1 is Element of the carrier of B
(B,A,h1) . a1 is ext-real V31() V32() Element of REAL
h1 . a1 is ext-real V31() V32() Element of REAL
V * (h1 . a1) is ext-real V31() V32() Element of REAL
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is set
A is Element of K19( the carrier of V)
B is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A
rng B is V117() V118() V119() Element of K19(REAL)
g1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A
rng g1 is V117() V118() V119() Element of K19(REAL)
B + g1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of V
rng (B + g1) is V117() V118() V119() Element of K19(REAL)
h1 is set
a1 is set
(B + g1) . a1 is ext-real V31() V32() Element of REAL
g1 is Element of the carrier of V
B . g1 is ext-real V31() V32() Element of REAL
g1 . g1 is ext-real V31() V32() Element of REAL
(B + g1) . g1 is ext-real V31() V32() Element of REAL
h1 is ext-real V31() V32() integer set
a1 is ext-real V31() V32() integer set
h1 + a1 is ext-real V31() V32() integer Element of INT
V is ext-real V31() V32() integer set
A is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of A is non empty set
K19( the carrier of A) is set
B is Element of K19( the carrier of A)
g1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of B
rng g1 is V117() V118() V119() Element of K19(REAL)
(A,V,g1) is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A
rng (A,V,g1) is V117() V118() V119() Element of K19(REAL)
h1 is set
a1 is set
(A,V,g1) . a1 is ext-real V31() V32() Element of REAL
g1 is Element of the carrier of A
g1 . g1 is ext-real V31() V32() Element of REAL
(A,V,g1) . g1 is ext-real V31() V32() Element of REAL
h1 is ext-real V31() V32() Element of REAL
h1 * g1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A
(h1 * g1) . g1 is ext-real V31() V32() Element of REAL
a1 is ext-real V31() V32() integer set
V * a1 is ext-real V31() V32() integer Element of INT
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of V
the carrier of V is non empty set
rng (ZeroLC V) is V117() V118() V119() Element of K19(REAL)
A is set
B is set
(ZeroLC V) . B is ext-real V31() V32() Element of REAL
g1 is Element of the carrier of V
(ZeroLC V) . g1 is ext-real V31() V32() Element of REAL
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is set
A is Element of K19( the carrier of V)
(V,A) is Element of K19( the carrier of V)
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A : rng b1 c= INT } is set
Lin A is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of (Lin A) is non empty set
B is set
g1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A
Sum g1 is Element of the carrier of V
rng g1 is V117() V118() V119() Element of K19(REAL)
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is set
A is Element of the carrier of V
B is Element of the carrier of V
A + B is Element of the carrier of V
g1 is Element of K19( the carrier of V)
(V,g1) is Element of K19( the carrier of V)
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of g1 : rng b1 c= INT } is set
h1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of g1
Sum h1 is Element of the carrier of V
rng h1 is V117() V118() V119() Element of K19(REAL)
a1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of g1
Sum a1 is Element of the carrier of V
rng a1 is V117() V118() V119() Element of K19(REAL)
h1 + a1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of V
g1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of g1
rng g1 is V117() V118() V119() Element of K19(REAL)
Sum g1 is Element of the carrier of V
V is ext-real V31() V32() integer set
A is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of A is non empty set
K19( the carrier of A) is set
B is Element of the carrier of A
V * B is Element of the carrier of A
g1 is Element of K19( the carrier of A)
(A,g1) is Element of K19( the carrier of A)
{ (Sum b1) where b1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of g1 : rng b1 c= INT } is set
h1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of g1
Sum h1 is Element of the carrier of A
rng h1 is V117() V118() V119() Element of K19(REAL)
a1 is ext-real V31() V32() Element of REAL
a1 * h1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A
(A,V,h1) is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A
g1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of g1
Sum g1 is Element of the carrier of A
rng (A,V,h1) is V117() V118() V119() Element of K19(REAL)
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is set
0. V is V52(V) Element of the carrier of V
A is Element of K19( the carrier of V)
(V,A) is Element of K19( the carrier of V)
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A : rng b1 c= INT } is set
ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of V
B is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A
Sum B is Element of the carrier of V
rng B is V117() V118() V119() Element of K19(REAL)
V is set
A is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of A is non empty set
K19( the carrier of A) is set
B is Element of K19( the carrier of A)
(A,B) is Element of K19( the carrier of A)
{ (Sum b1) where b1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of B : rng b1 c= INT } is set
K20( the carrier of A,REAL) is V12() non finite set
K19(K20( the carrier of A,REAL)) is V12() non finite set
g1 is Element of the carrier of A
h1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20( the carrier of A,REAL))
h1 . g1 is ext-real V31() V32() Element of REAL
Funcs ( the carrier of A,REAL) is non empty FUNCTION_DOMAIN of the carrier of A, REAL
a1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of A,REAL)
{g1} is non empty V12() finite 1 -element Element of K19( the carrier of A)
g1 is non empty V12() finite 1 -element Element of K19( the carrier of A)
h1 is Element of the carrier of A
a1 . h1 is ext-real V31() V32() Element of REAL
h1 is finite Element of K19( the carrier of A)
g1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A
Carrier g1 is finite Element of K19( the carrier of A)
{ b1 where b1 is Element of the carrier of A : not g1 . b1 = 0 } is set
{g1} is non empty V12() finite 1 -element Element of K19( the carrier of A)
h1 is set
a1 is Element of the carrier of A
g1 . a1 is ext-real V31() V32() Element of REAL
h1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of {g1}
Sum h1 is Element of the carrier of A
h1 . g1 is ext-real V31() V32() Element of REAL
(h1 . g1) * g1 is Element of the carrier of A
Carrier h1 is finite Element of K19( the carrier of A)
{ b1 where b1 is Element of the carrier of A : not h1 . b1 = 0 } is set
a1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of B
rng a1 is V117() V118() V119() Element of K19(REAL)
gn is set
hn is set
a1 . hn is ext-real V31() V32() Element of REAL
an is Element of the carrier of A
a1 . an is ext-real V31() V32() Element of REAL
an is Element of the carrier of A
an is Element of the carrier of A
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is set
A is Element of K19( the carrier of V)
(V,A) is Element of K19( the carrier of V)
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A : rng b1 c= INT } is set
B is Element of K19( the carrier of V)
(V,B) is Element of K19( the carrier of V)
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of B : rng b1 c= INT } is set
g1 is set
h1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A
Sum h1 is Element of the carrier of V
rng h1 is V117() V118() V119() Element of K19(REAL)
a1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of B
Sum a1 is Element of the carrier of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is set
A is Element of K19( the carrier of V)
(V,A) is Element of K19( the carrier of V)
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A : rng b1 c= INT } is set
B is Element of K19( the carrier of V)
A \/ B is Element of K19( the carrier of V)
(V,(A \/ B)) is Element of K19( the carrier of V)
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A \/ B : rng b1 c= INT } is set
(V,B) is Element of K19( the carrier of V)
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of B : rng b1 c= INT } is set
(V,A) + (V,B) is Element of K19( the carrier of V)
{ K180(V,b1,b2) where b1, b2 is Element of the carrier of V : ( b1 in (V,A) & b2 in (V,B) ) } is set
g1 is set
h1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A \/ B
Sum h1 is Element of the carrier of V
rng h1 is V117() V118() V119() Element of K19(REAL)
Carrier h1 is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not h1 . b1 = 0 } is set
(Carrier h1) \ A is finite Element of K19( the carrier of V)
(Carrier h1) /\ A is finite Element of K19( the carrier of V)
h1 is set
h1 . h1 is ext-real V31() V32() Element of REAL
K20( the carrier of V,REAL) is V12() non finite set
K19(K20( the carrier of V,REAL)) is V12() non finite set
h1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20( the carrier of V,REAL))
Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL
a1 is finite Element of K19( the carrier of V)
gn is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of V,REAL)
hn is Element of the carrier of V
gn . hn is ext-real V31() V32() Element of REAL
hn is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of V
rng hn is V117() V118() V119() Element of K19(REAL)
an is set
i is set
hn . i is ext-real V31() V32() Element of REAL
j is Element of the carrier of V
hn . j is ext-real V31() V32() Element of REAL
j is Element of the carrier of V
hn . j is ext-real V31() V32() Element of REAL
h1 . j is ext-real V31() V32() Element of REAL
j is Element of the carrier of V
Carrier hn is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not hn . b1 = 0 } is set
an is set
i is Element of the carrier of V
hn . i is ext-real V31() V32() Element of REAL
i is set
h1 . i is ext-real V31() V32() Element of REAL
i is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20( the carrier of V,REAL))
j is finite Element of K19( the carrier of V)
a0 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of V,REAL)
b0 is Element of the carrier of V
a0 . b0 is ext-real V31() V32() Element of REAL
b0 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of V
rng b0 is V117() V118() V119() Element of K19(REAL)
ag is set
bh is set
b0 . bh is ext-real V31() V32() Element of REAL
i is Element of the carrier of V
b0 . i is ext-real V31() V32() Element of REAL
i is Element of the carrier of V
b0 . i is ext-real V31() V32() Element of REAL
h1 . i is ext-real V31() V32() Element of REAL
i is Element of the carrier of V
ag is set
Carrier b0 is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not b0 . b1 = 0 } is set
ag is set
bh is Element of the carrier of V
b0 . bh is ext-real V31() V32() Element of REAL
an is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A
ag is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of B
an + ag is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of V
bh is Element of the carrier of V
h1 . bh is ext-real V31() V32() Element of REAL
(an + ag) . bh is ext-real V31() V32() Element of REAL
(an + ag) . bh is ext-real V31() V32() Element of REAL
an . bh is ext-real V31() V32() Element of REAL
ag . bh is ext-real V31() V32() Element of REAL
(an . bh) + (ag . bh) is ext-real V31() V32() Element of REAL
h1 . bh is ext-real V31() V32() Element of REAL
(h1 . bh) + (ag . bh) is ext-real V31() V32() Element of REAL
z0 is ext-real V31() V32() Element of REAL
(h1 . bh) + z0 is ext-real V31() V32() Element of REAL
(an + ag) . bh is ext-real V31() V32() Element of REAL
an . bh is ext-real V31() V32() Element of REAL
ag . bh is ext-real V31() V32() Element of REAL
(an . bh) + (ag . bh) is ext-real V31() V32() Element of REAL
z0 is ext-real V31() V32() Element of REAL
z0 + (ag . bh) is ext-real V31() V32() Element of REAL
h1 . bh is ext-real V31() V32() Element of REAL
(an + ag) . bh is ext-real V31() V32() Element of REAL
an . bh is ext-real V31() V32() Element of REAL
ag . bh is ext-real V31() V32() Element of REAL
(an . bh) + (ag . bh) is ext-real V31() V32() Element of REAL
z0 is ext-real V31() V32() Element of REAL
z0 + (ag . bh) is ext-real V31() V32() Element of REAL
z0 + z0 is ext-real V31() V32() Element of REAL
h1 . bh is ext-real V31() V32() Element of REAL
(an + ag) . bh is ext-real V31() V32() Element of REAL
h1 . bh is ext-real V31() V32() Element of REAL
(an + ag) . bh is ext-real V31() V32() Element of REAL
h1 . bh is ext-real V31() V32() Element of REAL
(an + ag) . bh is ext-real V31() V32() Element of REAL
h1 . bh is ext-real V31() V32() Element of REAL
(an + ag) . bh is ext-real V31() V32() Element of REAL
h1 . bh is ext-real V31() V32() Element of REAL
Sum an is Element of the carrier of V
Sum ag is Element of the carrier of V
(Sum an) + (Sum ag) is Element of the carrier of V
g1 is set
h1 is Element of the carrier of V
a1 is Element of the carrier of V
h1 + a1 is Element of the carrier of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is set
A is Element of K19( the carrier of V)
(V,A) is Element of K19( the carrier of V)
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A : rng b1 c= INT } is set
B is Element of K19( the carrier of V)
A /\ B is Element of K19( the carrier of V)
(V,(A /\ B)) is Element of K19( the carrier of V)
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A /\ B : rng b1 c= INT } is set
(V,B) is Element of K19( the carrier of V)
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of B : rng b1 c= INT } is set
(V,A) /\ (V,B) is Element of K19( the carrier of V)
V is set
A is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of A is non empty set
B is Element of the carrier of A
{B} is non empty V12() finite 1 -element Element of K19( the carrier of A)
K19( the carrier of A) is set
(A,{B}) is Element of K19( the carrier of A)
{ (Sum b1) where b1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of {B} : rng b1 c= INT } is set
g1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of {B}
Sum g1 is Element of the carrier of A
rng g1 is V117() V118() V119() Element of K19(REAL)
g1 . B is ext-real V31() V32() Element of REAL
(g1 . B) * B is Element of the carrier of A
h1 is Relation-like Function-like set
dom h1 is set
rng h1 is set
g1 is ext-real V31() V32() integer set
g1 * B is Element of the carrier of A
K20( the carrier of A,REAL) is V12() non finite set
K19(K20( the carrier of A,REAL)) is V12() non finite set
h1 is ext-real V31() V32() Element of REAL
a1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20( the carrier of A,REAL))
a1 . B is ext-real V31() V32() Element of REAL
Funcs ( the carrier of A,REAL) is non empty FUNCTION_DOMAIN of the carrier of A, REAL
h1 is Element of the carrier of A
g1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of A,REAL)
g1 . h1 is ext-real V31() V32() Element of REAL
h1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A
Carrier h1 is finite Element of K19( the carrier of A)
{ b1 where b1 is Element of the carrier of A : not h1 . b1 = 0 } is set
a1 is set
h1 . a1 is ext-real V31() V32() Element of REAL
a1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of {B}
Sum a1 is Element of the carrier of A
rng a1 is V117() V118() V119() Element of K19(REAL)
gn is set
hn is set
a1 . hn is ext-real V31() V32() Element of REAL
an is Element of the carrier of A
a1 . an is ext-real V31() V32() Element of REAL
an is Element of the carrier of A
a1 . an is ext-real V31() V32() Element of REAL
an is Element of the carrier of A
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
A is Element of the carrier of V
{A} is non empty V12() finite 1 -element Element of K19( the carrier of V)
K19( the carrier of V) is set
(V,{A}) is Element of K19( the carrier of V)
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of {A} : rng b1 c= INT } is set
V is set
A is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of A is non empty set
B is Element of the carrier of A
g1 is Element of the carrier of A
{g1} is non empty V12() finite 1 -element Element of K19( the carrier of A)
K19( the carrier of A) is set
(A,{g1}) is Element of K19( the carrier of A)
{ (Sum b1) where b1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of {g1} : rng b1 c= INT } is set
B + (A,{g1}) is Element of K19( the carrier of A)
{ K180(A,B,b1) where b1 is Element of the carrier of A : b1 in (A,{g1}) } is set
h1 is Element of the carrier of A
B + h1 is Element of the carrier of A
a1 is ext-real V31() V32() integer set
a1 * g1 is Element of the carrier of A
h1 is ext-real V31() V32() integer set
h1 * g1 is Element of the carrier of A
B + (h1 * g1) is Element of the carrier of A
V is set
A is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of A is non empty set
B is Element of the carrier of A
g1 is Element of the carrier of A
{B,g1} is non empty finite Element of K19( the carrier of A)
K19( the carrier of A) is set
(A,{B,g1}) is Element of K19( the carrier of A)
{ (Sum b1) where b1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of {B,g1} : rng b1 c= INT } is set
{B} is non empty V12() finite 1 -element Element of K19( the carrier of A)
h1 is ext-real V31() V32() integer set
h1 * B is Element of the carrier of A
a1 is ext-real V31() V32() integer set
0. A is V52(A) Element of the carrier of A
(h1 * B) + (0. A) is Element of the carrier of A
a1 * g1 is Element of the carrier of A
(h1 * B) + (a1 * g1) is Element of the carrier of A
h1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of {B,g1}
Sum h1 is Element of the carrier of A
rng h1 is V117() V118() V119() Element of K19(REAL)
h1 . B is ext-real V31() V32() Element of REAL
(h1 . B) * B is Element of the carrier of A
h1 . g1 is ext-real V31() V32() Element of REAL
(h1 . g1) * g1 is Element of the carrier of A
((h1 . B) * B) + ((h1 . g1) * g1) is Element of the carrier of A
a1 is Relation-like Function-like set
dom a1 is set
rng a1 is set
h1 is ext-real V31() V32() integer set
h1 * B is Element of the carrier of A
a1 is ext-real V31() V32() integer set
a1 * g1 is Element of the carrier of A
(h1 * B) + (a1 * g1) is Element of the carrier of A
h1 is ext-real V31() V32() integer set
h1 * B is Element of the carrier of A
a1 is ext-real V31() V32() integer set
a1 * g1 is Element of the carrier of A
(h1 * B) + (a1 * g1) is Element of the carrier of A
g1 is ext-real V31() V32() Element of REAL
h1 is ext-real V31() V32() Element of REAL
g1 + h1 is ext-real V31() V32() Element of REAL
(g1 + h1) * B is Element of the carrier of A
{B} is non empty V12() finite 1 -element Element of K19( the carrier of A)
(A,{B}) is Element of K19( the carrier of A)
{ (Sum b1) where b1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of {B} : rng b1 c= INT } is set
K20( the carrier of A,REAL) is V12() non finite set
K19(K20( the carrier of A,REAL)) is V12() non finite set
g1 is ext-real V31() V32() Element of REAL
h1 is ext-real V31() V32() Element of REAL
a1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20( the carrier of A,REAL))
a1 . B is ext-real V31() V32() Element of REAL
a1 . g1 is ext-real V31() V32() Element of REAL
Funcs ( the carrier of A,REAL) is non empty FUNCTION_DOMAIN of the carrier of A, REAL
hn is Element of the carrier of A
gn is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of A,REAL)
gn . hn is ext-real V31() V32() Element of REAL
hn is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A
Carrier hn is finite Element of K19( the carrier of A)
{ b1 where b1 is Element of the carrier of A : not hn . b1 = 0 } is set
an is set
hn . an is ext-real V31() V32() Element of REAL
an is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of {B,g1}
Sum an is Element of the carrier of A
rng an is V117() V118() V119() Element of K19(REAL)
i is set
j is set
an . j is ext-real V31() V32() Element of REAL
a0 is Element of the carrier of A
an . a0 is ext-real V31() V32() Element of REAL
a0 is Element of the carrier of A
an . a0 is ext-real V31() V32() Element of REAL
a0 is Element of the carrier of A
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
A is Element of the carrier of V
B is Element of the carrier of V
{A,B} is non empty finite Element of K19( the carrier of V)
K19( the carrier of V) is set
(V,{A,B}) is Element of K19( the carrier of V)
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of {A,B} : rng b1 c= INT } is set
V is set
A is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of A is non empty set
B is Element of the carrier of A
g1 is Element of the carrier of A
h1 is Element of the carrier of A
{g1,h1} is non empty finite Element of K19( the carrier of A)
K19( the carrier of A) is set
(A,{g1,h1}) is Element of K19( the carrier of A)
{ (Sum b1) where b1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of {g1,h1} : rng b1 c= INT } is set
B + (A,{g1,h1}) is Element of K19( the carrier of A)
{ K180(A,B,b1) where b1 is Element of the carrier of A : b1 in (A,{g1,h1}) } is set
a1 is Element of the carrier of A
B + a1 is Element of the carrier of A
g1 is ext-real V31() V32() integer set
g1 * g1 is Element of the carrier of A
h1 is ext-real V31() V32() integer set
h1 * h1 is Element of the carrier of A
(g1 * g1) + (h1 * h1) is Element of the carrier of A
B + (g1 * g1) is Element of the carrier of A
(B + (g1 * g1)) + (h1 * h1) is Element of the carrier of A
a1 is ext-real V31() V32() integer set
a1 * g1 is Element of the carrier of A
B + (a1 * g1) is Element of the carrier of A
g1 is ext-real V31() V32() integer set
g1 * h1 is Element of the carrier of A
(B + (a1 * g1)) + (g1 * h1) is Element of the carrier of A
(a1 * g1) + (g1 * h1) is Element of the carrier of A
B + ((a1 * g1) + (g1 * h1)) is Element of the carrier of A
V is set
A is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of A is non empty set
B is Element of the carrier of A
g1 is Element of the carrier of A
h1 is Element of the carrier of A
{B,g1,h1} is finite Element of K19( the carrier of A)
K19( the carrier of A) is set
(A,{B,g1,h1}) is Element of K19( the carrier of A)
{ (Sum b1) where b1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of {B,g1,h1} : rng b1 c= INT } is set
a1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of {B,g1,h1}
Sum a1 is Element of the carrier of A
rng a1 is V117() V118() V119() Element of K19(REAL)
a1 . B is ext-real V31() V32() Element of REAL
(a1 . B) * B is Element of the carrier of A
a1 . g1 is ext-real V31() V32() Element of REAL
(a1 . g1) * g1 is Element of the carrier of A
((a1 . B) * B) + ((a1 . g1) * g1) is Element of the carrier of A
a1 . h1 is ext-real V31() V32() Element of REAL
(a1 . h1) * h1 is Element of the carrier of A
(((a1 . B) * B) + ((a1 . g1) * g1)) + ((a1 . h1) * h1) is Element of the carrier of A
g1 is Relation-like Function-like set
dom g1 is set
rng g1 is set
{B,h1} is non empty finite Element of K19( the carrier of A)
{B,B,g1} is finite Element of K19( the carrier of A)
{h1,h1,B} is finite Element of K19( the carrier of A)
{B,g1} is non empty finite Element of K19( the carrier of A)
a1 is ext-real V31() V32() integer set
a1 * B is Element of the carrier of A
g1 is ext-real V31() V32() integer set
g1 * g1 is Element of the carrier of A
(a1 * B) + (g1 * g1) is Element of the carrier of A
h1 is ext-real V31() V32() integer set
0. A is V52(A) Element of the carrier of A
((a1 * B) + (g1 * g1)) + (0. A) is Element of the carrier of A
h1 * h1 is Element of the carrier of A
((a1 * B) + (g1 * g1)) + (h1 * h1) is Element of the carrier of A
a1 is ext-real V31() V32() integer set
a1 * B is Element of the carrier of A
g1 is ext-real V31() V32() integer set
g1 * h1 is Element of the carrier of A
(a1 * B) + (g1 * h1) is Element of the carrier of A
h1 is ext-real V31() V32() integer set
0. A is V52(A) Element of the carrier of A
(a1 * B) + (0. A) is Element of the carrier of A
((a1 * B) + (0. A)) + (g1 * h1) is Element of the carrier of A
h1 * g1 is Element of the carrier of A
(a1 * B) + (h1 * g1) is Element of the carrier of A
((a1 * B) + (h1 * g1)) + (g1 * h1) is Element of the carrier of A
{B,g1} is non empty finite Element of K19( the carrier of A)
a1 is ext-real V31() V32() integer set
a1 * B is Element of the carrier of A
g1 is ext-real V31() V32() integer set
g1 * g1 is Element of the carrier of A
(a1 * B) + (g1 * g1) is Element of the carrier of A
h1 is ext-real V31() V32() integer set
h1 * h1 is Element of the carrier of A
((a1 * B) + (g1 * g1)) + (h1 * h1) is Element of the carrier of A
a1 is ext-real V31() V32() integer set
a1 * B is Element of the carrier of A
g1 is ext-real V31() V32() integer set
g1 * g1 is Element of the carrier of A
(a1 * B) + (g1 * g1) is Element of the carrier of A
h1 is ext-real V31() V32() integer set
h1 * h1 is Element of the carrier of A
((a1 * B) + (g1 * g1)) + (h1 * h1) is Element of the carrier of A
a1 is ext-real V31() V32() integer set
a1 * B is Element of the carrier of A
g1 is ext-real V31() V32() integer set
g1 * g1 is Element of the carrier of A
(a1 * B) + (g1 * g1) is Element of the carrier of A
h1 is ext-real V31() V32() integer set
h1 * h1 is Element of the carrier of A
((a1 * B) + (g1 * g1)) + (h1 * h1) is Element of the carrier of A
{B,h1} is non empty finite Element of K19( the carrier of A)
a1 is ext-real V31() V32() Element of REAL
gn is ext-real V31() V32() Element of REAL
a1 + gn is ext-real V31() V32() Element of REAL
(a1 + gn) * B is Element of the carrier of A
hn is ext-real V31() V32() Element of REAL
hn * h1 is Element of the carrier of A
((a1 + gn) * B) + (hn * h1) is Element of the carrier of A
{B,B,g1} is finite Element of K19( the carrier of A)
{g1,B} is non empty finite Element of K19( the carrier of A)
gn is ext-real V31() V32() Element of REAL
gn * g1 is Element of the carrier of A
a1 is ext-real V31() V32() Element of REAL
a1 * B is Element of the carrier of A
hn is ext-real V31() V32() Element of REAL
hn * B is Element of the carrier of A
(a1 * B) + (hn * B) is Element of the carrier of A
(gn * g1) + ((a1 * B) + (hn * B)) is Element of the carrier of A
a1 + hn is ext-real V31() V32() Element of REAL
(a1 + hn) * B is Element of the carrier of A
(gn * g1) + ((a1 + hn) * B) is Element of the carrier of A
{g1,g1,B} is finite Element of K19( the carrier of A)
{B,g1} is non empty finite Element of K19( the carrier of A)
a1 is ext-real V31() V32() Element of REAL
a1 * B is Element of the carrier of A
gn is ext-real V31() V32() Element of REAL
gn * g1 is Element of the carrier of A
hn is ext-real V31() V32() Element of REAL
hn * g1 is Element of the carrier of A
(gn * g1) + (hn * g1) is Element of the carrier of A
(a1 * B) + ((gn * g1) + (hn * g1)) is Element of the carrier of A
gn + hn is ext-real V31() V32() Element of REAL
(gn + hn) * g1 is Element of the carrier of A
(a1 * B) + ((gn + hn) * g1) is Element of the carrier of A
K20( the carrier of A,REAL) is V12() non finite set
K19(K20( the carrier of A,REAL)) is V12() non finite set
a1 is ext-real V31() V32() Element of REAL
gn is ext-real V31() V32() Element of REAL
hn is ext-real V31() V32() Element of REAL
an is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20( the carrier of A,REAL))
an . B is ext-real V31() V32() Element of REAL
an . g1 is ext-real V31() V32() Element of REAL
an . h1 is ext-real V31() V32() Element of REAL
Funcs ( the carrier of A,REAL) is non empty FUNCTION_DOMAIN of the carrier of A, REAL
j is Element of the carrier of A
i is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of A,REAL)
i . j is ext-real V31() V32() Element of REAL
j is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A
Carrier j is finite Element of K19( the carrier of A)
{ b1 where b1 is Element of the carrier of A : not j . b1 = 0 } is set
a0 is set
j . a0 is ext-real V31() V32() Element of REAL
a0 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of {B,g1,h1}
Sum a0 is Element of the carrier of A
rng a0 is V117() V118() V119() Element of K19(REAL)
b0 is set
ag is set
a0 . ag is ext-real V31() V32() Element of REAL
bh is Element of the carrier of A
a0 . bh is ext-real V31() V32() Element of REAL
bh is Element of the carrier of A
a0 . bh is ext-real V31() V32() Element of REAL
bh is Element of the carrier of A
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
A is Element of the carrier of V
B is Element of the carrier of V
g1 is Element of the carrier of V
{A,B,g1} is finite Element of K19( the carrier of V)
K19( the carrier of V) is set
(V,{A,B,g1}) is Element of K19( the carrier of V)
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of {A,B,g1} : rng b1 c= INT } is set
V is set
A is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of A is non empty set
B is Element of the carrier of A
g1 is Element of the carrier of A
h1 is Element of the carrier of A
a1 is Element of the carrier of A
{g1,h1,a1} is finite Element of K19( the carrier of A)
K19( the carrier of A) is set
(A,{g1,h1,a1}) is Element of K19( the carrier of A)
{ (Sum b1) where b1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of {g1,h1,a1} : rng b1 c= INT } is set
B + (A,{g1,h1,a1}) is Element of K19( the carrier of A)
{ K180(A,B,b1) where b1 is Element of the carrier of A : b1 in (A,{g1,h1,a1}) } is set
g1 is Element of the carrier of A
B + g1 is Element of the carrier of A
h1 is ext-real V31() V32() integer set
h1 * g1 is Element of the carrier of A
a1 is ext-real V31() V32() integer set
a1 * h1 is Element of the carrier of A
(h1 * g1) + (a1 * h1) is Element of the carrier of A
gn is ext-real V31() V32() integer set
gn * a1 is Element of the carrier of A
((h1 * g1) + (a1 * h1)) + (gn * a1) is Element of the carrier of A
B + (h1 * g1) is Element of the carrier of A
(B + (h1 * g1)) + (a1 * h1) is Element of the carrier of A
((B + (h1 * g1)) + (a1 * h1)) + (gn * a1) is Element of the carrier of A
B + ((h1 * g1) + (a1 * h1)) is Element of the carrier of A
(B + ((h1 * g1) + (a1 * h1))) + (gn * a1) is Element of the carrier of A
g1 is ext-real V31() V32() integer set
g1 * g1 is Element of the carrier of A
B + (g1 * g1) is Element of the carrier of A
h1 is ext-real V31() V32() integer set
h1 * h1 is Element of the carrier of A
(B + (g1 * g1)) + (h1 * h1) is Element of the carrier of A
a1 is ext-real V31() V32() integer set
a1 * a1 is Element of the carrier of A
((B + (g1 * g1)) + (h1 * h1)) + (a1 * a1) is Element of the carrier of A
(g1 * g1) + (h1 * h1) is Element of the carrier of A
((g1 * g1) + (h1 * h1)) + (a1 * a1) is Element of the carrier of A
B + (((g1 * g1) + (h1 * h1)) + (a1 * a1)) is Element of the carrier of A
B + ((g1 * g1) + (h1 * h1)) is Element of the carrier of A
(B + ((g1 * g1) + (h1 * h1))) + (a1 * a1) is Element of the carrier of A
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is set
A is Element of K19( the carrier of V)
(V,A) is Element of K19( the carrier of V)
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A : rng b1 c= INT } is set
B is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng B is finite Element of K19( the carrier of V)
len B is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
g1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len g1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
Seg (len B) is finite len B -element Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT : ( 1 <= b1 & b1 <= len B ) } is set
Sum g1 is Element of the carrier of V
h1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len h1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
<*> the carrier of V is Relation-like NAT -defined the carrier of V -valued Function-like one-to-one constant functional empty ext-real V24() V25() V26() V28() V29() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered integer complex-valued ext-real-valued real-valued natural-valued FinSequence of the carrier of V
Sum (<*> the carrier of V) is Element of the carrier of V
0. V is V52(V) Element of the carrier of V
B is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
g1 is set
h1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum h1 is Element of the carrier of V
g1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng g1 is finite Element of K19( the carrier of V)
len g1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
B + 1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
len h1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
a1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len a1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
Seg (len g1) is finite len g1 -element Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT : ( 1 <= b1 & b1 <= len g1 ) } is set
g1 | B is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Seg B is finite B -element Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT : ( 1 <= b1 & b1 <= B ) } is set
g1 | (Seg B) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
h1 | B is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
h1 | (Seg B) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
a1 | B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a1 | (Seg B) is Relation-like NAT -defined INT -valued Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued set
h1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng h1 is finite Element of K19( the carrier of V)
len h1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
a1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len a1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
gn is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len gn is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
Seg (len h1) is finite len h1 -element Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT : ( 1 <= b1 & b1 <= len h1 ) } is set
hn is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
a1 /. hn is Element of the carrier of V
h1 /. hn is Element of the carrier of V
gn . hn is ext-real V31() V32() Element of REAL
(gn . hn) * (h1 /. hn) is Element of the carrier of V
hn is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
a1 /. hn is Element of the carrier of V
h1 /. hn is Element of the carrier of V
gn . hn is ext-real V31() V32() Element of REAL
(gn . hn) * (h1 /. hn) is Element of the carrier of V
dom g1 is finite Element of K19(NAT)
g1 /. hn is Element of the carrier of V
Seg (len h1) is finite len h1 -element Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT : ( 1 <= b1 & b1 <= len h1 ) } is set
dom h1 is finite Element of K19(NAT)
h1 /. hn is Element of the carrier of V
a1 . hn is ext-real V31() V32() integer Element of REAL
hn is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
a1 /. hn is Element of the carrier of V
h1 /. hn is Element of the carrier of V
gn . hn is ext-real V31() V32() Element of REAL
(gn . hn) * (h1 /. hn) is Element of the carrier of V
Sum a1 is Element of the carrier of V
h1 /. (B + 1) is Element of the carrier of V
g1 /. (B + 1) is Element of the carrier of V
a1 . (B + 1) is ext-real V31() V32() integer Element of REAL
(a1 . (B + 1)) * (g1 /. (B + 1)) is Element of the carrier of V
<*((a1 . (B + 1)) * (g1 /. (B + 1)))*> is Relation-like NAT -defined the carrier of V -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
[1,((a1 . (B + 1)) * (g1 /. (B + 1)))] is set
{1,((a1 . (B + 1)) * (g1 /. (B + 1)))} is non empty finite set
{1} is non empty V12() finite V37() 1 -element set
{{1,((a1 . (B + 1)) * (g1 /. (B + 1)))},{1}} is non empty finite V37() set
{[1,((a1 . (B + 1)) * (g1 /. (B + 1)))]} is Function-like non empty V12() finite 1 -element set
a1 ^ <*((a1 . (B + 1)) * (g1 /. (B + 1)))*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
dom g1 is finite Element of K19(NAT)
g1 . (B + 1) is set
Sum <*((a1 . (B + 1)) * (g1 /. (B + 1)))*> is Element of the carrier of V
(Sum a1) + (Sum <*((a1 . (B + 1)) * (g1 /. (B + 1)))*>) is Element of the carrier of V
(Sum a1) + ((a1 . (B + 1)) * (g1 /. (B + 1))) is Element of the carrier of V
g1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng g1 is finite Element of K19( the carrier of V)
len g1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
h1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len h1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
a1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len a1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
Seg (len g1) is finite len g1 -element Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT : ( 1 <= b1 & b1 <= len g1 ) } is set
Sum h1 is Element of the carrier of V
B is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng B is finite Element of K19( the carrier of V)
len B is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
g1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len g1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
h1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len h1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
Seg (len B) is finite len B -element Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT : ( 1 <= b1 & b1 <= len B ) } is set
Sum g1 is Element of the carrier of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is set
A is Element of K19( the carrier of V)
(V,A) is Element of K19( the carrier of V)
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A : rng b1 c= INT } is set
B is set
g1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A
Sum g1 is Element of the carrier of V
rng g1 is V117() V118() V119() Element of K19(REAL)
Carrier g1 is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not g1 . b1 = 0 } is set
h1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng h1 is finite Element of K19( the carrier of V)
g1 (#) h1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (g1 (#) h1) is Element of the carrier of V
len (g1 (#) h1) is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
len h1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
dom (g1 (#) h1) is finite Element of K19(NAT)
a1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
(g1 (#) h1) . a1 is set
h1 /. a1 is Element of the carrier of V
g1 . (h1 /. a1) is ext-real V31() V32() Element of REAL
(g1 . (h1 /. a1)) * (h1 /. a1) is Element of the carrier of V
a1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
Seg (len h1) is finite len h1 -element Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT : ( 1 <= b1 & b1 <= len h1 ) } is set
h1 /. a1 is Element of the carrier of V
g1 . (h1 /. a1) is ext-real V31() V32() Element of REAL
a1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
dom a1 is finite Element of K19(NAT)
len a1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
g1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
(g1 (#) h1) /. g1 is Element of the carrier of V
(g1 (#) h1) . g1 is set
h1 /. g1 is Element of the carrier of V
g1 . (h1 /. g1) is ext-real V31() V32() Element of REAL
(g1 . (h1 /. g1)) * (h1 /. g1) is Element of the carrier of V
a1 . g1 is ext-real V31() V32() integer Element of REAL
(a1 . g1) * (h1 /. g1) is Element of the carrier of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is set
g1 is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of g1 is non empty set
K19( the carrier of g1) is set
B is set
A is Element of K19( the carrier of V)
(V,A) is Element of K19( the carrier of V)
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A : rng b1 c= INT } is set
a1 is set
h1 is Relation-like NAT -defined the carrier of g1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of g1
Sum h1 is Element of the carrier of g1
g1 is Relation-like NAT -defined the carrier of g1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of g1
rng g1 is finite Element of K19( the carrier of g1)
h1 is Element of K19( the carrier of g1)
len g1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
len h1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
a1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len a1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
Seg (len g1) is finite len g1 -element Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT : ( 1 <= b1 & b1 <= len g1 ) } is set
(g1,h1) is Element of K19( the carrier of g1)
{ (Sum b1) where b1 is Relation-like the carrier of g1 -defined REAL -valued Function-like quasi_total complex-valued ext-real-valued real-valued Linear_Combination of h1 : rng b1 c= INT } is set
A is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
V is non empty set
the Element of V is Element of V
A |-> the Element of V is Relation-like NAT -defined V -valued Function-like finite A -element FinSequence-like FinSubsequence-like Element of A -tuples_on V
A -tuples_on V is functional non empty FinSequence-membered FinSequenceSet of V
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
A is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len A is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
Seg (len A) is finite len A -element Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT : ( 1 <= b1 & b1 <= len A ) } is set
{ (Sum b1) where b1 is Relation-like NAT -defined the carrier of V -valued Function-like finite len A -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V : ex b2 being Relation-like NAT -defined INT -valued Function-like finite len A -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set st
for b3 being ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set holds
( not b3 in Seg (len A) or b1 /. b3 = (b2 . b3) * (A /. b3) ) } is set
K19( the carrier of V) is set
B is set
g1 is Relation-like NAT -defined the carrier of V -valued Function-like finite len A -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum g1 is Element of the carrier of V
h1 is Relation-like NAT -defined INT -valued Function-like finite len A -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
A is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(V,A) is Element of K19( the carrier of V)
K19( the carrier of V) is set
len A is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
Seg (len A) is finite len A -element Element of K19(NAT)
{ b1 where b1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT : ( 1 <= b1 & b1 <= len A ) } is set
{ (Sum b1) where b1 is Relation-like NAT -defined the carrier of V -valued Function-like finite len A -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V : ex b2 being Relation-like NAT -defined INT -valued Function-like finite len A -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set st
for b3 being ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set holds
( not b3 in Seg (len A) or b1 /. b3 = (b2 . b3) * (A /. b3) ) } is set
B is set
g1 is Relation-like NAT -defined the carrier of V -valued Function-like finite len A -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum g1 is Element of the carrier of V
h1 is Relation-like NAT -defined INT -valued Function-like finite len A -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
h1 is Relation-like NAT -defined INT -valued Function-like finite len A -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
a1 is Relation-like NAT -defined the carrier of V -valued Function-like finite len A -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum a1 is Element of the carrier of V
g1 is Relation-like NAT -defined INT -valued Function-like finite len A -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
h1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
a1 /. h1 is Element of the carrier of V
A /. h1 is Element of the carrier of V
g1 . h1 is ext-real V31() V32() integer Element of REAL
(g1 . h1) * (A /. h1) is Element of the carrier of V
a1 is Relation-like NAT -defined INT -valued Function-like finite len A -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
g1 is Relation-like NAT -defined the carrier of V -valued Function-like finite len A -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum g1 is Element of the carrier of V
h1 is Relation-like NAT -defined INT -valued Function-like finite len A -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
V is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
A is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like