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 * b1) where b1 is Element of the carrier of V : b1 in M } is set
{ H1(b1) where b1 is Element of the carrier of V : S1[b1] } is 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 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 * b1) where b1 is Element of the carrier of V : b1 in M } is set
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
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in M & b2 in v ) } is set
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
{ (b1 - b2) where b1, b2 is Element of the carrier of V : ( b1 in M & b2 in v ) } is set
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 * b1) where b1 is Element of the carrier of V : b1 in M } is set
1 - v is ext-real V30() V31() Element of REAL
(V,M,(1 - v)) is Element of K10( the carrier of V)
{ ((1 - v) * b1) where b1 is Element of the carrier of V : b1 in M } is set
(V,M,v) + (V,M,(1 - v)) is Element of K10( the carrier of V)
Y is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in (V,M,v) & b2 in (V,M,(1 - v)) ) } is set
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 * b1) where b1 is Element of the carrier of V : b1 in M } is set
(V,M,(1 - Y)) is Element of K10( the carrier of V)
{ ((1 - Y) * b1) where b1 is Element of the carrier of V : b1 in M } is set
(V,M,Y) + (V,M,(1 - Y)) is Element of K10( the carrier of V)
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in (V,M,Y) & b2 in (V,M,(1 - Y)) ) } is set
v is ext-real V30() V31() Element of REAL
(V,M,v) is Element of K10( the carrier of V)
{ (v * b1) where b1 is Element of the carrier of V : b1 in M } is set
1 - v is ext-real V30() V31() Element of REAL
(V,M,(1 - v)) is Element of K10( the carrier of V)
{ ((1 - v) * b1) where b1 is Element of the carrier of V : b1 in M } is set
(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 * b1) where b1 is Element of the carrier of V : b1 in M } is set
1 - Y is ext-real V30() V31() Element of REAL
(V,M,(1 - Y)) is Element of K10( the carrier of V)
{ ((1 - Y) * b1) where b1 is Element of the carrier of V : b1 in M } is set
(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) * b1) where b1 is Element of the carrier of V : b1 in M } is set
(V,M,v) is Element of K10( the carrier of V)
{ (v * b1) where b1 is Element of the carrier of V : b1 in M } is set
(V,M,(1 - v)) + (V,M,v) is Element of K10( the carrier of V)
Y is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in (V,M,(1 - v)) & b2 in (V,M,v) ) } is set
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 * b1) where b1 is Element of the carrier of V : b1 in M } is set
1 - Y is ext-real V30() V31() Element of REAL
(V,v,(1 - Y)) is Element of K10( the carrier of V)
{ ((1 - Y) * b1) where b1 is Element of the carrier of V : b1 in v } is set
(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
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in (V,M,Y) & b2 in (V,v,(1 - Y)) ) } is set
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 * b1) where b1 is Element of the carrier of V : b1 in M } is set
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 * b1) where b1 is Element of the carrier of V : b1 in M } is set
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
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in M & b2 in v + Y ) } is set
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
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in v & b2 in Y ) } is set
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
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in M & b2 in v ) } is set
(r + f) + r1 is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in M + v & b2 in Y ) } is set
Y is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in M + v & b2 in Y ) } is set
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
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in M & b2 in v ) } is set
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
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in v & b2 in Y ) } is set
f + (r1 + F) is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in M & b2 in v + Y ) } is 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)
Y is ext-real V30() V31() Element of REAL
(V,M,Y) is Element of K10( the carrier of V)
{ (Y * b1) where b1 is Element of the carrier of V : b1 in M } is set
v is ext-real V30() V31() Element of REAL
(V,(V,M,Y),v) is Element of K10( the carrier of V)
{ (v * b1) where b1 is Element of the carrier of V : b1 in (V,M,Y) } is set
v * Y is ext-real V30() V31() Element of REAL
(V,M,(v * Y)) is Element of K10( the carrier of V)
{ ((v * Y) * b1) where b1 is Element of the carrier of V : b1 in M } is set
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 * b1) where b1 is Element of the carrier of V : b1 in M + v } is set
(V,M,Y) is Element of K10( the carrier of V)
{ (Y * b1) where b1 is Element of the carrier of V : b1 in M } is set
(V,v,Y) is Element of K10( the carrier of V)
{ (Y * b1) where b1 is Element of the carrier of V : b1 in v } is set
(V,M,Y) + (V,v,Y) is Element of K10( the carrier of V)
Y is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in (V,M,Y) & b2 in (V,v,Y) ) } is set
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
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in M & b2 in v ) } is set
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
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in M & b2 in v ) } is set
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
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in (V,M,Y) & b2 in (V,v,Y) ) } is 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
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 + b1) where b1 is Element of the carrier of V : b1 in M } is set
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 + b1) where b1 is Element of the carrier of V : b1 in M } is set
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 * b1) where b1 is Element of the carrier of V : b1 in M } is set
Y is ext-real V30() V31() Element of REAL
(V,v,Y) is Element of K10( the carrier of V)
{ (Y * b1) where b1 is Element of the carrier of V : b1 in v } is set
(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
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in (V,M,Y) & b2 in (V,v,Y) ) } is set
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) * b1) where b1 is Element of the carrier of V : b1 in M } is set
(V,M,v) is Element of K10( the carrier of V)
{ (v * b1) where b1 is Element of the carrier of V : b1 in M } is set
(V,M,Y) is Element of K10( the carrier of V)
{ (Y * b1) where b1 is Element of the carrier of V : b1 in M } is set
(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
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in (V,M,v) & b2 in (V,M,Y) ) } is 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)
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 * b1) where b1 is Element of the carrier of V : b1 in M } is set
(V,v,Y) is Element of K10( the carrier of V)
{ (Y * b1) where b1 is Element of the carrier of V : b1 in v } is set
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 * b1) where b1 is Element of the carrier of V : b1 in M } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in {} & b2 in v ) } is set
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
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in M & b2 in {(0. V)} ) } is set
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
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in M & b2 in {(0. V)} ) } is 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
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 * b1) where b1 is Element of the carrier of V : b1 in M } is set
(V,M,Y) is Element of K10( the carrier of V)
{ (Y * b1) where b1 is Element of the carrier of V : b1 in M } is set
(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) * b1) where b1 is Element of the carrier of V : b1 in M } is 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)
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)) * b1) where b1 is Element of the carrier of V : b1 in M } is set
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))) * b1) where b1 is Element of the carrier of V : b1 in M } is set
(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) * b1) where b1 is Element of the carrier of V : b1 in (V,M,(v / (v + Y))) + (V,M,(1 - (v / (v + Y)))) } is set
(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) * b1) where b1 is Element of the carrier of V : b1 in (V,M,(1 - (v / (v + Y)))) } is set
(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)) * b1) where b1 is Element of the carrier of V : b1 in M } is set
(V,(V,M,(v / (v + Y))),(v + Y)) is Element of K10( the carrier of V)
{ ((v + Y) * b1) where b1 is Element of the carrier of V : b1 in (V,M,(v / (v + Y))) } is set
(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)) * b1) where b1 is Element of the carrier of V : b1 in M } is 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
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 * b1) where b1 is Element of the carrier of V : b1 in M } is set
(V,M,Y) is Element of K10( the carrier of V)
{ (Y * b1) where b1 is Element of the carrier of V : b1 in M } is set
(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) * b1) where b1 is Element of the carrier of V : b1 in M } is set
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 * b1) where b1 is Element of the carrier of V : b1 in M } is set
r is ext-real V30() V31() Element of REAL
(V,v,r) is Element of K10( the carrier of V)
{ (r * b1) where b1 is Element of the carrier of V : b1 in v } is set
(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 * b1) where b1 is Element of the carrier of V : b1 in Y } is set
((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 * b1) where b1 is Element of the carrier of V : b1 in (V,M,Y) + (V,v,r) } is set
(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
{ b1 where b1 is Element of the carrier of V : Y <= b1 .|. v } is set
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
{ b1 where b1 is Element of the carrier of V : not b1 .|. v <= Y } is set
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
{ b1 where b1 is Element of the carrier of V : b1 .|. v <= Y } is set
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
{ b1 where b1 is Element of the carrier of V : not Y <= b1 .|. v } is set
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 ext-real V30() V31() set
(Y . M) + (Y . v) is ext-real V30() V31() 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 is V10() V13( NAT ) Function-like V38() FinSequence-like FinSubsequence-like set
rng V is set
M is set
v is set
Y is set
{M,v,Y} is non empty set
<*M,v,Y*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*M,Y,v*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*v,M,Y*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*v,Y,M*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*Y,M,v*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*Y,v,M*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
len V is ext-real V25() V29() V30() V31() V36() V37() V38() cardinal V63() V64() V65() V66() V67() V68() Element of NAT
dom V is V63() V64() V65() V66() V67() V68() Element of K10(NAT)
{1,2,3} is non empty V63() V64() V65() V66() V67() V68() Element of K10(REAL)
V . 2 is set
V . 3 is set
V . 1 is 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
Y is Element of the carrier of V
{M,v,Y} 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 {M,v,Y}
Sum Y is Element of the carrier of V
Y . M is ext-real V30() V31() set
(Y . M) * M is Element of the carrier of V
Y . v is ext-real V30() V31() set
(Y . v) * v is Element of the carrier of V
((Y . M) * M) + ((Y . v) * v) is Element of the carrier of V
Y . Y is ext-real V30() V31() set
(Y . Y) * Y is Element of the carrier of V
(((Y . M) * M) + ((Y . v) * v)) + ((Y . Y) * Y) is Element of the carrier of V
Carrier Y is Element of K10( the carrier of V)
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
0. V is V82(V) Element of the carrier of V
(0. V) + (0. V) is Element of the carrier of V
((0. V) + (0. V)) + (0. V) is Element of the carrier of V
0 * M is Element of the carrier of V
(0 * M) + (0. V) is Element of the carrier of V
((0 * M) + (0. V)) + (0. V) is Element of the carrier of V
0 * v is Element of the carrier of V
(0 * M) + (0 * v) is Element of the carrier of V
((0 * M) + (0 * v)) + (0. V) is Element of the carrier of V
0 * Y is Element of the carrier of V
((0 * M) + (0 * v)) + (0 * Y) is Element of the carrier of V
((Y . M) * M) + (0 * v) is Element of the carrier of V
(((Y . M) * M) + (0 * v)) + (0 * Y) is Element of the carrier of V
(((Y . M) * M) + ((Y . v) * v)) + (0 * Y) is Element of the carrier of V
{M} is non empty V2() 1 -element Element of K10( the carrier of V)
r 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 r is Element of K10( the carrier of V)
Sum r is Element of the carrier of V
r . M is ext-real V30() V31() set
(r . M) * M is Element of the carrier of V
0. V is V82(V) Element of the carrier of V
((r . M) * M) + (0. V) is Element of the carrier of V
(((r . M) * M) + (0. V)) + (0. V) is Element of the carrier of V
0 * v is Element of the carrier of V
((r . M) * M) + (0 * v) is Element of the carrier of V
(((r . M) * M) + (0 * v)) + (0. V) is Element of the carrier of V
0 * Y is Element of the carrier of V
(((r . M) * M) + (0 * v)) + (0 * Y) is Element of the carrier of V
r . v is ext-real V30() V31() set
(r . v) * v is Element of the carrier of V
((r . M) * M) + ((r . v) * v) is Element of the carrier of V
(((r . M) * M) + ((r . v) * v)) + (0 * Y) is Element of the carrier of V
r . Y is ext-real V30() V31() set
(r . Y) * Y is Element of the carrier of V
(((r . M) * M) + ((r . v) * v)) + ((r . Y) * Y) is Element of the carrier of V
{v} is non empty V2() 1 -element Element of K10( the carrier of V)
r 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 r is Element of K10( the carrier of V)
Sum r is Element of the carrier of V
r . v is ext-real V30() V31() set
(r . v) * v is Element of the carrier of V
0. V is V82(V) Element of the carrier of V
(0. V) + ((r . v) * v) is Element of the carrier of V
((0. V) + ((r . v) * v)) + (0. V) is Element of the carrier of V
0 * M is Element of the carrier of V
(0 * M) + ((r . v) * v) is Element of the carrier of V
((0 * M) + ((r . v) * v)) + (0. V) is Element of the carrier of V
0 * Y is Element of the carrier of V
((0 * M) + ((r . v) * v)) + (0 * Y) is Element of the carrier of V
r . M is ext-real V30() V31() set
(r . M) * M is Element of the carrier of V
((r . M) * M) + ((r . v) * v) is Element of the carrier of V
(((r . M) * M) + ((r . v) * v)) + (0 * Y) is Element of the carrier of V
r . Y is ext-real V30() V31() set
(r . Y) * Y is Element of the carrier of V
(((r . M) * M) + ((r . v) * v)) + ((r . Y) * Y) is Element of the carrier of V
{Y} is non empty V2() 1 -element Element of K10( the carrier of V)
r is V10() V13( the carrier of V) V14( REAL ) Function-like V33( the carrier of V, REAL ) V53() V54() V55() Linear_Combination of {Y}
Carrier r is Element of K10( the carrier of V)
Sum r is Element of the carrier of V
r . Y is ext-real V30() V31() set
(r . Y) * Y is Element of the carrier of V
0. V is V82(V) Element of the carrier of V
(0. V) + ((r . Y) * Y) is Element of the carrier of V
(0. V) + (0. V) is Element of the carrier of V
((0. V) + (0. V)) + ((r . Y) * Y) is Element of the carrier of V
0 * M is Element of the carrier of V
(0 * M) + (0. V) is Element of the carrier of V
((0 * M) + (0. V)) + ((r . Y) * Y) is Element of the carrier of V
0 * v is Element of the carrier of V
(0 * M) + (0 * v) is Element of the carrier of V
((0 * M) + (0 * v)) + ((r . Y) * Y) is Element of the carrier of V
r . M is ext-real V30() V31() set
(r . M) * M is Element of the carrier of V
((r . M) * M) + (0 * v) is Element of the carrier of V
(((r . M) * M) + (0 * v)) + ((r . Y) * Y) is Element of the carrier of V
r . v is ext-real V30() V31() set
(r . v) * v is Element of the carrier of V
((r . M) * M) + ((r . v) * v) is Element of the carrier of V
(((r . M) * M) + ((r . v) * v)) + ((r . Y) * Y) is Element of the carrier of V
{M,v} is non empty Element of K10( the carrier of V)
0. V is V82(V) Element of the carrier of V
(((Y . M) * M) + ((Y . v) * v)) + (0. V) is Element of the carrier of V
0 * Y is Element of the carrier of V
(((Y . M) * M) + ((Y . v) * v)) + (0 * Y) is Element of the carrier of V
{M,Y} is non empty Element of K10( the carrier of V)
((Y . M) * M) + ((Y . Y) * Y) is Element of the carrier of V
0. V is V82(V) Element of the carrier of V
((Y . M) * M) + (0. V) is Element of the carrier of V
(((Y . M) * M) + (0. V)) + ((Y . Y) * Y) is Element of the carrier of V
0 * v is Element of the carrier of V
((Y . M) * M) + (0 * v) is Element of the carrier of V
(((Y . M) * M) + (0 * v)) + ((Y . Y) * Y) is Element of the carrier of V
{v,Y} is non empty Element of K10( the carrier of V)
((Y . v) * v) + ((Y . Y) * Y) is Element of the carrier of V
0. V is V82(V) Element of the carrier of V
(0. V) + ((Y . v) * v) is Element of the carrier of V
((0. V) + ((Y . v) * v)) + ((Y . Y) * Y) is Element of the carrier of V
0 * M is Element of the carrier of V
(0 * M) + ((Y . v) * v) is Element of the carrier of V
((0 * M) + ((Y . v) * v)) + ((Y . Y) * Y) is Element of 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
Y (#) r is V10() V13( NAT ) V14( the carrier of V) Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (Y (#) r) is Element of the carrier of V
<*M,v,Y*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*M,Y,v*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*v,M,Y*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*v,Y,M*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*Y,M,v*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*Y,v,M*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*((Y . M) * M),((Y . v) * v),((Y . Y) * Y)*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*((Y . M) * M),((Y . Y) * Y),((Y . v) * v)*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*((Y . v) * v),((Y . M) * M),((Y . Y) * Y)*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*((Y . v) * v),((Y . Y) * Y),((Y . M) * M)*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*((Y . Y) * Y),((Y . M) * M),((Y . v) * v)*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*((Y . Y) * Y),((Y . v) * v),((Y . M) * M)*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
((Y . v) * v) + ((Y . Y) * Y) is Element of the carrier of V
((Y . M) * M) + (((Y . v) * v) + ((Y . Y) * Y)) is Element of the carrier of V
((Y . M) * M) + ((Y . Y) * Y) is Element of the carrier of V
((Y . v) * v) + (((Y . M) * M) + ((Y . Y) * Y)) is Element of the carrier of V
{M} is non empty V2() 1 -element Element of K10( the carrier of V)
{v} is non empty V2() 1 -element Element of K10( the carrier of V)
{Y} is non empty V2() 1 -element Element of K10( the carrier of V)
{M,v} is non empty Element of K10( the carrier of V)
{M,Y} is non empty Element of K10( the carrier of V)
{v,Y} is non empty Element of K10( 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
M is Element of the carrier of V
v is Element of the carrier of V
Y is Element of the carrier of V
{M,v,Y} 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
Y . Y is ext-real V30() V31() set
((Y . M) + (Y . v)) + (Y . Y) 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 . Y) * Y is Element of the carrier of V
(((Y . M) * M) + ((Y . v) * v)) + ((Y . Y) * Y) is Element of the carrier of V
r 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,Y}
Carrier r is Element of K10( the carrier of V)
F is V10() V13( NAT ) V14( the carrier of V) Function-like V38() FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng F is set
len F 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,Y} is non empty V25() cardinal set
{1,2,3} is non empty V63() V64() V65() V66() V67() V68() Element of K10(REAL)
f . 1 is ext-real V30() V31() set
F . 1 is set
r . (F . 1) is ext-real V30() V31() set
f /. 1 is ext-real V30() V31() Element of REAL
f . 3 is ext-real V30() V31() set
F . 3 is set
r . (F . 3) is ext-real V30() V31() set
f /. 3 is ext-real V30() V31() Element of REAL
f . 2 is ext-real V30() V31() set
F . 2 is set
r . (F . 2) is ext-real V30() V31() set
f /. 2 is ext-real V30() V31() Element of REAL
r1 is ext-real V30() V31() Element of REAL
r2 is ext-real V30() V31() Element of REAL
r3 is ext-real V30() V31() Element of REAL
<*r1,r2,r3*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
(r . (F . 1)) + (r . (F . 2)) is ext-real V30() V31() set
((r . (F . 1)) + (r . (F . 2))) + (r . (F . 3)) is ext-real V30() V31() set
<*M,v,Y*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
r . M is ext-real V30() V31() set
r . v is ext-real V30() V31() set
(r . M) + (r . v) is ext-real V30() V31() set
r . Y is ext-real V30() V31() set
((r . M) + (r . v)) + (r . Y) is ext-real V30() V31() set
<*M,Y,v*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
r . M is ext-real V30() V31() set
r . v is ext-real V30() V31() set
(r . M) + (r . v) is ext-real V30() V31() set
r . Y is ext-real V30() V31() set
((r . M) + (r . v)) + (r . Y) is ext-real V30() V31() set
<*v,M,Y*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
r . M is ext-real V30() V31() set
r . v is ext-real V30() V31() set
(r . M) + (r . v) is ext-real V30() V31() set
r . Y is ext-real V30() V31() set
((r . M) + (r . v)) + (r . Y) is ext-real V30() V31() set
<*v,Y,M*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
r . M is ext-real V30() V31() set
r . v is ext-real V30() V31() set
(r . M) + (r . v) is ext-real V30() V31() set
r . Y is ext-real V30() V31() set
((r . M) + (r . v)) + (r . Y) is ext-real V30() V31() set
<*Y,M,v*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
r . M is ext-real V30() V31() set
r . v is ext-real V30() V31() set
(r . M) + (r . v) is ext-real V30() V31() set
r . Y is ext-real V30() V31() set
((r . M) + (r . v)) + (r . Y) is ext-real V30() V31() set
<*Y,v,M*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
r . M is ext-real V30() V31() set
r . v is ext-real V30() V31() set
(r . M) + (r . v) is ext-real V30() V31() set
r . Y is ext-real V30() V31() set
((r . M) + (r . v)) + (r . Y) is ext-real V30() V31() set
<*M,v,Y*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*M,Y,v*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*v,M,Y*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*v,Y,M*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*Y,M,v*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*Y,v,M*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
r . M is ext-real V30() V31() set
r . v is ext-real V30() V31() set
(r . M) + (r . v) is ext-real V30() V31() set
r . Y is ext-real V30() V31() set
((r . M) + (r . v)) + (r . Y) is ext-real V30() V31() set
r . M is ext-real V30() V31() set
r . v is ext-real V30() V31() set
(r . M) + (r . v) is ext-real V30() V31() set
r . Y is ext-real V30() V31() set
((r . M) + (r . v)) + (r . Y) 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
{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 {M}
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
Carrier v is Element of K10( 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
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 {M,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
Carrier Y is Element of K10( the carrier of V)
{M} is non empty V2() 1 -element Element of K10( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not Y . b1 = 0 } is set
{v} is non empty V2() 1 -element Element of K10( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not Y . b1 = 0 } is set
{M} is non empty V2() 1 -element Element of K10( the carrier of V)
{v} is non empty V2() 1 -element Element of K10( 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
M is Element of the carrier of V
v is Element of the carrier of V
Y is Element of the carrier of V
{M,v,Y} 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 {M,v,Y}
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
Y . Y is ext-real V30() V31() set
((Y . M) + (Y . v)) + (Y . Y) 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 . Y) * Y is Element of the carrier of V
(((Y . M) * M) + ((Y . v) * v)) + ((Y . Y) * Y) is Element of the carrier of V
Carrier Y is Element of K10( the carrier of V)
{M} is non empty V2() 1 -element Element of K10( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not Y . b1 = 0 } is set
{v} is non empty V2() 1 -element Element of K10( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not Y . b1 = 0 } is set
{Y} is non empty V2() 1 -element Element of K10( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not Y . b1 = 0 } is set
{M,v} is non empty Element of K10( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not Y . b1 = 0 } is set
{v,Y} is non empty Element of K10( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not Y . b1 = 0 } is set
{M,Y} is non empty Element of K10( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not Y . b1 = 0 } is set
{M} is non empty V2() 1 -element Element of K10( the carrier of V)
{v} is non empty V2() 1 -element Element of K10( the carrier of V)
{Y} is non empty V2() 1 -element Element of K10( the carrier of V)
{M,v} is non empty Element of K10( the carrier of V)
{v,Y} is non empty Element of K10( the carrier of V)
{M,Y} is non empty Element of K10( 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
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)
K10( 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)
v . M 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
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)
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
{M,v} is non empty 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
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
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)
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 Element of the carrier of V
{M,v,Y} is non empty 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
Y . Y is ext-real V30() V31() set
((Y . M) + (Y . v)) + (Y . Y) 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 . Y) * Y is Element of the carrier of V
(((Y . M) * M) + ((Y . v) * v)) + ((Y . Y) * Y) is Element of the carrier of V
V is non empty RLSStruct
the carrier of V is non empty set
K10( the carrier of V) is non empty set
K10(K10( the carrier of V)) is non empty set
M is Element of K10( the carrier of V)
v is Element of K10(K10( the carrier of V))
Y is Element of K10(K10( the carrier of V))
Y 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,M) is Element of K10(K10( the carrier of V))
K10(K10( the carrier of V)) is non empty set
meet (V,M) is Element of K10( the carrier of V)
v 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,M) is (V) Element of K10( the carrier of V)
(V,M) is Element of K10(K10( the carrier of V))
K10(K10( the carrier of V)) is non empty set
meet (V,M) is Element of K10( the carrier of V)
v is (V) Element of K10( the carrier of V)
V is V10() V13( NAT ) Function-like V38() FinSequence-like FinSubsequence-like set
rng V is set
M is set
v is set
Y is set
{M,v,Y} is non empty set
<*M,v,Y*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*M,Y,v*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*v,M,Y*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*v,Y,M*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*Y,M,v*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like set
<*Y,v,M*> is non empty V10() V13( NAT ) Function-like V38() 3 -element FinSequence-like FinSubsequence-like 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,M,1) is Element of K10( the carrier of V)
{ (1 * b1) where b1 is Element of the carrier of V : b1 in M } is 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 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 * b1) where b1 is Element of the carrier of V : b1 in M } is 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
K10( the carrier of V) is non empty set
M is non empty Element of K10( the carrier of V)
(V,M,0) is Element of K10( the carrier of V)
{ (0 * b1) where b1 is Element of the carrier of V : b1 in M } is set
0. V is V82(V) Element of the carrier of V
{(0. V)} is non empty V2() 1 -element Element of K10( the carrier of V)
V is non empty right_zeroed 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)
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 + {(0. V)} is Element of K10( 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)
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 * b1) where b1 is Element of the carrier of V : b1 in M } is set
v is ext-real V30() V31() Element of REAL
(V,(V,M,Y),v) is Element of K10( the carrier of V)
{ (v * b1) where b1 is Element of the carrier of V : b1 in (V,M,Y) } is set
v * Y is ext-real V30() V31() Element of REAL
(V,M,(v * Y)) is Element of K10( the carrier of V)
{ ((v * Y) * b1) where b1 is Element of the carrier of V : b1 in M } is 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 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 * b1) where b1 is Element of the carrier of V : b1 in M + v } is set
(V,M,Y) is Element of K10( the carrier of V)
{ (Y * b1) where b1 is Element of the carrier of V : b1 in M } is set
(V,v,Y) is Element of K10( the carrier of V)
{ (Y * b1) where b1 is Element of the carrier of V : b1 in v } is set
(V,M,Y) + (V,v,Y) 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 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 * b1) where b1 is Element of the carrier of V : b1 in M } is set
(V,v,Y) is Element of K10( the carrier of V)
{ (Y * b1) where b1 is Element of the carrier of V : b1 in v } is set
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)
V is non empty RLSStruct
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is (V) Element of K10( the carrier of V)
v is (V) Element of K10( the carrier of V)
M /\ v is Element of K10( the carrier of V)
r is ext-real V30() V31() Element of REAL
Y is Element of the carrier of V
Y is Element of the carrier of V
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
Y is Element of K10( 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,M) is Element of K10(K10( the carrier of V))
K10(K10( the carrier of V)) is non empty set
(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)
v is set
Y 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
the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty set
the carrier of ((Omega). 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
K10( the carrier of V) is non empty set
M is Element of K10( the carrier of V)
(V,M) is (V) Element of K10( the carrier of V)
(V,M) is non empty Element of K10(K10( the carrier of V))
K10(K10( the carrier of V)) is non empty set
meet (V,M) is Element of K10( the carrier of V)
v is set
Y is set
Y is Element of K10( the carrier of V)