REAL is non empty non trivial non finite V63() V64() V65() V69() set
NAT is non trivial ordinal non finite cardinal limit_cardinal V63() V64() V65() V66() V67() V68() V69() Element of bool REAL
bool REAL is non empty non trivial non finite set
ExtREAL is non empty V64() set
[:NAT,ExtREAL:] is non trivial non finite V54() set
bool [:NAT,ExtREAL:] is non empty non trivial non finite set
bool ExtREAL is non empty set
omega is non trivial ordinal non finite cardinal limit_cardinal V63() V64() V65() V66() V67() V68() V69() set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
K189(NAT) is V47() set
COMPLEX is non empty non trivial non finite V63() V69() set
RAT is non empty non trivial non finite V63() V64() V65() V66() V69() set
INT is non empty non trivial non finite V63() V64() V65() V66() V67() V69() set
[:REAL,REAL:] is non empty non trivial non finite V53() V54() V55() set
bool [:REAL,REAL:] is non empty non trivial non finite set
{} is functional empty ordinal natural V31() real finite V37() cardinal {} -element FinSequence-membered ext-real non positive non negative V63() V64() V65() V66() V67() V68() V69() set
1 is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
{{},1} is non empty finite V37() V63() V64() V65() V66() V67() V68() set
2 is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
[:COMPLEX,COMPLEX:] is non empty non trivial non finite V53() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite V53() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is non empty non trivial non finite V53() V54() V55() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is V5( RAT ) non empty non trivial non finite V53() V54() V55() set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is V5( RAT ) non empty non trivial non finite V53() V54() V55() set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is V5( RAT ) V5( INT ) non empty non trivial non finite V53() V54() V55() set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is V5( RAT ) V5( INT ) non empty non trivial non finite V53() V54() V55() set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is V5( RAT ) V5( INT ) V53() V54() V55() V56() set
[:[:NAT,NAT:],NAT:] is V5( RAT ) V5( INT ) V53() V54() V55() V56() set
bool [:[:NAT,NAT:],NAT:] is non empty set
3 is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
0 is functional empty ordinal natural V31() real finite V37() cardinal {} -element FinSequence-membered ext-real non positive non negative V51() V52() V63() V64() V65() V66() V67() V68() V69() Element of NAT
0. is functional empty ordinal natural V31() real finite V37() cardinal {} -element FinSequence-membered ext-real non positive non negative V63() V64() V65() V66() V67() V68() V69() Element of ExtREAL
<*> ExtREAL is V1() V4( NAT ) V5( ExtREAL ) Function-like functional empty ordinal natural V31() real finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() FinSequence of ExtREAL
Sum (<*> ExtREAL) is ext-real Element of ExtREAL
-infty is non empty non real ext-real non positive negative Element of ExtREAL
<*> REAL is V1() V4( NAT ) V5( REAL ) Function-like functional empty ordinal natural V31() real finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() FinSequence of REAL
Sum (<*> REAL) is V31() real ext-real Element of REAL
addreal is V1() V4([:REAL,REAL:]) V5( REAL ) Function-like non empty total quasi_total V53() V54() V55() Element of bool [:[:REAL,REAL:],REAL:]
K190(REAL,(<*> REAL),addreal) is V31() real ext-real Element of REAL
Seg 1 is non empty trivial finite 1 -element V63() V64() V65() V66() V67() V68() Element of bool NAT
{1} is non empty trivial finite V37() 1 -element V63() V64() V65() V66() V67() V68() set
Seg 2 is non empty finite 2 -element V63() V64() V65() V66() V67() V68() Element of bool NAT
{1,2} is non empty finite V37() V63() V64() V65() V66() V67() V68() set
multreal is V1() V4([:REAL,REAL:]) V5( REAL ) Function-like non empty total quasi_total V53() V54() V55() Element of bool [:[:REAL,REAL:],REAL:]
+infty is non empty non real ext-real positive non negative set
-infty is non empty non real ext-real non positive negative set
X is non empty RLSStruct
the carrier of X is non empty set
f is non empty RLSStruct
the carrier of f is non empty set
[: the carrier of X, the carrier of f:] is non empty set
[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:] is non empty set
[:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
[: the carrier of X, the carrier of X:] is non empty set
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
[: the carrier of f, the carrier of f:] is non empty set
the addF of f is V1() V4([: the carrier of f, the carrier of f:]) V5( the carrier of f) Function-like non empty total quasi_total Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
p is Element of [: the carrier of X, the carrier of f:]
F is Element of [: the carrier of X, the carrier of f:]
y is set
z is set
[y,z] is set
s is set
k is set
[s,k] is set
z9 is Element of the carrier of X
p9 is Element of the carrier of X
[z9,p9] is Element of [: the carrier of X, the carrier of X:]
the addF of X . [z9,p9] is Element of the carrier of X
s1 is Element of the carrier of f
F9 is Element of the carrier of f
[s1,F9] is Element of [: the carrier of f, the carrier of f:]
the addF of f . [s1,F9] is Element of the carrier of f
[( the addF of X . [z9,p9]),( the addF of f . [s1,F9])] is Element of [: the carrier of X, the carrier of f:]
k9 is Element of [: the carrier of X, the carrier of f:]
k9 is Element of the carrier of X
y9 is Element of the carrier of X
[k9,y9] is Element of [: the carrier of X, the carrier of X:]
the addF of X . [k9,y9] is Element of the carrier of X
k9 is Element of the carrier of f
[k9,k9] is Element of [: the carrier of X, the carrier of f:]
i is Element of the carrier of f
[y9,i] is Element of [: the carrier of X, the carrier of f:]
[k9,i] is Element of [: the carrier of f, the carrier of f:]
the addF of f . [k9,i] is Element of the carrier of f
[( the addF of X . [k9,y9]),( the addF of f . [k9,i])] is Element of [: the carrier of X, the carrier of f:]
n is V1() V4([:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
p is V1() V4([:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
F is Element of [: the carrier of X, the carrier of f:]
y is Element of [: the carrier of X, the carrier of f:]
n . (F,y) is Element of [: the carrier of X, the carrier of f:]
[F,y] is set
n . [F,y] is set
p . (F,y) is Element of [: the carrier of X, the carrier of f:]
p . [F,y] is set
z is set
s is set
[z,s] is set
k is set
s1 is set
[k,s1] is set
p9 is Element of the carrier of X
k9 is Element of the carrier of X
[p9,k9] is Element of [: the carrier of X, the carrier of X:]
the addF of X . [p9,k9] is Element of the carrier of X
F9 is Element of the carrier of f
z9 is Element of the carrier of f
[F9,z9] is Element of [: the carrier of f, the carrier of f:]
the addF of f . [F9,z9] is Element of the carrier of f
[( the addF of X . [p9,k9]),( the addF of f . [F9,z9])] is Element of [: the carrier of X, the carrier of f:]
X is non empty RLSStruct
the carrier of X is non empty set
f is non empty RLSStruct
the carrier of f is non empty set
[: the carrier of X, the carrier of f:] is non empty set
[:REAL,[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
[:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
[:REAL, the carrier of X:] is non empty non trivial non finite set
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
[:REAL, the carrier of f:] is non empty non trivial non finite set
the Mult of f is V1() V4([:REAL, the carrier of f:]) V5( the carrier of f) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of f:], the carrier of f:]
[:[:REAL, the carrier of f:], the carrier of f:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of f:], the carrier of f:] is non empty non trivial non finite set
n is V31() real ext-real Element of REAL
p is Element of [: the carrier of X, the carrier of f:]
F is set
y is set
[F,y] is set
s is Element of the carrier of X
[n,s] is Element of [:REAL, the carrier of X:]
the Mult of X . [n,s] is Element of the carrier of X
z is Element of the carrier of f
[n,z] is Element of [:REAL, the carrier of f:]
the Mult of f . [n,z] is Element of the carrier of f
[( the Mult of X . [n,s]),( the Mult of f . [n,z])] is Element of [: the carrier of X, the carrier of f:]
k is Element of [: the carrier of X, the carrier of f:]
s1 is Element of the carrier of X
[n,s1] is Element of [:REAL, the carrier of X:]
the Mult of X . [n,s1] is Element of the carrier of X
F9 is Element of the carrier of f
[s1,F9] is Element of [: the carrier of X, the carrier of f:]
[n,F9] is Element of [:REAL, the carrier of f:]
the Mult of f . [n,F9] is Element of the carrier of f
[( the Mult of X . [n,s1]),( the Mult of f . [n,F9])] is Element of [: the carrier of X, the carrier of f:]
s1 is Element of the carrier of X
F9 is Element of the carrier of f
[s1,F9] is Element of [: the carrier of X, the carrier of f:]
[n,s1] is set
the Mult of X . [n,s1] is set
[n,F9] is set
the Mult of f . [n,F9] is set
[( the Mult of X . [n,s1]),( the Mult of f . [n,F9])] is set
n is V1() V4([:REAL,[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
p is V31() real ext-real Element of REAL
F is Element of [: the carrier of X, the carrier of f:]
n . (p,F) is Element of [: the carrier of X, the carrier of f:]
[p,F] is set
n . [p,F] is set
y is Element of the carrier of X
z is Element of the carrier of f
[y,z] is Element of [: the carrier of X, the carrier of f:]
[p,y] is Element of [:REAL, the carrier of X:]
the Mult of X . [p,y] is Element of the carrier of X
[p,z] is Element of [:REAL, the carrier of f:]
the Mult of f . [p,z] is Element of the carrier of f
[( the Mult of X . [p,y]),( the Mult of f . [p,z])] is Element of [: the carrier of X, the carrier of f:]
n is V1() V4([:REAL,[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
p is V1() V4([:REAL,[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
F is V31() real ext-real Element of REAL
y is Element of [: the carrier of X, the carrier of f:]
n . (F,y) is Element of [: the carrier of X, the carrier of f:]
[F,y] is set
n . [F,y] is set
p . (F,y) is Element of [: the carrier of X, the carrier of f:]
p . [F,y] is set
z is set
s is set
[z,s] is set
s1 is Element of the carrier of X
[F,s1] is Element of [:REAL, the carrier of X:]
the Mult of X . [F,s1] is Element of the carrier of X
k is Element of the carrier of f
[F,k] is Element of [:REAL, the carrier of f:]
the Mult of f . [F,k] is Element of the carrier of f
[( the Mult of X . [F,s1]),( the Mult of f . [F,k])] is Element of [: the carrier of X, the carrier of f:]
X is non empty RLSStruct
the carrier of X is non empty set
f is non empty RLSStruct
the carrier of f is non empty set
[: the carrier of X, the carrier of f:] is non empty set
0. X is V113(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
0. f is V113(f) Element of the carrier of f
the ZeroF of f is Element of the carrier of f
[(0. X),(0. f)] is Element of [: the carrier of X, the carrier of f:]
(X,f) is V1() V4([:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:] is non empty set
[:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
(X,f) is V1() V4([:REAL,[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:REAL,[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
[:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
RLSStruct(# [: the carrier of X, the carrier of f:],[(0. X),(0. f)],(X,f),(X,f) #) is non empty strict RLSStruct
X is non empty RLSStruct
f is non empty RLSStruct
(X,f) is RLSStruct
the carrier of X is non empty set
the carrier of f is non empty set
[: the carrier of X, the carrier of f:] is non empty set
0. X is V113(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
0. f is V113(f) Element of the carrier of f
the ZeroF of f is Element of the carrier of f
[(0. X),(0. f)] is Element of [: the carrier of X, the carrier of f:]
(X,f) is V1() V4([:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:] is non empty set
[:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
(X,f) is V1() V4([:REAL,[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:REAL,[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
[:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
RLSStruct(# [: the carrier of X, the carrier of f:],[(0. X),(0. f)],(X,f),(X,f) #) is non empty strict RLSStruct
X is non empty RLSStruct
the carrier of X is non empty set
f is non empty RLSStruct
the carrier of f is non empty set
(X,f) is non empty RLSStruct
[: the carrier of X, the carrier of f:] is non empty set
0. X is V113(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
0. f is V113(f) Element of the carrier of f
the ZeroF of f is Element of the carrier of f
[(0. X),(0. f)] is Element of [: the carrier of X, the carrier of f:]
(X,f) is V1() V4([:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:] is non empty set
[:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
(X,f) is V1() V4([:REAL,[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:REAL,[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
[:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
RLSStruct(# [: the carrier of X, the carrier of f:],[(0. X),(0. f)],(X,f),(X,f) #) is non empty strict RLSStruct
the carrier of (X,f) is non empty set
F is Element of the carrier of (X,f)
n is Element of the carrier of X
p is Element of the carrier of f
[n,p] is Element of [: the carrier of X, the carrier of f:]
y is V31() real ext-real Element of REAL
y * F is Element of the carrier of (X,f)
the Mult of (X,f) is V1() V4([:REAL, the carrier of (X,f):]) V5( the carrier of (X,f)) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of (X,f):], the carrier of (X,f):]
[:REAL, the carrier of (X,f):] is non empty non trivial non finite set
[:[:REAL, the carrier of (X,f):], the carrier of (X,f):] is non empty non trivial non finite set
bool [:[:REAL, the carrier of (X,f):], the carrier of (X,f):] is non empty non trivial non finite set
the Mult of (X,f) . (y,F) is set
[y,F] is set
the Mult of (X,f) . [y,F] is set
y * n is Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . (y,n) is set
[y,n] is set
the Mult of X . [y,n] is set
y * p is Element of the carrier of f
the Mult of f is V1() V4([:REAL, the carrier of f:]) V5( the carrier of f) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of f:], the carrier of f:]
[:REAL, the carrier of f:] is non empty non trivial non finite set
[:[:REAL, the carrier of f:], the carrier of f:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of f:], the carrier of f:] is non empty non trivial non finite set
the Mult of f . (y,p) is set
[y,p] is set
the Mult of f . [y,p] is set
[(y * n),(y * p)] is Element of [: the carrier of X, the carrier of f:]
X is non empty RLSStruct
the carrier of X is non empty set
f is non empty RLSStruct
the carrier of f is non empty set
(X,f) is non empty RLSStruct
[: the carrier of X, the carrier of f:] is non empty set
0. X is V113(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
0. f is V113(f) Element of the carrier of f
the ZeroF of f is Element of the carrier of f
[(0. X),(0. f)] is Element of [: the carrier of X, the carrier of f:]
(X,f) is V1() V4([:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:] is non empty set
[:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
(X,f) is V1() V4([:REAL,[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:REAL,[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
[:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
RLSStruct(# [: the carrier of X, the carrier of f:],[(0. X),(0. f)],(X,f),(X,f) #) is non empty strict RLSStruct
the carrier of (X,f) is non empty set
z is Element of the carrier of (X,f)
n is Element of the carrier of X
F is Element of the carrier of f
[n,F] is Element of [: the carrier of X, the carrier of f:]
s is Element of the carrier of (X,f)
p is Element of the carrier of X
y is Element of the carrier of f
[p,y] is Element of [: the carrier of X, the carrier of f:]
z + s is Element of the carrier of (X,f)
the addF of (X,f) is V1() V4([: the carrier of (X,f), the carrier of (X,f):]) V5( the carrier of (X,f)) Function-like non empty total quasi_total Element of bool [:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):]
[: the carrier of (X,f), the carrier of (X,f):] is non empty set
[:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):] is non empty set
bool [:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):] is non empty set
the addF of (X,f) . (z,s) is Element of the carrier of (X,f)
[z,s] is set
the addF of (X,f) . [z,s] is set
n + p is Element of the carrier of X
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . (n,p) is Element of the carrier of X
[n,p] is set
the addF of X . [n,p] is set
F + y is Element of the carrier of f
the addF of f is V1() V4([: the carrier of f, the carrier of f:]) V5( the carrier of f) Function-like non empty total quasi_total Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the addF of f . (F,y) is Element of the carrier of f
[F,y] is set
the addF of f . [F,y] is set
[(n + p),(F + y)] is Element of [: the carrier of X, the carrier of f:]
X is non empty Abelian RLSStruct
f is non empty Abelian RLSStruct
(X,f) is non empty RLSStruct
the carrier of X is non empty set
the carrier of f is non empty set
[: the carrier of X, the carrier of f:] is non empty set
0. X is V113(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
0. f is V113(f) Element of the carrier of f
the ZeroF of f is Element of the carrier of f
[(0. X),(0. f)] is Element of [: the carrier of X, the carrier of f:]
(X,f) is V1() V4([:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:] is non empty set
[:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
(X,f) is V1() V4([:REAL,[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:REAL,[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
[:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
RLSStruct(# [: the carrier of X, the carrier of f:],[(0. X),(0. f)],(X,f),(X,f) #) is non empty strict RLSStruct
the carrier of (X,f) is non empty set
n is Element of the carrier of (X,f)
p is Element of the carrier of (X,f)
n + p is Element of the carrier of (X,f)
the addF of (X,f) is V1() V4([: the carrier of (X,f), the carrier of (X,f):]) V5( the carrier of (X,f)) Function-like non empty total quasi_total Element of bool [:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):]
[: the carrier of (X,f), the carrier of (X,f):] is non empty set
[:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):] is non empty set
bool [:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):] is non empty set
the addF of (X,f) . (n,p) is Element of the carrier of (X,f)
[n,p] is set
the addF of (X,f) . [n,p] is set
p + n is Element of the carrier of (X,f)
the addF of (X,f) . (p,n) is Element of the carrier of (X,f)
[p,n] is set
the addF of (X,f) . [p,n] is set
F is set
y is set
[F,y] is set
k is set
s1 is set
[k,s1] is set
z9 is Element of the carrier of X
s is Element of the carrier of X
z9 + s is Element of the carrier of X
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . (z9,s) is Element of the carrier of X
[z9,s] is set
the addF of X . [z9,s] is set
F9 is Element of the carrier of f
z is Element of the carrier of f
F9 + z is Element of the carrier of f
the addF of f is V1() V4([: the carrier of f, the carrier of f:]) V5( the carrier of f) Function-like non empty total quasi_total Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the addF of f . (F9,z) is Element of the carrier of f
[F9,z] is set
the addF of f . [F9,z] is set
[(z9 + s),(F9 + z)] is Element of [: the carrier of X, the carrier of f:]
X is non empty add-associative RLSStruct
f is non empty add-associative RLSStruct
(X,f) is non empty RLSStruct
the carrier of X is non empty set
the carrier of f is non empty set
[: the carrier of X, the carrier of f:] is non empty set
0. X is V113(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
0. f is V113(f) Element of the carrier of f
the ZeroF of f is Element of the carrier of f
[(0. X),(0. f)] is Element of [: the carrier of X, the carrier of f:]
(X,f) is V1() V4([:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:] is non empty set
[:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
(X,f) is V1() V4([:REAL,[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:REAL,[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
[:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
RLSStruct(# [: the carrier of X, the carrier of f:],[(0. X),(0. f)],(X,f),(X,f) #) is non empty strict RLSStruct
the carrier of (X,f) is non empty set
n is Element of the carrier of (X,f)
p is Element of the carrier of (X,f)
n + p is Element of the carrier of (X,f)
the addF of (X,f) is V1() V4([: the carrier of (X,f), the carrier of (X,f):]) V5( the carrier of (X,f)) Function-like non empty total quasi_total Element of bool [:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):]
[: the carrier of (X,f), the carrier of (X,f):] is non empty set
[:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):] is non empty set
bool [:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):] is non empty set
the addF of (X,f) . (n,p) is Element of the carrier of (X,f)
[n,p] is set
the addF of (X,f) . [n,p] is set
F is Element of the carrier of (X,f)
(n + p) + F is Element of the carrier of (X,f)
the addF of (X,f) . ((n + p),F) is Element of the carrier of (X,f)
[(n + p),F] is set
the addF of (X,f) . [(n + p),F] is set
p + F is Element of the carrier of (X,f)
the addF of (X,f) . (p,F) is Element of the carrier of (X,f)
[p,F] is set
the addF of (X,f) . [p,F] is set
n + (p + F) is Element of the carrier of (X,f)
the addF of (X,f) . (n,(p + F)) is Element of the carrier of (X,f)
[n,(p + F)] is set
the addF of (X,f) . [n,(p + F)] is set
y is set
z is set
[y,z] is set
k is set
s1 is set
[k,s1] is set
k9 is set
k9 is set
[k9,k9] is set
p9 is Element of the carrier of X
k9 is Element of the carrier of X
p9 + k9 is Element of the carrier of X
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . (p9,k9) is Element of the carrier of X
[p9,k9] is set
the addF of X . [p9,k9] is set
s is Element of the carrier of f
y9 is Element of the carrier of f
s + y9 is Element of the carrier of f
the addF of f is V1() V4([: the carrier of f, the carrier of f:]) V5( the carrier of f) Function-like non empty total quasi_total Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the addF of f . (s,y9) is Element of the carrier of f
[s,y9] is set
the addF of f . [s,y9] is set
[(p9 + k9),(s + y9)] is Element of [: the carrier of X, the carrier of f:]
z9 is Element of the carrier of X
(p9 + k9) + z9 is Element of the carrier of X
the addF of X . ((p9 + k9),z9) is Element of the carrier of X
[(p9 + k9),z9] is set
the addF of X . [(p9 + k9),z9] is set
F9 is Element of the carrier of f
(s + y9) + F9 is Element of the carrier of f
the addF of f . ((s + y9),F9) is Element of the carrier of f
[(s + y9),F9] is set
the addF of f . [(s + y9),F9] is set
[((p9 + k9) + z9),((s + y9) + F9)] is Element of [: the carrier of X, the carrier of f:]
k9 + z9 is Element of the carrier of X
the addF of X . (k9,z9) is Element of the carrier of X
[k9,z9] is set
the addF of X . [k9,z9] is set
y9 + F9 is Element of the carrier of f
the addF of f . (y9,F9) is Element of the carrier of f
[y9,F9] is set
the addF of f . [y9,F9] is set
[(k9 + z9),(y9 + F9)] is Element of [: the carrier of X, the carrier of f:]
p9 + (k9 + z9) is Element of the carrier of X
the addF of X . (p9,(k9 + z9)) is Element of the carrier of X
[p9,(k9 + z9)] is set
the addF of X . [p9,(k9 + z9)] is set
s + (y9 + F9) is Element of the carrier of f
the addF of f . (s,(y9 + F9)) is Element of the carrier of f
[s,(y9 + F9)] is set
the addF of f . [s,(y9 + F9)] is set
[(p9 + (k9 + z9)),(s + (y9 + F9))] is Element of [: the carrier of X, the carrier of f:]
X is non empty right_zeroed RLSStruct
f is non empty right_zeroed RLSStruct
(X,f) is non empty RLSStruct
the carrier of X is non empty set
the carrier of f is non empty set
[: the carrier of X, the carrier of f:] is non empty set
0. X is V113(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
0. f is V113(f) Element of the carrier of f
the ZeroF of f is Element of the carrier of f
[(0. X),(0. f)] is Element of [: the carrier of X, the carrier of f:]
(X,f) is V1() V4([:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:] is non empty set
[:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
(X,f) is V1() V4([:REAL,[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:REAL,[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
[:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
RLSStruct(# [: the carrier of X, the carrier of f:],[(0. X),(0. f)],(X,f),(X,f) #) is non empty strict RLSStruct
the carrier of (X,f) is non empty set
0. (X,f) is V113((X,f)) Element of the carrier of (X,f)
the ZeroF of (X,f) is Element of the carrier of (X,f)
n is Element of the carrier of (X,f)
n + (0. (X,f)) is Element of the carrier of (X,f)
the addF of (X,f) is V1() V4([: the carrier of (X,f), the carrier of (X,f):]) V5( the carrier of (X,f)) Function-like non empty total quasi_total Element of bool [:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):]
[: the carrier of (X,f), the carrier of (X,f):] is non empty set
[:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):] is non empty set
bool [:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):] is non empty set
the addF of (X,f) . (n,(0. (X,f))) is Element of the carrier of (X,f)
[n,(0. (X,f))] is set
the addF of (X,f) . [n,(0. (X,f))] is set
p is set
F is set
[p,F] is set
y is Element of the carrier of f
y + (0. f) is Element of the carrier of f
the addF of f is V1() V4([: the carrier of f, the carrier of f:]) V5( the carrier of f) Function-like non empty total quasi_total Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the addF of f . (y,(0. f)) is Element of the carrier of f
[y,(0. f)] is set
the addF of f . [y,(0. f)] is set
z is Element of the carrier of X
z + (0. X) is Element of the carrier of X
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . (z,(0. X)) is Element of the carrier of X
[z,(0. X)] is set
the addF of X . [z,(0. X)] is set
X is non empty right_complementable RLSStruct
f is non empty right_complementable RLSStruct
(X,f) is non empty RLSStruct
the carrier of X is non empty set
the carrier of f is non empty set
[: the carrier of X, the carrier of f:] is non empty set
0. X is V113(X) right_complementable Element of the carrier of X
the ZeroF of X is right_complementable Element of the carrier of X
0. f is V113(f) right_complementable Element of the carrier of f
the ZeroF of f is right_complementable Element of the carrier of f
[(0. X),(0. f)] is Element of [: the carrier of X, the carrier of f:]
(X,f) is V1() V4([:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:] is non empty set
[:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
(X,f) is V1() V4([:REAL,[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:REAL,[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
[:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
RLSStruct(# [: the carrier of X, the carrier of f:],[(0. X),(0. f)],(X,f),(X,f) #) is non empty strict RLSStruct
the carrier of (X,f) is non empty set
n is Element of the carrier of (X,f)
p is set
F is set
[p,F] is set
y is right_complementable Element of the carrier of X
z is right_complementable Element of the carrier of X
y + z is right_complementable Element of the carrier of X
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . (y,z) is right_complementable Element of the carrier of X
[y,z] is set
the addF of X . [y,z] is set
s is right_complementable Element of the carrier of f
k is right_complementable Element of the carrier of f
s + k is right_complementable Element of the carrier of f
the addF of f is V1() V4([: the carrier of f, the carrier of f:]) V5( the carrier of f) Function-like non empty total quasi_total Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the addF of f . (s,k) is right_complementable Element of the carrier of f
[s,k] is set
the addF of f . [s,k] is set
[z,k] is Element of [: the carrier of X, the carrier of f:]
F9 is Element of the carrier of (X,f)
n + F9 is Element of the carrier of (X,f)
the addF of (X,f) is V1() V4([: the carrier of (X,f), the carrier of (X,f):]) V5( the carrier of (X,f)) Function-like non empty total quasi_total Element of bool [:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):]
[: the carrier of (X,f), the carrier of (X,f):] is non empty set
[:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):] is non empty set
bool [:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):] is non empty set
the addF of (X,f) . (n,F9) is Element of the carrier of (X,f)
[n,F9] is set
the addF of (X,f) . [n,F9] is set
0. (X,f) is V113((X,f)) Element of the carrier of (X,f)
the ZeroF of (X,f) is Element of the carrier of (X,f)
X is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
f is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
(X,f) is non empty RLSStruct
the carrier of X is non empty set
the carrier of f is non empty set
[: the carrier of X, the carrier of f:] is non empty set
0. X is V113(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
0. f is V113(f) Element of the carrier of f
the ZeroF of f is Element of the carrier of f
[(0. X),(0. f)] is Element of [: the carrier of X, the carrier of f:]
(X,f) is V1() V4([:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:] is non empty set
[:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
(X,f) is V1() V4([:REAL,[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:REAL,[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
[:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
RLSStruct(# [: the carrier of X, the carrier of f:],[(0. X),(0. f)],(X,f),(X,f) #) is non empty strict RLSStruct
the carrier of (X,f) is non empty set
n is V31() real ext-real set
F is Element of the carrier of (X,f)
y is Element of the carrier of (X,f)
F + y is Element of the carrier of (X,f)
the addF of (X,f) is V1() V4([: the carrier of (X,f), the carrier of (X,f):]) V5( the carrier of (X,f)) Function-like non empty total quasi_total Element of bool [:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):]
[: the carrier of (X,f), the carrier of (X,f):] is non empty set
[:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):] is non empty set
bool [:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):] is non empty set
the addF of (X,f) . (F,y) is Element of the carrier of (X,f)
[F,y] is set
the addF of (X,f) . [F,y] is set
n * (F + y) is Element of the carrier of (X,f)
the Mult of (X,f) is V1() V4([:REAL, the carrier of (X,f):]) V5( the carrier of (X,f)) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of (X,f):], the carrier of (X,f):]
[:REAL, the carrier of (X,f):] is non empty non trivial non finite set
[:[:REAL, the carrier of (X,f):], the carrier of (X,f):] is non empty non trivial non finite set
bool [:[:REAL, the carrier of (X,f):], the carrier of (X,f):] is non empty non trivial non finite set
the Mult of (X,f) . (n,(F + y)) is set
[n,(F + y)] is set
the Mult of (X,f) . [n,(F + y)] is set
n * F is Element of the carrier of (X,f)
the Mult of (X,f) . (n,F) is set
[n,F] is set
the Mult of (X,f) . [n,F] is set
n * y is Element of the carrier of (X,f)
the Mult of (X,f) . (n,y) is set
[n,y] is set
the Mult of (X,f) . [n,y] is set
(n * F) + (n * y) is Element of the carrier of (X,f)
the addF of (X,f) . ((n * F),(n * y)) is Element of the carrier of (X,f)
[(n * F),(n * y)] is set
the addF of (X,f) . [(n * F),(n * y)] is set
z is set
s is set
[z,s] is set
s1 is set
F9 is set
[s1,F9] is set
k is Element of the carrier of X
p9 is Element of the carrier of X
k + p9 is Element of the carrier of X
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . (k,p9) is Element of the carrier of X
[k,p9] is set
the addF of X . [k,p9] is set
p is V31() real ext-real Element of REAL
p * (k + p9) is Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . (p,(k + p9)) is set
[p,(k + p9)] is set
the Mult of X . [p,(k + p9)] is set
p * k is Element of the carrier of X
the Mult of X . (p,k) is set
[p,k] is set
the Mult of X . [p,k] is set
p * p9 is Element of the carrier of X
the Mult of X . (p,p9) is set
[p,p9] is set
the Mult of X . [p,p9] is set
(p * k) + (p * p9) is Element of the carrier of X
the addF of X . ((p * k),(p * p9)) is Element of the carrier of X
[(p * k),(p * p9)] is set
the addF of X . [(p * k),(p * p9)] is set
k9 is Element of the carrier of f
z9 is Element of the carrier of f
k9 + z9 is Element of the carrier of f
the addF of f is V1() V4([: the carrier of f, the carrier of f:]) V5( the carrier of f) Function-like non empty total quasi_total Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the addF of f . (k9,z9) is Element of the carrier of f
[k9,z9] is set
the addF of f . [k9,z9] is set
[(k + p9),(k9 + z9)] is Element of [: the carrier of X, the carrier of f:]
p * (F + y) is Element of the carrier of (X,f)
the Mult of (X,f) . (p,(F + y)) is set
[p,(F + y)] is set
the Mult of (X,f) . [p,(F + y)] is set
p * (k9 + z9) is Element of the carrier of f
the Mult of f is V1() V4([:REAL, the carrier of f:]) V5( the carrier of f) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of f:], the carrier of f:]
[:REAL, the carrier of f:] is non empty non trivial non finite set
[:[:REAL, the carrier of f:], the carrier of f:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of f:], the carrier of f:] is non empty non trivial non finite set
the Mult of f . (p,(k9 + z9)) is set
[p,(k9 + z9)] is set
the Mult of f . [p,(k9 + z9)] is set
[(p * (k + p9)),(p * (k9 + z9))] is Element of [: the carrier of X, the carrier of f:]
p * k9 is Element of the carrier of f
the Mult of f . (p,k9) is set
[p,k9] is set
the Mult of f . [p,k9] is set
p * z9 is Element of the carrier of f
the Mult of f . (p,z9) is set
[p,z9] is set
the Mult of f . [p,z9] is set
(p * k9) + (p * z9) is Element of the carrier of f
the addF of f . ((p * k9),(p * z9)) is Element of the carrier of f
[(p * k9),(p * z9)] is set
the addF of f . [(p * k9),(p * z9)] is set
p * y is Element of the carrier of (X,f)
the Mult of (X,f) . (p,y) is set
[p,y] is set
the Mult of (X,f) . [p,y] is set
[(p * p9),(p * z9)] is Element of [: the carrier of X, the carrier of f:]
p * F is Element of the carrier of (X,f)
the Mult of (X,f) . (p,F) is set
[p,F] is set
the Mult of (X,f) . [p,F] is set
[(p * k),(p * k9)] is Element of [: the carrier of X, the carrier of f:]
n is V31() real ext-real set
p is V31() real ext-real set
n * p is V31() real ext-real Element of REAL
z is Element of the carrier of (X,f)
(n * p) * z is Element of the carrier of (X,f)
the Mult of (X,f) is V1() V4([:REAL, the carrier of (X,f):]) V5( the carrier of (X,f)) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of (X,f):], the carrier of (X,f):]
[:REAL, the carrier of (X,f):] is non empty non trivial non finite set
[:[:REAL, the carrier of (X,f):], the carrier of (X,f):] is non empty non trivial non finite set
bool [:[:REAL, the carrier of (X,f):], the carrier of (X,f):] is non empty non trivial non finite set
the Mult of (X,f) . ((n * p),z) is set
[(n * p),z] is set
the Mult of (X,f) . [(n * p),z] is set
p * z is Element of the carrier of (X,f)
the Mult of (X,f) . (p,z) is set
[p,z] is set
the Mult of (X,f) . [p,z] is set
n * (p * z) is Element of the carrier of (X,f)
the Mult of (X,f) . (n,(p * z)) is set
[n,(p * z)] is set
the Mult of (X,f) . [n,(p * z)] is set
s is set
k is set
[s,k] is set
y is V31() real ext-real Element of REAL
y * z is Element of the carrier of (X,f)
the Mult of (X,f) . (y,z) is set
[y,z] is set
the Mult of (X,f) . [y,z] is set
F9 is Element of the carrier of X
y * F9 is Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . (y,F9) is set
[y,F9] is set
the Mult of X . [y,F9] is set
s1 is Element of the carrier of f
y * s1 is Element of the carrier of f
the Mult of f is V1() V4([:REAL, the carrier of f:]) V5( the carrier of f) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of f:], the carrier of f:]
[:REAL, the carrier of f:] is non empty non trivial non finite set
[:[:REAL, the carrier of f:], the carrier of f:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of f:], the carrier of f:] is non empty non trivial non finite set
the Mult of f . (y,s1) is set
[y,s1] is set
the Mult of f . [y,s1] is set
[(y * F9),(y * s1)] is Element of [: the carrier of X, the carrier of f:]
F is V31() real ext-real Element of REAL
F * (y * z) is Element of the carrier of (X,f)
the Mult of (X,f) . (F,(y * z)) is set
[F,(y * z)] is set
the Mult of (X,f) . [F,(y * z)] is set
F * (y * F9) is Element of the carrier of X
the Mult of X . (F,(y * F9)) is set
[F,(y * F9)] is set
the Mult of X . [F,(y * F9)] is set
F * (y * s1) is Element of the carrier of f
the Mult of f . (F,(y * s1)) is set
[F,(y * s1)] is set
the Mult of f . [F,(y * s1)] is set
[(F * (y * F9)),(F * (y * s1))] is Element of [: the carrier of X, the carrier of f:]
F * y is V31() real ext-real Element of REAL
(F * y) * s1 is Element of the carrier of f
the Mult of f . ((F * y),s1) is set
[(F * y),s1] is set
the Mult of f . [(F * y),s1] is set
(F * y) * F9 is Element of the carrier of X
the Mult of X . ((F * y),F9) is set
[(F * y),F9] is set
the Mult of X . [(F * y),F9] is set
n is V31() real ext-real set
p is V31() real ext-real set
n + p is V31() real ext-real Element of REAL
z is Element of the carrier of (X,f)
(n + p) * z is Element of the carrier of (X,f)
the Mult of (X,f) is V1() V4([:REAL, the carrier of (X,f):]) V5( the carrier of (X,f)) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of (X,f):], the carrier of (X,f):]
[:REAL, the carrier of (X,f):] is non empty non trivial non finite set
[:[:REAL, the carrier of (X,f):], the carrier of (X,f):] is non empty non trivial non finite set
bool [:[:REAL, the carrier of (X,f):], the carrier of (X,f):] is non empty non trivial non finite set
the Mult of (X,f) . ((n + p),z) is set
[(n + p),z] is set
the Mult of (X,f) . [(n + p),z] is set
n * z is Element of the carrier of (X,f)
the Mult of (X,f) . (n,z) is set
[n,z] is set
the Mult of (X,f) . [n,z] is set
p * z is Element of the carrier of (X,f)
the Mult of (X,f) . (p,z) is set
[p,z] is set
the Mult of (X,f) . [p,z] is set
(n * z) + (p * z) is Element of the carrier of (X,f)
the addF of (X,f) is V1() V4([: the carrier of (X,f), the carrier of (X,f):]) V5( the carrier of (X,f)) Function-like non empty total quasi_total Element of bool [:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):]
[: the carrier of (X,f), the carrier of (X,f):] is non empty set
[:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):] is non empty set
bool [:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):] is non empty set
the addF of (X,f) . ((n * z),(p * z)) is Element of the carrier of (X,f)
[(n * z),(p * z)] is set
the addF of (X,f) . [(n * z),(p * z)] is set
s is set
k is set
[s,k] is set
y is V31() real ext-real Element of REAL
y * z is Element of the carrier of (X,f)
the Mult of (X,f) . (y,z) is set
[y,z] is set
the Mult of (X,f) . [y,z] is set
F9 is Element of the carrier of X
y * F9 is Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . (y,F9) is set
[y,F9] is set
the Mult of X . [y,F9] is set
s1 is Element of the carrier of f
y * s1 is Element of the carrier of f
the Mult of f is V1() V4([:REAL, the carrier of f:]) V5( the carrier of f) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of f:], the carrier of f:]
[:REAL, the carrier of f:] is non empty non trivial non finite set
[:[:REAL, the carrier of f:], the carrier of f:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of f:], the carrier of f:] is non empty non trivial non finite set
the Mult of f . (y,s1) is set
[y,s1] is set
the Mult of f . [y,s1] is set
[(y * F9),(y * s1)] is Element of [: the carrier of X, the carrier of f:]
F is V31() real ext-real Element of REAL
F * z is Element of the carrier of (X,f)
the Mult of (X,f) . (F,z) is set
[F,z] is set
the Mult of (X,f) . [F,z] is set
F * F9 is Element of the carrier of X
the Mult of X . (F,F9) is set
[F,F9] is set
the Mult of X . [F,F9] is set
F * s1 is Element of the carrier of f
the Mult of f . (F,s1) is set
[F,s1] is set
the Mult of f . [F,s1] is set
[(F * F9),(F * s1)] is Element of [: the carrier of X, the carrier of f:]
(F * z) + (y * z) is Element of the carrier of (X,f)
the addF of (X,f) . ((F * z),(y * z)) is Element of the carrier of (X,f)
[(F * z),(y * z)] is set
the addF of (X,f) . [(F * z),(y * z)] is set
(F * F9) + (y * F9) is Element of the carrier of X
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . ((F * F9),(y * F9)) is Element of the carrier of X
[(F * F9),(y * F9)] is set
the addF of X . [(F * F9),(y * F9)] is set
(F * s1) + (y * s1) is Element of the carrier of f
the addF of f is V1() V4([: the carrier of f, the carrier of f:]) V5( the carrier of f) Function-like non empty total quasi_total Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the addF of f . ((F * s1),(y * s1)) is Element of the carrier of f
[(F * s1),(y * s1)] is set
the addF of f . [(F * s1),(y * s1)] is set
[((F * F9) + (y * F9)),((F * s1) + (y * s1))] is Element of [: the carrier of X, the carrier of f:]
F + y is V31() real ext-real Element of REAL
(F + y) * s1 is Element of the carrier of f
the Mult of f . ((F + y),s1) is set
[(F + y),s1] is set
the Mult of f . [(F + y),s1] is set
(F + y) * F9 is Element of the carrier of X
the Mult of X . ((F + y),F9) is set
[(F + y),F9] is set
the Mult of X . [(F + y),F9] is set
n is Element of the carrier of (X,f)
1 * n is Element of the carrier of (X,f)
the Mult of (X,f) is V1() V4([:REAL, the carrier of (X,f):]) V5( the carrier of (X,f)) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of (X,f):], the carrier of (X,f):]
[:REAL, the carrier of (X,f):] is non empty non trivial non finite set
[:[:REAL, the carrier of (X,f):], the carrier of (X,f):] is non empty non trivial non finite set
bool [:[:REAL, the carrier of (X,f):], the carrier of (X,f):] is non empty non trivial non finite set
the Mult of (X,f) . (1,n) is set
[1,n] is set
the Mult of (X,f) . [1,n] is set
p is set
F is set
[p,F] is set
y is Element of the carrier of f
1 * y is Element of the carrier of f
the Mult of f is V1() V4([:REAL, the carrier of f:]) V5( the carrier of f) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of f:], the carrier of f:]
[:REAL, the carrier of f:] is non empty non trivial non finite set
[:[:REAL, the carrier of f:], the carrier of f:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of f:], the carrier of f:] is non empty non trivial non finite set
the Mult of f . (1,y) is set
[1,y] is set
the Mult of f . [1,y] is set
z is Element of the carrier of X
1 * z is Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . (1,z) is set
[1,z] is set
the Mult of X . [1,z] is set
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V164() RLSStruct
the carrier of X is non empty set
f is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V164() RLSStruct
the carrier of f is non empty set
(X,f) is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V164() RLSStruct
[: the carrier of X, the carrier of f:] is non empty set
0. X is V113(X) left_complementable right_complementable complementable Element of the carrier of X
the ZeroF of X is left_complementable right_complementable complementable Element of the carrier of X
0. f is V113(f) left_complementable right_complementable complementable Element of the carrier of f
the ZeroF of f is left_complementable right_complementable complementable Element of the carrier of f
[(0. X),(0. f)] is Element of [: the carrier of X, the carrier of f:]
(X,f) is V1() V4([:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:] is non empty set
[:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
bool [:[:[: the carrier of X, the carrier of f:],[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty set
(X,f) is V1() V4([:REAL,[: the carrier of X, the carrier of f:]:]) V5([: the carrier of X, the carrier of f:]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:]
[:REAL,[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
[:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
bool [:[:REAL,[: the carrier of X, the carrier of f:]:],[: the carrier of X, the carrier of f:]:] is non empty non trivial non finite set
RLSStruct(# [: the carrier of X, the carrier of f:],[(0. X),(0. f)],(X,f),(X,f) #) is non empty strict RLSStruct
the carrier of (X,f) is non empty set
n is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg n is finite n -element V63() V64() V65() V66() V67() V68() Element of bool NAT
n + 1 is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg (n + 1) is non empty finite n + 1 -element V63() V64() V65() V66() V67() V68() Element of bool NAT
p is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
len p is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum p is left_complementable right_complementable complementable Element of the carrier of X
F is V1() V4( NAT ) V5( the carrier of f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of f
len F is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum F is left_complementable right_complementable complementable Element of the carrier of f
[(Sum p),(Sum F)] is Element of [: the carrier of X, the carrier of f:]
y is V1() V4( NAT ) V5( the carrier of (X,f)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (X,f)
len y is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum y is left_complementable right_complementable complementable Element of the carrier of (X,f)
0 + n is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
1 + n is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F | n is V1() V4( NAT ) V5( the carrier of f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of f
len (F | n) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
y | n is V1() V4( NAT ) V5( the carrier of (X,f)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (X,f)
p | n is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
z is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(y | n) . z is set
(p | n) . z is set
(F | n) . z is set
[((p | n) . z),((F | n) . z)] is set
F . z is set
y . z is set
p . z is set
z is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
p /. z is left_complementable right_complementable complementable Element of the carrier of X
p . z is set
F /. z is left_complementable right_complementable complementable Element of the carrier of f
F . z is set
y /. z is left_complementable right_complementable complementable Element of the carrier of (X,f)
y . z is set
F /. (n + 1) is left_complementable right_complementable complementable Element of the carrier of f
F . (n + 1) is set
y | (Seg n) is V1() V4( NAT ) V5( the carrier of (X,f)) Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of (X,f):]
[:NAT, the carrier of (X,f):] is non trivial non finite set
bool [:NAT, the carrier of (X,f):] is non empty non trivial non finite set
y . (n + 1) is set
<*(y . (n + 1))*> is V1() V4( NAT ) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
(y | n) ^ <*(y . (n + 1))*> is V1() V4( NAT ) Function-like non empty finite FinSequence-like FinSubsequence-like set
y /. (n + 1) is left_complementable right_complementable complementable Element of the carrier of (X,f)
<*(y /. (n + 1))*> is V1() V4( NAT ) V5( the carrier of (X,f)) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of (X,f)
(y | n) ^ <*(y /. (n + 1))*> is V1() V4( NAT ) V5( the carrier of (X,f)) Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (X,f)
Sum (y | n) is left_complementable right_complementable complementable Element of the carrier of (X,f)
Sum <*(y /. (n + 1))*> is left_complementable right_complementable complementable Element of the carrier of (X,f)
(Sum (y | n)) + (Sum <*(y /. (n + 1))*>) is left_complementable right_complementable complementable Element of the carrier of (X,f)
the addF of (X,f) is V1() V4([: the carrier of (X,f), the carrier of (X,f):]) V5( the carrier of (X,f)) Function-like non empty total quasi_total Element of bool [:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):]
[: the carrier of (X,f), the carrier of (X,f):] is non empty set
[:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):] is non empty set
bool [:[: the carrier of (X,f), the carrier of (X,f):], the carrier of (X,f):] is non empty set
the addF of (X,f) . ((Sum (y | n)),(Sum <*(y /. (n + 1))*>)) is left_complementable right_complementable complementable Element of the carrier of (X,f)
[(Sum (y | n)),(Sum <*(y /. (n + 1))*>)] is set
the addF of (X,f) . [(Sum (y | n)),(Sum <*(y /. (n + 1))*>)] is set
(Sum (y | n)) + (y /. (n + 1)) is left_complementable right_complementable complementable Element of the carrier of (X,f)
the addF of (X,f) . ((Sum (y | n)),(y /. (n + 1))) is left_complementable right_complementable complementable Element of the carrier of (X,f)
[(Sum (y | n)),(y /. (n + 1))] is set
the addF of (X,f) . [(Sum (y | n)),(y /. (n + 1))] is set
F | (Seg n) is V1() V4( NAT ) V5( the carrier of f) Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of f:]
[:NAT, the carrier of f:] is non trivial non finite set
bool [:NAT, the carrier of f:] is non empty non trivial non finite set
<*(F . (n + 1))*> is V1() V4( NAT ) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
(F | n) ^ <*(F . (n + 1))*> is V1() V4( NAT ) Function-like non empty finite FinSequence-like FinSubsequence-like set
<*(F /. (n + 1))*> is V1() V4( NAT ) V5( the carrier of f) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of f
(F | n) ^ <*(F /. (n + 1))*> is V1() V4( NAT ) V5( the carrier of f) Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of f
Sum (F | n) is left_complementable right_complementable complementable Element of the carrier of f
Sum <*(F /. (n + 1))*> is left_complementable right_complementable complementable Element of the carrier of f
(Sum (F | n)) + (Sum <*(F /. (n + 1))*>) is left_complementable right_complementable complementable Element of the carrier of f
the addF of f is V1() V4([: the carrier of f, the carrier of f:]) V5( the carrier of f) Function-like non empty total quasi_total Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the addF of f . ((Sum (F | n)),(Sum <*(F /. (n + 1))*>)) is left_complementable right_complementable complementable Element of the carrier of f
[(Sum (F | n)),(Sum <*(F /. (n + 1))*>)] is set
the addF of f . [(Sum (F | n)),(Sum <*(F /. (n + 1))*>)] is set
(Sum (F | n)) + (F /. (n + 1)) is left_complementable right_complementable complementable Element of the carrier of f
the addF of f . ((Sum (F | n)),(F /. (n + 1))) is left_complementable right_complementable complementable Element of the carrier of f
[(Sum (F | n)),(F /. (n + 1))] is set
the addF of f . [(Sum (F | n)),(F /. (n + 1))] is set
p | (Seg n) is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of X:]
[:NAT, the carrier of X:] is non trivial non finite set
bool [:NAT, the carrier of X:] is non empty non trivial non finite set
p . (n + 1) is set
<*(p . (n + 1))*> is V1() V4( NAT ) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
(p | n) ^ <*(p . (n + 1))*> is V1() V4( NAT ) Function-like non empty finite FinSequence-like FinSubsequence-like set
p /. (n + 1) is left_complementable right_complementable complementable Element of the carrier of X
<*(p /. (n + 1))*> is V1() V4( NAT ) V5( the carrier of X) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of X
(p | n) ^ <*(p /. (n + 1))*> is V1() V4( NAT ) V5( the carrier of X) Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
Sum (p | n) is left_complementable right_complementable complementable Element of the carrier of X
Sum <*(p /. (n + 1))*> is left_complementable right_complementable complementable Element of the carrier of X
(Sum (p | n)) + (Sum <*(p /. (n + 1))*>) is left_complementable right_complementable complementable Element of the carrier of X
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . ((Sum (p | n)),(Sum <*(p /. (n + 1))*>)) is left_complementable right_complementable complementable Element of the carrier of X
[(Sum (p | n)),(Sum <*(p /. (n + 1))*>)] is set
the addF of X . [(Sum (p | n)),(Sum <*(p /. (n + 1))*>)] is set
(Sum (p | n)) + (p /. (n + 1)) is left_complementable right_complementable complementable Element of the carrier of X
the addF of X . ((Sum (p | n)),(p /. (n + 1))) is left_complementable right_complementable complementable Element of the carrier of X
[(Sum (p | n)),(p /. (n + 1))] is set
the addF of X . [(Sum (p | n)),(p /. (n + 1))] is set
[(p /. (n + 1)),(F /. (n + 1))] is Element of [: the carrier of X, the carrier of f:]
len (y | n) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
len (p | n) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
[(Sum (p | n)),(Sum (F | n))] is Element of [: the carrier of X, the carrier of f:]
Seg 0 is functional empty ordinal natural V31() real finite V37() cardinal 0 -element {} -element FinSequence-membered ext-real non positive non negative V63() V64() V65() V66() V67() V68() V69() Element of bool NAT
n is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
len n is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum n is left_complementable right_complementable complementable Element of the carrier of X
p is V1() V4( NAT ) V5( the carrier of f) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of f
len p is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum p is left_complementable right_complementable complementable Element of the carrier of f
[(Sum n),(Sum p)] is Element of [: the carrier of X, the carrier of f:]
F is V1() V4( NAT ) V5( the carrier of (X,f)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (X,f)
len F is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum F is left_complementable right_complementable complementable Element of the carrier of (X,f)
<*> the carrier of X is V1() V4( NAT ) V5( the carrier of X) Function-like functional empty ordinal natural V31() real finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() FinSequence of the carrier of X
<*> the carrier of (X,f) is V1() V4( NAT ) V5( the carrier of (X,f)) Function-like functional empty ordinal natural V31() real finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() FinSequence of the carrier of (X,f)
0. (X,f) is V113((X,f)) left_complementable right_complementable complementable Element of the carrier of (X,f)
the ZeroF of (X,f) is left_complementable right_complementable complementable Element of the carrier of (X,f)
<*> the carrier of f is V1() V4( NAT ) V5( the carrier of f) Function-like functional empty ordinal natural V31() real finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() FinSequence of the carrier of f
RLSStruct(# REAL,0,addreal,multreal #) is non empty strict RLSStruct
() is non empty RLSStruct
the carrier of () is non empty set
X is Element of the carrier of ()
f is Element of the carrier of ()
X + f is Element of the carrier of ()
the addF of () is V1() V4([: the carrier of (), the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (X,f) is Element of the carrier of ()
[X,f] is set
the addF of () . [X,f] is set
f + X is Element of the carrier of ()
the addF of () . (f,X) is Element of the carrier of ()
[f,X] is set
the addF of () . [f,X] is set
n is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
n + p is V31() real ext-real Element of REAL
the carrier of () is non empty set
X is Element of the carrier of ()
f is Element of the carrier of ()
X + f is Element of the carrier of ()
the addF of () is V1() V4([: the carrier of (), the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (X,f) is Element of the carrier of ()
[X,f] is set
the addF of () . [X,f] is set
n is Element of the carrier of ()
(X + f) + n is Element of the carrier of ()
the addF of () . ((X + f),n) is Element of the carrier of ()
[(X + f),n] is set
the addF of () . [(X + f),n] is set
f + n is Element of the carrier of ()
the addF of () . (f,n) is Element of the carrier of ()
[f,n] is set
the addF of () . [f,n] is set
X + (f + n) is Element of the carrier of ()
the addF of () . (X,(f + n)) is Element of the carrier of ()
[X,(f + n)] is set
the addF of () . [X,(f + n)] is set
F is V31() real ext-real Element of REAL
y is V31() real ext-real Element of REAL
F + y is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
p + (F + y) is V31() real ext-real Element of REAL
p + F is V31() real ext-real Element of REAL
(p + F) + y is V31() real ext-real Element of REAL
the carrier of () is non empty set
X is Element of the carrier of ()
0. () is V113(()) Element of the carrier of ()
the ZeroF of () is Element of the carrier of ()
X + (0. ()) is Element of the carrier of ()
the addF of () is V1() V4([: the carrier of (), the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (X,(0. ())) is Element of the carrier of ()
[X,(0. ())] is set
the addF of () . [X,(0. ())] is set
f is V31() real ext-real Element of REAL
f + 0 is V31() real ext-real Element of REAL
the carrier of () is non empty set
X is Element of the carrier of ()
f is V31() real ext-real Element of REAL
- f is V31() real ext-real Element of REAL
n is Element of the carrier of ()
X + n is Element of the carrier of ()
the addF of () is V1() V4([: the carrier of (), the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (X,n) is Element of the carrier of ()
[X,n] is set
the addF of () . [X,n] is set
0. () is V113(()) Element of the carrier of ()
the ZeroF of () is Element of the carrier of ()
f + (- f) is V31() real ext-real Element of REAL
the carrier of () is non empty set
X is V31() real ext-real set
n is Element of the carrier of ()
p is Element of the carrier of ()
n + p is Element of the carrier of ()
the addF of () is V1() V4([: the carrier of (), the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (n,p) is Element of the carrier of ()
[n,p] is set
the addF of () . [n,p] is set
X * (n + p) is Element of the carrier of ()
the Mult of () is V1() V4([:REAL, the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is non empty non trivial non finite set
[:[:REAL, the carrier of ():], the carrier of ():] is non empty non trivial non finite set
bool [:[:REAL, the carrier of ():], the carrier of ():] is non empty non trivial non finite set
the Mult of () . (X,(n + p)) is set
[X,(n + p)] is set
the Mult of () . [X,(n + p)] is set
X * n is Element of the carrier of ()
the Mult of () . (X,n) is set
[X,n] is set
the Mult of () . [X,n] is set
X * p is Element of the carrier of ()
the Mult of () . (X,p) is set
[X,p] is set
the Mult of () . [X,p] is set
(X * n) + (X * p) is Element of the carrier of ()
the addF of () . ((X * n),(X * p)) is Element of the carrier of ()
[(X * n),(X * p)] is set
the addF of () . [(X * n),(X * p)] is set
f is V31() real ext-real Element of REAL
f * n is Element of the carrier of ()
the Mult of () . (f,n) is set
[f,n] is set
the Mult of () . [f,n] is set
F is V31() real ext-real Element of REAL
f * F is V31() real ext-real Element of REAL
f * p is Element of the carrier of ()
the Mult of () . (f,p) is set
[f,p] is set
the Mult of () . [f,p] is set
y is V31() real ext-real Element of REAL
f * y is V31() real ext-real Element of REAL
F + y is V31() real ext-real Element of REAL
f * (n + p) is Element of the carrier of ()
the Mult of () . (f,(n + p)) is set
[f,(n + p)] is set
the Mult of () . [f,(n + p)] is set
f * (F + y) is V31() real ext-real Element of REAL
(f * F) + (f * y) is V31() real ext-real Element of REAL
(f * n) + (f * p) is Element of the carrier of ()
the addF of () . ((f * n),(f * p)) is Element of the carrier of ()
[(f * n),(f * p)] is set
the addF of () . [(f * n),(f * p)] is set
X is V31() real ext-real set
f is V31() real ext-real set
X + f is V31() real ext-real Element of REAL
F is Element of the carrier of ()
(X + f) * F is Element of the carrier of ()
the Mult of () is V1() V4([:REAL, the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is non empty non trivial non finite set
[:[:REAL, the carrier of ():], the carrier of ():] is non empty non trivial non finite set
bool [:[:REAL, the carrier of ():], the carrier of ():] is non empty non trivial non finite set
the Mult of () . ((X + f),F) is set
[(X + f),F] is set
the Mult of () . [(X + f),F] is set
X * F is Element of the carrier of ()
the Mult of () . (X,F) is set
[X,F] is set
the Mult of () . [X,F] is set
f * F is Element of the carrier of ()
the Mult of () . (f,F) is set
[f,F] is set
the Mult of () . [f,F] is set
(X * F) + (f * F) is Element of the carrier of ()
the addF of () is V1() V4([: the carrier of (), the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . ((X * F),(f * F)) is Element of the carrier of ()
[(X * F),(f * F)] is set
the addF of () . [(X * F),(f * F)] is set
p is V31() real ext-real Element of REAL
p * F is Element of the carrier of ()
the Mult of () . (p,F) is set
[p,F] is set
the Mult of () . [p,F] is set
y is V31() real ext-real Element of REAL
p * y is V31() real ext-real Element of REAL
n is V31() real ext-real Element of REAL
n * F is Element of the carrier of ()
the Mult of () . (n,F) is set
[n,F] is set
the Mult of () . [n,F] is set
n * y is V31() real ext-real Element of REAL
(n * F) + (p * F) is Element of the carrier of ()
the addF of () . ((n * F),(p * F)) is Element of the carrier of ()
[(n * F),(p * F)] is set
the addF of () . [(n * F),(p * F)] is set
(n * y) + (p * y) is V31() real ext-real Element of REAL
n + p is V31() real ext-real Element of REAL
(n + p) * y is V31() real ext-real Element of REAL
(n + p) * F is Element of the carrier of ()
the Mult of () . ((n + p),F) is set
[(n + p),F] is set
the Mult of () . [(n + p),F] is set
X is V31() real ext-real set
f is V31() real ext-real set
X * f is V31() real ext-real Element of REAL
F is Element of the carrier of ()
(X * f) * F is Element of the carrier of ()
the Mult of () is V1() V4([:REAL, the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is non empty non trivial non finite set
[:[:REAL, the carrier of ():], the carrier of ():] is non empty non trivial non finite set
bool [:[:REAL, the carrier of ():], the carrier of ():] is non empty non trivial non finite set
the Mult of () . ((X * f),F) is set
[(X * f),F] is set
the Mult of () . [(X * f),F] is set
f * F is Element of the carrier of ()
the Mult of () . (f,F) is set
[f,F] is set
the Mult of () . [f,F] is set
X * (f * F) is Element of the carrier of ()
the Mult of () . (X,(f * F)) is set
[X,(f * F)] is set
the Mult of () . [X,(f * F)] is set
p is V31() real ext-real Element of REAL
p * F is Element of the carrier of ()
the Mult of () . (p,F) is set
[p,F] is set
the Mult of () . [p,F] is set
y is V31() real ext-real Element of REAL
p * y is V31() real ext-real Element of REAL
n is V31() real ext-real Element of REAL
n * (p * F) is Element of the carrier of ()
the Mult of () . (n,(p * F)) is set
[n,(p * F)] is set
the Mult of () . [n,(p * F)] is set
n * (p * y) is V31() real ext-real Element of REAL
n * p is V31() real ext-real Element of REAL
(n * p) * y is V31() real ext-real Element of REAL
(n * p) * F is Element of the carrier of ()
the Mult of () . ((n * p),F) is set
[(n * p),F] is set
the Mult of () . [(n * p),F] is set
X is Element of the carrier of ()
1 * X is Element of the carrier of ()
the Mult of () is V1() V4([:REAL, the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is non empty non trivial non finite set
[:[:REAL, the carrier of ():], the carrier of ():] is non empty non trivial non finite set
bool [:[:REAL, the carrier of ():], the carrier of ():] is non empty non trivial non finite set
the Mult of () . (1,X) is set
[1,X] is set
the Mult of () . [1,X] is set
f is V31() real ext-real Element of REAL
1 * f is V31() real ext-real Element of REAL
X is non empty RLSStruct
the carrier of X is non empty set
(X,()) is non empty RLSStruct
the carrier of () is non empty set
[: the carrier of X, the carrier of ():] is non empty set
0. X is V113(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
0. () is V113(()) left_complementable right_complementable complementable Element of the carrier of ()
the ZeroF of () is left_complementable right_complementable complementable Element of the carrier of ()
[(0. X),(0. ())] is Element of [: the carrier of X, the carrier of ():]
(X,()) is V1() V4([:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:]) V5([: the carrier of X, the carrier of ():]) Function-like non empty total quasi_total Element of bool [:[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:]
[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:] is non empty set
[:[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty set
bool [:[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty set
(X,()) is V1() V4([:REAL,[: the carrier of X, the carrier of ():]:]) V5([: the carrier of X, the carrier of ():]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:]
[:REAL,[: the carrier of X, the carrier of ():]:] is non empty non trivial non finite set
[:[:REAL,[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty non trivial non finite set
bool [:[:REAL,[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty non trivial non finite set
RLSStruct(# [: the carrier of X, the carrier of ():],[(0. X),(0. ())],(X,()),(X,()) #) is non empty strict RLSStruct
the carrier of (X,()) is non empty set
f is Element of the carrier of X
n is Element of the carrier of (X,())
F is V31() real ext-real Element of REAL
[f,F] is Element of [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty non trivial non finite V53() V54() V55() set
p is V31() real ext-real Element of REAL
p * n is Element of the carrier of (X,())
the Mult of (X,()) is V1() V4([:REAL, the carrier of (X,()):]) V5( the carrier of (X,())) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of (X,()):], the carrier of (X,()):]
[:REAL, the carrier of (X,()):] is non empty non trivial non finite set
[:[:REAL, the carrier of (X,()):], the carrier of (X,()):] is non empty non trivial non finite set
bool [:[:REAL, the carrier of (X,()):], the carrier of (X,()):] is non empty non trivial non finite set
the Mult of (X,()) . (p,n) is set
[p,n] is set
the Mult of (X,()) . [p,n] is set
p * f is Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . (p,f) is set
[p,f] is set
the Mult of X . [p,f] is set
p * F is V31() real ext-real Element of REAL
[(p * f),(p * F)] is Element of [: the carrier of X,REAL:]
y is left_complementable right_complementable complementable Element of the carrier of ()
p * y is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () is V1() V4([:REAL, the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is non empty non trivial non finite set
[:[:REAL, the carrier of ():], the carrier of ():] is non empty non trivial non finite set
bool [:[:REAL, the carrier of ():], the carrier of ():] is non empty non trivial non finite set
the Mult of () . (p,y) is set
[p,y] is set
the Mult of () . [p,y] is set
X is non empty RLSStruct
the carrier of X is non empty set
(X,()) is non empty RLSStruct
the carrier of () is non empty set
[: the carrier of X, the carrier of ():] is non empty set
0. X is V113(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
0. () is V113(()) left_complementable right_complementable complementable Element of the carrier of ()
the ZeroF of () is left_complementable right_complementable complementable Element of the carrier of ()
[(0. X),(0. ())] is Element of [: the carrier of X, the carrier of ():]
(X,()) is V1() V4([:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:]) V5([: the carrier of X, the carrier of ():]) Function-like non empty total quasi_total Element of bool [:[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:]
[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:] is non empty set
[:[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty set
bool [:[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty set
(X,()) is V1() V4([:REAL,[: the carrier of X, the carrier of ():]:]) V5([: the carrier of X, the carrier of ():]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:]
[:REAL,[: the carrier of X, the carrier of ():]:] is non empty non trivial non finite set
[:[:REAL,[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty non trivial non finite set
bool [:[:REAL,[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty non trivial non finite set
RLSStruct(# [: the carrier of X, the carrier of ():],[(0. X),(0. ())],(X,()),(X,()) #) is non empty strict RLSStruct
the carrier of (X,()) is non empty set
f is Element of the carrier of X
n is Element of the carrier of X
f + n is Element of the carrier of X
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . (f,n) is Element of the carrier of X
[f,n] is set
the addF of X . [f,n] is set
p is V31() real ext-real Element of REAL
[f,p] is Element of [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty non trivial non finite V53() V54() V55() set
F is V31() real ext-real Element of REAL
[n,F] is Element of [: the carrier of X,REAL:]
p + F is V31() real ext-real Element of REAL
[(f + n),(p + F)] is Element of [: the carrier of X,REAL:]
y is Element of the carrier of (X,())
z is Element of the carrier of (X,())
y + z is Element of the carrier of (X,())
the addF of (X,()) is V1() V4([: the carrier of (X,()), the carrier of (X,()):]) V5( the carrier of (X,())) Function-like non empty total quasi_total Element of bool [:[: the carrier of (X,()), the carrier of (X,()):], the carrier of (X,()):]
[: the carrier of (X,()), the carrier of (X,()):] is non empty set
[:[: the carrier of (X,()), the carrier of (X,()):], the carrier of (X,()):] is non empty set
bool [:[: the carrier of (X,()), the carrier of (X,()):], the carrier of (X,()):] is non empty set
the addF of (X,()) . (y,z) is Element of the carrier of (X,())
[y,z] is set
the addF of (X,()) . [y,z] is set
s is left_complementable right_complementable complementable Element of the carrier of ()
k is left_complementable right_complementable complementable Element of the carrier of ()
s + k is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () is V1() V4([: the carrier of (), the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (s,k) is left_complementable right_complementable complementable Element of the carrier of ()
[s,k] is set
the addF of () . [s,k] is set
the carrier of () is non empty set
X is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
len X is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
dom X is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
Sum X is left_complementable right_complementable complementable Element of the carrier of ()
f is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
len f is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum f is V31() real ext-real Element of REAL
K190(REAL,f,addreal) is V31() real ext-real Element of REAL
n is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
n + 1 is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
p is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
len p is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
dom p is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
Sum p is left_complementable right_complementable complementable Element of the carrier of ()
F is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
len F is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum F is V31() real ext-real Element of REAL
K190(REAL,F,addreal) is V31() real ext-real Element of REAL
0 + n is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
1 + n is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
p | n is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
len (p | n) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg (n + 1) is non empty finite n + 1 -element V63() V64() V65() V66() V67() V68() Element of bool NAT
y is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
p . y is set
p /. y is left_complementable right_complementable complementable Element of the carrier of ()
F . y is V31() real ext-real Element of REAL
Seg n is finite n -element V63() V64() V65() V66() V67() V68() Element of bool NAT
dom (p | n) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
F | n is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
y is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(p | n) . y is set
(F | n) . y is V31() real ext-real Element of REAL
F . y is V31() real ext-real Element of REAL
p . y is set
len (F | n) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum (p | n) is left_complementable right_complementable complementable Element of the carrier of ()
Sum (F | n) is V31() real ext-real Element of REAL
K190(REAL,(F | n),addreal) is V31() real ext-real Element of REAL
F | (Seg n) is V1() V4( NAT ) V5( REAL ) Function-like finite FinSubsequence-like V53() V54() V55() Element of bool [:NAT,REAL:]
[:NAT,REAL:] is non trivial non finite V53() V54() V55() set
bool [:NAT,REAL:] is non empty non trivial non finite set
F . (n + 1) is V31() real ext-real Element of REAL
<*(F . (n + 1))*> is V1() V4( NAT ) V5( REAL ) Function-like one-to-one non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V53() V54() V55() V57() V58() V59() V60() FinSequence of REAL
(F | n) ^ <*(F . (n + 1))*> is V1() V4( NAT ) V5( REAL ) Function-like non empty finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
p /. (n + 1) is left_complementable right_complementable complementable Element of the carrier of ()
p | (Seg n) is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of ():]
[:NAT, the carrier of ():] is non trivial non finite set
bool [:NAT, the carrier of ():] is non empty non trivial non finite set
p . (n + 1) is set
<*(p . (n + 1))*> is V1() V4( NAT ) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
(p | n) ^ <*(p . (n + 1))*> is V1() V4( NAT ) Function-like non empty finite FinSequence-like FinSubsequence-like set
<*(p /. (n + 1))*> is V1() V4( NAT ) V5( the carrier of ()) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
(p | n) ^ <*(p /. (n + 1))*> is V1() V4( NAT ) V5( the carrier of ()) Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
Sum <*(p /. (n + 1))*> is left_complementable right_complementable complementable Element of the carrier of ()
(Sum (p | n)) + (Sum <*(p /. (n + 1))*>) is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () is V1() V4([: the carrier of (), the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . ((Sum (p | n)),(Sum <*(p /. (n + 1))*>)) is left_complementable right_complementable complementable Element of the carrier of ()
[(Sum (p | n)),(Sum <*(p /. (n + 1))*>)] is set
the addF of () . [(Sum (p | n)),(Sum <*(p /. (n + 1))*>)] is set
(Sum (p | n)) + (p /. (n + 1)) is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () . ((Sum (p | n)),(p /. (n + 1))) is left_complementable right_complementable complementable Element of the carrier of ()
[(Sum (p | n)),(p /. (n + 1))] is set
the addF of () . [(Sum (p | n)),(p /. (n + 1))] is set
(Sum (F | n)) + (F . (n + 1)) is V31() real ext-real Element of REAL
n is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
len n is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
dom n is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
Sum n is left_complementable right_complementable complementable Element of the carrier of ()
p is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
len p is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum p is V31() real ext-real Element of REAL
K190(REAL,p,addreal) is V31() real ext-real Element of REAL
<*> the carrier of () is V1() V4( NAT ) V5( the carrier of ()) Function-like functional empty ordinal natural V31() real finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() FinSequence of the carrier of ()
0. () is V113(()) left_complementable right_complementable complementable Element of the carrier of ()
the ZeroF of () is left_complementable right_complementable complementable Element of the carrier of ()
X is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
Sum X is ext-real Element of ExtREAL
f is ext-real Element of ExtREAL
<*f*> is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V54() V57() V58() V59() V60() FinSequence of ExtREAL
X ^ <*f*> is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
Sum (X ^ <*f*>) is ext-real Element of ExtREAL
(Sum X) + f is ext-real Element of ExtREAL
len (X ^ <*f*>) is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
n is V1() V4( NAT ) V5( ExtREAL ) Function-like total quasi_total V54() Element of bool [:NAT,ExtREAL:]
n . (len (X ^ <*f*>)) is ext-real Element of ExtREAL
n . 0 is ext-real Element of ExtREAL
len X is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
len <*f*> is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(len X) + (len <*f*>) is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(len X) + 1 is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
p is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
p + 1 is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
n . (p + 1) is ext-real Element of ExtREAL
n . p is ext-real Element of ExtREAL
X . (p + 1) is ext-real Element of ExtREAL
(n . p) + (X . (p + 1)) is ext-real Element of ExtREAL
Seg (len X) is finite len X -element V63() V64() V65() V66() V67() V68() Element of bool NAT
dom X is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
(X ^ <*f*>) . (p + 1) is ext-real Element of ExtREAL
(n . p) + ((X ^ <*f*>) . (p + 1)) is ext-real Element of ExtREAL
n . (len X) is ext-real Element of ExtREAL
n . ((len X) + 1) is ext-real Element of ExtREAL
(X ^ <*f*>) . ((len X) + 1) is ext-real Element of ExtREAL
(n . (len X)) + ((X ^ <*f*>) . ((len X) + 1)) is ext-real Element of ExtREAL
X is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
rng X is finite V64() Element of bool ExtREAL
Sum X is ext-real Element of ExtREAL
f is ext-real Element of ExtREAL
<*f*> is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V54() V57() V58() V59() V60() FinSequence of ExtREAL
X ^ <*f*> is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
rng (X ^ <*f*>) is finite V64() Element of bool ExtREAL
Sum (X ^ <*f*>) is ext-real Element of ExtREAL
(Sum X) + f is ext-real Element of ExtREAL
rng <*f*> is finite V64() Element of bool ExtREAL
(rng X) \/ (rng <*f*>) is finite V64() Element of bool ExtREAL
{f} is non empty trivial finite 1 -element V64() Element of bool ExtREAL
rng (<*> ExtREAL) is finite V37() V63() V64() V65() V66() V67() V68() Element of bool ExtREAL
+infty is non empty non real ext-real positive non negative Element of ExtREAL
X is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
rng X is finite V64() Element of bool ExtREAL
Sum X is ext-real Element of ExtREAL
f is ext-real Element of ExtREAL
<*f*> is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V54() V57() V58() V59() V60() FinSequence of ExtREAL
X ^ <*f*> is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
rng (X ^ <*f*>) is finite V64() Element of bool ExtREAL
Sum (X ^ <*f*>) is ext-real Element of ExtREAL
(Sum X) + f is ext-real Element of ExtREAL
rng <*f*> is finite V64() Element of bool ExtREAL
(rng X) \/ (rng <*f*>) is finite V64() Element of bool ExtREAL
{f} is non empty trivial finite 1 -element V64() Element of bool ExtREAL
rng (<*> ExtREAL) is finite V37() V63() V64() V65() V66() V67() V68() Element of bool ExtREAL
X is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len X is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
dom X is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
Sum X is ext-real Element of ExtREAL
f is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
len f is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum f is V31() real ext-real Element of REAL
K190(REAL,f,addreal) is V31() real ext-real Element of REAL
n is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
n + 1 is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
p is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len p is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
dom p is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
Sum p is ext-real Element of ExtREAL
F is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
len F is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum F is V31() real ext-real Element of REAL
K190(REAL,F,addreal) is V31() real ext-real Element of REAL
Seg (n + 1) is non empty finite n + 1 -element V63() V64() V65() V66() V67() V68() Element of bool NAT
p . (n + 1) is ext-real Element of ExtREAL
F . (n + 1) is V31() real ext-real Element of REAL
0 + n is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
1 + n is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
p | n is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len (p | n) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg n is finite n -element V63() V64() V65() V66() V67() V68() Element of bool NAT
dom (p | n) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
F | n is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
y is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(p | n) . y is ext-real Element of ExtREAL
(F | n) . y is V31() real ext-real Element of REAL
F . y is V31() real ext-real Element of REAL
p . y is ext-real Element of ExtREAL
len (F | n) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum (p | n) is ext-real Element of ExtREAL
Sum (F | n) is V31() real ext-real Element of REAL
K190(REAL,(F | n),addreal) is V31() real ext-real Element of REAL
F | (Seg n) is V1() V4( NAT ) V5( REAL ) Function-like finite FinSubsequence-like V53() V54() V55() Element of bool [:NAT,REAL:]
[:NAT,REAL:] is non trivial non finite V53() V54() V55() set
bool [:NAT,REAL:] is non empty non trivial non finite set
<*(F . (n + 1))*> is V1() V4( NAT ) V5( REAL ) Function-like one-to-one non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V53() V54() V55() V57() V58() V59() V60() FinSequence of REAL
(F | n) ^ <*(F . (n + 1))*> is V1() V4( NAT ) V5( REAL ) Function-like non empty finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
p | (Seg n) is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSubsequence-like V54() Element of bool [:NAT,ExtREAL:]
<*(p . (n + 1))*> is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V54() V57() V58() V59() V60() FinSequence of ExtREAL
(p | n) ^ <*(p . (n + 1))*> is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
(Sum (p | n)) + (p . (n + 1)) is ext-real Element of ExtREAL
(Sum (F | n)) + (F . (n + 1)) is V31() real ext-real Element of REAL
n is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len n is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
dom n is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
Sum n is ext-real Element of ExtREAL
p is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
len p is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum p is V31() real ext-real Element of REAL
K190(REAL,p,addreal) is V31() real ext-real Element of REAL
X is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg X is finite X -element V63() V64() V65() V66() V67() V68() Element of bool NAT
f is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len f is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum f is ext-real Element of ExtREAL
n is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
len n is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum n is left_complementable right_complementable complementable Element of the carrier of ()
dom f is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
F is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
Sum F is V31() real ext-real Element of REAL
K190(REAL,F,addreal) is V31() real ext-real Element of REAL
dom n is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
y is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
n . y is set
F . y is V31() real ext-real Element of REAL
len F is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
{0.} is non empty trivial finite V37() 1 -element V63() V64() V65() V66() V67() V68() Element of bool ExtREAL
X is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
rng X is finite V64() Element of bool ExtREAL
Sum X is ext-real Element of ExtREAL
f is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
rng f is finite V64() Element of bool ExtREAL
Sum f is ext-real Element of ExtREAL
n is ext-real Element of ExtREAL
<*n*> is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V54() V57() V58() V59() V60() FinSequence of ExtREAL
f ^ <*n*> is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
rng (f ^ <*n*>) is finite V64() Element of bool ExtREAL
Sum (f ^ <*n*>) is ext-real Element of ExtREAL
rng <*n*> is finite V64() Element of bool ExtREAL
(rng f) \/ (rng <*n*>) is finite V64() Element of bool ExtREAL
{n} is non empty trivial finite 1 -element V64() Element of bool ExtREAL
(Sum f) + n is ext-real Element of ExtREAL
rng (<*> ExtREAL) is finite V37() V63() V64() V65() V66() V67() V68() Element of bool ExtREAL
{0} is non empty trivial finite V37() 1 -element V63() V64() V65() V66() V67() V68() Element of bool REAL
X is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
rng X is finite V63() V64() V65() Element of bool REAL
Sum X is V31() real ext-real Element of REAL
K190(REAL,X,addreal) is V31() real ext-real Element of REAL
f is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
rng f is finite V63() V64() V65() Element of bool REAL
Sum f is V31() real ext-real Element of REAL
K190(REAL,f,addreal) is V31() real ext-real Element of REAL
n is V31() real ext-real Element of REAL
<*n*> is V1() V4( NAT ) V5( REAL ) Function-like one-to-one non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V53() V54() V55() V57() V58() V59() V60() FinSequence of REAL
f ^ <*n*> is V1() V4( NAT ) V5( REAL ) Function-like non empty finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
rng (f ^ <*n*>) is finite V63() V64() V65() Element of bool REAL
Sum (f ^ <*n*>) is V31() real ext-real Element of REAL
K190(REAL,(f ^ <*n*>),addreal) is V31() real ext-real Element of REAL
rng <*n*> is finite V63() V64() V65() Element of bool REAL
(rng f) \/ (rng <*n*>) is finite V63() V64() V65() Element of bool REAL
{n} is non empty trivial finite 1 -element V63() V64() V65() Element of bool REAL
(Sum f) + n is V31() real ext-real Element of REAL
rng (<*> REAL) is finite V37() V63() V64() V65() V66() V67() V68() Element of bool REAL
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V164() RLSStruct
the carrier of X is non empty set
0. X is V113(X) left_complementable right_complementable complementable Element of the carrier of X
the ZeroF of X is left_complementable right_complementable complementable Element of the carrier of X
{(0. X)} is non empty trivial finite 1 -element Element of bool the carrier of X
bool the carrier of X is non empty set
f is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
rng f is finite Element of bool the carrier of X
Sum f is left_complementable right_complementable complementable Element of the carrier of X
n is left_complementable right_complementable complementable Element of the carrier of X
<*n*> is V1() V4( NAT ) V5( the carrier of X) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of X
f ^ <*n*> is V1() V4( NAT ) V5( the carrier of X) Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
rng (f ^ <*n*>) is finite Element of bool the carrier of X
Sum (f ^ <*n*>) is left_complementable right_complementable complementable Element of the carrier of X
rng <*n*> is finite Element of bool the carrier of X
(rng f) \/ (rng <*n*>) is finite Element of bool the carrier of X
{n} is non empty trivial finite 1 -element Element of bool the carrier of X
Sum <*n*> is left_complementable right_complementable complementable Element of the carrier of X
(Sum f) + (Sum <*n*>) is left_complementable right_complementable complementable Element of the carrier of X
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . ((Sum f),(Sum <*n*>)) is left_complementable right_complementable complementable Element of the carrier of X
[(Sum f),(Sum <*n*>)] is set
the addF of X . [(Sum f),(Sum <*n*>)] is set
(Sum f) + n is left_complementable right_complementable complementable Element of the carrier of X
the addF of X . ((Sum f),n) is left_complementable right_complementable complementable Element of the carrier of X
[(Sum f),n] is set
the addF of X . [(Sum f),n] is set
f is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
rng f is finite Element of bool the carrier of X
Sum f is left_complementable right_complementable complementable Element of the carrier of X
<*> the carrier of X is V1() V4( NAT ) V5( the carrier of X) Function-like functional empty ordinal natural V31() real finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() FinSequence of the carrier of X
rng (<*> the carrier of X) is finite V37() V63() V64() V65() V66() V67() V68() Element of bool the carrier of X
Sum (<*> the carrier of X) is left_complementable right_complementable complementable Element of the carrier of X
X is non empty RLSStruct
the carrier of X is non empty set
[: the carrier of X,ExtREAL:] is non empty V54() set
bool [: the carrier of X,ExtREAL:] is non empty set
f is V1() V4( the carrier of X) V5( ExtREAL ) Function-like non empty total quasi_total V54() Element of bool [: the carrier of X,ExtREAL:]
{ [b1,b2] where b1 is Element of the carrier of X, b2 is V31() real ext-real Element of REAL : f . b1 <= R_EAL b2 } is set
(X,()) is non empty RLSStruct
[: the carrier of X, the carrier of ():] is non empty set
0. X is V113(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
0. () is V113(()) left_complementable right_complementable complementable Element of the carrier of ()
the ZeroF of () is left_complementable right_complementable complementable Element of the carrier of ()
[(0. X),(0. ())] is Element of [: the carrier of X, the carrier of ():]
(X,()) is V1() V4([:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:]) V5([: the carrier of X, the carrier of ():]) Function-like non empty total quasi_total Element of bool [:[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:]
[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:] is non empty set
[:[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty set
bool [:[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty set
(X,()) is V1() V4([:REAL,[: the carrier of X, the carrier of ():]:]) V5([: the carrier of X, the carrier of ():]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:]
[:REAL,[: the carrier of X, the carrier of ():]:] is non empty non trivial non finite set
[:[:REAL,[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty non trivial non finite set
bool [:[:REAL,[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty non trivial non finite set
RLSStruct(# [: the carrier of X, the carrier of ():],[(0. X),(0. ())],(X,()),(X,()) #) is non empty strict RLSStruct
the carrier of (X,()) is non empty set
bool the carrier of (X,()) is non empty set
[: the carrier of X,REAL:] is non empty non trivial non finite V53() V54() V55() set
{ H1(b1,b2) where b1 is Element of the carrier of X, b2 is V31() real ext-real Element of REAL : S1[b1,b2] } is set
bool [: the carrier of X,REAL:] is non empty non trivial non finite set
X is non empty RLSStruct
the carrier of X is non empty set
[: the carrier of X,ExtREAL:] is non empty V54() set
bool [: the carrier of X,ExtREAL:] is non empty set
X is ext-real Element of ExtREAL
f is ext-real Element of ExtREAL
n is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
F is V31() real ext-real Element of REAL
F * n is V31() real ext-real Element of REAL
y is V31() real ext-real Element of REAL
y * p is V31() real ext-real Element of REAL
(F * n) + (y * p) is V31() real ext-real Element of REAL
R_EAL F is ext-real Element of ExtREAL
(R_EAL F) * X is ext-real Element of ExtREAL
R_EAL y is ext-real Element of ExtREAL
(R_EAL y) * f is ext-real Element of ExtREAL
((R_EAL F) * X) + ((R_EAL y) * f) is ext-real Element of ExtREAL
X is non empty RLSStruct
the carrier of X is non empty set
[: the carrier of X,ExtREAL:] is non empty V54() set
bool [: the carrier of X,ExtREAL:] is non empty set
f is V1() V4( the carrier of X) V5( ExtREAL ) Function-like non empty total quasi_total V54() Element of bool [: the carrier of X,ExtREAL:]
(X,()) is non empty RLSStruct
[: the carrier of X, the carrier of ():] is non empty set
0. X is V113(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
[(0. X),(0. ())] is Element of [: the carrier of X, the carrier of ():]
(X,()) is V1() V4([:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:]) V5([: the carrier of X, the carrier of ():]) Function-like non empty total quasi_total Element of bool [:[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:]
[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:] is non empty set
[:[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty set
bool [:[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty set
(X,()) is V1() V4([:REAL,[: the carrier of X, the carrier of ():]:]) V5([: the carrier of X, the carrier of ():]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:]
[:REAL,[: the carrier of X, the carrier of ():]:] is non empty non trivial non finite set
[:[:REAL,[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty non trivial non finite set
bool [:[:REAL,[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty non trivial non finite set
RLSStruct(# [: the carrier of X, the carrier of ():],[(0. X),(0. ())],(X,()),(X,()) #) is non empty strict RLSStruct
(X,f) is Element of bool the carrier of (X,())
the carrier of (X,()) is non empty set
bool the carrier of (X,()) is non empty set
{ [b1,b2] where b1 is Element of the carrier of X, b2 is V31() real ext-real Element of REAL : f . b1 <= R_EAL b2 } is set
n is Element of the carrier of X
p is Element of the carrier of X
f . n is ext-real Element of ExtREAL
f . p is ext-real Element of ExtREAL
F is V31() real ext-real Element of REAL
F * n is Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . (F,n) is set
[F,n] is set
the Mult of X . [F,n] is set
1 - F is V31() real ext-real Element of REAL
(1 - F) * p is Element of the carrier of X
the Mult of X . ((1 - F),p) is set
[(1 - F),p] is set
the Mult of X . [(1 - F),p] is set
(F * n) + ((1 - F) * p) is Element of the carrier of X
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . ((F * n),((1 - F) * p)) is Element of the carrier of X
[(F * n),((1 - F) * p)] is set
the addF of X . [(F * n),((1 - F) * p)] is set
f . ((F * n) + ((1 - F) * p)) is ext-real Element of ExtREAL
R_EAL F is ext-real Element of ExtREAL
(R_EAL F) * (f . n) is ext-real Element of ExtREAL
R_EAL (1 - F) is ext-real Element of ExtREAL
(R_EAL (1 - F)) * (f . p) is ext-real Element of ExtREAL
((R_EAL F) * (f . n)) + ((R_EAL (1 - F)) * (f . p)) is ext-real Element of ExtREAL
k is V31() real ext-real Element of REAL
[n,k] is Element of [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty non trivial non finite V53() V54() V55() set
s is V31() real ext-real Element of REAL
[p,s] is Element of [: the carrier of X,REAL:]
R_EAL s is ext-real Element of ExtREAL
s1 is Element of the carrier of (X,())
F * s1 is Element of the carrier of (X,())
the Mult of (X,()) is V1() V4([:REAL, the carrier of (X,()):]) V5( the carrier of (X,())) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of (X,()):], the carrier of (X,()):]
[:REAL, the carrier of (X,()):] is non empty non trivial non finite set
[:[:REAL, the carrier of (X,()):], the carrier of (X,()):] is non empty non trivial non finite set
bool [:[:REAL, the carrier of (X,()):], the carrier of (X,()):] is non empty non trivial non finite set
the Mult of (X,()) . (F,s1) is set
[F,s1] is set
the Mult of (X,()) . [F,s1] is set
F * k is V31() real ext-real Element of REAL
[(F * n),(F * k)] is Element of [: the carrier of X,REAL:]
F9 is Element of the carrier of (X,())
(1 - F) * F9 is Element of the carrier of (X,())
the Mult of (X,()) . ((1 - F),F9) is set
[(1 - F),F9] is set
the Mult of (X,()) . [(1 - F),F9] is set
(1 - F) * s is V31() real ext-real Element of REAL
[((1 - F) * p),((1 - F) * s)] is Element of [: the carrier of X,REAL:]
R_EAL k is ext-real Element of ExtREAL
(F * s1) + ((1 - F) * F9) is Element of the carrier of (X,())
the addF of (X,()) is V1() V4([: the carrier of (X,()), the carrier of (X,()):]) V5( the carrier of (X,())) Function-like non empty total quasi_total Element of bool [:[: the carrier of (X,()), the carrier of (X,()):], the carrier of (X,()):]
[: the carrier of (X,()), the carrier of (X,()):] is non empty set
[:[: the carrier of (X,()), the carrier of (X,()):], the carrier of (X,()):] is non empty set
bool [:[: the carrier of (X,()), the carrier of (X,()):], the carrier of (X,()):] is non empty set
the addF of (X,()) . ((F * s1),((1 - F) * F9)) is Element of the carrier of (X,())
[(F * s1),((1 - F) * F9)] is set
the addF of (X,()) . [(F * s1),((1 - F) * F9)] is set
(F * k) + ((1 - F) * s) is V31() real ext-real Element of REAL
[((F * n) + ((1 - F) * p)),((F * k) + ((1 - F) * s))] is Element of [: the carrier of X,REAL:]
z9 is Element of the carrier of X
p9 is V31() real ext-real Element of REAL
[z9,p9] is Element of [: the carrier of X,REAL:]
f . z9 is ext-real Element of ExtREAL
R_EAL p9 is ext-real Element of ExtREAL
s is V31() real ext-real Element of REAL
(1 - F) * s is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
F * s is V31() real ext-real Element of REAL
(X,()) is non empty RLSStruct
[: the carrier of X, the carrier of ():] is non empty set
0. X is V113(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
[(0. X),(0. ())] is Element of [: the carrier of X, the carrier of ():]
(X,()) is V1() V4([:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:]) V5([: the carrier of X, the carrier of ():]) Function-like non empty total quasi_total Element of bool [:[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:]
[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:] is non empty set
[:[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty set
bool [:[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty set
(X,()) is V1() V4([:REAL,[: the carrier of X, the carrier of ():]:]) V5([: the carrier of X, the carrier of ():]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:]
[:REAL,[: the carrier of X, the carrier of ():]:] is non empty non trivial non finite set
[:[:REAL,[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty non trivial non finite set
bool [:[:REAL,[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty non trivial non finite set
RLSStruct(# [: the carrier of X, the carrier of ():],[(0. X),(0. ())],(X,()),(X,()) #) is non empty strict RLSStruct
the carrier of (X,()) is non empty set
(X,f) is Element of bool the carrier of (X,())
bool the carrier of (X,()) is non empty set
{ [b1,b2] where b1 is Element of the carrier of X, b2 is V31() real ext-real Element of REAL : f . b1 <= R_EAL b2 } is set
n is Element of the carrier of (X,())
p is Element of the carrier of (X,())
F is V31() real ext-real Element of REAL
F * n is Element of the carrier of (X,())
the Mult of (X,()) is V1() V4([:REAL, the carrier of (X,()):]) V5( the carrier of (X,())) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of (X,()):], the carrier of (X,()):]
[:REAL, the carrier of (X,()):] is non empty non trivial non finite set
[:[:REAL, the carrier of (X,()):], the carrier of (X,()):] is non empty non trivial non finite set
bool [:[:REAL, the carrier of (X,()):], the carrier of (X,()):] is non empty non trivial non finite set
the Mult of (X,()) . (F,n) is set
[F,n] is set
the Mult of (X,()) . [F,n] is set
1 - F is V31() real ext-real Element of REAL
(1 - F) * p is Element of the carrier of (X,())
the Mult of (X,()) . ((1 - F),p) is set
[(1 - F),p] is set
the Mult of (X,()) . [(1 - F),p] is set
(F * n) + ((1 - F) * p) is Element of the carrier of (X,())
the addF of (X,()) is V1() V4([: the carrier of (X,()), the carrier of (X,()):]) V5( the carrier of (X,())) Function-like non empty total quasi_total Element of bool [:[: the carrier of (X,()), the carrier of (X,()):], the carrier of (X,()):]
[: the carrier of (X,()), the carrier of (X,()):] is non empty set
[:[: the carrier of (X,()), the carrier of (X,()):], the carrier of (X,()):] is non empty set
bool [:[: the carrier of (X,()), the carrier of (X,()):], the carrier of (X,()):] is non empty set
the addF of (X,()) . ((F * n),((1 - F) * p)) is Element of the carrier of (X,())
[(F * n),((1 - F) * p)] is set
the addF of (X,()) . [(F * n),((1 - F) * p)] is set
y is Element of the carrier of X
z is V31() real ext-real Element of REAL
[y,z] is Element of [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty non trivial non finite V53() V54() V55() set
f . y is ext-real Element of ExtREAL
R_EAL z is ext-real Element of ExtREAL
(1 - F) * y is Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . ((1 - F),y) is set
[(1 - F),y] is set
the Mult of X . [(1 - F),y] is set
(1 - F) * z is V31() real ext-real Element of REAL
[((1 - F) * y),((1 - F) * z)] is Element of [: the carrier of X,REAL:]
k is Element of the carrier of X
s1 is V31() real ext-real Element of REAL
[k,s1] is Element of [: the carrier of X,REAL:]
f . k is ext-real Element of ExtREAL
R_EAL s1 is ext-real Element of ExtREAL
s is V31() real ext-real Element of REAL
(1 - F) * s is V31() real ext-real Element of REAL
F9 is V31() real ext-real Element of REAL
F * F9 is V31() real ext-real Element of REAL
(F * F9) + ((1 - F) * s) is V31() real ext-real Element of REAL
(F * F9) + ((1 - F) * z) is V31() real ext-real Element of REAL
F * s1 is V31() real ext-real Element of REAL
(F * s1) + ((1 - F) * z) is V31() real ext-real Element of REAL
R_EAL ((F * F9) + ((1 - F) * s)) is ext-real Element of ExtREAL
R_EAL F is ext-real Element of ExtREAL
(R_EAL F) * (f . k) is ext-real Element of ExtREAL
R_EAL (1 - F) is ext-real Element of ExtREAL
(R_EAL (1 - F)) * (f . y) is ext-real Element of ExtREAL
((R_EAL F) * (f . k)) + ((R_EAL (1 - F)) * (f . y)) is ext-real Element of ExtREAL
F * k is Element of the carrier of X
the Mult of X . (F,k) is set
[F,k] is set
the Mult of X . [F,k] is set
(F * k) + ((1 - F) * y) is Element of the carrier of X
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . ((F * k),((1 - F) * y)) is Element of the carrier of X
[(F * k),((1 - F) * y)] is set
the addF of X . [(F * k),((1 - F) * y)] is set
f . ((F * k) + ((1 - F) * y)) is ext-real Element of ExtREAL
z9 is V31() real ext-real Element of REAL
R_EAL ((F * s1) + ((1 - F) * z)) is ext-real Element of ExtREAL
[((F * k) + ((1 - F) * y)),((F * s1) + ((1 - F) * z))] is Element of [: the carrier of X,REAL:]
[(F * k),(F * s1)] is Element of [: the carrier of X,REAL:]
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V164() RLSStruct
the carrier of X is non empty set
[: the carrier of X,ExtREAL:] is non empty V54() set
bool [: the carrier of X,ExtREAL:] is non empty set
f is V1() V4( the carrier of X) V5( ExtREAL ) Function-like non empty total quasi_total V54() Element of bool [: the carrier of X,ExtREAL:]
n is left_complementable right_complementable complementable Element of the carrier of X
p is left_complementable right_complementable complementable Element of the carrier of X
f . n is ext-real Element of ExtREAL
f . p is ext-real Element of ExtREAL
F is V31() real ext-real Element of REAL
F * n is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . (F,n) is set
[F,n] is set
the Mult of X . [F,n] is set
1 - F is V31() real ext-real Element of REAL
(1 - F) * p is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . ((1 - F),p) is set
[(1 - F),p] is set
the Mult of X . [(1 - F),p] is set
(F * n) + ((1 - F) * p) is left_complementable right_complementable complementable Element of the carrier of X
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . ((F * n),((1 - F) * p)) is left_complementable right_complementable complementable Element of the carrier of X
[(F * n),((1 - F) * p)] is set
the addF of X . [(F * n),((1 - F) * p)] is set
f . ((F * n) + ((1 - F) * p)) is ext-real Element of ExtREAL
R_EAL F is ext-real Element of ExtREAL
(R_EAL F) * (f . n) is ext-real Element of ExtREAL
R_EAL (1 - F) is ext-real Element of ExtREAL
(R_EAL (1 - F)) * (f . p) is ext-real Element of ExtREAL
((R_EAL F) * (f . n)) + ((R_EAL (1 - F)) * (f . p)) is ext-real Element of ExtREAL
0. X is V113(X) left_complementable right_complementable complementable Element of the carrier of X
the ZeroF of X is left_complementable right_complementable complementable Element of the carrier of X
0. X is V113(X) left_complementable right_complementable complementable Element of the carrier of X
the ZeroF of X is left_complementable right_complementable complementable Element of the carrier of X
F is V31() real ext-real Element of REAL
n is left_complementable right_complementable complementable Element of the carrier of X
F * n is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . (F,n) is set
[F,n] is set
the Mult of X . [F,n] is set
p is left_complementable right_complementable complementable Element of the carrier of X
1 - F is V31() real ext-real Element of REAL
(1 - F) * p is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . ((1 - F),p) is set
[(1 - F),p] is set
the Mult of X . [(1 - F),p] is set
(F * n) + ((1 - F) * p) is left_complementable right_complementable complementable Element of the carrier of X
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . ((F * n),((1 - F) * p)) is left_complementable right_complementable complementable Element of the carrier of X
[(F * n),((1 - F) * p)] is set
the addF of X . [(F * n),((1 - F) * p)] is set
f . ((F * n) + ((1 - F) * p)) is ext-real Element of ExtREAL
R_EAL F is ext-real Element of ExtREAL
f . n is ext-real Element of ExtREAL
(R_EAL F) * (f . n) is ext-real Element of ExtREAL
R_EAL (1 - F) is ext-real Element of ExtREAL
f . p is ext-real Element of ExtREAL
(R_EAL (1 - F)) * (f . p) is ext-real Element of ExtREAL
((R_EAL F) * (f . n)) + ((R_EAL (1 - F)) * (f . p)) is ext-real Element of ExtREAL
[: the carrier of (),ExtREAL:] is non empty V54() set
bool [: the carrier of (),ExtREAL:] is non empty set
bool the carrier of () is non empty set
X is V1() V4( REAL ) V5( REAL ) Function-like V53() V54() V55() Element of bool [:REAL,REAL:]
dom X is V63() V64() V65() Element of bool REAL
f is V1() V4( the carrier of ()) V5( ExtREAL ) Function-like non empty total quasi_total V54() Element of bool [: the carrier of (),ExtREAL:]
n is Element of bool the carrier of ()
p is left_complementable right_complementable complementable Element of the carrier of ()
f . p is ext-real Element of ExtREAL
F is V31() real ext-real Element of REAL
X . F is V31() real ext-real Element of REAL
p is left_complementable right_complementable complementable Element of the carrier of ()
f . p is ext-real Element of ExtREAL
F is V31() real ext-real Element of REAL
f . F is ext-real Element of ExtREAL
X . F is V31() real ext-real Element of REAL
p is V31() real ext-real Element of REAL
1 - p is V31() real ext-real Element of REAL
F is V31() real ext-real Element of REAL
y is V31() real ext-real Element of REAL
p * F is V31() real ext-real Element of REAL
(1 - p) * y is V31() real ext-real Element of REAL
(p * F) + ((1 - p) * y) is V31() real ext-real Element of REAL
X . ((p * F) + ((1 - p) * y)) is V31() real ext-real Element of REAL
X . F is V31() real ext-real Element of REAL
p * (X . F) is V31() real ext-real Element of REAL
X . y is V31() real ext-real Element of REAL
(1 - p) * (X . y) is V31() real ext-real Element of REAL
(p * (X . F)) + ((1 - p) * (X . y)) is V31() real ext-real Element of REAL
f . F is ext-real Element of ExtREAL
f . ((p * F) + ((1 - p) * y)) is ext-real Element of ExtREAL
f . y is ext-real Element of ExtREAL
z is left_complementable right_complementable complementable Element of the carrier of ()
(1 - p) * z is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () is V1() V4([:REAL, the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is non empty non trivial non finite set
[:[:REAL, the carrier of ():], the carrier of ():] is non empty non trivial non finite set
bool [:[:REAL, the carrier of ():], the carrier of ():] is non empty non trivial non finite set
the Mult of () . ((1 - p),z) is set
[(1 - p),z] is set
the Mult of () . [(1 - p),z] is set
s is left_complementable right_complementable complementable Element of the carrier of ()
p * s is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () . (p,s) is set
[p,s] is set
the Mult of () . [p,s] is set
(p * s) + ((1 - p) * z) is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () is V1() V4([: the carrier of (), the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . ((p * s),((1 - p) * z)) is left_complementable right_complementable complementable Element of the carrier of ()
[(p * s),((1 - p) * z)] is set
the addF of () . [(p * s),((1 - p) * z)] is set
f . ((p * s) + ((1 - p) * z)) is ext-real Element of ExtREAL
X . s is V31() real ext-real Element of REAL
p * (X . s) is V31() real ext-real Element of REAL
X . z is V31() real ext-real Element of REAL
(1 - p) * (X . z) is V31() real ext-real Element of REAL
(p * (X . s)) + ((1 - p) * (X . z)) is V31() real ext-real Element of REAL
R_EAL p is ext-real Element of ExtREAL
f . s is ext-real Element of ExtREAL
(R_EAL p) * (f . s) is ext-real Element of ExtREAL
R_EAL (1 - p) is ext-real Element of ExtREAL
f . z is ext-real Element of ExtREAL
(R_EAL (1 - p)) * (f . z) is ext-real Element of ExtREAL
((R_EAL p) * (f . s)) + ((R_EAL (1 - p)) * (f . z)) is ext-real Element of ExtREAL
p is left_complementable right_complementable complementable Element of the carrier of ()
F is left_complementable right_complementable complementable Element of the carrier of ()
y is V31() real ext-real Element of REAL
y * p is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () is V1() V4([:REAL, the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is non empty non trivial non finite set
[:[:REAL, the carrier of ():], the carrier of ():] is non empty non trivial non finite set
bool [:[:REAL, the carrier of ():], the carrier of ():] is non empty non trivial non finite set
the Mult of () . (y,p) is set
[y,p] is set
the Mult of () . [y,p] is set
1 - y is V31() real ext-real Element of REAL
(1 - y) * F is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () . ((1 - y),F) is set
[(1 - y),F] is set
the Mult of () . [(1 - y),F] is set
(y * p) + ((1 - y) * F) is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () is V1() V4([: the carrier of (), the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . ((y * p),((1 - y) * F)) is left_complementable right_complementable complementable Element of the carrier of ()
[(y * p),((1 - y) * F)] is set
the addF of () . [(y * p),((1 - y) * F)] is set
f . p is ext-real Element of ExtREAL
f . F is ext-real Element of ExtREAL
z is V31() real ext-real Element of REAL
y * z is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
(1 - y) * s is V31() real ext-real Element of REAL
(y * z) + ((1 - y) * s) is V31() real ext-real Element of REAL
R_EAL y is ext-real Element of ExtREAL
(R_EAL y) * (f . p) is ext-real Element of ExtREAL
R_EAL (1 - y) is ext-real Element of ExtREAL
(R_EAL (1 - y)) * (f . F) is ext-real Element of ExtREAL
((R_EAL y) * (f . p)) + ((R_EAL (1 - y)) * (f . F)) is ext-real Element of ExtREAL
f . ((y * p) + ((1 - y) * F)) is ext-real Element of ExtREAL
p is left_complementable right_complementable complementable Element of the carrier of ()
F is left_complementable right_complementable complementable Element of the carrier of ()
f . p is ext-real Element of ExtREAL
f . F is ext-real Element of ExtREAL
y is V31() real ext-real Element of REAL
y * p is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () is V1() V4([:REAL, the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is non empty non trivial non finite set
[:[:REAL, the carrier of ():], the carrier of ():] is non empty non trivial non finite set
bool [:[:REAL, the carrier of ():], the carrier of ():] is non empty non trivial non finite set
the Mult of () . (y,p) is set
[y,p] is set
the Mult of () . [y,p] is set
1 - y is V31() real ext-real Element of REAL
(1 - y) * F is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () . ((1 - y),F) is set
[(1 - y),F] is set
the Mult of () . [(1 - y),F] is set
(y * p) + ((1 - y) * F) is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () is V1() V4([: the carrier of (), the carrier of ():]) V5( the carrier of ()) Function-like non empty total quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . ((y * p),((1 - y) * F)) is left_complementable right_complementable complementable Element of the carrier of ()
[(y * p),((1 - y) * F)] is set
the addF of () . [(y * p),((1 - y) * F)] is set
f . ((y * p) + ((1 - y) * F)) is ext-real Element of ExtREAL
R_EAL y is ext-real Element of ExtREAL
(R_EAL y) * (f . p) is ext-real Element of ExtREAL
R_EAL (1 - y) is ext-real Element of ExtREAL
(R_EAL (1 - y)) * (f . F) is ext-real Element of ExtREAL
((R_EAL y) * (f . p)) + ((R_EAL (1 - y)) * (f . F)) is ext-real Element of ExtREAL
z is V31() real ext-real Element of REAL
X . z is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
X . s is V31() real ext-real Element of REAL
y * (X . s) is V31() real ext-real Element of REAL
(1 - y) * (X . z) is V31() real ext-real Element of REAL
(y * (X . s)) + ((1 - y) * (X . z)) is V31() real ext-real Element of REAL
(1 - y) * z is V31() real ext-real Element of REAL
y * s is V31() real ext-real Element of REAL
(y * s) + ((1 - y) * z) is V31() real ext-real Element of REAL
X . ((y * s) + ((1 - y) * z)) is V31() real ext-real Element of REAL
z is V31() real ext-real Element of REAL
f . z is ext-real Element of ExtREAL
s is V31() real ext-real Element of REAL
f . s is ext-real Element of ExtREAL
k is V31() real ext-real Element of REAL
y * k is V31() real ext-real Element of REAL
s is V31() real ext-real Element of REAL
f . s is ext-real Element of ExtREAL
z is V31() real ext-real Element of REAL
f . z is ext-real Element of ExtREAL
k is V31() real ext-real Element of REAL
(1 - y) * k is V31() real ext-real Element of REAL
z is V31() real ext-real Element of REAL
f . z is ext-real Element of ExtREAL
s is V31() real ext-real Element of REAL
f . s is ext-real Element of ExtREAL
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V164() RLSStruct
the carrier of X is non empty set
bool the carrier of X is non empty set
f is Element of bool the carrier of X
n is non empty ordinal natural V31() real finite cardinal ext-real positive non negative set
Seg n is non empty finite n -element V63() V64() V65() V66() V67() V68() Element of bool NAT
n + 1 is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg (n + 1) is non empty finite n + 1 -element V63() V64() V65() V66() V67() V68() Element of bool NAT
p is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
len p is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum p is V31() real ext-real Element of REAL
K190(REAL,p,addreal) is V31() real ext-real Element of REAL
F is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
len F is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
y is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
len y is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum y is left_complementable right_complementable complementable Element of the carrier of X
p . (n + 1) is V31() real ext-real Element of REAL
1 - (p . (n + 1)) is V31() real ext-real Element of REAL
p | n is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
dom (p | n) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
len (p | n) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg (len (p | n)) is finite len (p | n) -element V63() V64() V65() V66() V67() V68() Element of bool NAT
p . 1 is V31() real ext-real Element of REAL
(p | n) . 1 is V31() real ext-real Element of REAL
p | (Seg n) is V1() V4( NAT ) V5( REAL ) Function-like finite FinSubsequence-like V53() V54() V55() Element of bool [:NAT,REAL:]
[:NAT,REAL:] is non trivial non finite V53() V54() V55() set
bool [:NAT,REAL:] is non empty non trivial non finite set
<*(p . (n + 1))*> is V1() V4( NAT ) V5( REAL ) Function-like one-to-one non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V53() V54() V55() V57() V58() V59() V60() FinSequence of REAL
(p | n) ^ <*(p . (n + 1))*> is V1() V4( NAT ) V5( REAL ) Function-like non empty finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
Sum (p | n) is V31() real ext-real Element of REAL
K190(REAL,(p | n),addreal) is V31() real ext-real Element of REAL
(Sum (p | n)) + (p . (n + 1)) is V31() real ext-real Element of REAL
0 + n is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
1 + n is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s is ordinal natural V31() real finite cardinal ext-real non negative set
(p | n) . s is V31() real ext-real Element of REAL
p . s is V31() real ext-real Element of REAL
F | n is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
1 / (1 - (p . (n + 1))) is V31() real ext-real Element of REAL
(1 / (1 - (p . (n + 1)))) * (p | n) is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
(1 / (1 - (p . (n + 1)))) multreal is V1() V4( REAL ) V5( REAL ) Function-like non empty total quasi_total V53() V54() V55() Element of bool [:REAL,REAL:]
id REAL is V1() V4( REAL ) V5( REAL ) non empty total quasi_total V53() V54() V55() Element of bool [:REAL,REAL:]
K386(multreal,(1 / (1 - (p . (n + 1)))),(id REAL)) is set
((1 / (1 - (p . (n + 1)))) multreal) * (p | n) is V1() finite V53() V54() V55() set
s1 is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
len s1 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
dom s1 is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
len (F | n) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
dom (F | n) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
y | n is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
F9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(y | n) . F9 is set
s1 . F9 is set
z9 is left_complementable right_complementable complementable Element of the carrier of X
(1 / (1 - (p . (n + 1)))) * z9 is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . ((1 / (1 - (p . (n + 1)))),z9) is set
[(1 / (1 - (p . (n + 1)))),z9] is set
the Mult of X . [(1 / (1 - (p . (n + 1)))),z9] is set
(F | n) /. F9 is left_complementable right_complementable complementable Element of the carrier of X
F /. F9 is left_complementable right_complementable complementable Element of the carrier of X
y . F9 is set
((1 / (1 - (p . (n + 1)))) * (p | n)) . F9 is V31() real ext-real Element of REAL
(((1 / (1 - (p . (n + 1)))) * (p | n)) . F9) * ((F | n) /. F9) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . ((((1 / (1 - (p . (n + 1)))) * (p | n)) . F9),((F | n) /. F9)) is set
[(((1 / (1 - (p . (n + 1)))) * (p | n)) . F9),((F | n) /. F9)] is set
the Mult of X . [(((1 / (1 - (p . (n + 1)))) * (p | n)) . F9),((F | n) /. F9)] is set
(p | n) . F9 is V31() real ext-real Element of REAL
(1 / (1 - (p . (n + 1)))) * ((p | n) . F9) is V31() real ext-real Element of REAL
((1 / (1 - (p . (n + 1)))) * ((p | n) . F9)) * ((F | n) /. F9) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . (((1 / (1 - (p . (n + 1)))) * ((p | n) . F9)),((F | n) /. F9)) is set
[((1 / (1 - (p . (n + 1)))) * ((p | n) . F9)),((F | n) /. F9)] is set
the Mult of X . [((1 / (1 - (p . (n + 1)))) * ((p | n) . F9)),((F | n) /. F9)] is set
p . F9 is V31() real ext-real Element of REAL
(1 / (1 - (p . (n + 1)))) * (p . F9) is V31() real ext-real Element of REAL
((1 / (1 - (p . (n + 1)))) * (p . F9)) * ((F | n) /. F9) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . (((1 / (1 - (p . (n + 1)))) * (p . F9)),((F | n) /. F9)) is set
[((1 / (1 - (p . (n + 1)))) * (p . F9)),((F | n) /. F9)] is set
the Mult of X . [((1 / (1 - (p . (n + 1)))) * (p . F9)),((F | n) /. F9)] is set
(p . F9) * ((F | n) /. F9) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . ((p . F9),((F | n) /. F9)) is set
[(p . F9),((F | n) /. F9)] is set
the Mult of X . [(p . F9),((F | n) /. F9)] is set
(1 / (1 - (p . (n + 1)))) * ((p . F9) * ((F | n) /. F9)) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . ((1 / (1 - (p . (n + 1)))),((p . F9) * ((F | n) /. F9))) is set
[(1 / (1 - (p . (n + 1)))),((p . F9) * ((F | n) /. F9))] is set
the Mult of X . [(1 / (1 - (p . (n + 1)))),((p . F9) * ((F | n) /. F9))] is set
dom ((1 / (1 - (p . (n + 1)))) * (p | n)) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
len ((1 / (1 - (p . (n + 1)))) * (p | n)) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg (len ((1 / (1 - (p . (n + 1)))) * (p | n))) is finite len ((1 / (1 - (p . (n + 1)))) * (p | n)) -element V63() V64() V65() V66() V67() V68() Element of bool NAT
F /. (n + 1) is left_complementable right_complementable complementable Element of the carrier of X
y | (Seg n) is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of X:]
[:NAT, the carrier of X:] is non trivial non finite set
bool [:NAT, the carrier of X:] is non empty non trivial non finite set
y . (n + 1) is set
<*(y . (n + 1))*> is V1() V4( NAT ) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
(y | n) ^ <*(y . (n + 1))*> is V1() V4( NAT ) Function-like non empty finite FinSequence-like FinSubsequence-like set
(p . (n + 1)) * (F /. (n + 1)) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . ((p . (n + 1)),(F /. (n + 1))) is set
[(p . (n + 1)),(F /. (n + 1))] is set
the Mult of X . [(p . (n + 1)),(F /. (n + 1))] is set
Sum (y | n) is left_complementable right_complementable complementable Element of the carrier of X
<*((p . (n + 1)) * (F /. (n + 1)))*> is V1() V4( NAT ) V5( the carrier of X) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of X
Sum <*((p . (n + 1)) * (F /. (n + 1)))*> is left_complementable right_complementable complementable Element of the carrier of X
(Sum (y | n)) + (Sum <*((p . (n + 1)) * (F /. (n + 1)))*>) is left_complementable right_complementable complementable Element of the carrier of X
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . ((Sum (y | n)),(Sum <*((p . (n + 1)) * (F /. (n + 1)))*>)) is left_complementable right_complementable complementable Element of the carrier of X
[(Sum (y | n)),(Sum <*((p . (n + 1)) * (F /. (n + 1)))*>)] is set
the addF of X . [(Sum (y | n)),(Sum <*((p . (n + 1)) * (F /. (n + 1)))*>)] is set
1 - (1 - (p . (n + 1))) is V31() real ext-real Element of REAL
(1 - (1 - (p . (n + 1)))) * (F /. (n + 1)) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . ((1 - (1 - (p . (n + 1)))),(F /. (n + 1))) is set
[(1 - (1 - (p . (n + 1)))),(F /. (n + 1))] is set
the Mult of X . [(1 - (1 - (p . (n + 1)))),(F /. (n + 1))] is set
(Sum (y | n)) + ((1 - (1 - (p . (n + 1)))) * (F /. (n + 1))) is left_complementable right_complementable complementable Element of the carrier of X
the addF of X . ((Sum (y | n)),((1 - (1 - (p . (n + 1)))) * (F /. (n + 1)))) is left_complementable right_complementable complementable Element of the carrier of X
[(Sum (y | n)),((1 - (1 - (p . (n + 1)))) * (F /. (n + 1)))] is set
the addF of X . [(Sum (y | n)),((1 - (1 - (p . (n + 1)))) * (F /. (n + 1)))] is set
(1 - (p . (n + 1))) " is V31() real ext-real Element of REAL
F9 is ordinal natural V31() real finite cardinal ext-real non negative set
((1 / (1 - (p . (n + 1)))) * (p | n)) . F9 is V31() real ext-real Element of REAL
s1 . F9 is set
(F | n) /. F9 is left_complementable right_complementable complementable Element of the carrier of X
(((1 / (1 - (p . (n + 1)))) * (p | n)) . F9) * ((F | n) /. F9) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . ((((1 / (1 - (p . (n + 1)))) * (p | n)) . F9),((F | n) /. F9)) is set
[(((1 / (1 - (p . (n + 1)))) * (p | n)) . F9),((F | n) /. F9)] is set
the Mult of X . [(((1 / (1 - (p . (n + 1)))) * (p | n)) . F9),((F | n) /. F9)] is set
(p | n) . F9 is V31() real ext-real Element of REAL
(1 / (1 - (p . (n + 1)))) * ((p | n) . F9) is V31() real ext-real Element of REAL
p . F9 is V31() real ext-real Element of REAL
(1 / (1 - (p . (n + 1)))) * (p . F9) is V31() real ext-real Element of REAL
F /. F9 is left_complementable right_complementable complementable Element of the carrier of X
len (y | n) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum s1 is left_complementable right_complementable complementable Element of the carrier of X
(1 - (p . (n + 1))) * (Sum s1) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . ((1 - (p . (n + 1))),(Sum s1)) is set
[(1 - (p . (n + 1))),(Sum s1)] is set
the Mult of X . [(1 - (p . (n + 1))),(Sum s1)] is set
(1 / (1 - (p . (n + 1)))) * (Sum (y | n)) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . ((1 / (1 - (p . (n + 1)))),(Sum (y | n))) is set
[(1 / (1 - (p . (n + 1)))),(Sum (y | n))] is set
the Mult of X . [(1 / (1 - (p . (n + 1)))),(Sum (y | n))] is set
(1 - (p . (n + 1))) * ((1 / (1 - (p . (n + 1)))) * (Sum (y | n))) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . ((1 - (p . (n + 1))),((1 / (1 - (p . (n + 1)))) * (Sum (y | n)))) is set
[(1 - (p . (n + 1))),((1 / (1 - (p . (n + 1)))) * (Sum (y | n)))] is set
the Mult of X . [(1 - (p . (n + 1))),((1 / (1 - (p . (n + 1)))) * (Sum (y | n)))] is set
(1 - (p . (n + 1))) * (1 / (1 - (p . (n + 1)))) is V31() real ext-real Element of REAL
((1 - (p . (n + 1))) * (1 / (1 - (p . (n + 1))))) * (Sum (y | n)) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . (((1 - (p . (n + 1))) * (1 / (1 - (p . (n + 1))))),(Sum (y | n))) is set
[((1 - (p . (n + 1))) * (1 / (1 - (p . (n + 1))))),(Sum (y | n))] is set
the Mult of X . [((1 - (p . (n + 1))) * (1 / (1 - (p . (n + 1))))),(Sum (y | n))] is set
1 * (Sum (y | n)) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . (1,(Sum (y | n))) is set
[1,(Sum (y | n))] is set
the Mult of X . [1,(Sum (y | n))] is set
Sum ((1 / (1 - (p . (n + 1)))) * (p | n)) is V31() real ext-real Element of REAL
K190(REAL,((1 / (1 - (p . (n + 1)))) * (p | n)),addreal) is V31() real ext-real Element of REAL
(1 / (1 - (p . (n + 1)))) * (1 - (p . (n + 1))) is V31() real ext-real Element of REAL
n is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
len n is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum n is V31() real ext-real Element of REAL
K190(REAL,n,addreal) is V31() real ext-real Element of REAL
p is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
len p is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
len F is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum F is left_complementable right_complementable complementable Element of the carrier of X
n . 1 is V31() real ext-real Element of REAL
<*(n . 1)*> is V1() V4( NAT ) V5( REAL ) Function-like one-to-one non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V53() V54() V55() V57() V58() V59() V60() FinSequence of REAL
F . 1 is set
p /. 1 is left_complementable right_complementable complementable Element of the carrier of X
(n . 1) * (p /. 1) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . ((n . 1),(p /. 1)) is set
[(n . 1),(p /. 1)] is set
the Mult of X . [(n . 1),(p /. 1)] is set
<*(F . 1)*> is V1() V4( NAT ) Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
n is left_complementable right_complementable complementable Element of the carrier of X
p is left_complementable right_complementable complementable Element of the carrier of X
F is V31() real ext-real Element of REAL
F * n is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . (F,n) is set
[F,n] is set
the Mult of X . [F,n] is set
1 - F is V31() real ext-real Element of REAL
(1 - F) * p is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . ((1 - F),p) is set
[(1 - F),p] is set
the Mult of X . [(1 - F),p] is set
(F * n) + ((1 - F) * p) is left_complementable right_complementable complementable Element of the carrier of X
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . ((F * n),((1 - F) * p)) is left_complementable right_complementable complementable Element of the carrier of X
[(F * n),((1 - F) * p)] is set
the addF of X . [(F * n),((1 - F) * p)] is set
<*(F * n),((1 - F) * p)*> is V1() V4( NAT ) V5( the carrier of X) Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of X
<*n,p*> is V1() V4( NAT ) V5( the carrier of X) Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of X
<*F,(1 - F)*> is V1() V4( NAT ) V5( REAL ) Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
k is ordinal natural V31() real finite cardinal ext-real non negative set
<*F,(1 - F)*> . k is V31() real ext-real Element of REAL
<*(F * n),((1 - F) * p)*> . k is set
<*n,p*> /. k is left_complementable right_complementable complementable Element of the carrier of X
(<*F,(1 - F)*> . k) * (<*n,p*> /. k) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . ((<*F,(1 - F)*> . k),(<*n,p*> /. k)) is set
[(<*F,(1 - F)*> . k),(<*n,p*> /. k)] is set
the Mult of X . [(<*F,(1 - F)*> . k),(<*n,p*> /. k)] is set
len <*n,p*> is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum <*F,(1 - F)*> is V31() real ext-real Element of REAL
K190(REAL,<*F,(1 - F)*>,addreal) is V31() real ext-real Element of REAL
F + (1 - F) is V31() real ext-real Element of REAL
len <*(F * n),((1 - F) * p)*> is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
len <*F,(1 - F)*> is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum <*(F * n),((1 - F) * p)*> is left_complementable right_complementable complementable Element of the carrier of X
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V164() RLSStruct
the carrier of X is non empty set
[: the carrier of X,ExtREAL:] is non empty V54() set
bool [: the carrier of X,ExtREAL:] is non empty set
f is V1() V4( the carrier of X) V5( ExtREAL ) Function-like non empty total quasi_total V54() Element of bool [: the carrier of X,ExtREAL:]
n is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg n is non empty finite n -element V63() V64() V65() V66() V67() V68() Element of bool NAT
p is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
F is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len F is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
rng F is finite V64() Element of bool ExtREAL
y is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
dom F is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
z is set
F . z is ext-real Element of ExtREAL
s is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
p . s is V31() real ext-real Element of REAL
F . s is ext-real Element of ExtREAL
R_EAL (p . s) is ext-real Element of ExtREAL
y /. s is left_complementable right_complementable complementable Element of the carrier of X
f . (y /. s) is ext-real Element of ExtREAL
(R_EAL (p . s)) * (f . (y /. s)) is ext-real Element of ExtREAL
k is V31() real ext-real Element of REAL
(p . s) * k is V31() real ext-real Element of REAL
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V164() RLSStruct
the carrier of X is non empty set
[: the carrier of X,ExtREAL:] is non empty V54() set
bool [: the carrier of X,ExtREAL:] is non empty set
f is V1() V4( the carrier of X) V5( ExtREAL ) Function-like non empty total quasi_total V54() Element of bool [: the carrier of X,ExtREAL:]
n is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg n is non empty finite n -element V63() V64() V65() V66() V67() V68() Element of bool NAT
p is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
len p is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum p is V31() real ext-real Element of REAL
K190(REAL,p,addreal) is V31() real ext-real Element of REAL
F is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len F is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum F is ext-real Element of ExtREAL
y is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
len y is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
z is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
len z is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum z is left_complementable right_complementable complementable Element of the carrier of X
f . (Sum z) is ext-real Element of ExtREAL
s is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
p . s is V31() real ext-real Element of REAL
F . s is ext-real Element of ExtREAL
R_EAL (p . s) is ext-real Element of ExtREAL
y /. s is left_complementable right_complementable complementable Element of the carrier of X
f . (y /. s) is ext-real Element of ExtREAL
(R_EAL (p . s)) * (f . (y /. s)) is ext-real Element of ExtREAL
rng F is finite V64() Element of bool ExtREAL
(X,()) is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V164() RLSStruct
[: the carrier of X, the carrier of ():] is non empty set
0. X is V113(X) left_complementable right_complementable complementable Element of the carrier of X
the ZeroF of X is left_complementable right_complementable complementable Element of the carrier of X
[(0. X),(0. ())] is Element of [: the carrier of X, the carrier of ():]
(X,()) is V1() V4([:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:]) V5([: the carrier of X, the carrier of ():]) Function-like non empty total quasi_total Element of bool [:[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:]
[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:] is non empty set
[:[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty set
bool [:[:[: the carrier of X, the carrier of ():],[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty set
(X,()) is V1() V4([:REAL,[: the carrier of X, the carrier of ():]:]) V5([: the carrier of X, the carrier of ():]) Function-like non empty total quasi_total Element of bool [:[:REAL,[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:]
[:REAL,[: the carrier of X, the carrier of ():]:] is non empty non trivial non finite set
[:[:REAL,[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty non trivial non finite set
bool [:[:REAL,[: the carrier of X, the carrier of ():]:],[: the carrier of X, the carrier of ():]:] is non empty non trivial non finite set
RLSStruct(# [: the carrier of X, the carrier of ():],[(0. X),(0. ())],(X,()),(X,()) #) is non empty strict RLSStruct
k is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
y /. k is left_complementable right_complementable complementable Element of the carrier of X
f . (y /. k) is ext-real Element of ExtREAL
s is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V164() RLSStruct
the carrier of s is non empty set
k is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
y /. k is left_complementable right_complementable complementable Element of the carrier of X
f . (y /. k) is ext-real Element of ExtREAL
[(y /. k),(f . (y /. k))] is Element of [: the carrier of X,ExtREAL:]
s1 is V31() real ext-real Element of REAL
[(y /. k),s1] is Element of [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty non trivial non finite V53() V54() V55() set
z9 is left_complementable right_complementable complementable Element of the carrier of s
k is V1() V4( NAT ) V5( the carrier of s) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
dom k is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
len k is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s1 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
F . s1 is ext-real Element of ExtREAL
y /. s1 is left_complementable right_complementable complementable Element of the carrier of X
f . (y /. s1) is ext-real Element of ExtREAL
p . s1 is V31() real ext-real Element of REAL
R_EAL (p . s1) is ext-real Element of ExtREAL
(R_EAL (p . s1)) * (f . (y /. s1)) is ext-real Element of ExtREAL
F9 is V31() real ext-real Element of REAL
(p . s1) * F9 is V31() real ext-real Element of REAL
z9 is left_complementable right_complementable complementable Element of the carrier of ()
s1 is V1() V4( NAT ) V5( the carrier of ()) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
dom s1 is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
len s1 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
bool the carrier of s is non empty set
(X,f) is Element of bool the carrier of (X,())
the carrier of (X,()) is non empty set
bool the carrier of (X,()) is non empty set
{ [b1,b2] where b1 is Element of the carrier of X, b2 is V31() real ext-real Element of REAL : f . b1 <= R_EAL b2 } is set
z9 is V1() V4( NAT ) V5( the carrier of s) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of s
len z9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
dom z9 is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
F9 is Element of bool the carrier of s
p9 is ordinal natural V31() real finite cardinal ext-real non negative set
p . p9 is V31() real ext-real Element of REAL
z9 . p9 is set
k /. p9 is left_complementable right_complementable complementable Element of the carrier of s
(p . p9) * (k /. p9) is left_complementable right_complementable complementable Element of the carrier of s
the Mult of s is V1() V4([:REAL, the carrier of s:]) V5( the carrier of s) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of s:], the carrier of s:]
[:REAL, the carrier of s:] is non empty non trivial non finite set
[:[:REAL, the carrier of s:], the carrier of s:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of s:], the carrier of s:] is non empty non trivial non finite set
the Mult of s . ((p . p9),(k /. p9)) is set
[(p . p9),(k /. p9)] is set
the Mult of s . [(p . p9),(k /. p9)] is set
y /. p9 is left_complementable right_complementable complementable Element of the carrier of X
f . (y /. p9) is ext-real Element of ExtREAL
k9 is V31() real ext-real Element of REAL
R_EAL k9 is ext-real Element of ExtREAL
[(y /. p9),k9] is Element of [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty non trivial non finite V53() V54() V55() set
Sum z9 is left_complementable right_complementable complementable Element of the carrier of s
p9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s1 . p9 is set
F . p9 is ext-real Element of ExtREAL
s1 /. p9 is left_complementable right_complementable complementable Element of the carrier of ()
p9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
z9 . p9 is set
z . p9 is set
s1 . p9 is set
[(z . p9),(s1 . p9)] is set
y /. p9 is left_complementable right_complementable complementable Element of the carrier of X
f . (y /. p9) is ext-real Element of ExtREAL
k /. p9 is left_complementable right_complementable complementable Element of the carrier of s
k9 is V31() real ext-real Element of REAL
[(y /. p9),k9] is Element of [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty non trivial non finite V53() V54() V55() set
p . p9 is V31() real ext-real Element of REAL
(p . p9) * (k /. p9) is left_complementable right_complementable complementable Element of the carrier of s
the Mult of s is V1() V4([:REAL, the carrier of s:]) V5( the carrier of s) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of s:], the carrier of s:]
[:REAL, the carrier of s:] is non empty non trivial non finite set
[:[:REAL, the carrier of s:], the carrier of s:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of s:], the carrier of s:] is non empty non trivial non finite set
the Mult of s . ((p . p9),(k /. p9)) is set
[(p . p9),(k /. p9)] is set
the Mult of s . [(p . p9),(k /. p9)] is set
(p . p9) * (y /. p9) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . ((p . p9),(y /. p9)) is set
[(p . p9),(y /. p9)] is set
the Mult of X . [(p . p9),(y /. p9)] is set
(p . p9) * k9 is V31() real ext-real Element of REAL
[((p . p9) * (y /. p9)),((p . p9) * k9)] is Element of [: the carrier of X,REAL:]
[(z . p9),((p . p9) * k9)] is set
F . p9 is ext-real Element of ExtREAL
R_EAL (p . p9) is ext-real Element of ExtREAL
(R_EAL (p . p9)) * (f . (y /. p9)) is ext-real Element of ExtREAL
Sum s1 is left_complementable right_complementable complementable Element of the carrier of ()
[(Sum z),(Sum s1)] is Element of [: the carrier of X, the carrier of ():]
[(Sum z),(Sum F)] is Element of [: the carrier of X,ExtREAL:]
p9 is left_complementable right_complementable complementable Element of the carrier of X
k9 is V31() real ext-real Element of REAL
[p9,k9] is Element of [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty non trivial non finite V53() V54() V55() set
f . p9 is ext-real Element of ExtREAL
R_EAL k9 is ext-real Element of ExtREAL
s is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
y /. s is left_complementable right_complementable complementable Element of the carrier of X
f . (y /. s) is ext-real Element of ExtREAL
s is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
y /. s is left_complementable right_complementable complementable Element of the carrier of X
f . (y /. s) is ext-real Element of ExtREAL
F . s is ext-real Element of ExtREAL
p . s is V31() real ext-real Element of REAL
R_EAL (p . s) is ext-real Element of ExtREAL
(R_EAL (p . s)) * (f . (y /. s)) is ext-real Element of ExtREAL
dom F is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
s is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
y /. s is left_complementable right_complementable complementable Element of the carrier of X
f . (y /. s) is ext-real Element of ExtREAL
p is left_complementable right_complementable complementable Element of the carrier of X
F is left_complementable right_complementable complementable Element of the carrier of X
f . p is ext-real Element of ExtREAL
f . F is ext-real Element of ExtREAL
y is V31() real ext-real Element of REAL
y * p is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . (y,p) is set
[y,p] is set
the Mult of X . [y,p] is set
1 - y is V31() real ext-real Element of REAL
(1 - y) * F is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . ((1 - y),F) is set
[(1 - y),F] is set
the Mult of X . [(1 - y),F] is set
(y * p) + ((1 - y) * F) is left_complementable right_complementable complementable Element of the carrier of X
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . ((y * p),((1 - y) * F)) is left_complementable right_complementable complementable Element of the carrier of X
[(y * p),((1 - y) * F)] is set
the addF of X . [(y * p),((1 - y) * F)] is set
f . ((y * p) + ((1 - y) * F)) is ext-real Element of ExtREAL
R_EAL y is ext-real Element of ExtREAL
(R_EAL y) * (f . p) is ext-real Element of ExtREAL
R_EAL (1 - y) is ext-real Element of ExtREAL
(R_EAL (1 - y)) * (f . F) is ext-real Element of ExtREAL
((R_EAL y) * (f . p)) + ((R_EAL (1 - y)) * (f . F)) is ext-real Element of ExtREAL
<*((R_EAL y) * (f . p)),((R_EAL (1 - y)) * (f . F))*> is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
<*(y * p),((1 - y) * F)*> is V1() V4( NAT ) V5( the carrier of X) Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of X
<*p,F*> is V1() V4( NAT ) V5( the carrier of X) Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of X
<*y,(1 - y)*> is V1() V4( NAT ) V5( REAL ) Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
s1 is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
s is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
k is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
z is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
F9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s1 . F9 is V31() real ext-real Element of REAL
s . F9 is set
k /. F9 is left_complementable right_complementable complementable Element of the carrier of X
(s1 . F9) * (k /. F9) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X . ((s1 . F9),(k /. F9)) is set
[(s1 . F9),(k /. F9)] is set
the Mult of X . [(s1 . F9),(k /. F9)] is set
z . F9 is ext-real Element of ExtREAL
R_EAL (s1 . F9) is ext-real Element of ExtREAL
f . (k /. F9) is ext-real Element of ExtREAL
(R_EAL (s1 . F9)) * (f . (k /. F9)) is ext-real Element of ExtREAL
len s1 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum s1 is V31() real ext-real Element of REAL
K190(REAL,s1,addreal) is V31() real ext-real Element of REAL
y + (1 - y) is V31() real ext-real Element of REAL
len s is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum s is left_complementable right_complementable complementable Element of the carrier of X
len k is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
len z is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum z is ext-real Element of ExtREAL
X is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
dom X is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
[:(dom X),(dom X):] is V5( RAT ) V5( INT ) finite V53() V54() V55() V56() set
bool [:(dom X),(dom X):] is non empty finite V37() set
{ H1(b1) where b1 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT : ( H1(b1) in dom X & S1[b1] ) } is set
{ H1(b1) where b1 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT : ( H1(b1) in dom X & S2[b1] ) } is set
len X is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg (len X) is finite len X -element V63() V64() V65() V66() V67() V68() Element of bool NAT
F is finite set
Sgm F is V1() V4( NAT ) V5( NAT ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() V56() FinSequence of NAT
rng (Sgm F) is finite V63() V64() V65() V66() V67() V68() Element of bool REAL
y is finite set
Sgm y is V1() V4( NAT ) V5( NAT ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() V56() FinSequence of NAT
rng (Sgm y) is finite V63() V64() V65() V66() V67() V68() Element of bool REAL
F /\ y is finite set
z is set
s is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
X . s is V31() real ext-real Element of REAL
k is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
X . k is V31() real ext-real Element of REAL
(Sgm F) ^ (Sgm y) is V1() V4( NAT ) V5( NAT ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() V56() FinSequence of NAT
len (Sgm F) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
card F is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of omega
k is set
s1 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
X . s1 is V31() real ext-real Element of REAL
s1 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
X . s1 is V31() real ext-real Element of REAL
s1 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
X . s1 is V31() real ext-real Element of REAL
F \/ y is finite set
rng ((Sgm F) ^ (Sgm y)) is finite V63() V64() V65() V66() V67() V68() Element of bool REAL
len (Sgm y) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
card y is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of omega
len ((Sgm F) ^ (Sgm y)) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(card F) + (card y) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
card (F \/ y) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of omega
card (Seg (len X)) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of omega
dom ((Sgm F) ^ (Sgm y)) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
Seg (len (Sgm F)) is finite len (Sgm F) -element V63() V64() V65() V66() V67() V68() Element of bool NAT
dom (Sgm y) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
k is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
((Sgm F) ^ (Sgm y)) . k is ordinal natural V31() real finite cardinal ext-real non negative Element of REAL
(len (Sgm F)) + 1 is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
((len (Sgm F)) + 1) - (len (Sgm F)) is V31() real ext-real V51() V52() Element of INT
k - (len (Sgm F)) is V31() real ext-real V51() V52() Element of INT
s1 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s1 + (len (Sgm F)) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(Sgm y) . s1 is ordinal natural V31() real finite cardinal ext-real non negative Element of REAL
(len (Sgm F)) + (len (Sgm y)) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(len X) - (len (Sgm F)) is V31() real ext-real V51() V52() Element of INT
Seg (len (Sgm y)) is finite len (Sgm y) -element V63() V64() V65() V66() V67() V68() Element of bool NAT
Seg (card y) is finite card y -element V63() V64() V65() V66() V67() V68() Element of bool NAT
k is V1() V4( dom X) V5( dom X) Function-like total quasi_total finite V53() V54() V55() V56() Element of bool [:(dom X),(dom X):]
s1 is V1() V4( dom X) V5( dom X) Function-like one-to-one total quasi_total onto bijective finite V53() V54() V55() V56() Element of bool [:(dom X),(dom X):]
F9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s1 . F9 is ordinal natural V31() real finite cardinal ext-real non negative Element of REAL
X . (s1 . F9) is V31() real ext-real Element of REAL
dom (Sgm F) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
(Sgm F) . F9 is ordinal natural V31() real finite cardinal ext-real non negative Element of REAL
z9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
X . z9 is V31() real ext-real Element of REAL
z9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
z9 + (len (Sgm F)) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(Sgm y) . z9 is ordinal natural V31() real finite cardinal ext-real non negative Element of REAL
z9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
X . z9 is V31() real ext-real Element of REAL
X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V164() RLSStruct
the carrier of X is non empty set
[: the carrier of X,ExtREAL:] is non empty V54() set
bool [: the carrier of X,ExtREAL:] is non empty set
f is V1() V4( the carrier of X) V5( ExtREAL ) Function-like non empty total quasi_total V54() Element of bool [: the carrier of X,ExtREAL:]
n is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg n is non empty finite n -element V63() V64() V65() V66() V67() V68() Element of bool NAT
p is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
len p is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum p is V31() real ext-real Element of REAL
K190(REAL,p,addreal) is V31() real ext-real Element of REAL
F is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len F is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum F is ext-real Element of ExtREAL
y is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
len y is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
z is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
len z is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum z is left_complementable right_complementable complementable Element of the carrier of X
f . (Sum z) is ext-real Element of ExtREAL
dom p is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
[:(dom p),(dom p):] is V5( RAT ) V5( INT ) finite V53() V54() V55() V56() set
bool [:(dom p),(dom p):] is non empty finite V37() set
k is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg k is finite k -element V63() V64() V65() V66() V67() V68() Element of bool NAT
s is V1() V4( dom p) V5( dom p) Function-like one-to-one total quasi_total onto bijective finite V53() V54() V55() V56() Element of bool [:(dom p),(dom p):]
dom F is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
[:(Seg n),ExtREAL:] is non empty V54() set
bool [:(Seg n),ExtREAL:] is non empty set
s1 is V1() V4( NAT ) V5( Seg n) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() V56() FinSequence of Seg n
F * s1 is V1() V4( NAT ) V5( ExtREAL ) Function-like finite V54() Element of bool [:NAT,ExtREAL:]
F9 is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
F9 | k is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
F9 /^ k is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
(F9 | k) ^ (F9 /^ k) is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
n - k is V31() real ext-real V51() V52() Element of INT
z9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
z9 + k is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s . (z9 + k) is ordinal natural V31() real finite cardinal ext-real non negative Element of REAL
p . (s . (z9 + k)) is V31() real ext-real Element of REAL
0 + k is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(n - k) + k is V31() real ext-real V51() V52() Element of INT
dom z is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
[:(Seg n), the carrier of X:] is non empty set
bool [:(Seg n), the carrier of X:] is non empty set
z * s1 is V1() V4( NAT ) V5( the carrier of X) Function-like finite Element of bool [:NAT, the carrier of X:]
[:NAT, the carrier of X:] is non trivial non finite set
bool [:NAT, the carrier of X:] is non empty non trivial non finite set
dom s is finite V63() V64() V65() V66() V67() V68() Element of bool (dom p)
bool (dom p) is non empty finite V37() set
len s1 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
z9 is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
len z9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
z9 /^ k is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
Sum (z9 /^ k) is left_complementable right_complementable complementable Element of the carrier of X
0. X is V113(X) left_complementable right_complementable complementable Element of the carrier of X
the ZeroF of X is left_complementable right_complementable complementable Element of the carrier of X
<*> the carrier of X is V1() V4( NAT ) V5( the carrier of X) Function-like functional empty ordinal natural V31() real finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() FinSequence of the carrier of X
rng (z9 /^ k) is finite Element of bool the carrier of X
bool the carrier of X is non empty set
{(0. X)} is non empty trivial finite 1 -element Element of bool the carrier of X
k9 is set
dom (z9 /^ k) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
k9 is set
(z9 /^ k) . k9 is set
len (z9 /^ k) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
p9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
y9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg p9 is finite p9 -element V63() V64() V65() V66() V67() V68() Element of bool NAT
y9 + k is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s . (y9 + k) is ordinal natural V31() real finite cardinal ext-real non negative Element of REAL
z . (s . (y9 + k)) is set
y /. (s . (y9 + k)) is left_complementable right_complementable complementable Element of the carrier of X
p . (s . (y9 + k)) is V31() real ext-real Element of REAL
(p . (s . (y9 + k))) * (y /. (s . (y9 + k))) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . ((p . (s . (y9 + k))),(y /. (s . (y9 + k)))) is set
[(p . (s . (y9 + k))),(y /. (s . (y9 + k)))] is set
the Mult of X . [(p . (s . (y9 + k))),(y /. (s . (y9 + k)))] is set
dom z9 is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
z9 . (y9 + k) is set
[:(Seg n),REAL:] is non empty non trivial non finite V53() V54() V55() set
bool [:(Seg n),REAL:] is non empty non trivial non finite set
p * s1 is V1() V4( NAT ) V5( REAL ) Function-like finite V53() V54() V55() Element of bool [:NAT,REAL:]
[:NAT,REAL:] is non trivial non finite V53() V54() V55() set
bool [:NAT,REAL:] is non empty non trivial non finite set
min (k,n) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
p9 is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
p9 | k is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
p9 /^ k is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
(p9 | k) ^ (p9 /^ k) is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
Sum p9 is V31() real ext-real Element of REAL
K190(REAL,p9,addreal) is V31() real ext-real Element of REAL
Sum (p9 | k) is V31() real ext-real Element of REAL
K190(REAL,(p9 | k),addreal) is V31() real ext-real Element of REAL
Sum (p9 /^ k) is V31() real ext-real Element of REAL
K190(REAL,(p9 /^ k),addreal) is V31() real ext-real Element of REAL
(Sum (p9 | k)) + (Sum (p9 /^ k)) is V31() real ext-real Element of REAL
len F9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum (F9 /^ k) is ext-real Element of ExtREAL
rng (F9 /^ k) is finite V64() Element of bool ExtREAL
k9 is set
dom (F9 /^ k) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
i is set
(F9 /^ k) . i is ext-real Element of ExtREAL
len (F9 /^ k) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
y9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
i is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg y9 is finite y9 -element V63() V64() V65() V66() V67() V68() Element of bool NAT
i + k is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
s . (i + k) is ordinal natural V31() real finite cardinal ext-real non negative Element of REAL
p . (s . (i + k)) is V31() real ext-real Element of REAL
dom F9 is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
F . (s . (i + k)) is ext-real Element of ExtREAL
R_EAL 0 is ext-real Element of ExtREAL
y /. (s . (i + k)) is left_complementable right_complementable complementable Element of the carrier of X
f . (y /. (s . (i + k))) is ext-real Element of ExtREAL
(R_EAL 0) * (f . (y /. (s . (i + k)))) is ext-real Element of ExtREAL
F9 . (i + k) is ext-real Element of ExtREAL
F9 | (Seg k) is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSubsequence-like V54() Element of bool [:NAT,ExtREAL:]
len (F9 | k) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
k9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
y9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
p . y9 is V31() real ext-real Element of REAL
F . y9 is ext-real Element of ExtREAL
R_EAL (p . y9) is ext-real Element of ExtREAL
y /. y9 is left_complementable right_complementable complementable Element of the carrier of X
f . (y /. y9) is ext-real Element of ExtREAL
(R_EAL (p . y9)) * (f . (y /. y9)) is ext-real Element of ExtREAL
rng F is finite V64() Element of bool ExtREAL
rng F9 is finite V64() Element of bool ExtREAL
rng (F9 | k) is finite V64() Element of bool ExtREAL
rng (F9 /^ k) is finite V64() Element of bool ExtREAL
(rng (F9 | k)) \/ (rng (F9 /^ k)) is finite V64() Element of bool ExtREAL
z9 | k is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
z9 | (Seg k) is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of X:]
len (z9 | k) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
len p9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
rng (p9 /^ k) is finite V63() V64() V65() Element of bool REAL
k9 is set
dom (p9 /^ k) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
i is set
(p9 /^ k) . i is V31() real ext-real Element of REAL
len (p9 /^ k) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
y9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
i is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg y9 is finite y9 -element V63() V64() V65() V66() V67() V68() Element of bool NAT
i + k is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
dom p9 is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
s . (i + k) is ordinal natural V31() real finite cardinal ext-real non negative Element of REAL
p . (s . (i + k)) is V31() real ext-real Element of REAL
p9 . (i + k) is V31() real ext-real Element of REAL
p9 | (Seg k) is V1() V4( NAT ) V5( REAL ) Function-like finite FinSubsequence-like V53() V54() V55() Element of bool [:NAT,REAL:]
len (p9 | k) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum F9 is ext-real Element of ExtREAL
Sum (F9 | k) is ext-real Element of ExtREAL
(Sum (F9 | k)) + (Sum (F9 /^ k)) is ext-real Element of ExtREAL
(z9 | k) ^ (z9 /^ k) is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
Sum z9 is left_complementable right_complementable complementable Element of the carrier of X
Sum (z9 | k) is left_complementable right_complementable complementable Element of the carrier of X
(Sum (z9 | k)) + (Sum (z9 /^ k)) is left_complementable right_complementable complementable Element of the carrier of X
the addF of X is V1() V4([: the carrier of X, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X . ((Sum (z9 | k)),(Sum (z9 /^ k))) is left_complementable right_complementable complementable Element of the carrier of X
[(Sum (z9 | k)),(Sum (z9 /^ k))] is set
the addF of X . [(Sum (z9 | k)),(Sum (z9 /^ k))] is set
dom y is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
y * s1 is V1() V4( NAT ) V5( the carrier of X) Function-like finite Element of bool [:NAT, the carrier of X:]
y9 is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
y9 | k is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
y9 | (Seg k) is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of X:]
len y9 is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
len (y9 | k) is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
k9 is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg k9 is non empty finite k9 -element V63() V64() V65() V66() V67() V68() Element of bool NAT
i is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
(p9 | k) . i is V31() real ext-real Element of REAL
(z9 | k) . i is set
(y9 | k) /. i is left_complementable right_complementable complementable Element of the carrier of X
((p9 | k) . i) * ((y9 | k) /. i) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . (((p9 | k) . i),((y9 | k) /. i)) is set
[((p9 | k) . i),((y9 | k) /. i)] is set
the Mult of X . [((p9 | k) . i),((y9 | k) /. i)] is set
(F9 | k) . i is ext-real Element of ExtREAL
R_EAL ((p9 | k) . i) is ext-real Element of ExtREAL
f . ((y9 | k) /. i) is ext-real Element of ExtREAL
(R_EAL ((p9 | k) . i)) * (f . ((y9 | k) /. i)) is ext-real Element of ExtREAL
dom (p9 | k) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
(p9 | k) /. i is V31() real ext-real Element of REAL
p9 /. i is V31() real ext-real Element of REAL
dom p9 is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
(dom p9) /\ (Seg k) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
p9 . i is V31() real ext-real Element of REAL
s . i is ordinal natural V31() real finite cardinal ext-real non negative Element of REAL
p . (s . i) is V31() real ext-real Element of REAL
dom (y9 | k) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
y9 /. i is left_complementable right_complementable complementable Element of the carrier of X
dom y9 is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
(dom y9) /\ (Seg k) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
y9 . i is set
y . (s . i) is set
dom (F9 | k) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
(F9 | k) /. i is ext-real Element of ExtREAL
F9 /. i is ext-real Element of ExtREAL
dom F9 is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
(dom F9) /\ (Seg k) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
F9 . i is ext-real Element of ExtREAL
F . (s . i) is ext-real Element of ExtREAL
dom (z9 | k) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
(z9 | k) /. i is left_complementable right_complementable complementable Element of the carrier of X
z9 /. i is left_complementable right_complementable complementable Element of the carrier of X
dom z9 is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
(dom z9) /\ (Seg k) is finite V63() V64() V65() V66() V67() V68() Element of bool NAT
z9 . i is set
z . (s . i) is set
y /. (s . i) is left_complementable right_complementable complementable Element of the carrier of X
n is non empty ordinal natural V31() real finite cardinal ext-real positive non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Seg n is non empty finite n -element V63() V64() V65() V66() V67() V68() Element of bool NAT
p is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like V53() V54() V55() FinSequence of REAL
len p is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum p is V31() real ext-real Element of REAL
K190(REAL,p,addreal) is V31() real ext-real Element of REAL
F is V1() V4( NAT ) V5( ExtREAL ) Function-like finite FinSequence-like FinSubsequence-like V54() FinSequence of ExtREAL
len F is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum F is ext-real Element of ExtREAL
y is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
len y is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
z is V1() V4( NAT ) V5( the carrier of X) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X
len z is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
Sum z is left_complementable right_complementable complementable Element of the carrier of X
f . (Sum z) is ext-real Element of ExtREAL
s is ordinal natural V31() real finite cardinal ext-real non negative V51() V52() V63() V64() V65() V66() V67() V68() Element of NAT
p . s is V31() real ext-real Element of REAL
z . s is set
y /. s is left_complementable right_complementable complementable Element of the carrier of X
(p . s) * (y /. s) is left_complementable right_complementable complementable Element of the carrier of X
the Mult of X is V1() V4([:REAL, the carrier of X:]) V5( the carrier of X) Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is non empty non trivial non finite set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty non trivial non finite set
the Mult of X . ((p . s),(y /. s)) is set
[(p . s),(y /. s)] is set
the Mult of X . [(p . s),(y /. s)] is set
F . s is ext-real Element of ExtREAL
R_EAL (p . s) is ext-real Element of ExtREAL
f . (y /. s) is ext-real Element of ExtREAL
(R_EAL (p . s)) * (f . (y /. s)) is ext-real Element of ExtREAL