:: CONVFUN1 semantic presentation

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