:: LPSPACE1 semantic presentation

REAL is non empty V29() V166() V167() V168() V172() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() Element of bool REAL

bool REAL is non empty set

ExtREAL is non empty V167() set

[:NAT,ExtREAL:] is non empty V174() set

bool [:NAT,ExtREAL:] is non empty set

bool ExtREAL is non empty set

COMPLEX is non empty V29() V166() V172() set

omega is non empty epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() set

bool omega is non empty set

bool NAT is non empty set

[:NAT,REAL:] is non empty V173() V174() V175() set

bool [:NAT,REAL:] is non empty set

bool (bool REAL) is non empty set

RAT is non empty V29() V166() V167() V168() V169() V172() set

INT is non empty V29() V166() V167() V168() V169() V170() V172() set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V166() V167() V168() V169() V170() V171() V172() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V108() V166() V167() V168() V169() V170() V171() V204() Element of NAT

{{},1} is non empty V166() V167() V168() V169() V170() V171() set

bool RAT is non empty set

[:COMPLEX,COMPLEX:] is non empty V173() set

bool [:COMPLEX,COMPLEX:] is non empty set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V173() set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set

[:REAL,REAL:] is non empty V173() V174() V175() set

bool [:REAL,REAL:] is non empty set

[:[:REAL,REAL:],REAL:] is non empty V173() V174() V175() set

bool [:[:REAL,REAL:],REAL:] is non empty set

[:RAT,RAT:] is non empty V17( RAT ) V173() V174() V175() set

bool [:RAT,RAT:] is non empty set

[:[:RAT,RAT:],RAT:] is non empty V17( RAT ) V173() V174() V175() set

bool [:[:RAT,RAT:],RAT:] is non empty set

[:INT,INT:] is non empty V17( RAT ) V17( INT ) V173() V174() V175() set

bool [:INT,INT:] is non empty set

[:[:INT,INT:],INT:] is non empty V17( RAT ) V17( INT ) V173() V174() V175() set

bool [:[:INT,INT:],INT:] is non empty set

[:NAT,NAT:] is non empty V17( RAT ) V17( INT ) V173() V174() V175() V176() set

[:[:NAT,NAT:],NAT:] is non empty V17( RAT ) V17( INT ) V173() V174() V175() V176() set

bool [:[:NAT,NAT:],NAT:] is non empty set

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V108() V166() V167() V168() V169() V170() V171() V172() V204() Element of NAT

+infty is non empty non real ext-real positive non negative Element of ExtREAL

-infty is non empty non real ext-real non positive negative Element of ExtREAL

0. is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V166() V167() V168() V169() V170() V171() V172() Element of ExtREAL

+infty is non empty non real ext-real positive non negative set

-infty is non empty non real ext-real non positive negative set

{-infty} is non empty V167() set

{+infty} is non empty V167() set

X is non empty RLSStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

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

the carrier of X is non empty set

bool the carrier of X is non empty set

S is Element of bool the carrier of X

M is Element of the carrier of X

x is Element of the carrier of X

M + x is Element of the carrier of X

the addF of X is V13() V16([: the carrier of X, the carrier of X:]) V17( the carrier of X) Function-like V41([: the carrier of X, the carrier of X:], the carrier of X) 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 . (M,x) is Element of the carrier of X

[M,x] is set

{M,x} is non empty set

{M} is non empty set

{{M,x},{M}} is non empty set

the addF of X . [M,x] is set

a is Element of the carrier of X

y is V11() real ext-real Element of REAL

y * a is Element of the carrier of X

the Mult of X is V13() V16([:REAL, the carrier of X:]) V17( the carrier of X) Function-like V41([:REAL, the carrier of X:], the carrier of X) Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:REAL, the carrier of X:] is non empty set

[:[:REAL, the carrier of X:], the carrier of X:] is non empty set

bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set

the Mult of X . (y,a) is set

[y,a] is set

{y,a} is non empty set

{y} is non empty V166() V167() V168() set

{{y,a},{y}} is non empty set

the Mult of X . [y,a] is set

M is Element of the carrier of X

x is Element of the carrier of X

M + x is Element of the carrier of X

the addF of X is V13() V16([: the carrier of X, the carrier of X:]) V17( the carrier of X) Function-like V41([: the carrier of X, the carrier of X:], the carrier of X) 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 . (M,x) is Element of the carrier of X

[M,x] is set

{M,x} is non empty set

{M} is non empty set

{{M,x},{M}} is non empty set

the addF of X . [M,x] is set

a is Element of the carrier of X

y is V11() real ext-real Element of REAL

y * a is Element of the carrier of X

the Mult of X is V13() V16([:REAL, the carrier of X:]) V17( the carrier of X) Function-like V41([:REAL, the carrier of X:], the carrier of X) Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:REAL, the carrier of X:] is non empty set

[:[:REAL, the carrier of X:], the carrier of X:] is non empty set

bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set

the Mult of X . (y,a) is set

[y,a] is set

{y,a} is non empty set

{y} is non empty V166() V167() V168() set

{{y,a},{y}} is non empty set

the Mult of X . [y,a] is set

X is non empty RLSStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

M is set

M is Element of bool the carrier of X

x is non empty Element of bool the carrier of X

a is Element of the carrier of X

y is V11() real ext-real Element of REAL

y * a is Element of the carrier of X

the Mult of X is V13() V16([:REAL, the carrier of X:]) V17( the carrier of X) Function-like V41([:REAL, the carrier of X:], the carrier of X) Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:REAL, the carrier of X:] is non empty set

[:[:REAL, the carrier of X:], the carrier of X:] is non empty set

bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set

the Mult of X . (y,a) is set

[y,a] is set

{y,a} is non empty set

{y} is non empty V166() V167() V168() set

{{y,a},{y}} is non empty set

the Mult of X . [y,a] is set

f is Element of the carrier of X

g is Element of the carrier of X

f + g is Element of the carrier of X

the addF of X is V13() V16([: the carrier of X, the carrier of X:]) V17( the carrier of X) Function-like V41([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set

the addF of X . (f,g) is Element of the carrier of X

[f,g] is set

{f,g} is non empty set

{f} is non empty set

{{f,g},{f}} is non empty set

the addF of X . [f,g] is set

X is non empty RLSStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

[:REAL, the carrier of X:] is non empty set

the Mult of X is V13() V16([:REAL, the carrier of X:]) V17( the carrier of X) Function-like V41([:REAL, the carrier of X:], the carrier of X) Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:[:REAL, the carrier of X:], the carrier of X:] is non empty set

bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set

S is non empty (X) Element of bool the carrier of X

[:REAL,S:] is non empty set

the Mult of X | [:REAL,S:] is V13() V16([:REAL, the carrier of X:]) V17( the carrier of X) Function-like Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:[:REAL,S:],S:] is non empty set

bool [:[:REAL,S:],S:] is non empty set

dom the Mult of X is V13() V16( REAL ) V17( the carrier of X) Element of bool [:REAL, the carrier of X:]

bool [:REAL, the carrier of X:] is non empty set

M is set

x is set

y is set

[x,y] is set

{x,y} is non empty set

{x} is non empty set

{{x,y},{x}} is non empty set

a is V11() real ext-real Element of REAL

[a,y] is set

{a,y} is non empty set

{a} is non empty V166() V167() V168() set

{{a,y},{a}} is non empty set

dom ( the Mult of X | [:REAL,S:]) is V13() V16( REAL ) V17( the carrier of X) Element of bool [:REAL, the carrier of X:]

( the Mult of X | [:REAL,S:]) . M is set

f is Element of the carrier of X

a * f is Element of the carrier of X

the Mult of X . (a,f) is set

[a,f] is set

{a,f} is non empty set

{{a,f},{a}} is non empty set

the Mult of X . [a,f] is set

X is non empty Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

0. X is V55(X) Element of the carrier of X

the ZeroF of X is Element of the carrier of X

the addF of X is V13() V16([: the carrier of X, the carrier of X:]) V17( the carrier of X) Function-like V41([: the carrier of X, the carrier of X:], the carrier of X) 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

[:REAL, the carrier of X:] is non empty set

the Mult of X is V13() V16([:REAL, the carrier of X:]) V17( the carrier of X) Function-like V41([:REAL, the carrier of X:], the carrier of X) Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:[:REAL, the carrier of X:], the carrier of X:] is non empty set

bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set

S is non empty Element of bool the carrier of X

[:S,S:] is non empty set

[:[:S,S:],S:] is non empty set

bool [:[:S,S:],S:] is non empty set

[:REAL,S:] is non empty set

[:[:REAL,S:],S:] is non empty set

bool [:[:REAL,S:],S:] is non empty set

the addF of X || S is set

K65( the addF of X,[:S,S:]) is V13() set

the Mult of X | [:REAL,S:] is V13() V16([:REAL, the carrier of X:]) V17( the carrier of X) Function-like Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

M is Element of S

x is V13() V16([:S,S:]) V17(S) Function-like V41([:S,S:],S) Element of bool [:[:S,S:],S:]

y is V13() V16([:REAL,S:]) V17(S) Function-like V41([:REAL,S:],S) Element of bool [:[:REAL,S:],S:]

RLSStruct(# S,M,x,y #) is non empty strict RLSStruct

the carrier of RLSStruct(# S,M,x,y #) is non empty set

f is Element of the carrier of RLSStruct(# S,M,x,y #)

g is V11() real ext-real Element of REAL

g * f is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) is V13() V16([:REAL, the carrier of RLSStruct(# S,M,x,y #):]) V17( the carrier of RLSStruct(# S,M,x,y #)) Function-like V41([:REAL, the carrier of RLSStruct(# S,M,x,y #):], the carrier of RLSStruct(# S,M,x,y #)) Element of bool [:[:REAL, the carrier of RLSStruct(# S,M,x,y #):], the carrier of RLSStruct(# S,M,x,y #):]

[:REAL, the carrier of RLSStruct(# S,M,x,y #):] is non empty set

[:[:REAL, the carrier of RLSStruct(# S,M,x,y #):], the carrier of RLSStruct(# S,M,x,y #):] is non empty set

bool [:[:REAL, the carrier of RLSStruct(# S,M,x,y #):], the carrier of RLSStruct(# S,M,x,y #):] is non empty set

the Mult of RLSStruct(# S,M,x,y #) . (g,f) is set

[g,f] is set

{g,f} is non empty set

{g} is non empty V166() V167() V168() set

{{g,f},{g}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [g,f] is set

[g,f] is Element of [:REAL, the carrier of RLSStruct(# S,M,x,y #):]

the Mult of X . [g,f] is set

the Mult of X . (g,f) is set

the Mult of X . [g,f] is set

g is Element of the carrier of RLSStruct(# S,M,x,y #)

f is Element of the carrier of RLSStruct(# S,M,x,y #)

g + f is Element of the carrier of RLSStruct(# S,M,x,y #)

the addF of RLSStruct(# S,M,x,y #) is V13() V16([: the carrier of RLSStruct(# S,M,x,y #), the carrier of RLSStruct(# S,M,x,y #):]) V17( the carrier of RLSStruct(# S,M,x,y #)) Function-like V41([: the carrier of RLSStruct(# S,M,x,y #), the carrier of RLSStruct(# S,M,x,y #):], the carrier of RLSStruct(# S,M,x,y #)) Element of bool [:[: the carrier of RLSStruct(# S,M,x,y #), the carrier of RLSStruct(# S,M,x,y #):], the carrier of RLSStruct(# S,M,x,y #):]

[: the carrier of RLSStruct(# S,M,x,y #), the carrier of RLSStruct(# S,M,x,y #):] is non empty set

[:[: the carrier of RLSStruct(# S,M,x,y #), the carrier of RLSStruct(# S,M,x,y #):], the carrier of RLSStruct(# S,M,x,y #):] is non empty set

bool [:[: the carrier of RLSStruct(# S,M,x,y #), the carrier of RLSStruct(# S,M,x,y #):], the carrier of RLSStruct(# S,M,x,y #):] is non empty set

the addF of RLSStruct(# S,M,x,y #) . (g,f) is Element of the carrier of RLSStruct(# S,M,x,y #)

[g,f] is set

{g,f} is non empty set

{g} is non empty set

{{g,f},{g}} is non empty set

the addF of RLSStruct(# S,M,x,y #) . [g,f] is set

[g,f] is Element of [: the carrier of RLSStruct(# S,M,x,y #), the carrier of RLSStruct(# S,M,x,y #):]

the addF of X . [g,f] is set

the addF of X . (g,f) is set

the addF of X . [g,f] is set

f is Element of the carrier of RLSStruct(# S,M,x,y #)

A is Element of the carrier of RLSStruct(# S,M,x,y #)

f + A is Element of the carrier of RLSStruct(# S,M,x,y #)

the addF of RLSStruct(# S,M,x,y #) . (f,A) is Element of the carrier of RLSStruct(# S,M,x,y #)

[f,A] is set

{f,A} is non empty set

{f} is non empty set

{{f,A},{f}} is non empty set

the addF of RLSStruct(# S,M,x,y #) . [f,A] is set

n is Element of the carrier of X

n is Element of the carrier of X

n + n is Element of the carrier of X

the addF of X . (n,n) is Element of the carrier of X

[n,n] is set

{n,n} is non empty set

{n} is non empty set

{{n,n},{n}} is non empty set

the addF of X . [n,n] is set

n + n is Element of the carrier of X

the addF of X . (n,n) is Element of the carrier of X

[n,n] is set

{n,n} is non empty set

{n} is non empty set

{{n,n},{n}} is non empty set

the addF of X . [n,n] is set

A + f is Element of the carrier of RLSStruct(# S,M,x,y #)

the addF of RLSStruct(# S,M,x,y #) . (A,f) is Element of the carrier of RLSStruct(# S,M,x,y #)

[A,f] is set

{A,f} is non empty set

{A} is non empty set

{{A,f},{A}} is non empty set

the addF of RLSStruct(# S,M,x,y #) . [A,f] is set

f is Element of the carrier of RLSStruct(# S,M,x,y #)

A is Element of the carrier of RLSStruct(# S,M,x,y #)

n is Element of the carrier of RLSStruct(# S,M,x,y #)

f + A is Element of the carrier of RLSStruct(# S,M,x,y #)

the addF of RLSStruct(# S,M,x,y #) . (f,A) is Element of the carrier of RLSStruct(# S,M,x,y #)

[f,A] is set

{f,A} is non empty set

{f} is non empty set

{{f,A},{f}} is non empty set

the addF of RLSStruct(# S,M,x,y #) . [f,A] is set

(f + A) + n is Element of the carrier of RLSStruct(# S,M,x,y #)

the addF of RLSStruct(# S,M,x,y #) . ((f + A),n) is Element of the carrier of RLSStruct(# S,M,x,y #)

[(f + A),n] is set

{(f + A),n} is non empty set

{(f + A)} is non empty set

{{(f + A),n},{(f + A)}} is non empty set

the addF of RLSStruct(# S,M,x,y #) . [(f + A),n] is set

a1 is Element of the carrier of X

the addF of X . ((f + A),a1) is set

[(f + A),a1] is set

{(f + A),a1} is non empty set

{{(f + A),a1},{(f + A)}} is non empty set

the addF of X . [(f + A),a1] is set

n is Element of the carrier of X

c is Element of the carrier of X

n + c is Element of the carrier of X

the addF of X . (n,c) is Element of the carrier of X

[n,c] is set

{n,c} is non empty set

{n} is non empty set

{{n,c},{n}} is non empty set

the addF of X . [n,c] is set

(n + c) + a1 is Element of the carrier of X

the addF of X . ((n + c),a1) is Element of the carrier of X

[(n + c),a1] is set

{(n + c),a1} is non empty set

{(n + c)} is non empty set

{{(n + c),a1},{(n + c)}} is non empty set

the addF of X . [(n + c),a1] is set

c + a1 is Element of the carrier of X

the addF of X . (c,a1) is Element of the carrier of X

[c,a1] is set

{c,a1} is non empty set

{c} is non empty set

{{c,a1},{c}} is non empty set

the addF of X . [c,a1] is set

n + (c + a1) is Element of the carrier of X

the addF of X . (n,(c + a1)) is Element of the carrier of X

[n,(c + a1)] is set

{n,(c + a1)} is non empty set

{{n,(c + a1)},{n}} is non empty set

the addF of X . [n,(c + a1)] is set

A + n is Element of the carrier of RLSStruct(# S,M,x,y #)

the addF of RLSStruct(# S,M,x,y #) . (A,n) is Element of the carrier of RLSStruct(# S,M,x,y #)

[A,n] is set

{A,n} is non empty set

{A} is non empty set

{{A,n},{A}} is non empty set

the addF of RLSStruct(# S,M,x,y #) . [A,n] is set

the addF of X . (n,(A + n)) is set

[n,(A + n)] is set

{n,(A + n)} is non empty set

{{n,(A + n)},{n}} is non empty set

the addF of X . [n,(A + n)] is set

f + (A + n) is Element of the carrier of RLSStruct(# S,M,x,y #)

the addF of RLSStruct(# S,M,x,y #) . (f,(A + n)) is Element of the carrier of RLSStruct(# S,M,x,y #)

[f,(A + n)] is set

{f,(A + n)} is non empty set

{{f,(A + n)},{f}} is non empty set

the addF of RLSStruct(# S,M,x,y #) . [f,(A + n)] is set

f is Element of the carrier of RLSStruct(# S,M,x,y #)

0. RLSStruct(# S,M,x,y #) is V55( RLSStruct(# S,M,x,y #)) Element of the carrier of RLSStruct(# S,M,x,y #)

the ZeroF of RLSStruct(# S,M,x,y #) is Element of the carrier of RLSStruct(# S,M,x,y #)

f + (0. RLSStruct(# S,M,x,y #)) is Element of the carrier of RLSStruct(# S,M,x,y #)

the addF of RLSStruct(# S,M,x,y #) . (f,(0. RLSStruct(# S,M,x,y #))) is Element of the carrier of RLSStruct(# S,M,x,y #)

[f,(0. RLSStruct(# S,M,x,y #))] is set

{f,(0. RLSStruct(# S,M,x,y #))} is non empty set

{f} is non empty set

{{f,(0. RLSStruct(# S,M,x,y #))},{f}} is non empty set

the addF of RLSStruct(# S,M,x,y #) . [f,(0. RLSStruct(# S,M,x,y #))] is set

A is Element of the carrier of X

A + (0. X) is Element of the carrier of X

the addF of X . (A,(0. X)) is Element of the carrier of X

[A,(0. X)] is set

{A,(0. X)} is non empty set

{A} is non empty set

{{A,(0. X)},{A}} is non empty set

the addF of X . [A,(0. X)] is set

f is V11() real ext-real set

A is Element of the carrier of RLSStruct(# S,M,x,y #)

n is Element of the carrier of RLSStruct(# S,M,x,y #)

A + n is Element of the carrier of RLSStruct(# S,M,x,y #)

the addF of RLSStruct(# S,M,x,y #) . (A,n) is Element of the carrier of RLSStruct(# S,M,x,y #)

[A,n] is set

{A,n} is non empty set

{A} is non empty set

{{A,n},{A}} is non empty set

the addF of RLSStruct(# S,M,x,y #) . [A,n] is set

n is V11() real ext-real Element of REAL

n * (A + n) is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . (n,(A + n)) is set

[n,(A + n)] is set

{n,(A + n)} is non empty set

{n} is non empty V166() V167() V168() set

{{n,(A + n)},{n}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [n,(A + n)] is set

the Mult of X . (n,(A + n)) is set

the Mult of X . [n,(A + n)] is set

c is Element of the carrier of X

a1 is Element of the carrier of X

c + a1 is Element of the carrier of X

the addF of X . (c,a1) is Element of the carrier of X

[c,a1] is set

{c,a1} is non empty set

{c} is non empty set

{{c,a1},{c}} is non empty set

the addF of X . [c,a1] is set

n * (c + a1) is Element of the carrier of X

the Mult of X . (n,(c + a1)) is set

[n,(c + a1)] is set

{n,(c + a1)} is non empty set

{{n,(c + a1)},{n}} is non empty set

the Mult of X . [n,(c + a1)] is set

n * c is Element of the carrier of X

the Mult of X . (n,c) is set

[n,c] is set

{n,c} is non empty set

{{n,c},{n}} is non empty set

the Mult of X . [n,c] is set

n * a1 is Element of the carrier of X

the Mult of X . (n,a1) is set

[n,a1] is set

{n,a1} is non empty set

{{n,a1},{n}} is non empty set

the Mult of X . [n,a1] is set

(n * c) + (n * a1) is Element of the carrier of X

the addF of X . ((n * c),(n * a1)) is Element of the carrier of X

[(n * c),(n * a1)] is set

{(n * c),(n * a1)} is non empty set

{(n * c)} is non empty set

{{(n * c),(n * a1)},{(n * c)}} is non empty set

the addF of X . [(n * c),(n * a1)] is set

the Mult of X . (n,c) is Element of the carrier of X

n * n is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . (n,n) is set

[n,n] is set

{n,n} is non empty set

{{n,n},{n}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [n,n] is set

the addF of X . (( the Mult of X . (n,c)),(n * n)) is set

[( the Mult of X . (n,c)),(n * n)] is set

{( the Mult of X . (n,c)),(n * n)} is non empty set

{( the Mult of X . (n,c))} is non empty set

{{( the Mult of X . (n,c)),(n * n)},{( the Mult of X . (n,c))}} is non empty set

the addF of X . [( the Mult of X . (n,c)),(n * n)] is set

n * A is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . (n,A) is set

[n,A] is set

{n,A} is non empty set

{{n,A},{n}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [n,A] is set

the addF of X . ((n * A),(n * n)) is set

[(n * A),(n * n)] is set

{(n * A),(n * n)} is non empty set

{(n * A)} is non empty set

{{(n * A),(n * n)},{(n * A)}} is non empty set

the addF of X . [(n * A),(n * n)] is set

(n * A) + (n * n) is Element of the carrier of RLSStruct(# S,M,x,y #)

the addF of RLSStruct(# S,M,x,y #) . ((n * A),(n * n)) is Element of the carrier of RLSStruct(# S,M,x,y #)

the addF of RLSStruct(# S,M,x,y #) . [(n * A),(n * n)] is set

f * (A + n) is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . (f,(A + n)) is set

[f,(A + n)] is set

{f,(A + n)} is non empty set

{f} is non empty V166() V167() V168() set

{{f,(A + n)},{f}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [f,(A + n)] is set

f * A is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . (f,A) is set

[f,A] is set

{f,A} is non empty set

{{f,A},{f}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [f,A] is set

f * n is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . (f,n) is set

[f,n] is set

{f,n} is non empty set

{{f,n},{f}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [f,n] is set

(f * A) + (f * n) is Element of the carrier of RLSStruct(# S,M,x,y #)

the addF of RLSStruct(# S,M,x,y #) . ((f * A),(f * n)) is Element of the carrier of RLSStruct(# S,M,x,y #)

[(f * A),(f * n)] is set

{(f * A),(f * n)} is non empty set

{(f * A)} is non empty set

{{(f * A),(f * n)},{(f * A)}} is non empty set

the addF of RLSStruct(# S,M,x,y #) . [(f * A),(f * n)] is set

f is V11() real ext-real set

A is V11() real ext-real set

n is Element of the carrier of RLSStruct(# S,M,x,y #)

n is V11() real ext-real Element of REAL

c is V11() real ext-real Element of REAL

n + c is V11() real ext-real Element of REAL

(n + c) * n is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . ((n + c),n) is set

[(n + c),n] is set

{(n + c),n} is non empty set

{(n + c)} is non empty V166() V167() V168() set

{{(n + c),n},{(n + c)}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [(n + c),n] is set

a1 is Element of the carrier of X

(n + c) * a1 is Element of the carrier of X

the Mult of X . ((n + c),a1) is set

[(n + c),a1] is set

{(n + c),a1} is non empty set

{{(n + c),a1},{(n + c)}} is non empty set

the Mult of X . [(n + c),a1] is set

n * a1 is Element of the carrier of X

the Mult of X . (n,a1) is set

[n,a1] is set

{n,a1} is non empty set

{n} is non empty V166() V167() V168() set

{{n,a1},{n}} is non empty set

the Mult of X . [n,a1] is set

c * a1 is Element of the carrier of X

the Mult of X . (c,a1) is set

[c,a1] is set

{c,a1} is non empty set

{c} is non empty V166() V167() V168() set

{{c,a1},{c}} is non empty set

the Mult of X . [c,a1] is set

(n * a1) + (c * a1) is Element of the carrier of X

the addF of X . ((n * a1),(c * a1)) is Element of the carrier of X

[(n * a1),(c * a1)] is set

{(n * a1),(c * a1)} is non empty set

{(n * a1)} is non empty set

{{(n * a1),(c * a1)},{(n * a1)}} is non empty set

the addF of X . [(n * a1),(c * a1)] is set

the Mult of X . (n,a1) is Element of the carrier of X

c * n is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . (c,n) is set

[c,n] is set

{c,n} is non empty set

{{c,n},{c}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [c,n] is set

the addF of X . (( the Mult of X . (n,a1)),(c * n)) is set

[( the Mult of X . (n,a1)),(c * n)] is set

{( the Mult of X . (n,a1)),(c * n)} is non empty set

{( the Mult of X . (n,a1))} is non empty set

{{( the Mult of X . (n,a1)),(c * n)},{( the Mult of X . (n,a1))}} is non empty set

the addF of X . [( the Mult of X . (n,a1)),(c * n)] is set

n * n is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . (n,n) is set

[n,n] is set

{n,n} is non empty set

{{n,n},{n}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [n,n] is set

the addF of X . ((n * n),(c * n)) is set

[(n * n),(c * n)] is set

{(n * n),(c * n)} is non empty set

{(n * n)} is non empty set

{{(n * n),(c * n)},{(n * n)}} is non empty set

the addF of X . [(n * n),(c * n)] is set

(n * n) + (c * n) is Element of the carrier of RLSStruct(# S,M,x,y #)

the addF of RLSStruct(# S,M,x,y #) . ((n * n),(c * n)) is Element of the carrier of RLSStruct(# S,M,x,y #)

the addF of RLSStruct(# S,M,x,y #) . [(n * n),(c * n)] is set

f + A is V11() real ext-real set

(f + A) * n is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . ((f + A),n) is set

[(f + A),n] is set

{(f + A),n} is non empty set

{(f + A)} is non empty V166() V167() V168() set

{{(f + A),n},{(f + A)}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [(f + A),n] is set

f * n is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . (f,n) is set

[f,n] is set

{f,n} is non empty set

{f} is non empty V166() V167() V168() set

{{f,n},{f}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [f,n] is set

A * n is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . (A,n) is set

[A,n] is set

{A,n} is non empty set

{A} is non empty V166() V167() V168() set

{{A,n},{A}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [A,n] is set

(f * n) + (A * n) is Element of the carrier of RLSStruct(# S,M,x,y #)

the addF of RLSStruct(# S,M,x,y #) . ((f * n),(A * n)) is Element of the carrier of RLSStruct(# S,M,x,y #)

[(f * n),(A * n)] is set

{(f * n),(A * n)} is non empty set

{(f * n)} is non empty set

{{(f * n),(A * n)},{(f * n)}} is non empty set

the addF of RLSStruct(# S,M,x,y #) . [(f * n),(A * n)] is set

f is V11() real ext-real set

A is V11() real ext-real set

n is Element of the carrier of RLSStruct(# S,M,x,y #)

n is V11() real ext-real Element of REAL

c is V11() real ext-real Element of REAL

n * c is V11() real ext-real Element of REAL

(n * c) * n is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . ((n * c),n) is set

[(n * c),n] is set

{(n * c),n} is non empty set

{(n * c)} is non empty V166() V167() V168() set

{{(n * c),n},{(n * c)}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [(n * c),n] is set

a1 is Element of the carrier of X

(n * c) * a1 is Element of the carrier of X

the Mult of X . ((n * c),a1) is set

[(n * c),a1] is set

{(n * c),a1} is non empty set

{{(n * c),a1},{(n * c)}} is non empty set

the Mult of X . [(n * c),a1] is set

c * a1 is Element of the carrier of X

the Mult of X . (c,a1) is set

[c,a1] is set

{c,a1} is non empty set

{c} is non empty V166() V167() V168() set

{{c,a1},{c}} is non empty set

the Mult of X . [c,a1] is set

n * (c * a1) is Element of the carrier of X

the Mult of X . (n,(c * a1)) is set

[n,(c * a1)] is set

{n,(c * a1)} is non empty set

{n} is non empty V166() V167() V168() set

{{n,(c * a1)},{n}} is non empty set

the Mult of X . [n,(c * a1)] is set

c * n is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . (c,n) is set

[c,n] is set

{c,n} is non empty set

{{c,n},{c}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [c,n] is set

the Mult of X . (n,(c * n)) is set

[n,(c * n)] is set

{n,(c * n)} is non empty set

{{n,(c * n)},{n}} is non empty set

the Mult of X . [n,(c * n)] is set

n * (c * n) is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . (n,(c * n)) is set

the Mult of RLSStruct(# S,M,x,y #) . [n,(c * n)] is set

f * A is V11() real ext-real set

(f * A) * n is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . ((f * A),n) is set

[(f * A),n] is set

{(f * A),n} is non empty set

{(f * A)} is non empty V166() V167() V168() set

{{(f * A),n},{(f * A)}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [(f * A),n] is set

A * n is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . (A,n) is set

[A,n] is set

{A,n} is non empty set

{A} is non empty V166() V167() V168() set

{{A,n},{A}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [A,n] is set

f * (A * n) is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . (f,(A * n)) is set

[f,(A * n)] is set

{f,(A * n)} is non empty set

{f} is non empty V166() V167() V168() set

{{f,(A * n)},{f}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [f,(A * n)] is set

f is Element of the carrier of RLSStruct(# S,M,x,y #)

1 * f is Element of the carrier of RLSStruct(# S,M,x,y #)

the Mult of RLSStruct(# S,M,x,y #) . (1,f) is set

[1,f] is set

{1,f} is non empty set

{1} is non empty V166() V167() V168() V169() V170() V171() set

{{1,f},{1}} is non empty set

the Mult of RLSStruct(# S,M,x,y #) . [1,f] is set

A is Element of the carrier of X

1 * A is Element of the carrier of X

the Mult of X . (1,A) is set

[1,A] is set

{1,A} is non empty set

{{1,A},{1}} is non empty set

the Mult of X . [1,A] is set

X is non empty Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

0. X is V55(X) Element of the carrier of X

the ZeroF of X is Element of the carrier of X

S is non empty add-closed (X) Element of bool the carrier of X

In ((0. X),S) is Element of S

add| (S,X) is V13() V16([:S,S:]) V17(S) Function-like V41([:S,S:],S) Element of bool [:[:S,S:],S:]

[:S,S:] is non empty set

[:[:S,S:],S:] is non empty set

bool [:[:S,S:],S:] is non empty set

the addF of X is V13() V16([: the carrier of X, the carrier of X:]) V17( the carrier of X) Function-like V41([: the carrier of X, the carrier of X:], the carrier of X) 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 || S is set

K65( the addF of X,[:S,S:]) is V13() set

(X,S) is V13() V16([:REAL,S:]) V17(S) Function-like V41([:REAL,S:],S) Element of bool [:[:REAL,S:],S:]

[:REAL,S:] is non empty set

[:[:REAL,S:],S:] is non empty set

bool [:[:REAL,S:],S:] is non empty set

[:REAL, the carrier of X:] is non empty set

the Mult of X is V13() V16([:REAL, the carrier of X:]) V17( the carrier of X) Function-like V41([:REAL, the carrier of X:], the carrier of X) Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:[:REAL, the carrier of X:], the carrier of X:] is non empty set

bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set

the Mult of X | [:REAL,S:] is V13() V16([:REAL, the carrier of X:]) V17( the carrier of X) Function-like Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #) is non empty strict RLSStruct

X is non empty RLSStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

0. X is V55(X) Element of the carrier of X

the ZeroF of X is Element of the carrier of X

S is non empty add-closed (X) Element of bool the carrier of X

In ((0. X),S) is Element of S

add| (S,X) is V13() V16([:S,S:]) V17(S) Function-like V41([:S,S:],S) Element of bool [:[:S,S:],S:]

[:S,S:] is non empty set

[:[:S,S:],S:] is non empty set

bool [:[:S,S:],S:] is non empty set

the addF of X is V13() V16([: the carrier of X, the carrier of X:]) V17( the carrier of X) Function-like V41([: the carrier of X, the carrier of X:], the carrier of X) 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 || S is set

K65( the addF of X,[:S,S:]) is V13() set

(X,S) is V13() V16([:REAL,S:]) V17(S) Function-like V41([:REAL,S:],S) Element of bool [:[:REAL,S:],S:]

[:REAL,S:] is non empty set

[:[:REAL,S:],S:] is non empty set

bool [:[:REAL,S:],S:] is non empty set

[:REAL, the carrier of X:] is non empty set

the Mult of X is V13() V16([:REAL, the carrier of X:]) V17( the carrier of X) Function-like V41([:REAL, the carrier of X:], the carrier of X) Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:[:REAL, the carrier of X:], the carrier of X:] is non empty set

bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set

the Mult of X | [:REAL,S:] is V13() V16([:REAL, the carrier of X:]) V17( the carrier of X) Function-like Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #) is non empty strict RLSStruct

the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #) is non empty set

M is Element of the carrier of X

x is Element of the carrier of X

M + x is Element of the carrier of X

the addF of X . (M,x) is Element of the carrier of X

[M,x] is set

{M,x} is non empty set

{M} is non empty set

{{M,x},{M}} is non empty set

the addF of X . [M,x] is set

y is Element of the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #)

a is Element of the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #)

y + a is Element of the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #)

the addF of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #) is V13() V16([: the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #), the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #):]) V17( the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #)) Function-like V41([: the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #), the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #):], the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #)) Element of bool [:[: the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #), the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #):], the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #):]

[: the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #), the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #):] is non empty set

[:[: the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #), the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #):], the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #):] is non empty set

bool [:[: the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #), the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #):], the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #):] is non empty set

the addF of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #) . (y,a) is Element of the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #)

[y,a] is set

{y,a} is non empty set

{y} is non empty set

{{y,a},{y}} is non empty set

the addF of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #) . [y,a] is set

[M,x] is Element of [: the carrier of X, the carrier of X:]

X is non empty RLSStruct

the carrier of X is non empty set

bool the carrier of X is non empty set

0. X is V55(X) Element of the carrier of X

the ZeroF of X is Element of the carrier of X

S is non empty add-closed (X) Element of bool the carrier of X

In ((0. X),S) is Element of S

add| (S,X) is V13() V16([:S,S:]) V17(S) Function-like V41([:S,S:],S) Element of bool [:[:S,S:],S:]

[:S,S:] is non empty set

[:[:S,S:],S:] is non empty set

bool [:[:S,S:],S:] is non empty set

the addF of X is V13() V16([: the carrier of X, the carrier of X:]) V17( the carrier of X) Function-like V41([: the carrier of X, the carrier of X:], the carrier of X) 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 || S is set

K65( the addF of X,[:S,S:]) is V13() set

(X,S) is V13() V16([:REAL,S:]) V17(S) Function-like V41([:REAL,S:],S) Element of bool [:[:REAL,S:],S:]

[:REAL,S:] is non empty set

[:[:REAL,S:],S:] is non empty set

bool [:[:REAL,S:],S:] is non empty set

[:REAL, the carrier of X:] is non empty set

the Mult of X is V13() V16([:REAL, the carrier of X:]) V17( the carrier of X) Function-like V41([:REAL, the carrier of X:], the carrier of X) Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:[:REAL, the carrier of X:], the carrier of X:] is non empty set

bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set

the Mult of X | [:REAL,S:] is V13() V16([:REAL, the carrier of X:]) V17( the carrier of X) Function-like Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #) is non empty strict RLSStruct

the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #) is non empty set

M is V11() real ext-real Element of REAL

x is Element of the carrier of X

M * x is Element of the carrier of X

the Mult of X . (M,x) is set

[M,x] is set

{M,x} is non empty set

{M} is non empty V166() V167() V168() set

{{M,x},{M}} is non empty set

the Mult of X . [M,x] is set

y is Element of the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #)

M * y is Element of the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #)

the Mult of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #) is V13() V16([:REAL, the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #):]) V17( the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #)) Function-like V41([:REAL, the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #):], the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #)) Element of bool [:[:REAL, the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #):], the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #):]

[:REAL, the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #):] is non empty set

[:[:REAL, the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #):], the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #):] is non empty set

bool [:[:REAL, the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #):], the carrier of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #):] is non empty set

the Mult of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #) . (M,y) is set

[M,y] is set

{M,y} is non empty set

{{M,y},{M}} is non empty set

the Mult of RLSStruct(# S,(In ((0. X),S)),(add| (S,X)),(X,S) #) . [M,y] is set

[M,x] is Element of [:REAL, the carrier of X:]

X is non empty set

S is non empty set

PFuncs (X,S) is non empty functional PartFunc-set of X,S

[:(PFuncs (X,S)),(PFuncs (X,S)):] is non empty set

[:[:(PFuncs (X,S)),(PFuncs (X,S)):],(PFuncs (X,S)):] is non empty set

bool [:[:(PFuncs (X,S)),(PFuncs (X,S)):],(PFuncs (X,S)):] is non empty set

M is V13() V16([:(PFuncs (X,S)),(PFuncs (X,S)):]) V17( PFuncs (X,S)) Function-like V41([:(PFuncs (X,S)),(PFuncs (X,S)):], PFuncs (X,S)) Element of bool [:[:(PFuncs (X,S)),(PFuncs (X,S)):],(PFuncs (X,S)):]

x is V13() V16(X) V17(S) Function-like Element of PFuncs (X,S)

y is V13() V16(X) V17(S) Function-like Element of PFuncs (X,S)

M . (x,y) is set

[x,y] is set

{x,y} is non empty set

{x} is non empty set

{{x,y},{x}} is non empty set

M . [x,y] is set

a is V13() V16(X) V17(S) Function-like Element of PFuncs (X,S)

f is V13() V16(X) V17(S) Function-like Element of PFuncs (X,S)

M . (a,f) is Element of PFuncs (X,S)

[a,f] is set

{a,f} is non empty set

{a} is non empty set

{{a,f},{a}} is non empty set

M . [a,f] is set

X is non empty set

PFuncs (X,REAL) is non empty functional PartFunc-set of X, REAL

[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):] is non empty set

[:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set

bool [:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set

S is V13() V16([:(PFuncs (X,REAL)),(PFuncs (X,REAL)):]) V17( PFuncs (X,REAL)) Function-like V41([:(PFuncs (X,REAL)),(PFuncs (X,REAL)):], PFuncs (X,REAL)) Element of bool [:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):]

S is V13() V16([:(PFuncs (X,REAL)),(PFuncs (X,REAL)):]) V17( PFuncs (X,REAL)) Function-like V41([:(PFuncs (X,REAL)),(PFuncs (X,REAL)):], PFuncs (X,REAL)) Element of bool [:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):]

M is V13() V16([:(PFuncs (X,REAL)),(PFuncs (X,REAL)):]) V17( PFuncs (X,REAL)) Function-like V41([:(PFuncs (X,REAL)),(PFuncs (X,REAL)):], PFuncs (X,REAL)) Element of bool [:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):]

x is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

y is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

(X,REAL,S,x,y) is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

[x,y] is set

{x,y} is non empty set

{x} is non empty set

{{x,y},{x}} is non empty set

S . [x,y] is set

x (#) y is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

(X,REAL,M,x,y) is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

M . [x,y] is set

X is non empty set

PFuncs (X,REAL) is non empty functional PartFunc-set of X, REAL

[:REAL,(PFuncs (X,REAL)):] is non empty set

[:[:REAL,(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set

bool [:[:REAL,(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set

S is V13() V16([:REAL,(PFuncs (X,REAL)):]) V17( PFuncs (X,REAL)) Function-like V41([:REAL,(PFuncs (X,REAL)):], PFuncs (X,REAL)) Element of bool [:[:REAL,(PFuncs (X,REAL)):],(PFuncs (X,REAL)):]

S is V13() V16([:REAL,(PFuncs (X,REAL)):]) V17( PFuncs (X,REAL)) Function-like V41([:REAL,(PFuncs (X,REAL)):], PFuncs (X,REAL)) Element of bool [:[:REAL,(PFuncs (X,REAL)):],(PFuncs (X,REAL)):]

M is V13() V16([:REAL,(PFuncs (X,REAL)):]) V17( PFuncs (X,REAL)) Function-like V41([:REAL,(PFuncs (X,REAL)):], PFuncs (X,REAL)) Element of bool [:[:REAL,(PFuncs (X,REAL)):],(PFuncs (X,REAL)):]

x is V11() real ext-real Element of REAL

y is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

S . (x,y) is Element of PFuncs (X,REAL)

[x,y] is set

{x,y} is non empty set

{x} is non empty V166() V167() V168() set

{{x,y},{x}} is non empty set

S . [x,y] is set

x (#) y is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

M . (x,y) is Element of PFuncs (X,REAL)

M . [x,y] is set

X is non empty set

X --> 0 is V13() V16(X) V17( NAT ) V17( RAT ) V17( INT ) Function-like V41(X, NAT ) V173() V174() V175() V176() Element of bool [:X,NAT:]

[:X,NAT:] is non empty V17( RAT ) V17( INT ) V173() V174() V175() V176() set

bool [:X,NAT:] is non empty set

PFuncs (X,REAL) is non empty functional PartFunc-set of X, REAL

[:X,REAL:] is non empty V173() V174() V175() set

bool [:X,REAL:] is non empty set

X is non empty set

X --> 1 is V13() V16(X) V17( NAT ) V17( RAT ) V17( INT ) Function-like V41(X, NAT ) V173() V174() V175() V176() Element of bool [:X,NAT:]

[:X,NAT:] is non empty V17( RAT ) V17( INT ) V173() V174() V175() V176() set

bool [:X,NAT:] is non empty set

PFuncs (X,REAL) is non empty functional PartFunc-set of X, REAL

[:X,REAL:] is non empty V173() V174() V175() set

bool [:X,REAL:] is non empty set

X is non empty set

PFuncs (X,REAL) is non empty functional PartFunc-set of X, REAL

addpfunc X is V13() V16([:(PFuncs (X,REAL)),(PFuncs (X,REAL)):]) V17( PFuncs (X,REAL)) Function-like V41([:(PFuncs (X,REAL)),(PFuncs (X,REAL)):], PFuncs (X,REAL)) Element of bool [:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):]

[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):] is non empty set

[:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set

bool [:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set

S is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

dom S is Element of bool X

bool X is non empty set

M is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

dom M is Element of bool X

x is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

(X,REAL,(addpfunc X),M,x) is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

[M,x] is set

{M,x} is non empty set

{M} is non empty set

{{M,x},{M}} is non empty set

(addpfunc X) . [M,x] is set

dom x is Element of bool X

(dom M) /\ (dom x) is Element of bool X

M + x is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

dom (M + x) is Element of bool X

y is Element of X

S . y is V11() real ext-real set

(M + x) . y is V11() real ext-real set

M . y is V11() real ext-real set

x . y is V11() real ext-real set

(M . y) + (x . y) is V11() real ext-real set

a is Element of X

(X,REAL,(addpfunc X),M,x) . a is V11() real ext-real set

(M + x) . a is V11() real ext-real set

M . a is V11() real ext-real set

x . a is V11() real ext-real set

(M . a) + (x . a) is V11() real ext-real set

S . a is V11() real ext-real set

dom (X,REAL,(addpfunc X),M,x) is Element of bool X

X is non empty set

PFuncs (X,REAL) is non empty functional PartFunc-set of X, REAL

(X) is V13() V16([:(PFuncs (X,REAL)),(PFuncs (X,REAL)):]) V17( PFuncs (X,REAL)) Function-like V41([:(PFuncs (X,REAL)),(PFuncs (X,REAL)):], PFuncs (X,REAL)) Element of bool [:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):]

[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):] is non empty set

[:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set

bool [:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set

S is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

dom S is Element of bool X

bool X is non empty set

M is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

dom M is Element of bool X

x is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

(X,REAL,(X),M,x) is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

[M,x] is set

{M,x} is non empty set

{M} is non empty set

{{M,x},{M}} is non empty set

(X) . [M,x] is set

dom x is Element of bool X

(dom M) /\ (dom x) is Element of bool X

M (#) x is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

dom (M (#) x) is Element of bool X

a is Element of X

S . a is V11() real ext-real set

(M (#) x) . a is V11() real ext-real set

M . a is V11() real ext-real set

x . a is V11() real ext-real set

(M . a) * (x . a) is V11() real ext-real set

a is Element of X

(X,REAL,(X),M,x) . a is V11() real ext-real set

(M (#) x) . a is V11() real ext-real set

M . a is V11() real ext-real set

x . a is V11() real ext-real set

(M . a) * (x . a) is V11() real ext-real set

S . a is V11() real ext-real set

dom (X,REAL,(X),M,x) is Element of bool X

X is non empty set

(X) is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

PFuncs (X,REAL) is non empty functional PartFunc-set of X, REAL

X --> 0 is V13() V16(X) V17( NAT ) V17( RAT ) V17( INT ) Function-like V41(X, NAT ) V173() V174() V175() V176() Element of bool [:X,NAT:]

[:X,NAT:] is non empty V17( RAT ) V17( INT ) V173() V174() V175() V176() set

bool [:X,NAT:] is non empty set

(X) is V13() V16(X) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (X,REAL)

X --> 1 is V13() V16(X) V17( NAT ) V17( RAT ) V17( INT ) Function-like V41(X, NAT ) V173() V174() V175() V176() Element of bool [:X,NAT:]

the Element of X is Element of X

(X) . the Element of X is V11() real ext-real set

X is V11() real ext-real Element of REAL

S is non empty set

PFuncs (S,REAL) is non empty functional PartFunc-set of S, REAL

(S) is V13() V16([:REAL,(PFuncs (S,REAL)):]) V17( PFuncs (S,REAL)) Function-like V41([:REAL,(PFuncs (S,REAL)):], PFuncs (S,REAL)) Element of bool [:[:REAL,(PFuncs (S,REAL)):],(PFuncs (S,REAL)):]

[:REAL,(PFuncs (S,REAL)):] is non empty set

[:[:REAL,(PFuncs (S,REAL)):],(PFuncs (S,REAL)):] is non empty set

bool [:[:REAL,(PFuncs (S,REAL)):],(PFuncs (S,REAL)):] is non empty set

M is V13() V16(S) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (S,REAL)

dom M is Element of bool S

bool S is non empty set

x is V13() V16(S) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (S,REAL)

(S) . (X,x) is Element of PFuncs (S,REAL)

[X,x] is set

{X,x} is non empty set

{X} is non empty V166() V167() V168() set

{{X,x},{X}} is non empty set

(S) . [X,x] is set

dom x is Element of bool S

X (#) x is V13() V16(S) V17( REAL ) Function-like V173() V174() V175() Element of PFuncs (S,REAL)

dom (X (#) x) is Element of bool S

y is Element of