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