:: CONVEX1 semantic presentation

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

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

K10(REAL) is non empty V38() set

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

NAT is V25() V38() cardinal limit_cardinal V63() V64() V65() V66() V67() V68() V69() set

K10(NAT) is non empty V38() set

K10(NAT) is non empty V38() set

K254(NAT) is V52() set

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

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

2 is non empty ext-real positive non negative V25() V29() V30() V31() V36() V37() V38() cardinal V63() V64() V65() V66() V67() V68() Element of NAT

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

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

1 is non empty ext-real positive non negative V25() V29() V30() V31() V36() V37() V38() cardinal V63() V64() V65() V66() V67() V68() Element of NAT

3 is non empty ext-real positive non negative V25() V29() V30() V31() V36() V37() V38() cardinal V63() V64() V65() V66() V67() V68() Element of NAT

0 is empty functional ext-real non positive non negative V25() V29() V30() V31() V36() V37() V38() cardinal {} -element FinSequence-membered V63() V64() V65() V66() V67() V68() V69() Element of NAT

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

Sum (<*> REAL) is ext-real V30() V31() Element of REAL

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

K255(REAL,(<*> REAL),K192()) is ext-real V30() V31() Element of REAL

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

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

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

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

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

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

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

V is non empty RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

v is ext-real V30() V31() Element of REAL

M is Element of K10( the carrier of V)

{ (v * b

{ H

V is non empty RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is ext-real V30() V31() Element of REAL

(V,M,v) is Element of K10( the carrier of V)

{ (v * b

Y is Element of the carrier of V

Y is Element of the carrier of V

r is ext-real V30() V31() Element of REAL

r * Y is Element of the carrier of V

1 - r is ext-real V30() V31() Element of REAL

(1 - r) * Y is Element of the carrier of V

(r * Y) + ((1 - r) * Y) is Element of the carrier of V

F is Element of the carrier of V

v * F is Element of the carrier of V

f is Element of the carrier of V

v * f is Element of the carrier of V

v * r is ext-real V30() V31() Element of REAL

(v * r) * f is Element of the carrier of V

(1 - r) * (v * F) is Element of the carrier of V

((v * r) * f) + ((1 - r) * (v * F)) is Element of the carrier of V

v * (1 - r) is ext-real V30() V31() Element of REAL

(v * (1 - r)) * F is Element of the carrier of V

((v * r) * f) + ((v * (1 - r)) * F) is Element of the carrier of V

r * f is Element of the carrier of V

v * (r * f) is Element of the carrier of V

(v * (r * f)) + ((v * (1 - r)) * F) is Element of the carrier of V

(1 - r) * F is Element of the carrier of V

v * ((1 - r) * F) is Element of the carrier of V

(v * (r * f)) + (v * ((1 - r) * F)) is Element of the carrier of V

(r * f) + ((1 - r) * F) is Element of the carrier of V

v * ((r * f) + ((1 - r) * F)) is Element of the carrier of V

V is non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is Element of K10( the carrier of V)

M + v is Element of K10( the carrier of V)

Y is Element of the carrier of V

Y is Element of the carrier of V

r is ext-real V30() V31() Element of REAL

r * Y is Element of the carrier of V

1 - r is ext-real V30() V31() Element of REAL

(1 - r) * Y is Element of the carrier of V

(r * Y) + ((1 - r) * Y) is Element of the carrier of V

{ (b

F is Element of the carrier of V

f is Element of the carrier of V

F + f is Element of the carrier of V

r1 is Element of the carrier of V

r3 is Element of the carrier of V

r1 + r3 is Element of the carrier of V

r * r1 is Element of the carrier of V

r * r3 is Element of the carrier of V

(r * r1) + (r * r3) is Element of the carrier of V

(1 - r) * (F + f) is Element of the carrier of V

((r * r1) + (r * r3)) + ((1 - r) * (F + f)) is Element of the carrier of V

(1 - r) * F is Element of the carrier of V

(1 - r) * f is Element of the carrier of V

((1 - r) * F) + ((1 - r) * f) is Element of the carrier of V

((r * r1) + (r * r3)) + (((1 - r) * F) + ((1 - r) * f)) is Element of the carrier of V

((r * r1) + (r * r3)) + ((1 - r) * F) is Element of the carrier of V

(((r * r1) + (r * r3)) + ((1 - r) * F)) + ((1 - r) * f) is Element of the carrier of V

(r * r1) + ((1 - r) * F) is Element of the carrier of V

((r * r1) + ((1 - r) * F)) + (r * r3) is Element of the carrier of V

(((r * r1) + ((1 - r) * F)) + (r * r3)) + ((1 - r) * f) is Element of the carrier of V

(r * r3) + ((1 - r) * f) is Element of the carrier of V

((r * r1) + ((1 - r) * F)) + ((r * r3) + ((1 - r) * f)) is Element of the carrier of V

V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is Element of K10( the carrier of V)

M - v is Element of K10( the carrier of V)

Y is Element of the carrier of V

Y is Element of the carrier of V

r is ext-real V30() V31() Element of REAL

r * Y is Element of the carrier of V

1 - r is ext-real V30() V31() Element of REAL

(1 - r) * Y is Element of the carrier of V

(r * Y) + ((1 - r) * Y) is Element of the carrier of V

{ (b

F is Element of the carrier of V

f is Element of the carrier of V

F - f is Element of the carrier of V

- f is Element of the carrier of V

F + (- f) is Element of the carrier of V

r1 is Element of the carrier of V

r3 is Element of the carrier of V

r1 - r3 is Element of the carrier of V

- r3 is Element of the carrier of V

r1 + (- r3) is Element of the carrier of V

r * r1 is Element of the carrier of V

r * r3 is Element of the carrier of V

(r * r1) - (r * r3) is Element of the carrier of V

- (r * r3) is Element of the carrier of V

(r * r1) + (- (r * r3)) is Element of the carrier of V

(1 - r) * (F - f) is Element of the carrier of V

((r * r1) - (r * r3)) + ((1 - r) * (F - f)) is Element of the carrier of V

(1 - r) * F is Element of the carrier of V

(1 - r) * f is Element of the carrier of V

((1 - r) * F) - ((1 - r) * f) is Element of the carrier of V

- ((1 - r) * f) is Element of the carrier of V

((1 - r) * F) + (- ((1 - r) * f)) is Element of the carrier of V

((r * r1) - (r * r3)) + (((1 - r) * F) - ((1 - r) * f)) is Element of the carrier of V

((r * r1) - (r * r3)) + ((1 - r) * F) is Element of the carrier of V

(((r * r1) - (r * r3)) + ((1 - r) * F)) - ((1 - r) * f) is Element of the carrier of V

(((r * r1) - (r * r3)) + ((1 - r) * F)) + (- ((1 - r) * f)) is Element of the carrier of V

(r * r3) - ((1 - r) * F) is Element of the carrier of V

- ((1 - r) * F) is Element of the carrier of V

(r * r3) + (- ((1 - r) * F)) is Element of the carrier of V

(r * r1) - ((r * r3) - ((1 - r) * F)) is Element of the carrier of V

- ((r * r3) - ((1 - r) * F)) is Element of the carrier of V

(r * r1) + (- ((r * r3) - ((1 - r) * F))) is Element of the carrier of V

((r * r1) - ((r * r3) - ((1 - r) * F))) - ((1 - r) * f) is Element of the carrier of V

((r * r1) - ((r * r3) - ((1 - r) * F))) + (- ((1 - r) * f)) is Element of the carrier of V

((1 - r) * F) + (- (r * r3)) is Element of the carrier of V

(r * r1) + (((1 - r) * F) + (- (r * r3))) is Element of the carrier of V

((r * r1) + (((1 - r) * F) + (- (r * r3)))) - ((1 - r) * f) is Element of the carrier of V

((r * r1) + (((1 - r) * F) + (- (r * r3)))) + (- ((1 - r) * f)) is Element of the carrier of V

(r * r1) + ((1 - r) * F) is Element of the carrier of V

((r * r1) + ((1 - r) * F)) + (- (r * r3)) is Element of the carrier of V

(((r * r1) + ((1 - r) * F)) + (- (r * r3))) - ((1 - r) * f) is Element of the carrier of V

(((r * r1) + ((1 - r) * F)) + (- (r * r3))) + (- ((1 - r) * f)) is Element of the carrier of V

(- (r * r3)) - ((1 - r) * f) is Element of the carrier of V

(- (r * r3)) + (- ((1 - r) * f)) is Element of the carrier of V

((r * r1) + ((1 - r) * F)) + ((- (r * r3)) - ((1 - r) * f)) is Element of the carrier of V

(r * r3) + ((1 - r) * f) is Element of the carrier of V

((r * r1) + ((1 - r) * F)) - ((r * r3) + ((1 - r) * f)) is Element of the carrier of V

- ((r * r3) + ((1 - r) * f)) is Element of the carrier of V

((r * r1) + ((1 - r) * F)) + (- ((r * r3) + ((1 - r) * f))) is Element of the carrier of V

V is non empty RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is ext-real V30() V31() Element of REAL

(V,M,v) is Element of K10( the carrier of V)

{ (v * b

1 - v is ext-real V30() V31() Element of REAL

(V,M,(1 - v)) is Element of K10( the carrier of V)

{ ((1 - v) * b

(V,M,v) + (V,M,(1 - v)) is Element of K10( the carrier of V)

Y is Element of the carrier of V

{ (b

Y is Element of the carrier of V

r is Element of the carrier of V

Y + r is Element of the carrier of V

F is Element of the carrier of V

v * F is Element of the carrier of V

f is Element of the carrier of V

(1 - v) * f is Element of the carrier of V

v is Element of the carrier of V

Y is Element of the carrier of V

Y is ext-real V30() V31() Element of REAL

Y * v is Element of the carrier of V

1 - Y is ext-real V30() V31() Element of REAL

(1 - Y) * Y is Element of the carrier of V

(Y * v) + ((1 - Y) * Y) is Element of the carrier of V

(V,M,Y) is Element of K10( the carrier of V)

{ (Y * b

(V,M,(1 - Y)) is Element of K10( the carrier of V)

{ ((1 - Y) * b

(V,M,Y) + (V,M,(1 - Y)) is Element of K10( the carrier of V)

{ (b

v is ext-real V30() V31() Element of REAL

(V,M,v) is Element of K10( the carrier of V)

{ (v * b

1 - v is ext-real V30() V31() Element of REAL

(V,M,(1 - v)) is Element of K10( the carrier of V)

{ ((1 - v) * b

(V,M,v) + (V,M,(1 - v)) is Element of K10( the carrier of V)

Y is ext-real V30() V31() Element of REAL

(V,M,Y) is Element of K10( the carrier of V)

{ (Y * b

1 - Y is ext-real V30() V31() Element of REAL

(V,M,(1 - Y)) is Element of K10( the carrier of V)

{ ((1 - Y) * b

(V,M,Y) + (V,M,(1 - Y)) is Element of K10( the carrier of V)

V is non empty Abelian RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is ext-real V30() V31() Element of REAL

1 - v is ext-real V30() V31() Element of REAL

(V,M,(1 - v)) is Element of K10( the carrier of V)

{ ((1 - v) * b

(V,M,v) is Element of K10( the carrier of V)

{ (v * b

(V,M,(1 - v)) + (V,M,v) is Element of K10( the carrier of V)

Y is Element of the carrier of V

{ (b

Y is Element of the carrier of V

r is Element of the carrier of V

Y + r is Element of the carrier of V

F is Element of the carrier of V

(1 - v) * F is Element of the carrier of V

f is Element of the carrier of V

v * f is Element of the carrier of V

V is non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is Element of K10( the carrier of V)

Y is ext-real V30() V31() Element of REAL

(V,M,Y) is Element of K10( the carrier of V)

{ (Y * b

1 - Y is ext-real V30() V31() Element of REAL

(V,v,(1 - Y)) is Element of K10( the carrier of V)

{ ((1 - Y) * b

(V,M,Y) + (V,v,(1 - Y)) is Element of K10( the carrier of V)

Y is Element of the carrier of V

r is Element of the carrier of V

F is ext-real V30() V31() Element of REAL

F * Y is Element of the carrier of V

1 - F is ext-real V30() V31() Element of REAL

(1 - F) * r is Element of the carrier of V

(F * Y) + ((1 - F) * r) is Element of the carrier of V

{ (b

f is Element of the carrier of V

r1 is Element of the carrier of V

f + r1 is Element of the carrier of V

r3 is Element of the carrier of V

r2 is Element of the carrier of V

r3 + r2 is Element of the carrier of V

u2 is Element of the carrier of V

Y * u2 is Element of the carrier of V

y1 is Element of the carrier of V

Y * y1 is Element of the carrier of V

F * r3 is Element of the carrier of V

(1 - F) * f is Element of the carrier of V

(F * r3) + ((1 - F) * f) is Element of the carrier of V

F * Y is ext-real V30() V31() Element of REAL

(F * Y) * y1 is Element of the carrier of V

(1 - F) * (Y * u2) is Element of the carrier of V

((F * Y) * y1) + ((1 - F) * (Y * u2)) is Element of the carrier of V

(1 - F) * Y is ext-real V30() V31() Element of REAL

((1 - F) * Y) * u2 is Element of the carrier of V

((F * Y) * y1) + (((1 - F) * Y) * u2) is Element of the carrier of V

F * y1 is Element of the carrier of V

Y * (F * y1) is Element of the carrier of V

(Y * (F * y1)) + (((1 - F) * Y) * u2) is Element of the carrier of V

(1 - F) * u2 is Element of the carrier of V

Y * ((1 - F) * u2) is Element of the carrier of V

(Y * (F * y1)) + (Y * ((1 - F) * u2)) is Element of the carrier of V

(F * y1) + ((1 - F) * u2) is Element of the carrier of V

Y * ((F * y1) + ((1 - F) * u2)) is Element of the carrier of V

x1 is Element of the carrier of V

(1 - Y) * x1 is Element of the carrier of V

y2 is Element of the carrier of V

(1 - Y) * y2 is Element of the carrier of V

F * r2 is Element of the carrier of V

(1 - F) * r1 is Element of the carrier of V

(F * r2) + ((1 - F) * r1) is Element of the carrier of V

F * (1 - Y) is ext-real V30() V31() Element of REAL

(F * (1 - Y)) * y2 is Element of the carrier of V

(1 - F) * ((1 - Y) * x1) is Element of the carrier of V

((F * (1 - Y)) * y2) + ((1 - F) * ((1 - Y) * x1)) is Element of the carrier of V

(1 - F) * (1 - Y) is ext-real V30() V31() Element of REAL

((1 - F) * (1 - Y)) * x1 is Element of the carrier of V

((F * (1 - Y)) * y2) + (((1 - F) * (1 - Y)) * x1) is Element of the carrier of V

F * y2 is Element of the carrier of V

(1 - Y) * (F * y2) is Element of the carrier of V

((1 - Y) * (F * y2)) + (((1 - F) * (1 - Y)) * x1) is Element of the carrier of V

(1 - F) * x1 is Element of the carrier of V

(1 - Y) * ((1 - F) * x1) is Element of the carrier of V

((1 - Y) * (F * y2)) + ((1 - Y) * ((1 - F) * x1)) is Element of the carrier of V

(F * y2) + ((1 - F) * x1) is Element of the carrier of V

(1 - Y) * ((F * y2) + ((1 - F) * x1)) is Element of the carrier of V

(F * Y) + ((1 - F) * r) is Element of the carrier of V

(F * r3) + (F * r2) is Element of the carrier of V

(1 - F) * (f + r1) is Element of the carrier of V

((F * r3) + (F * r2)) + ((1 - F) * (f + r1)) is Element of the carrier of V

((1 - F) * f) + ((1 - F) * r1) is Element of the carrier of V

((F * r3) + (F * r2)) + (((1 - F) * f) + ((1 - F) * r1)) is Element of the carrier of V

((F * r3) + (F * r2)) + ((1 - F) * f) is Element of the carrier of V

(((F * r3) + (F * r2)) + ((1 - F) * f)) + ((1 - F) * r1) is Element of the carrier of V

((F * r3) + ((1 - F) * f)) + (F * r2) is Element of the carrier of V

(((F * r3) + ((1 - F) * f)) + (F * r2)) + ((1 - F) * r1) is Element of the carrier of V

((F * r3) + ((1 - F) * f)) + ((F * r2) + ((1 - F) * r1)) is Element of the carrier of V

V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

(V,M,1) is Element of K10( the carrier of V)

{ (1 * b

v is Element of the carrier of V

1 * v is Element of the carrier of V

v is Element of the carrier of V

Y is Element of the carrier of V

1 * Y is Element of the carrier of V

V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

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

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

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

(V,M,0) is Element of K10( the carrier of V)

{ (0 * b

v is Element of the carrier of V

Y is set

Y is Element of the carrier of V

0 * Y is Element of the carrier of V

v is Element of the carrier of V

Y is Element of the carrier of V

0 * Y is Element of the carrier of V

V is non empty add-associative addLoopStr

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is Element of K10( the carrier of V)

M + v is Element of K10( the carrier of V)

Y is Element of K10( the carrier of V)

(M + v) + Y is Element of K10( the carrier of V)

v + Y is Element of K10( the carrier of V)

M + (v + Y) is Element of K10( the carrier of V)

Y is Element of the carrier of V

{ (b

r is Element of the carrier of V

F is Element of the carrier of V

r + F is Element of the carrier of V

{ (b

f is Element of the carrier of V

r1 is Element of the carrier of V

f + r1 is Element of the carrier of V

r + f is Element of the carrier of V

{ (b

(r + f) + r1 is Element of the carrier of V

{ (b

Y is Element of the carrier of V

{ (b

r is Element of the carrier of V

F is Element of the carrier of V

r + F is Element of the carrier of V

{ (b

f is Element of the carrier of V

r1 is Element of the carrier of V

f + r1 is Element of the carrier of V

r1 + F is Element of the carrier of V

{ (b

f + (r1 + F) is Element of the carrier of V

{ (b

V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

Y is ext-real V30() V31() Element of REAL

(V,M,Y) is Element of K10( the carrier of V)

{ (Y * b

v is ext-real V30() V31() Element of REAL

(V,(V,M,Y),v) is Element of K10( the carrier of V)

{ (v * b

v * Y is ext-real V30() V31() Element of REAL

(V,M,(v * Y)) is Element of K10( the carrier of V)

{ ((v * Y) * b

Y is Element of the carrier of V

r is Element of the carrier of V

v * r is Element of the carrier of V

F is Element of the carrier of V

Y * F is Element of the carrier of V

(v * Y) * F is Element of the carrier of V

Y is Element of the carrier of V

r is Element of the carrier of V

(v * Y) * r is Element of the carrier of V

Y * r is Element of the carrier of V

v * (Y * r) is Element of the carrier of V

V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is Element of K10( the carrier of V)

M + v is Element of K10( the carrier of V)

Y is ext-real V30() V31() Element of REAL

(V,(M + v),Y) is Element of K10( the carrier of V)

{ (Y * b

(V,M,Y) is Element of K10( the carrier of V)

{ (Y * b

(V,v,Y) is Element of K10( the carrier of V)

{ (Y * b

(V,M,Y) + (V,v,Y) is Element of K10( the carrier of V)

Y is Element of the carrier of V

{ (b

r is Element of the carrier of V

F is Element of the carrier of V

r + F is Element of the carrier of V

f is Element of the carrier of V

Y * f is Element of the carrier of V

r1 is Element of the carrier of V

Y * r1 is Element of the carrier of V

r1 + f is Element of the carrier of V

{ (b

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

Y is Element of the carrier of V

r is Element of the carrier of V

Y * r is Element of the carrier of V

{ (b

F is Element of the carrier of V

f is Element of the carrier of V

F + f is Element of the carrier of V

Y * F is Element of the carrier of V

Y * f is Element of the carrier of V

(Y * F) + (Y * f) is Element of the carrier of V

{ (b

V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is Element of the carrier of V

v + M is Element of K10( the carrier of V)

Y is Element of the carrier of V

Y is Element of the carrier of V

r is ext-real V30() V31() Element of REAL

r * Y is Element of the carrier of V

1 - r is ext-real V30() V31() Element of REAL

(1 - r) * Y is Element of the carrier of V

(r * Y) + ((1 - r) * Y) is Element of the carrier of V

v + Y is Element of the carrier of V

{ (v + b

v + Y is Element of the carrier of V

r * (v + Y) is Element of the carrier of V

(1 - r) * (v + Y) is Element of the carrier of V

(r * (v + Y)) + ((1 - r) * (v + Y)) is Element of the carrier of V

r * v is Element of the carrier of V

(r * v) + (r * Y) is Element of the carrier of V

((r * v) + (r * Y)) + ((1 - r) * (v + Y)) is Element of the carrier of V

(1 - r) * v is Element of the carrier of V

((1 - r) * v) + ((1 - r) * Y) is Element of the carrier of V

((r * v) + (r * Y)) + (((1 - r) * v) + ((1 - r) * Y)) is Element of the carrier of V

((r * v) + (r * Y)) + ((1 - r) * v) is Element of the carrier of V

(((r * v) + (r * Y)) + ((1 - r) * v)) + ((1 - r) * Y) is Element of the carrier of V

(r * v) + ((1 - r) * v) is Element of the carrier of V

((r * v) + ((1 - r) * v)) + (r * Y) is Element of the carrier of V

(((r * v) + ((1 - r) * v)) + (r * Y)) + ((1 - r) * Y) is Element of the carrier of V

r + (1 - r) is ext-real V30() V31() Element of REAL

(r + (1 - r)) * v is Element of the carrier of V

((r + (1 - r)) * v) + (r * Y) is Element of the carrier of V

(((r + (1 - r)) * v) + (r * Y)) + ((1 - r) * Y) is Element of the carrier of V

v + (r * Y) is Element of the carrier of V

(v + (r * Y)) + ((1 - r) * Y) is Element of the carrier of V

(r * Y) + ((1 - r) * Y) is Element of the carrier of V

v + ((r * Y) + ((1 - r) * Y)) is Element of the carrier of V

r1 is Element of the carrier of V

v + r1 is Element of the carrier of V

Y is Element of the carrier of V

Y is Element of the carrier of V

r is ext-real V30() V31() Element of REAL

r * Y is Element of the carrier of V

1 - r is ext-real V30() V31() Element of REAL

(1 - r) * Y is Element of the carrier of V

(r * Y) + ((1 - r) * Y) is Element of the carrier of V

{ (v + b

F is Element of the carrier of V

v + F is Element of the carrier of V

f is Element of the carrier of V

v + f is Element of the carrier of V

(r * Y) + ((1 - r) * Y) is Element of the carrier of V

r * v is Element of the carrier of V

r * f is Element of the carrier of V

(r * v) + (r * f) is Element of the carrier of V

(1 - r) * (v + F) is Element of the carrier of V

((r * v) + (r * f)) + ((1 - r) * (v + F)) is Element of the carrier of V

(1 - r) * v is Element of the carrier of V

(1 - r) * F is Element of the carrier of V

((1 - r) * v) + ((1 - r) * F) is Element of the carrier of V

((r * v) + (r * f)) + (((1 - r) * v) + ((1 - r) * F)) is Element of the carrier of V

((r * v) + (r * f)) + ((1 - r) * v) is Element of the carrier of V

(((r * v) + (r * f)) + ((1 - r) * v)) + ((1 - r) * F) is Element of the carrier of V

(r * v) + ((1 - r) * v) is Element of the carrier of V

((r * v) + ((1 - r) * v)) + (r * f) is Element of the carrier of V

(((r * v) + ((1 - r) * v)) + (r * f)) + ((1 - r) * F) is Element of the carrier of V

r + (1 - r) is ext-real V30() V31() Element of REAL

(r + (1 - r)) * v is Element of the carrier of V

((r + (1 - r)) * v) + (r * f) is Element of the carrier of V

(((r + (1 - r)) * v) + (r * f)) + ((1 - r) * F) is Element of the carrier of V

v + (r * f) is Element of the carrier of V

(v + (r * f)) + ((1 - r) * F) is Element of the carrier of V

(r * f) + ((1 - r) * F) is Element of the carrier of V

v + ((r * f) + ((1 - r) * F)) is Element of the carrier of V

V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() RLSStruct

(0). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() Subspace of V

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

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of the carrier of V

v is Element of the carrier of V

Y is ext-real V30() V31() Element of REAL

Y * M is Element of the carrier of V

1 - Y is ext-real V30() V31() Element of REAL

(1 - Y) * v is Element of the carrier of V

(Y * M) + ((1 - Y) * v) is Element of the carrier of V

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

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

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

(Y * M) + ((1 - Y) * v) is Element of the carrier of V

(1 - Y) * (0. V) is Element of the carrier of V

(0. V) + ((1 - Y) * (0. V)) is Element of the carrier of V

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

V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() RLSStruct

(Omega). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() Subspace of V

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

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of the carrier of V

v is Element of the carrier of V

Y is ext-real V30() V31() Element of REAL

Y * M is Element of the carrier of V

1 - Y is ext-real V30() V31() Element of REAL

(1 - Y) * v is Element of the carrier of V

(Y * M) + ((1 - Y) * v) is Element of the carrier of V

the ZeroF of V is Element of the carrier of V

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

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

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

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

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

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

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

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

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

(Y * M) + ((1 - Y) * v) is Element of the carrier of V

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

V is non empty RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

Y is ext-real V30() V31() Element of REAL

v is Element of the carrier of V

Y is Element of the carrier of V

Y * v is Element of the carrier of V

1 - Y is ext-real V30() V31() Element of REAL

(1 - Y) * Y is Element of the carrier of V

(Y * v) + ((1 - Y) * Y) is Element of the carrier of V

V is non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is Element of K10( the carrier of V)

Y is ext-real V30() V31() Element of REAL

(V,M,Y) is Element of K10( the carrier of V)

{ (Y * b

Y is ext-real V30() V31() Element of REAL

(V,v,Y) is Element of K10( the carrier of V)

{ (Y * b

(V,M,Y) + (V,v,Y) is Element of K10( the carrier of V)

r is Element of the carrier of V

F is Element of the carrier of V

f is ext-real V30() V31() Element of REAL

f * r is Element of the carrier of V

1 - f is ext-real V30() V31() Element of REAL

(1 - f) * F is Element of the carrier of V

(f * r) + ((1 - f) * F) is Element of the carrier of V

{ (b

r1 is Element of the carrier of V

r3 is Element of the carrier of V

r1 + r3 is Element of the carrier of V

r2 is Element of the carrier of V

u2 is Element of the carrier of V

r2 + u2 is Element of the carrier of V

y1 is Element of the carrier of V

Y * y1 is Element of the carrier of V

x1 is Element of the carrier of V

Y * x1 is Element of the carrier of V

f * r2 is Element of the carrier of V

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

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

Y * f is ext-real V30() V31() Element of REAL

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

(1 - f) * (Y * y1) is Element of the carrier of V

((Y * f) * x1) + ((1 - f) * (Y * y1)) is Element of the carrier of V

Y * (1 - f) is ext-real V30() V31() Element of REAL

(Y * (1 - f)) * y1 is Element of the carrier of V

((Y * f) * x1) + ((Y * (1 - f)) * y1) is Element of the carrier of V

f * x1 is Element of the carrier of V

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

(Y * (f * x1)) + ((Y * (1 - f)) * y1) is Element of the carrier of V

(1 - f) * y1 is Element of the carrier of V

Y * ((1 - f) * y1) is Element of the carrier of V

(Y * (f * x1)) + (Y * ((1 - f) * y1)) is Element of the carrier of V

(f * x1) + ((1 - f) * y1) is Element of the carrier of V

Y * ((f * x1) + ((1 - f) * y1)) is Element of the carrier of V

y2 is Element of the carrier of V

Y * y2 is Element of the carrier of V

x2 is Element of the carrier of V

Y * x2 is Element of the carrier of V

f * u2 is Element of the carrier of V

(1 - f) * r3 is Element of the carrier of V

(f * u2) + ((1 - f) * r3) is Element of the carrier of V

Y * f is ext-real V30() V31() Element of REAL

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

(1 - f) * (Y * y2) is Element of the carrier of V

((Y * f) * x2) + ((1 - f) * (Y * y2)) is Element of the carrier of V

Y * (1 - f) is ext-real V30() V31() Element of REAL

(Y * (1 - f)) * y2 is Element of the carrier of V

((Y * f) * x2) + ((Y * (1 - f)) * y2) is Element of the carrier of V

f * x2 is Element of the carrier of V

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

(Y * (f * x2)) + ((Y * (1 - f)) * y2) is Element of the carrier of V

(1 - f) * y2 is Element of the carrier of V

Y * ((1 - f) * y2) is Element of the carrier of V

(Y * (f * x2)) + (Y * ((1 - f) * y2)) is Element of the carrier of V

(f * x2) + ((1 - f) * y2) is Element of the carrier of V

Y * ((f * x2) + ((1 - f) * y2)) is Element of the carrier of V

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

(1 - f) * (r1 + r3) is Element of the carrier of V

(f * (r2 + u2)) + ((1 - f) * (r1 + r3)) is Element of the carrier of V

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

((f * r2) + (f * u2)) + ((1 - f) * (r1 + r3)) is Element of the carrier of V

((1 - f) * r1) + ((1 - f) * r3) is Element of the carrier of V

((f * r2) + (f * u2)) + (((1 - f) * r1) + ((1 - f) * r3)) is Element of the carrier of V

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

(((f * r2) + (f * u2)) + ((1 - f) * r1)) + ((1 - f) * r3) is Element of the carrier of V

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

(((f * r2) + ((1 - f) * r1)) + (f * u2)) + ((1 - f) * r3) is Element of the carrier of V

((f * r2) + ((1 - f) * r1)) + ((f * u2) + ((1 - f) * r3)) is Element of the carrier of V

V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is ext-real V30() V31() Element of REAL

Y is ext-real V30() V31() Element of REAL

v + Y is ext-real V30() V31() Element of REAL

(V,M,(v + Y)) is Element of K10( the carrier of V)

{ ((v + Y) * b

(V,M,v) is Element of K10( the carrier of V)

{ (v * b

(V,M,Y) is Element of K10( the carrier of V)

{ (Y * b

(V,M,v) + (V,M,Y) is Element of K10( the carrier of V)

Y is Element of the carrier of V

r is Element of the carrier of V

(v + Y) * r is Element of the carrier of V

Y * r is Element of the carrier of V

v * r is Element of the carrier of V

(v * r) + (Y * r) is Element of the carrier of V

{ (b

V is non empty RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is Element of K10( the carrier of V)

Y is ext-real V30() V31() Element of REAL

(V,M,Y) is Element of K10( the carrier of V)

{ (Y * b

(V,v,Y) is Element of K10( the carrier of V)

{ (Y * b

Y is Element of the carrier of V

r is Element of the carrier of V

Y * r is Element of the carrier of V

V is non empty RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

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

v is ext-real V30() V31() Element of REAL

(V,M,v) is Element of K10( the carrier of V)

{ (v * b

Y is Element of the carrier of V

Y is Element of the carrier of V

v * Y is Element of the carrier of V

V is non empty addLoopStr

the carrier of V is non empty set

K10( the carrier of V) is non empty set

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

v is Element of K10( the carrier of V)

M + v is Element of K10( the carrier of V)

{ (b

Y is Element of the carrier of V

Y is Element of the carrier of V

r is Element of the carrier of V

Y + r is Element of the carrier of V

V is non empty right_zeroed addLoopStr

the carrier of V is non empty set

K10( the carrier of V) is non empty set

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

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

M is Element of K10( the carrier of V)

M + {(0. V)} is Element of K10( the carrier of V)

v is Element of the carrier of V

{ (b

Y is Element of the carrier of V

Y is Element of the carrier of V

Y + Y is Element of the carrier of V

v is Element of the carrier of V

v + (0. V) is Element of the carrier of V

{ (b

V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is ext-real V30() V31() Element of REAL

Y is ext-real V30() V31() Element of REAL

(V,M,v) is Element of K10( the carrier of V)

{ (v * b

(V,M,Y) is Element of K10( the carrier of V)

{ (Y * b

(V,M,v) + (V,M,Y) is Element of K10( the carrier of V)

v + Y is ext-real V30() V31() Element of REAL

(V,M,(v + Y)) is Element of K10( the carrier of V)

{ ((v + Y) * b

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

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

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

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

v / (v + Y) is ext-real V30() V31() Element of REAL

(V,M,(v / (v + Y))) is Element of K10( the carrier of V)

{ ((v / (v + Y)) * b

1 - (v / (v + Y)) is ext-real V30() V31() Element of REAL

(V,M,(1 - (v / (v + Y)))) is Element of K10( the carrier of V)

{ ((1 - (v / (v + Y))) * b

(V,M,(v / (v + Y))) + (V,M,(1 - (v / (v + Y)))) is Element of K10( the carrier of V)

(V,((V,M,(v / (v + Y))) + (V,M,(1 - (v / (v + Y))))),(v + Y)) is Element of K10( the carrier of V)

{ ((v + Y) * b

(v + Y) / (v + Y) is ext-real V30() V31() Element of REAL

((v + Y) / (v + Y)) - (v / (v + Y)) is ext-real V30() V31() Element of REAL

(v + Y) - v is ext-real V30() V31() Element of REAL

((v + Y) - v) / (v + Y) is ext-real V30() V31() Element of REAL

Y / (v + Y) is ext-real V30() V31() Element of REAL

(V,(V,M,(1 - (v / (v + Y)))),(v + Y)) is Element of K10( the carrier of V)

{ ((v + Y) * b

(Y / (v + Y)) * (v + Y) is ext-real V30() V31() Element of REAL

(V,M,((Y / (v + Y)) * (v + Y))) is Element of K10( the carrier of V)

{ (((Y / (v + Y)) * (v + Y)) * b

(V,(V,M,(v / (v + Y))),(v + Y)) is Element of K10( the carrier of V)

{ ((v + Y) * b

(v / (v + Y)) * (v + Y) is ext-real V30() V31() Element of REAL

(V,M,((v / (v + Y)) * (v + Y))) is Element of K10( the carrier of V)

{ (((v / (v + Y)) * (v + Y)) * b

V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is ext-real V30() V31() Element of REAL

Y is ext-real V30() V31() Element of REAL

(V,M,v) is Element of K10( the carrier of V)

{ (v * b

(V,M,Y) is Element of K10( the carrier of V)

{ (Y * b

(V,M,v) + (V,M,Y) is Element of K10( the carrier of V)

v + Y is ext-real V30() V31() Element of REAL

(V,M,(v + Y)) is Element of K10( the carrier of V)

{ ((v + Y) * b

V is non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is Element of K10( the carrier of V)

Y is Element of K10( the carrier of V)

Y is ext-real V30() V31() Element of REAL

(V,M,Y) is Element of K10( the carrier of V)

{ (Y * b

r is ext-real V30() V31() Element of REAL

(V,v,r) is Element of K10( the carrier of V)

{ (r * b

(V,M,Y) + (V,v,r) is Element of K10( the carrier of V)

F is ext-real V30() V31() Element of REAL

(V,Y,F) is Element of K10( the carrier of V)

{ (F * b

((V,M,Y) + (V,v,r)) + (V,Y,F) is Element of K10( the carrier of V)

(V,((V,M,Y) + (V,v,r)),1) is Element of K10( the carrier of V)

{ (1 * b

(V,((V,M,Y) + (V,v,r)),1) + (V,Y,F) is Element of K10( the carrier of V)

V is non empty RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

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

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

meet M is Element of K10( the carrier of V)

v is Element of the carrier of V

Y is Element of the carrier of V

Y is ext-real V30() V31() Element of REAL

Y * v is Element of the carrier of V

1 - Y is ext-real V30() V31() Element of REAL

(1 - Y) * Y is Element of the carrier of V

(Y * v) + ((1 - Y) * Y) is Element of the carrier of V

r is set

F is Element of K10( the carrier of V)

V is non empty RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is Element of the carrier of V

Y is Element of the carrier of V

Y is ext-real V30() V31() Element of REAL

Y * v is Element of the carrier of V

1 - Y is ext-real V30() V31() Element of REAL

(1 - Y) * Y is Element of the carrier of V

(Y * v) + ((1 - Y) * Y) is Element of the carrier of V

1 - (1 - Y) is ext-real V30() V31() Element of REAL

V is non empty RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

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

V is non empty RLSStruct

the carrier of V is non empty set

K10( the carrier of V) is non empty set

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

V is non empty RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is Element of the carrier of V

Y is ext-real V30() V31() Element of REAL

{ b

Y is Element of the carrier of V

r is Element of the carrier of V

F is ext-real V30() V31() Element of REAL

F * Y is Element of the carrier of V

1 - F is ext-real V30() V31() Element of REAL

(1 - F) * r is Element of the carrier of V

(F * Y) + ((1 - F) * r) is Element of the carrier of V

0 + F is ext-real V30() V31() Element of REAL

f is Element of the carrier of V

f .|. v is ext-real V30() V31() Element of REAL

((1 - F) * r) .|. v is ext-real V30() V31() Element of REAL

(1 - F) * (f .|. v) is ext-real V30() V31() Element of REAL

(1 - F) * Y is ext-real V30() V31() Element of REAL

r1 is Element of the carrier of V

r1 .|. v is ext-real V30() V31() Element of REAL

(F * Y) .|. v is ext-real V30() V31() Element of REAL

F * (r1 .|. v) is ext-real V30() V31() Element of REAL

F * Y is ext-real V30() V31() Element of REAL

((F * Y) + ((1 - F) * r)) .|. v is ext-real V30() V31() Element of REAL

((F * Y) .|. v) + (((1 - F) * r) .|. v) is ext-real V30() V31() Element of REAL

(F * Y) + ((1 - F) * Y) is ext-real V30() V31() Element of REAL

V is non empty RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is Element of the carrier of V

Y is ext-real V30() V31() Element of REAL

{ b

Y is Element of the carrier of V

r is Element of the carrier of V

F is ext-real V30() V31() Element of REAL

F * Y is Element of the carrier of V

1 - F is ext-real V30() V31() Element of REAL

(1 - F) * r is Element of the carrier of V

(F * Y) + ((1 - F) * r) is Element of the carrier of V

0 + F is ext-real V30() V31() Element of REAL

f is Element of the carrier of V

f .|. v is ext-real V30() V31() Element of REAL

((1 - F) * r) .|. v is ext-real V30() V31() Element of REAL

(1 - F) * (f .|. v) is ext-real V30() V31() Element of REAL

(1 - F) * Y is ext-real V30() V31() Element of REAL

r1 is Element of the carrier of V

r1 .|. v is ext-real V30() V31() Element of REAL

(F * Y) .|. v is ext-real V30() V31() Element of REAL

F * (r1 .|. v) is ext-real V30() V31() Element of REAL

F * Y is ext-real V30() V31() Element of REAL

((F * Y) + ((1 - F) * r)) .|. v is ext-real V30() V31() Element of REAL

((F * Y) .|. v) + (((1 - F) * r) .|. v) is ext-real V30() V31() Element of REAL

(F * Y) + ((1 - F) * Y) is ext-real V30() V31() Element of REAL

V is non empty RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is Element of the carrier of V

Y is ext-real V30() V31() Element of REAL

{ b

Y is Element of the carrier of V

r is Element of the carrier of V

F is ext-real V30() V31() Element of REAL

F * Y is Element of the carrier of V

1 - F is ext-real V30() V31() Element of REAL

(1 - F) * r is Element of the carrier of V

(F * Y) + ((1 - F) * r) is Element of the carrier of V

0 + F is ext-real V30() V31() Element of REAL

f is Element of the carrier of V

f .|. v is ext-real V30() V31() Element of REAL

((1 - F) * r) .|. v is ext-real V30() V31() Element of REAL

(1 - F) * (f .|. v) is ext-real V30() V31() Element of REAL

(1 - F) * Y is ext-real V30() V31() Element of REAL

r1 is Element of the carrier of V

r1 .|. v is ext-real V30() V31() Element of REAL

(F * Y) .|. v is ext-real V30() V31() Element of REAL

F * (r1 .|. v) is ext-real V30() V31() Element of REAL

F * Y is ext-real V30() V31() Element of REAL

((F * Y) + ((1 - F) * r)) .|. v is ext-real V30() V31() Element of REAL

((F * Y) .|. v) + (((1 - F) * r) .|. v) is ext-real V30() V31() Element of REAL

(F * Y) + ((1 - F) * Y) is ext-real V30() V31() Element of REAL

V is non empty RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

K10( the carrier of V) is non empty set

M is Element of K10( the carrier of V)

v is Element of the carrier of V

Y is ext-real V30() V31() Element of REAL

{ b

Y is Element of the carrier of V

r is Element of the carrier of V

F is ext-real V30() V31() Element of REAL

F * Y is Element of the carrier of V

1 - F is ext-real V30() V31() Element of REAL

(1 - F) * r is Element of the carrier of V

(F * Y) + ((1 - F) * r) is Element of the carrier of V

0 + F is ext-real V30() V31() Element of REAL

f is Element of the carrier of V

f .|. v is ext-real V30() V31() Element of REAL

((1 - F) * r) .|. v is ext-real V30() V31() Element of REAL

(1 - F) * (f .|. v) is ext-real V30() V31() Element of REAL

(1 - F) * Y is ext-real V30() V31() Element of REAL

r1 is Element of the carrier of V

r1 .|. v is ext-real V30() V31() Element of REAL

(F * Y) .|. v is ext-real V30() V31() Element of REAL

F * (r1 .|. v) is ext-real V30() V31() Element of REAL

F * Y is ext-real V30() V31() Element of REAL

((F * Y) + ((1 - F) * r)) .|. v is ext-real V30() V31() Element of REAL

((F * Y) .|. v) + (((1 - F) * r) .|. v) is ext-real V30() V31() Element of REAL

(F * Y) + ((1 - F) * Y) is ext-real V30() V31() Element of REAL

V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() RLSStruct

the carrier of V is non empty set

V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() RLSStruct

the carrier of V is non empty set

M is V10() V13( the carrier of V) V14( REAL ) Function-like V33( the carrier of V, REAL ) V53() V54() V55() Linear_Combination of V

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

K10( the carrier of V) is non empty set

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

rng v is set

len v is ext-real V25() V29() V30() V31() V36() V37() V38() cardinal V63() V64() V65() V66() V67() V68() Element of NAT

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

len Y is ext-real V25() V29() V30() V31() V36() V37() V38() cardinal V63() V64() V65() V66() V67() V68() Element of NAT

Sum Y is ext-real V30() V31() Element of REAL

K255(REAL,Y,K192()) is ext-real V30() V31() Element of REAL

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

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

len Y is ext-real V25() V29() V30() V31() V36() V37() V38() cardinal V63() V64() V65() V66() V67() V68() Element of NAT

Sum Y is ext-real V30() V31() Element of REAL

K255(REAL,Y,K192()) is ext-real V30() V31() Element of REAL

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

V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() RLSStruct

the carrier of V is non empty set

M is V10() V13( the carrier of V) V14( REAL ) Function-like V33( the carrier of V, REAL ) V53() V54() V55() Linear_Combination of V

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

K10( the carrier of V) is non empty set

v is Element of the carrier of V

M . v is ext-real V30() V31() set

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

rng Y is set

len Y is ext-real V25() V29() V30() V31() V36() V37() V38() cardinal V63() V64() V65() V66() V67() V68() Element of NAT

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

Y is set

Y . Y is set

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

len F is ext-real V25() V29() V30() V31() V36() V37() V38() cardinal V63() V64() V65() V66() V67() V68() Element of NAT

Sum F is ext-real V30() V31() Element of REAL

K255(REAL,F,K192()) is ext-real V30() V31() Element of REAL

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

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

len F is ext-real V25() V29() V30() V31() V36() V37() V38() cardinal V63() V64() V65() V66() V67() V68() Element of NAT

Sum F is ext-real V30() V31() Element of REAL

K255(REAL,F,K192()) is ext-real V30() V31() Element of REAL

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

r is ext-real V25() V29() V30() V31() V36() V37() V38() cardinal V63() V64() V65() V66() V67() V68() Element of NAT

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

F . r is ext-real V30() V31() set

V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() RLSStruct

the carrier of V is non empty set

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

M is V10() V13( the carrier of V) V14( REAL ) Function-like V33( the carrier of V, REAL ) V53() V54() V55() Linear_Combination of V

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

K10( the carrier of V) is non empty set

V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() RLSStruct

the carrier of V is non empty set

M is Element of the carrier of V

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

K10( the carrier of V) is non empty set

v is V10() V13( the carrier of V) V14( REAL ) Function-like V33( the carrier of V, REAL ) V53() V54() V55() Linear_Combination of V

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

v . M is ext-real V30() V31() set

Sum v is Element of the carrier of V

(v . M) * M is Element of the carrier of V

Y is V10() V13( the carrier of V) V14( REAL ) Function-like V33( the carrier of V, REAL ) V53() V54() V55() Linear_Combination of {M}

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

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

rng Y is set

len Y is ext-real V25() V29() V30() V31() V36() V37() V38() cardinal V63() V64() V65() V66() V67() V68() Element of NAT

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

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

len r is ext-real V25() V29() V30() V31() V36() V37() V38() cardinal V63() V64() V65() V66() V67() V68() Element of NAT

Sum r is ext-real V30() V31() Element of REAL

K255(REAL,r,K192()) is ext-real V30() V31() Element of REAL

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

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

len r is ext-real V25() V29() V30() V31() V36() V37() V38() cardinal V63() V64() V65() V66() V67() V68() Element of NAT

Sum r is ext-real V30() V31() Element of REAL

K255(REAL,r,K192()) is ext-real V30() V31() Element of REAL

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

r /. 1 is ext-real V30() V31() Element of REAL

card (Carrier Y) is V25() cardinal set

r . 1 is ext-real V30() V31() set

F is ext-real V30() V31() Element of REAL

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

Y . 1 is set

Y . (Y . 1) is ext-real V30() V31() set

V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() RLSStruct

the carrier of V is non empty set

M is Element of the carrier of V

v is Element of the carrier of V

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

K10( the carrier of V) is non empty set

Y is V10() V13( the carrier of V) V14( REAL ) Function-like V33( the carrier of V, REAL ) V53() V54() V55() Linear_Combination of V

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

Y . M is ext-real V30() V31() set

Y . v is ext-real V30() V31() set

(Y . M) + (Y . v) is ext-real V30() V31() set

Sum Y is Element of the carrier of V

(Y . M) * M is Element of the carrier of V

(Y . v) * v is Element of the carrier of V

((Y . M) * M) + ((Y . v) * v) is Element of the carrier of V

Y is V10() V13( the carrier of V) V14( REAL ) Function-like V33( the carrier of V, REAL ) V53() V54() V55() Linear_Combination of {M,v}

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

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

rng r is set

len r is ext-real V25() V29() V30() V31() V36() V37() V38() cardinal V63() V64() V65() V66() V67() V68() Element of NAT

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

len F is ext-real V25() V29() V30() V31() V36() V37() V38() cardinal V63() V64() V65() V66() V67() V68() Element of NAT

Sum F is ext-real V30() V31() Element of REAL

K255(REAL,F,K192()) is ext-real V30() V31() Element of REAL

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

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

len F is ext-real V25() V29() V30() V31() V36() V37() V38() cardinal V63() V64() V65() V66() V67() V68() Element of NAT

Sum F is ext-real V30() V31() Element of REAL

K255(REAL,F,K192()) is ext-real V30() V31() Element of REAL

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

card {M,v} is non empty V25() cardinal set

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

F . 1 is ext-real V30() V31() set

r . 1 is set

Y . (r . 1) is ext-real V30() V31() set

F /. 1 is ext-real V30() V31() Element of REAL

F . 2 is ext-real V30() V31() set

r . 2 is set

Y . (r . 2) is ext-real V30() V31() set

F /. 2 is ext-real V30() V31() Element of REAL

f is ext-real V30() V31() Element of REAL

r1 is ext-real V30() V31() Element of REAL

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

<*M,v*> is non empty V10() V13( NAT ) Function-like V38() 2 -element FinSequence-like FinSubsequence-like set

Y . M is ext-real V30() V31() set

Y . v is ext-real V30() V31() set

(Y . M) + (Y . v) is ext-real V30() V31() set

<*v,M*> is non empty V10() V13( NAT ) Function-like V38() 2 -element FinSequence-like FinSubsequence-like set

Y . M is ext-real V30() V31() set

Y . v is ext-real V30() V31() set

(Y . M) + (Y . v) is ext-real V30() V31() set

<*M,v*> is non empty V10() V13( NAT ) Function-like V38() 2 -element FinSequence-like FinSubsequence-like set

<*v,M*> is non empty V10() V13( NAT ) Function-like V38() 2 -element FinSequence-like FinSubsequence-like set

Y . M is ext-real V30() V31() set

Y . v is