:: RLVECT_X semantic presentation

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

{ b

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 b

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 b

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 b

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 b

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 b

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 b

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)

{ b

{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)

{ b

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 b

B is Element of K19( the carrier of V)

(V,B) is Element of K19( the carrier of V)

{ (Sum b

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 b

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 b

(V,B) is Element of K19( the carrier of V)

{ (Sum b

(V,A) + (V,B) is Element of K19( the carrier of V)

{ K180(V,b

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)

{ b

(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)

{ b

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)

{ b

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 b

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 b

(V,B) is Element of K19( the carrier of V)

{ (Sum b

(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 b

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)

{ b

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 b

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 b

B + (A,{g1}) is Element of K19( the carrier of A)

{ K180(A,B,b

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 b

{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 b

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)

{ b

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 b

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 b

B + (A,{g1,h1}) is Element of K19( the carrier of A)

{ K180(A,B,b

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 b

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)

{ b

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 b

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 b

B + (A,{g1,h1,a1}) is Element of K19( the carrier of A)

{ K180(A,B,b

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 b

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)

{ b

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)

{ b

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)

{ b

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)

{ b

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)

{ b

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)

{ b

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)

{ b

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 b

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)

{ b

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)

{ b

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 b

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)

{ b

(g1,h1) is Element of K19( the carrier of g1)

{ (Sum b

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)

{ b

{ (Sum b

for b

( not b

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)

{ b

{ (Sum b

for b

( not b

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