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