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 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 Element of the carrier of V
g1 is Element of the carrier of V
h1 is ext-real V31() V32() integer Element of INT
h1 * B is Element of the carrier of V
a1 is ext-real V31() V32() integer Element of INT
a1 * g1 is Element of the carrier of V
(h1 * B) + (a1 * g1) is Element of the carrier of V
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
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
gn 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
hn is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
h1 . hn is ext-real V31() V32() integer Element of REAL
h1 * (h1 . hn) is ext-real V31() V32() integer Element of INT
gn . hn is ext-real V31() V32() integer Element of REAL
a1 * (gn . hn) is ext-real V31() V32() integer Element of INT
(h1 * (h1 . hn)) + (a1 * (gn . hn)) is ext-real V31() V32() integer Element of INT
hn 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 hn is finite Element of K19(NAT)
len hn is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
i is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
g1 /. i is Element of the carrier of V
h1 * (g1 /. i) is Element of the carrier of V
a1 /. i is Element of the carrier of V
a1 * (a1 /. i) is Element of the carrier of V
(h1 * (g1 /. i)) + (a1 * (a1 /. i)) is Element of the carrier of V
i is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
dom i is finite Element of K19(NAT)
len i is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
a0 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
j 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
j /. a0 is Element of the carrier of V
j . a0 is set
g1 /. a0 is Element of the carrier of V
h1 * (g1 /. a0) is Element of the carrier of V
a1 /. a0 is Element of the carrier of V
a1 * (a1 /. a0) is Element of the carrier of V
(h1 * (g1 /. a0)) + (a1 * (a1 /. a0)) is Element of the carrier of V
a0 is ext-real V31() V32() Element of REAL
a0 (#) g1 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
dom (a0 (#) g1) is Element of K19(NAT)
dom g1 is finite len A -element Element of K19(NAT)
len g1 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
rng (a0 (#) g1) is Element of K19( the carrier of V)
b0 is ext-real V31() V32() Element of REAL
b0 (#) a1 is Relation-like NAT -defined the carrier of V -valued Function-like Element of K19(K20(NAT, the carrier of V))
dom (b0 (#) a1) is Element of K19(NAT)
dom a1 is finite len A -element Element of K19(NAT)
len a1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
Seg (len a1) is finite len a1 -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 a1 ) } is set
rng (b0 (#) a1) is Element of K19( the carrier of V)
ag is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len ag is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
i is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
dom ag is finite Element of K19(NAT)
j . i is set
g1 /. i is Element of the carrier of V
h1 * (g1 /. i) is Element of the carrier of V
a1 /. i is Element of the carrier of V
a1 * (a1 /. i) is Element of the carrier of V
(h1 * (g1 /. i)) + (a1 * (a1 /. i)) is Element of the carrier of V
ag /. i is Element of the carrier of V
(ag /. i) + (a1 * (a1 /. i)) is Element of the carrier of V
bh is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
bh /. i is Element of the carrier of V
(ag /. i) + (bh /. i) is Element of the carrier of V
len bh is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
len j is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
an 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
i is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
j /. i is Element of the carrier of V
A /. i is Element of the carrier of V
an . i is ext-real V31() V32() integer Element of REAL
(an . i) * (A /. i) is Element of the carrier of V
g1 /. i is Element of the carrier of V
h1 * (g1 /. i) is Element of the carrier of V
a1 /. i is Element of the carrier of V
a1 * (a1 /. i) is Element of the carrier of V
(h1 * (g1 /. i)) + (a1 * (a1 /. i)) is Element of the carrier of V
h1 . i is ext-real V31() V32() integer Element of REAL
(h1 . i) * (A /. i) is Element of the carrier of V
h1 * ((h1 . i) * (A /. i)) is Element of the carrier of V
(h1 * ((h1 . i) * (A /. i))) + (a1 * (a1 /. i)) is Element of the carrier of V
gn . i is ext-real V31() V32() integer Element of REAL
(gn . i) * (A /. i) is Element of the carrier of V
a1 * ((gn . i) * (A /. i)) is Element of the carrier of V
(h1 * ((h1 . i) * (A /. i))) + (a1 * ((gn . i) * (A /. i))) is Element of the carrier of V
h1 * (h1 . i) is ext-real V31() V32() integer Element of INT
(h1 * (h1 . i)) * (A /. i) is Element of the carrier of V
((h1 * (h1 . i)) * (A /. i)) + (a1 * ((gn . i) * (A /. i))) is Element of the carrier of V
a1 * (gn . i) is ext-real V31() V32() integer Element of INT
(a1 * (gn . i)) * (A /. i) is Element of the carrier of V
((h1 * (h1 . i)) * (A /. i)) + ((a1 * (gn . i)) * (A /. i)) is Element of the carrier of V
(h1 * (h1 . i)) + (a1 * (gn . i)) is ext-real V31() V32() integer Element of INT
((h1 * (h1 . i)) + (a1 * (gn . i))) * (A /. i) is Element of the carrier of V
Sum ag is Element of the carrier of V
a1 * (Sum a1) is Element of the carrier of V
(Sum ag) + (a1 * (Sum a1)) is Element of the carrier of V
Sum bh is Element of the carrier of V
(Sum ag) + (Sum bh) is Element of the carrier of V
Sum j 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
0. V is V52(V) Element 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
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
(Seg (len A)) --> (0. V) is Relation-like Seg (len A) -defined the carrier of V -valued Function-like quasi_total finite FinSequence-like FinSubsequence-like Element of K19(K20((Seg (len A)), the carrier of V))
K20((Seg (len A)), the carrier of V) is set
K19(K20((Seg (len A)), the carrier of V)) is set
Sum A is Element of the carrier of V
B is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
dom A is finite Element of K19(NAT)
g1 is Element of the carrier of V
A . B is set
- g1 is Element of the carrier of V
- (Sum A) 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
0. V is V52(V) Element 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
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
(Seg (len A)) --> (0. V) is Relation-like Seg (len A) -defined the carrier of V -valued Function-like quasi_total finite FinSequence-like FinSubsequence-like Element of K19(K20((Seg (len A)), the carrier of V))
K20((Seg (len A)), the carrier of V) is set
K19(K20((Seg (len A)), the carrier of V)) is set
Sum A is Element of the carrier of V
B is Element of the carrier of V
g1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
{g1} is non empty V12() finite V37() 1 -element set
{g1} --> B is Relation-like {g1} -defined the carrier of V -valued Function-like quasi_total finite Element of K19(K20({g1}, the carrier of V))
K20({g1}, the carrier of V) is set
K19(K20({g1}, the carrier of V)) is set
((Seg (len A)) --> (0. V)) +* ({g1} --> B) is Relation-like Function-like finite 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
len h1 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
(Seg (len h1)) --> (0. V) is Relation-like Seg (len h1) -defined the carrier of V -valued Function-like quasi_total finite FinSequence-like FinSubsequence-like Element of K19(K20((Seg (len h1)), the carrier of V))
K20((Seg (len h1)), the carrier of V) is set
K19(K20((Seg (len h1)), the carrier of V)) is set
((Seg (len h1)) --> (0. V)) +* ({g1} --> B) is Relation-like Function-like finite set
Sum h1 is Element of the carrier of V
h1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
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
h1 + 1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
Seg (len a1) is finite len a1 -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 a1 ) } is set
(Seg (len a1)) --> (0. V) is Relation-like Seg (len a1) -defined the carrier of V -valued Function-like quasi_total finite FinSequence-like FinSubsequence-like Element of K19(K20((Seg (len a1)), the carrier of V))
K20((Seg (len a1)), the carrier of V) is set
K19(K20((Seg (len a1)), the carrier of V)) is set
((Seg (len a1)) --> (0. V)) +* ({g1} --> B) is Relation-like Function-like finite set
a1 | h1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Seg h1 is finite 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 <= h1 ) } is set
a1 | (Seg h1) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seg (h1 + 1) is finite h1 + 1 -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 <= h1 + 1 ) } is set
dom a1 is finite Element of K19(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
a1 . (h1 + 1) is set
<*(a1 . (h1 + 1))*> is Relation-like NAT -defined Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like set
[1,(a1 . (h1 + 1))] is set
{1,(a1 . (h1 + 1))} is non empty finite set
{1} is non empty V12() finite V37() 1 -element set
{{1,(a1 . (h1 + 1))},{1}} is non empty finite V37() set
{[1,(a1 . (h1 + 1))]} is Function-like non empty V12() finite 1 -element set
(a1 | h1) ^ <*(a1 . (h1 + 1))*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
a1 /. (h1 + 1) is Element of the carrier of V
<*(a1 /. (h1 + 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 /. (h1 + 1))] is set
{1,(a1 /. (h1 + 1))} is non empty finite set
{{1,(a1 /. (h1 + 1))},{1}} is non empty finite V37() set
{[1,(a1 /. (h1 + 1))]} is Function-like non empty V12() finite 1 -element set
g1 ^ <*(a1 /. (h1 + 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
Sum a1 is Element of the carrier of V
Sum g1 is Element of the carrier of V
Sum <*(a1 /. (h1 + 1))*> is Element of the carrier of V
(Sum g1) + (Sum <*(a1 /. (h1 + 1))*>) is Element of the carrier of V
dom ({g1} --> B) is finite V37() Element of K19({g1})
K19({g1}) is finite V37() set
h1 is Relation-like Function-like set
a1 is Relation-like Function-like set
dom a1 is set
{(h1 + 1)} is non empty V12() finite V37() 1 -element Element of K19(NAT)
h1 | (Seg h1) is Relation-like Function-like finite set
(Seg (len a1)) /\ (Seg h1) is finite Element of K19(NAT)
((Seg (len a1)) /\ (Seg h1)) --> (0. V) is Relation-like (Seg (len a1)) /\ (Seg h1) -defined the carrier of V -valued Function-like quasi_total finite Element of K19(K20(((Seg (len a1)) /\ (Seg h1)), the carrier of V))
K20(((Seg (len a1)) /\ (Seg h1)), the carrier of V) is set
K19(K20(((Seg (len a1)) /\ (Seg h1)), the carrier of V)) is set
(Seg h1) --> (0. V) is Relation-like Seg h1 -defined the carrier of V -valued Function-like quasi_total finite FinSequence-like FinSubsequence-like Element of K19(K20((Seg h1), the carrier of V))
K20((Seg h1), the carrier of V) is set
K19(K20((Seg h1), the carrier of V)) is set
a1 . (h1 + 1) is set
(0. V) + B is Element of the carrier of V
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
h1 | (Seg h1) is Relation-like Function-like finite set
a1 | (Seg h1) is Relation-like Function-like finite set
(h1 | (Seg h1)) +* (a1 | (Seg h1)) is Relation-like Function-like finite set
(Seg (len a1)) /\ (Seg h1) is finite Element of K19(NAT)
((Seg (len a1)) /\ (Seg h1)) --> (0. V) is Relation-like (Seg (len a1)) /\ (Seg h1) -defined the carrier of V -valued Function-like quasi_total finite Element of K19(K20(((Seg (len a1)) /\ (Seg h1)), the carrier of V))
K20(((Seg (len a1)) /\ (Seg h1)), the carrier of V) is set
K19(K20(((Seg (len a1)) /\ (Seg h1)), the carrier of V)) is set
(((Seg (len a1)) /\ (Seg h1)) --> (0. V)) +* (a1 | (Seg h1)) is Relation-like Function-like finite set
(Seg (len g1)) --> (0. V) is Relation-like Seg (len g1) -defined the carrier of V -valued Function-like quasi_total finite FinSequence-like FinSubsequence-like Element of K19(K20((Seg (len g1)), the carrier of V))
K20((Seg (len g1)), the carrier of V) is set
K19(K20((Seg (len g1)), the carrier of V)) is set
((Seg (len g1)) --> (0. V)) +* (a1 | (Seg h1)) is Relation-like Function-like finite set
{g1} /\ (Seg h1) is finite Element of K19(NAT)
({g1} /\ (Seg h1)) --> B is Relation-like {g1} /\ (Seg h1) -defined the carrier of V -valued Function-like quasi_total finite Element of K19(K20(({g1} /\ (Seg h1)), the carrier of V))
K20(({g1} /\ (Seg h1)), the carrier of V) is set
K19(K20(({g1} /\ (Seg h1)), the carrier of V)) is set
((Seg (len g1)) --> (0. V)) +* (({g1} /\ (Seg h1)) --> B) is Relation-like Function-like finite set
((Seg (len g1)) --> (0. V)) +* ({g1} --> B) is Relation-like Function-like finite set
{(h1 + 1)} is non empty V12() finite V37() 1 -element Element of K19(NAT)
dom a1 is set
h1 . (h1 + 1) is set
B + (0. V) is Element of the carrier of V
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
Seg (len a1) is finite len a1 -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 a1 ) } is set
(Seg (len a1)) --> (0. V) is Relation-like Seg (len a1) -defined the carrier of V -valued Function-like quasi_total finite FinSequence-like FinSubsequence-like Element of K19(K20((Seg (len a1)), the carrier of V))
K20((Seg (len a1)), the carrier of V) is set
K19(K20((Seg (len a1)), the carrier of V)) is set
((Seg (len a1)) --> (0. V)) +* ({g1} --> B) is Relation-like Function-like finite set
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
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
(V,A) is Element of K19( the carrier of V)
K19( the carrier of V) 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 ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
A /. B is Element of the carrier of V
(Seg (len A)) --> 0 is Relation-like Seg (len A) -defined NAT -valued INT -valued Function-like quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg (len A)),NAT))
K20((Seg (len A)),NAT) is set
K19(K20((Seg (len A)),NAT)) is set
{B} is non empty V12() finite V37() 1 -element set
{B} --> 1 is Relation-like {B} -defined NAT -valued INT -valued Function-like quasi_total finite complex-valued ext-real-valued real-valued natural-valued Element of K19(K20({B},NAT))
K20({B},NAT) is V12() non finite set
K19(K20({B},NAT)) is V12() non finite set
((Seg (len A)) --> 0) +* ({B} --> 1) is Relation-like RAT -valued INT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued set
dom (((Seg (len A)) --> 0) +* ({B} --> 1)) is finite set
dom ((Seg (len A)) --> 0) is finite Element of K19(NAT)
dom ({B} --> 1) is finite V37() Element of K19({B})
K19({B}) is finite V37() set
(dom ((Seg (len A)) --> 0)) \/ (dom ({B} --> 1)) is finite set
(Seg (len A)) \/ (dom ({B} --> 1)) is finite set
(Seg (len A)) \/ {B} is non empty finite set
rng (((Seg (len A)) --> 0) +* ({B} --> 1)) is finite V117() V118() V119() V120() V121() V122() Element of K19(RAT)
K19(RAT) is V12() non finite set
rng ((Seg (len A)) --> 0) is finite V117() V118() V119() V121() V122() Element of K19(INT)
K19(INT) is V12() non finite set
rng ({B} --> 1) is finite V117() V118() V119() V121() V122() Element of K19(INT)
(rng ((Seg (len A)) --> 0)) \/ (rng ({B} --> 1)) is finite Element of K19(INT)
h1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of INT
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 len A -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
g1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
A /. g1 is Element of the carrier of V
a1 . g1 is ext-real V31() V32() integer Element of REAL
(a1 . g1) * (A /. g1) 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
dom g1 is finite Element of K19(NAT)
len g1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
a1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
h1 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
h1 /. a1 is Element of the carrier of V
h1 . a1 is set
A /. a1 is Element of the carrier of V
a1 . a1 is ext-real V31() V32() integer Element of REAL
(a1 . a1) * (A /. a1) is Element of the carrier of V
Sum h1 is Element of the carrier of V
len h1 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
0. V is V52(V) Element of the carrier of V
(Seg (len h1)) --> (0. V) is Relation-like Seg (len h1) -defined the carrier of V -valued Function-like quasi_total finite FinSequence-like FinSubsequence-like Element of K19(K20((Seg (len h1)), the carrier of V))
K20((Seg (len h1)), the carrier of V) is set
K19(K20((Seg (len h1)), the carrier of V)) is set
{B} --> (A /. B) is Relation-like {B} -defined the carrier of V -valued Function-like quasi_total finite Element of K19(K20({B}, the carrier of V))
K20({B}, the carrier of V) is set
K19(K20({B}, the carrier of V)) is set
((Seg (len h1)) --> (0. V)) +* ({B} --> (A /. B)) is Relation-like Function-like finite set
(Seg (len A)) --> (0. V) is Relation-like Seg (len A) -defined the carrier of V -valued Function-like quasi_total finite FinSequence-like FinSubsequence-like Element of K19(K20((Seg (len A)), the carrier of V))
K20((Seg (len A)), the carrier of V) is set
K19(K20((Seg (len A)), the carrier of V)) is set
a1 is Relation-like Function-like set
dom a1 is set
gn is Relation-like Function-like set
dom gn is set
a1 +* gn is Relation-like Function-like set
hn is Relation-like Function-like set
dom hn is set
(Seg (len A)) \/ {B} is non empty finite set
rng a1 is set
{(0. V)} is non empty V12() finite 1 -element Element of K19( the carrier of V)
rng gn is set
{(A /. B)} is non empty V12() finite 1 -element Element of K19( the carrier of V)
an is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng an is finite set
(rng a1) \/ (rng gn) is set
dom h1 is finite len A -element Element of K19(NAT)
i is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
j is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
h1 /. j is Element of the carrier of V
i /. j is Element of the carrier of V
dom ({B} --> 1) is finite V37() Element of K19({B})
K19({B}) is finite V37() set
h1 . B is set
a1 . B is ext-real V31() V32() integer Element of REAL
(a1 . B) * (A /. B) is Element of the carrier of V
({B} --> 1) . B is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of REAL
i . j is set
gn . j is set
h1 . j is set
A /. j is Element of the carrier of V
a1 . j is ext-real V31() V32() integer Element of REAL
(a1 . j) * (A /. j) is Element of the carrier of V
((Seg (len A)) --> 0) . j is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of REAL
i . j is set
a1 . j 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
rng A is finite Element of K19( the carrier of V)
K19( the carrier of V) is set
(V,A) is Element of K19( 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
B is set
dom A is finite Element of K19(NAT)
g1 is set
A . g1 is set
h1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
A /. 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 Relation-like NAT -defined the carrier of V -valued Function-like non empty 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 non empty ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
Seg (len A) is non empty 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
A /. 1 is Element of the carrier of V
B is ext-real V31() V32() integer Element of INT
B * (A /. 1) is Element of the carrier of V
(B * (A /. 1)) + (B * (A /. 1)) is Element of the carrier of V
0. V is V52(V) Element of the carrier of V
(B * (A /. 1)) + (0. V) is Element of the carrier of V
(0. V) + (0. V) is Element of the carrier of V
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
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
Sum a1 is Element of the carrier of V
g1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len g1 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
h1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
a1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng a1 is finite Element of K19( the carrier of V)
len a1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
h1 + 1 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
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 a1) is finite len a1 -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 a1 ) } is set
a1 | h1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Seg h1 is finite 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 <= h1 ) } is set
a1 | (Seg h1) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
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
g1 | (Seg h1) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
h1 | h1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
h1 | (Seg h1) is Relation-like NAT -defined INT -valued Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued set
a1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng a1 is finite Element of K19( the carrier of V)
len a1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
hn is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len hn is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
gn is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len gn is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
Seg (len a1) is finite len a1 -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 a1 ) } is set
an is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
gn /. an is Element of the carrier of V
a1 /. an is Element of the carrier of V
hn . an is ext-real V31() V32() integer Element of REAL
(hn . an) * (a1 /. an) is Element of the carrier of V
an is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
gn /. an is Element of the carrier of V
a1 /. an is Element of the carrier of V
hn . an is ext-real V31() V32() integer Element of REAL
(hn . an) * (a1 /. an) is Element of the carrier of V
dom a1 is finite Element of K19(NAT)
a1 /. an is Element of the carrier of V
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
dom g1 is finite Element of K19(NAT)
g1 /. an is Element of the carrier of V
h1 . an is ext-real V31() V32() integer Element of REAL
an is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
gn /. an is Element of the carrier of V
a1 /. an is Element of the carrier of V
hn . an is ext-real V31() V32() integer Element of REAL
(hn . an) * (a1 /. an) is Element of the carrier of V
Sum gn is Element of the carrier of V
g1 /. (h1 + 1) is Element of the carrier of V
a1 /. (h1 + 1) is Element of the carrier of V
h1 . (h1 + 1) is ext-real V31() V32() integer Element of REAL
(h1 . (h1 + 1)) * (a1 /. (h1 + 1)) is Element of the carrier of V
<*((h1 . (h1 + 1)) * (a1 /. (h1 + 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,((h1 . (h1 + 1)) * (a1 /. (h1 + 1)))] is set
{1,((h1 . (h1 + 1)) * (a1 /. (h1 + 1)))} is non empty finite set
{1} is non empty V12() finite V37() 1 -element set
{{1,((h1 . (h1 + 1)) * (a1 /. (h1 + 1)))},{1}} is non empty finite V37() set
{[1,((h1 . (h1 + 1)) * (a1 /. (h1 + 1)))]} is Function-like non empty V12() finite 1 -element set
gn ^ <*((h1 . (h1 + 1)) * (a1 /. (h1 + 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 a1 is finite Element of K19(NAT)
a1 . (h1 + 1) is set
g1 is ext-real V31() V32() integer Element of INT
g1 * (h1 . (h1 + 1)) is ext-real V31() V32() integer Element of INT
(g1 * (h1 . (h1 + 1))) * (a1 /. (h1 + 1)) is Element of the carrier of V
B * (a1 /. (h1 + 1)) is Element of the carrier of V
((g1 * (h1 . (h1 + 1))) * (a1 /. (h1 + 1))) + (B * (a1 /. (h1 + 1))) is Element of the carrier of V
((g1 * (h1 . (h1 + 1))) * (a1 /. (h1 + 1))) + (0. V) is Element of the carrier of V
g1 * (Sum gn) is Element of the carrier of V
g1 * ((h1 . (h1 + 1)) * (a1 /. (h1 + 1))) is Element of the carrier of V
(g1 * (Sum gn)) + (g1 * ((h1 . (h1 + 1)) * (a1 /. (h1 + 1)))) is Element of the carrier of V
(g1 * (Sum gn)) + ((h1 . (h1 + 1)) * (a1 /. (h1 + 1))) is Element of the carrier of V
Sum g1 is Element of the carrier of V
Sum <*((h1 . (h1 + 1)) * (a1 /. (h1 + 1)))*> is Element of the carrier of V
(Sum gn) + (Sum <*((h1 . (h1 + 1)) * (a1 /. (h1 + 1)))*>) is Element of the carrier of V
(Sum gn) + ((h1 . (h1 + 1)) * (a1 /. (h1 + 1))) is Element of the carrier of V
a1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng a1 is finite Element of K19( the carrier of V)
len a1 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
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 a1) is finite len a1 -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 a1 ) } is set
Sum g1 is Element of the carrier of V
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
g1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len g1 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
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
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
A 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
rng A is finite Element of K19( the carrier of V)
K19( the carrier of V) is set
(V,(rng 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 rng A : rng b1 c= INT } is set
(V,A) is Element of K19( the carrier of V)
len A is non empty ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
Seg (len A) is non empty 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
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
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 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
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
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 (V,A) is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
Lin A is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
B is set
the carrier of (Lin A) is non empty set
B is Element of K19( the carrier of V)
Lin B is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace 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
h1 is set
g1 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 is Element of the carrier of V
a1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng a1 is finite Element of K19( the carrier of V)
len a1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
len g1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
Seg (len a1) is finite len a1 -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 a1 ) } is set
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
h1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
a1 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
h1 + 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 | h1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Seg h1 is finite 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 <= h1 ) } is set
g1 | (Seg h1) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
h1 | h1 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 h1) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
a1 | h1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a1 | (Seg h1) is Relation-like NAT -defined INT -valued Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued set
gn is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng gn is finite Element of K19( the carrier of V)
len gn is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
an is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len an is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
hn is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len hn is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
Seg (len gn) is finite len gn -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 gn ) } is set
i is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
hn /. i is Element of the carrier of V
gn /. i is Element of the carrier of V
an . i is ext-real V31() V32() integer Element of REAL
(an . i) * (gn /. i) is Element of the carrier of V
i is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
hn /. i is Element of the carrier of V
gn /. i is Element of the carrier of V
an . i is ext-real V31() V32() integer Element of REAL
(an . i) * (gn /. i) is Element of the carrier of V
dom g1 is finite Element of K19(NAT)
g1 /. i 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 /. i is Element of the carrier of V
a1 . i is ext-real V31() V32() integer Element of REAL
i is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer set
hn /. i is Element of the carrier of V
gn /. i is Element of the carrier of V
an . i is ext-real V31() V32() integer Element of REAL
(an . i) * (gn /. i) is Element of the carrier of V
h1 /. (h1 + 1) is Element of the carrier of V
g1 /. (h1 + 1) is Element of the carrier of V
a1 . (h1 + 1) is ext-real V31() V32() integer Element of REAL
(a1 . (h1 + 1)) * (g1 /. (h1 + 1)) is Element of the carrier of V
<*((a1 . (h1 + 1)) * (g1 /. (h1 + 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 . (h1 + 1)) * (g1 /. (h1 + 1)))] is set
{1,((a1 . (h1 + 1)) * (g1 /. (h1 + 1)))} is non empty finite set
{1} is non empty V12() finite V37() 1 -element set
{{1,((a1 . (h1 + 1)) * (g1 /. (h1 + 1)))},{1}} is non empty finite V37() set
{[1,((a1 . (h1 + 1)) * (g1 /. (h1 + 1)))]} is Function-like non empty V12() finite 1 -element set
hn ^ <*((a1 . (h1 + 1)) * (g1 /. (h1 + 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 . (h1 + 1) is set
g1 is ext-real V31() V32() integer Element of INT
g1 * (a1 . (h1 + 1)) is ext-real V31() V32() integer Element of INT
(g1 * (a1 . (h1 + 1))) * (g1 /. (h1 + 1)) is Element of the carrier of V
B is ext-real V31() V32() integer Element of INT
B * (g1 /. (h1 + 1)) is Element of the carrier of V
((g1 * (a1 . (h1 + 1))) * (g1 /. (h1 + 1))) + (B * (g1 /. (h1 + 1))) is Element of the carrier of V
0. V is V52(V) Element of the carrier of V
((g1 * (a1 . (h1 + 1))) * (g1 /. (h1 + 1))) + (0. V) is Element of the carrier of V
Sum hn is Element of the carrier of V
g1 * (Sum hn) is Element of the carrier of V
(g1 * (Sum hn)) + ((g1 * (a1 . (h1 + 1))) * (g1 /. (h1 + 1))) is Element of the carrier of V
Sum <*((a1 . (h1 + 1)) * (g1 /. (h1 + 1)))*> is Element of the carrier of V
(Sum hn) + (Sum <*((a1 . (h1 + 1)) * (g1 /. (h1 + 1)))*>) is Element of the carrier of V
(Sum hn) + ((a1 . (h1 + 1)) * (g1 /. (h1 + 1))) is Element of the carrier of V
a1 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
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
h1 is set
g1 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 is Element of the carrier of V
a1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng a1 is finite Element of K19( the carrier of V)
len a1 is ext-real V24() V25() V26() V30() V31() V32() finite cardinal integer Element of NAT
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 a1) is finite len a1 -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 a1 ) } 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
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
(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 (V,A) : rng b1 c= INT } is set
B is set
B 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
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
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
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
Lin B is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
Lin (V,B) is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V