REAL is non empty V37() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V37() V42() V43() Element of bool REAL
bool REAL is non empty V37() set
COMPLEX is non empty V37() set
RAT is non empty V37() set
INT is non empty V37() set
[:COMPLEX,COMPLEX:] is Relation-like non empty V37() set
bool [:COMPLEX,COMPLEX:] is non empty V37() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty V37() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V37() set
[:REAL,REAL:] is Relation-like non empty V37() set
bool [:REAL,REAL:] is non empty V37() set
[:[:REAL,REAL:],REAL:] is Relation-like non empty V37() set
bool [:[:REAL,REAL:],REAL:] is non empty V37() set
[:RAT,RAT:] is Relation-like non empty V37() set
bool [:RAT,RAT:] is non empty V37() set
[:[:RAT,RAT:],RAT:] is Relation-like non empty V37() set
bool [:[:RAT,RAT:],RAT:] is non empty V37() set
[:INT,INT:] is Relation-like non empty V37() set
bool [:INT,INT:] is non empty V37() set
[:[:INT,INT:],INT:] is Relation-like non empty V37() set
bool [:[:INT,INT:],INT:] is non empty V37() set
[:NAT,NAT:] is Relation-like non empty V37() set
[:[:NAT,NAT:],NAT:] is Relation-like non empty V37() set
bool [:[:NAT,NAT:],NAT:] is non empty V37() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V37() V42() V43() set
bool NAT is non empty V37() set
bool NAT is non empty V37() set
{} is Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real V37() V42() V44( {} ) set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V33() real V37() V42() Element of NAT
{{},1} is non empty set
addreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like quasi_total commutative associative Element of bool [:[:REAL,REAL:],REAL:]
multreal is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like quasi_total commutative associative Element of bool [:[:REAL,REAL:],REAL:]
c1 is set
a is non empty set
Funcs (c1,a) is non empty FUNCTION_DOMAIN of c1,a
[:(Funcs (c1,a)),(Funcs (c1,a)):] is Relation-like non empty set
[:[:(Funcs (c1,a)),(Funcs (c1,a)):],(Funcs (c1,a)):] is Relation-like non empty set
bool [:[:(Funcs (c1,a)),(Funcs (c1,a)):],(Funcs (c1,a)):] is non empty set
b is Relation-like [:(Funcs (c1,a)),(Funcs (c1,a)):] -defined Funcs (c1,a) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,a)),(Funcs (c1,a)):],(Funcs (c1,a)):]
v is Relation-like c1 -defined a -valued Function-like quasi_total Element of Funcs (c1,a)
a is Relation-like c1 -defined a -valued Function-like quasi_total Element of Funcs (c1,a)
b . (v,a) is set
[v,a] is set
b . [v,a] is set
b is Element of Funcs (c1,a)
h is Element of Funcs (c1,a)
b . (b,h) is Element of Funcs (c1,a)
[b,h] is set
b . [b,h] is set
b is non empty set
v is non empty set
[:b,v:] is Relation-like non empty set
c1 is non empty set
a is non empty set
Funcs (c1,a) is non empty FUNCTION_DOMAIN of c1,a
[:[:b,v:],(Funcs (c1,a)):] is Relation-like non empty set
bool [:[:b,v:],(Funcs (c1,a)):] is non empty set
a is Relation-like [:b,v:] -defined Funcs (c1,a) -valued Function-like quasi_total Element of bool [:[:b,v:],(Funcs (c1,a)):]
b is Element of [:b,v:]
a . b is set
a . b is Element of Funcs (c1,a)
c1 is non empty set
[:c1,c1:] is Relation-like non empty set
[:[:c1,c1:],c1:] is Relation-like non empty set
bool [:[:c1,c1:],c1:] is non empty set
a is set
[:a,c1:] is Relation-like set
bool [:a,c1:] is non empty set
b is Relation-like [:c1,c1:] -defined c1 -valued Function-like quasi_total Element of bool [:[:c1,c1:],c1:]
v is Relation-like a -defined c1 -valued Function-like quasi_total Element of bool [:a,c1:]
a is Relation-like a -defined c1 -valued Function-like quasi_total Element of bool [:a,c1:]
b .: (v,a) is Relation-like Function-like set
K291(v,a) is Relation-like Function-like set
K291(v,a) * b is Relation-like c1 -valued set
Funcs (a,c1) is non empty FUNCTION_DOMAIN of a,c1
b .: (v,a) is Relation-like a -defined c1 -valued Function-like quasi_total Element of bool [:a,c1:]
c1 is non empty set
[:c1,c1:] is Relation-like non empty set
[:[:c1,c1:],c1:] is Relation-like non empty set
bool [:[:c1,c1:],c1:] is non empty set
a is set
[:a,c1:] is Relation-like set
bool [:a,c1:] is non empty set
b is Relation-like [:c1,c1:] -defined c1 -valued Function-like quasi_total Element of bool [:[:c1,c1:],c1:]
v is Element of c1
a is Relation-like a -defined c1 -valued Function-like quasi_total Element of bool [:a,c1:]
b [;] (v,a) is Relation-like Function-like set
dom a is set
(dom a) --> v is Relation-like dom a -defined c1 -valued Function-like constant V14( dom a) set
{v} is non empty trivial V44(1) set
[:(dom a),{v}:] is Relation-like set
K291(((dom a) --> v),a) is Relation-like Function-like set
K291(((dom a) --> v),a) * b is Relation-like c1 -valued set
Funcs (a,c1) is non empty FUNCTION_DOMAIN of a,c1
b [;] (v,a) is Relation-like a -defined c1 -valued Function-like quasi_total Element of bool [:a,c1:]
c1 is set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
a is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
b is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
v is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1,REAL,a,b,v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[b,v] is set
a . [b,v] is set
(REAL,c1,addreal,b,v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(b,v) is Relation-like Function-like set
K291(b,v) * addreal is Relation-like REAL -valued set
a is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
b is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
v is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
a is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1,REAL,a,v,a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[v,a] is set
a . [v,a] is set
(REAL,c1,addreal,v,a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(v,a) is Relation-like Function-like set
K291(v,a) * addreal is Relation-like REAL -valued set
(c1,REAL,b,v,a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
b . [v,a] is set
c1 is set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
a is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
b is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
v is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1,REAL,a,b,v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[b,v] is set
a . [b,v] is set
(REAL,c1,multreal,b,v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(b,v) is Relation-like Function-like set
K291(b,v) * multreal is Relation-like REAL -valued set
a is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
b is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
v is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
a is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1,REAL,a,v,a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[v,a] is set
a . [v,a] is set
(REAL,c1,multreal,v,a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(v,a) is Relation-like Function-like set
K291(v,a) * multreal is Relation-like REAL -valued set
(c1,REAL,b,v,a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
b . [v,a] is set
c1 is set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
[:REAL,(Funcs (c1,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty V37() set
a is Relation-like [:REAL,(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
b is V33() real Element of REAL
v is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
a . (b,v) is Element of Funcs (c1,REAL)
[b,v] is set
a . [b,v] is set
(REAL,c1,multreal,b,v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
dom v is set
(dom v) --> b is Relation-like dom v -defined REAL -valued Function-like constant V14( dom v) set
{b} is non empty trivial V44(1) set
[:(dom v),{b}:] is Relation-like set
K291(((dom v) --> b),v) is Relation-like Function-like set
K291(((dom v) --> b),v) * multreal is Relation-like REAL -valued set
a is Relation-like [:REAL,(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
b is Relation-like [:REAL,(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
v is V33() real Element of REAL
a is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
a . (v,a) is Element of Funcs (c1,REAL)
[v,a] is set
a . [v,a] is set
(REAL,c1,multreal,v,a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
dom a is set
(dom a) --> v is Relation-like dom a -defined REAL -valued Function-like constant V14( dom a) set
{v} is non empty trivial V44(1) set
[:(dom a),{v}:] is Relation-like set
K291(((dom a) --> v),a) is Relation-like Function-like set
K291(((dom a) --> v),a) * multreal is Relation-like REAL -valued set
b . (v,a) is Element of Funcs (c1,REAL)
b . [v,a] is set
c1 is set
0 is Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real V37() V42() V44( {} ) Element of NAT
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like set
bool [:c1,NAT:] is non empty set
{0} is non empty trivial V44(1) set
[:c1,{0}:] is Relation-like set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
[:c1,REAL:] is Relation-like set
bool [:c1,REAL:] is non empty set
c1 is set
c1 --> 1 is Relation-like non-empty c1 -defined NAT -valued Function-like constant V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like set
bool [:c1,NAT:] is non empty set
{1} is non empty trivial V44(1) set
[:c1,{1}:] is Relation-like set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
[:c1,REAL:] is Relation-like set
bool [:c1,REAL:] is non empty set
c1 is non empty set
a is non empty set
[:c1,a:] is Relation-like non empty set
bool [:c1,a:] is non empty set
b is Element of c1
v is Relation-like c1 -defined a -valued Function-like quasi_total Element of bool [:c1,a:]
dom v is set
c1 is non empty set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
a is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
b is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
v is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1,REAL,(c1),b,v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[b,v] is set
(c1) . [b,v] is set
a is Element of c1
(REAL,c1,addreal,b,v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(b,v) is Relation-like Function-like set
K291(b,v) * addreal is Relation-like REAL -valued set
dom (REAL,c1,addreal,b,v) is set
(c1,REAL,(c1),b,v) . a is V33() real Element of REAL
(REAL,c1,addreal,b,v) . a is V33() real Element of REAL
b . a is V33() real Element of REAL
v . a is V33() real Element of REAL
addreal . ((b . a),(v . a)) is V33() real Element of REAL
[(b . a),(v . a)] is set
addreal . [(b . a),(v . a)] is set
(b . a) + (v . a) is V33() real Element of REAL
a . a is V33() real Element of REAL
a is Element of c1
a . a is V33() real Element of REAL
(REAL,c1,addreal,b,v) . a is V33() real Element of REAL
b . a is V33() real Element of REAL
v . a is V33() real Element of REAL
addreal . ((b . a),(v . a)) is V33() real Element of REAL
[(b . a),(v . a)] is set
addreal . [(b . a),(v . a)] is set
(b . a) + (v . a) is V33() real Element of REAL
a is Element of c1
a . a is V33() real Element of REAL
b . a is V33() real Element of REAL
v . a is V33() real Element of REAL
(b . a) + (v . a) is V33() real Element of REAL
b is Element of c1
a . b is V33() real Element of REAL
b . b is V33() real Element of REAL
v . b is V33() real Element of REAL
(b . b) + (v . b) is V33() real Element of REAL
c1 is non empty set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
a is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
b is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
v is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1,REAL,(c1),b,v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[b,v] is set
(c1) . [b,v] is set
a is Element of c1
(REAL,c1,multreal,b,v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(b,v) is Relation-like Function-like set
K291(b,v) * multreal is Relation-like REAL -valued set
dom (REAL,c1,multreal,b,v) is set
(c1,REAL,(c1),b,v) . a is V33() real Element of REAL
(REAL,c1,multreal,b,v) . a is V33() real Element of REAL
b . a is V33() real Element of REAL
v . a is V33() real Element of REAL
multreal . ((b . a),(v . a)) is V33() real Element of REAL
[(b . a),(v . a)] is set
multreal . [(b . a),(v . a)] is set
(b . a) * (v . a) is V33() real Element of REAL
a . a is V33() real Element of REAL
a is Element of c1
a . a is V33() real Element of REAL
(REAL,c1,multreal,b,v) . a is V33() real Element of REAL
b . a is V33() real Element of REAL
v . a is V33() real Element of REAL
multreal . ((b . a),(v . a)) is V33() real Element of REAL
[(b . a),(v . a)] is set
multreal . [(b . a),(v . a)] is set
(b . a) * (v . a) is V33() real Element of REAL
a is Element of c1
a . a is V33() real Element of REAL
b . a is V33() real Element of REAL
v . a is V33() real Element of REAL
(b . a) * (v . a) is V33() real Element of REAL
b is Element of c1
a . b is V33() real Element of REAL
b . b is V33() real Element of REAL
v . b is V33() real Element of REAL
(b . b) * (v . b) is V33() real Element of REAL
c1 is non empty set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like non empty V37() set
bool [:c1,NAT:] is non empty V37() set
[:c1,{0}:] is Relation-like non empty set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 1 is Relation-like non-empty c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,{1}:] is Relation-like non empty set
the Element of c1 is Element of c1
(c1) . the Element of c1 is V33() real Element of REAL
c1 is non empty set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:REAL,(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:REAL,(Funcs (c1,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty V37() set
a is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
b is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
v is V33() real Element of REAL
[v,b] is Element of [:REAL,(Funcs (c1,REAL)):]
(c1,REAL,REAL,(Funcs (c1,REAL)),(c1),[v,b]) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
a is Element of c1
a . a is V33() real Element of REAL
b . a is V33() real Element of REAL
v * (b . a) is V33() real Element of REAL
(c1) . (v,b) is Element of Funcs (c1,REAL)
[v,b] is set
(c1) . [v,b] is set
(REAL,c1,multreal,v,b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
dom b is set
(dom b) --> v is Relation-like dom b -defined REAL -valued Function-like constant V14( dom b) set
{v} is non empty trivial V44(1) set
[:(dom b),{v}:] is Relation-like set
K291(((dom b) --> v),b) is Relation-like Function-like set
K291(((dom b) --> v),b) * multreal is Relation-like REAL -valued set
(REAL,c1,multreal,v,b) . a is V33() real Element of REAL
multreal . (v,(b . a)) is V33() real Element of REAL
[v,(b . a)] is set
multreal . [v,(b . a)] is set
a is Element of c1
a . a is V33() real Element of REAL
(c1,REAL,REAL,(Funcs (c1,REAL)),(c1),[v,b]) . a is V33() real Element of REAL
(REAL,c1,multreal,v,b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
dom b is set
(dom b) --> v is Relation-like dom b -defined REAL -valued Function-like constant V14( dom b) set
{v} is non empty trivial V44(1) set
[:(dom b),{v}:] is Relation-like set
K291(((dom b) --> v),b) is Relation-like Function-like set
K291(((dom b) --> v),b) * multreal is Relation-like REAL -valued set
(c1) . (v,b) is Element of Funcs (c1,REAL)
[v,b] is set
(c1) . [v,b] is set
b . a is V33() real Element of REAL
v * (b . a) is V33() real Element of REAL
multreal . (v,(b . a)) is V33() real Element of REAL
[v,(b . a)] is set
multreal . [v,(b . a)] is set
(c1) . (v,b) is Element of Funcs (c1,REAL)
[v,b] is set
(c1) . [v,b] is set
a is Element of c1
a . a is V33() real Element of REAL
b . a is V33() real Element of REAL
v * (b . a) is V33() real Element of REAL
c1 is set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
a is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
b is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1,REAL,(c1),a,b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[a,b] is set
(c1) . [a,b] is set
(c1,REAL,(c1),b,a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[b,a] is set
(c1) . [b,a] is set
(REAL,c1,addreal,a,b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(a,b) is Relation-like Function-like set
K291(a,b) * addreal is Relation-like REAL -valued set
(REAL,c1,addreal,b,a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(b,a) is Relation-like Function-like set
K291(b,a) * addreal is Relation-like REAL -valued set
c1 is set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
a is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
b is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
v is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1,REAL,(c1),b,v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[b,v] is set
(c1) . [b,v] is set
(c1,REAL,(c1),a,(c1,REAL,(c1),b,v)) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[a,(c1,REAL,(c1),b,v)] is set
(c1) . [a,(c1,REAL,(c1),b,v)] is set
(c1,REAL,(c1),a,b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[a,b] is set
(c1) . [a,b] is set
(c1,REAL,(c1),(c1,REAL,(c1),a,b),v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[(c1,REAL,(c1),a,b),v] is set
(c1) . [(c1,REAL,(c1),a,b),v] is set
(REAL,c1,addreal,b,v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(b,v) is Relation-like Function-like set
K291(b,v) * addreal is Relation-like REAL -valued set
(c1,REAL,(c1),a,(REAL,c1,addreal,b,v)) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[a,(REAL,c1,addreal,b,v)] is set
(c1) . [a,(REAL,c1,addreal,b,v)] is set
(REAL,c1,addreal,a,(REAL,c1,addreal,b,v)) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(a,(REAL,c1,addreal,b,v)) is Relation-like Function-like set
K291(a,(REAL,c1,addreal,b,v)) * addreal is Relation-like REAL -valued set
(REAL,c1,addreal,a,b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(a,b) is Relation-like Function-like set
K291(a,b) * addreal is Relation-like REAL -valued set
(REAL,c1,addreal,(REAL,c1,addreal,a,b),v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291((REAL,c1,addreal,a,b),v) is Relation-like Function-like set
K291((REAL,c1,addreal,a,b),v) * addreal is Relation-like REAL -valued set
(c1,REAL,(c1),(REAL,c1,addreal,a,b),v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[(REAL,c1,addreal,a,b),v] is set
(c1) . [(REAL,c1,addreal,a,b),v] is set
c1 is set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
a is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
b is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1,REAL,(c1),a,b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[a,b] is set
(c1) . [a,b] is set
(c1,REAL,(c1),b,a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[b,a] is set
(c1) . [b,a] is set
(REAL,c1,multreal,a,b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(a,b) is Relation-like Function-like set
K291(a,b) * multreal is Relation-like REAL -valued set
(REAL,c1,multreal,b,a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(b,a) is Relation-like Function-like set
K291(b,a) * multreal is Relation-like REAL -valued set
c1 is set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
a is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
b is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
v is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1,REAL,(c1),b,v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[b,v] is set
(c1) . [b,v] is set
(c1,REAL,(c1),a,(c1,REAL,(c1),b,v)) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[a,(c1,REAL,(c1),b,v)] is set
(c1) . [a,(c1,REAL,(c1),b,v)] is set
(c1,REAL,(c1),a,b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[a,b] is set
(c1) . [a,b] is set
(c1,REAL,(c1),(c1,REAL,(c1),a,b),v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[(c1,REAL,(c1),a,b),v] is set
(c1) . [(c1,REAL,(c1),a,b),v] is set
(REAL,c1,multreal,b,v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(b,v) is Relation-like Function-like set
K291(b,v) * multreal is Relation-like REAL -valued set
(c1,REAL,(c1),a,(REAL,c1,multreal,b,v)) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[a,(REAL,c1,multreal,b,v)] is set
(c1) . [a,(REAL,c1,multreal,b,v)] is set
(REAL,c1,multreal,a,(REAL,c1,multreal,b,v)) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(a,(REAL,c1,multreal,b,v)) is Relation-like Function-like set
K291(a,(REAL,c1,multreal,b,v)) * multreal is Relation-like REAL -valued set
(REAL,c1,multreal,a,b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(a,b) is Relation-like Function-like set
K291(a,b) * multreal is Relation-like REAL -valued set
(REAL,c1,multreal,(REAL,c1,multreal,a,b),v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291((REAL,c1,multreal,a,b),v) is Relation-like Function-like set
K291((REAL,c1,multreal,a,b),v) * multreal is Relation-like REAL -valued set
(c1,REAL,(c1),(REAL,c1,multreal,a,b),v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[(REAL,c1,multreal,a,b),v] is set
(c1) . [(REAL,c1,multreal,a,b),v] is set
c1 is set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 1 is Relation-like non-empty c1 -defined NAT -valued Function-like constant V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like set
bool [:c1,NAT:] is non empty set
[:c1,{1}:] is Relation-like set
a is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1,REAL,(c1),(c1),a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[(c1),a] is set
(c1) . [(c1),a] is set
(REAL,c1,multreal,(c1),a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291((c1),a) is Relation-like Function-like set
K291((c1),a) * multreal is Relation-like REAL -valued set
b is non empty set
Funcs (b,REAL) is non empty FUNCTION_DOMAIN of b, REAL
(b) is Relation-like [:(Funcs (b,REAL)),(Funcs (b,REAL)):] -defined Funcs (b,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):]
[:(Funcs (b,REAL)),(Funcs (b,REAL)):] is Relation-like non empty set
[:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):] is non empty set
(b) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
b --> 1 is Relation-like non-empty b -defined NAT -valued Function-like constant non empty V14(b) quasi_total Element of bool [:b,NAT:]
[:b,NAT:] is Relation-like non empty V37() set
bool [:b,NAT:] is non empty V37() set
[:b,{1}:] is Relation-like non empty set
v is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
(b,REAL,(b),(b),v) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
[(b),v] is set
(b) . [(b),v] is set
a is Element of b
(b,REAL,(b),(b),v) . a is V33() real Element of REAL
(b) . a is V33() real Element of REAL
v . a is V33() real Element of REAL
((b) . a) * (v . a) is V33() real Element of REAL
1 * (v . a) is V33() real Element of REAL
c1 is set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like set
bool [:c1,NAT:] is non empty set
[:c1,{0}:] is Relation-like set
a is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1,REAL,(c1),(c1),a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[(c1),a] is set
(c1) . [(c1),a] is set
(REAL,c1,addreal,(c1),a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291((c1),a) is Relation-like Function-like set
K291((c1),a) * addreal is Relation-like REAL -valued set
b is non empty set
Funcs (b,REAL) is non empty FUNCTION_DOMAIN of b, REAL
(b) is Relation-like [:(Funcs (b,REAL)),(Funcs (b,REAL)):] -defined Funcs (b,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):]
[:(Funcs (b,REAL)),(Funcs (b,REAL)):] is Relation-like non empty set
[:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):] is non empty set
(b) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
b --> 0 is Relation-like b -defined NAT -valued Function-like constant non empty V14(b) quasi_total Element of bool [:b,NAT:]
[:b,NAT:] is Relation-like non empty V37() set
bool [:b,NAT:] is non empty V37() set
[:b,{0}:] is Relation-like non empty set
v is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
(b,REAL,(b),(b),v) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
[(b),v] is set
(b) . [(b),v] is set
a is Element of b
(b,REAL,(b),(b),v) . a is V33() real Element of REAL
(b) . a is V33() real Element of REAL
v . a is V33() real Element of REAL
((b) . a) + (v . a) is V33() real Element of REAL
0 + (v . a) is V33() real Element of REAL
- 1 is V33() real Element of REAL
c1 is set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
[:REAL,(Funcs (c1,REAL)):] is Relation-like non empty V37() set
(c1) is Relation-like [:REAL,(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty V37() set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like set
bool [:c1,NAT:] is non empty set
[:c1,{0}:] is Relation-like set
a is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[(- 1),a] is Element of [:REAL,(Funcs (c1,REAL)):]
(c1) . [(- 1),a] is Element of Funcs (c1,REAL)
(c1,REAL,(c1),a,((c1) . [(- 1),a])) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[a,((c1) . [(- 1),a])] is set
(c1) . [a,((c1) . [(- 1),a])] is set
b is non empty set
Funcs (b,REAL) is non empty FUNCTION_DOMAIN of b, REAL
v is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
a is Element of b
v . a is V33() real Element of REAL
(b) is Relation-like [:(Funcs (b,REAL)),(Funcs (b,REAL)):] -defined Funcs (b,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):]
[:(Funcs (b,REAL)),(Funcs (b,REAL)):] is Relation-like non empty set
[:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):] is non empty set
(b) is Relation-like [:REAL,(Funcs (b,REAL)):] -defined Funcs (b,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):]
[:REAL,(Funcs (b,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):] is non empty V37() set
[(- 1),v] is Element of [:REAL,(Funcs (b,REAL)):]
(b,REAL,REAL,(Funcs (b,REAL)),(b),[(- 1),v]) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
(b,REAL,(b),v,(b,REAL,REAL,(Funcs (b,REAL)),(b),[(- 1),v])) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
[v,(b,REAL,REAL,(Funcs (b,REAL)),(b),[(- 1),v])] is set
(b) . [v,(b,REAL,REAL,(Funcs (b,REAL)),(b),[(- 1),v])] is set
(b,REAL,(b),v,(b,REAL,REAL,(Funcs (b,REAL)),(b),[(- 1),v])) . a is V33() real Element of REAL
(b,REAL,REAL,(Funcs (b,REAL)),(b),[(- 1),v]) . a is V33() real Element of REAL
(v . a) + ((b,REAL,REAL,(Funcs (b,REAL)),(b),[(- 1),v]) . a) is V33() real Element of REAL
(- 1) * (v . a) is V33() real Element of REAL
(v . a) + ((- 1) * (v . a)) is V33() real Element of REAL
(b) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
b --> 0 is Relation-like b -defined NAT -valued Function-like constant non empty V14(b) quasi_total Element of bool [:b,NAT:]
[:b,NAT:] is Relation-like non empty V37() set
bool [:b,NAT:] is non empty V37() set
[:b,{0}:] is Relation-like non empty set
(b) . a is V33() real Element of REAL
c1 is set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:REAL,(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:REAL,(Funcs (c1,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty V37() set
a is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1) . (1,a) is Element of Funcs (c1,REAL)
[1,a] is set
(c1) . [1,a] is set
(REAL,c1,multreal,1,a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
dom a is set
(dom a) --> 1 is Relation-like non-empty dom a -defined NAT -valued Function-like constant V14( dom a) set
[:(dom a),{1}:] is Relation-like set
K291(((dom a) --> 1),a) is Relation-like Function-like set
K291(((dom a) --> 1),a) * multreal is Relation-like REAL -valued set
b is non empty set
Funcs (b,REAL) is non empty FUNCTION_DOMAIN of b, REAL
(b) is Relation-like [:REAL,(Funcs (b,REAL)):] -defined Funcs (b,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):]
[:REAL,(Funcs (b,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):] is non empty V37() set
v is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
(b) . (1,v) is Element of Funcs (b,REAL)
[1,v] is set
(b) . [1,v] is set
a is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
b is Element of b
a . b is V33() real Element of REAL
v . b is V33() real Element of REAL
1 * (v . b) is V33() real Element of REAL
c1 is V33() real Element of REAL
a is V33() real Element of REAL
c1 * a is V33() real Element of REAL
b is set
Funcs (b,REAL) is non empty FUNCTION_DOMAIN of b, REAL
(b) is Relation-like [:REAL,(Funcs (b,REAL)):] -defined Funcs (b,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):]
[:REAL,(Funcs (b,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):] is non empty V37() set
v is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
(b) . (a,v) is Element of Funcs (b,REAL)
[a,v] is set
(b) . [a,v] is set
(b) . (c1,((b) . (a,v))) is Element of Funcs (b,REAL)
[c1,((b) . (a,v))] is set
(b) . [c1,((b) . (a,v))] is set
(b) . ((c1 * a),v) is Element of Funcs (b,REAL)
[(c1 * a),v] is set
(b) . [(c1 * a),v] is set
(REAL,b,multreal,a,v) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
dom v is set
(dom v) --> a is Relation-like dom v -defined REAL -valued Function-like constant V14( dom v) set
{a} is non empty trivial V44(1) set
[:(dom v),{a}:] is Relation-like set
K291(((dom v) --> a),v) is Relation-like Function-like set
K291(((dom v) --> a),v) * multreal is Relation-like REAL -valued set
(REAL,b,multreal,c1,(REAL,b,multreal,a,v)) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
dom (REAL,b,multreal,a,v) is set
(dom (REAL,b,multreal,a,v)) --> c1 is Relation-like dom (REAL,b,multreal,a,v) -defined REAL -valued Function-like constant V14( dom (REAL,b,multreal,a,v)) set
{c1} is non empty trivial V44(1) set
[:(dom (REAL,b,multreal,a,v)),{c1}:] is Relation-like set
K291(((dom (REAL,b,multreal,a,v)) --> c1),(REAL,b,multreal,a,v)) is Relation-like Function-like set
K291(((dom (REAL,b,multreal,a,v)) --> c1),(REAL,b,multreal,a,v)) * multreal is Relation-like REAL -valued set
(REAL,b,multreal,(c1 * a),v) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
(dom v) --> (c1 * a) is Relation-like dom v -defined REAL -valued Function-like constant V14( dom v) set
{(c1 * a)} is non empty trivial V44(1) set
[:(dom v),{(c1 * a)}:] is Relation-like set
K291(((dom v) --> (c1 * a)),v) is Relation-like Function-like set
K291(((dom v) --> (c1 * a)),v) * multreal is Relation-like REAL -valued set
a is non empty set
Funcs (a,REAL) is non empty FUNCTION_DOMAIN of a, REAL
(a) is Relation-like [:REAL,(Funcs (a,REAL)):] -defined Funcs (a,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (a,REAL)):],(Funcs (a,REAL)):]
[:REAL,(Funcs (a,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (a,REAL)):],(Funcs (a,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (a,REAL)):],(Funcs (a,REAL)):] is non empty V37() set
b is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
[a,b] is Element of [:REAL,(Funcs (a,REAL)):]
(a,REAL,REAL,(Funcs (a,REAL)),(a),[a,b]) is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
[c1,(a,REAL,REAL,(Funcs (a,REAL)),(a),[a,b])] is Element of [:REAL,(Funcs (a,REAL)):]
(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,(a,REAL,REAL,(Funcs (a,REAL)),(a),[a,b])]) is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
h is Element of a
(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,(a,REAL,REAL,(Funcs (a,REAL)),(a),[a,b])]) . h is V33() real Element of REAL
(a,REAL,REAL,(Funcs (a,REAL)),(a),[a,b]) . h is V33() real Element of REAL
c1 * ((a,REAL,REAL,(Funcs (a,REAL)),(a),[a,b]) . h) is V33() real Element of REAL
b . h is V33() real Element of REAL
a * (b . h) is V33() real Element of REAL
c1 * (a * (b . h)) is V33() real Element of REAL
(c1 * a) * (b . h) is V33() real Element of REAL
[(c1 * a),b] is Element of [:REAL,(Funcs (a,REAL)):]
(a,REAL,REAL,(Funcs (a,REAL)),(a),[(c1 * a),b]) is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
(a,REAL,REAL,(Funcs (a,REAL)),(a),[(c1 * a),b]) . h is V33() real Element of REAL
c1 is V33() real Element of REAL
a is V33() real Element of REAL
c1 + a is V33() real Element of REAL
b is set
Funcs (b,REAL) is non empty FUNCTION_DOMAIN of b, REAL
(b) is Relation-like [:(Funcs (b,REAL)),(Funcs (b,REAL)):] -defined Funcs (b,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):]
[:(Funcs (b,REAL)),(Funcs (b,REAL)):] is Relation-like non empty set
[:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):] is non empty set
(b) is Relation-like [:REAL,(Funcs (b,REAL)):] -defined Funcs (b,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):]
[:REAL,(Funcs (b,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):] is non empty V37() set
v is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
(b) . (c1,v) is Element of Funcs (b,REAL)
[c1,v] is set
(b) . [c1,v] is set
(b) . (a,v) is Element of Funcs (b,REAL)
[a,v] is set
(b) . [a,v] is set
(b,REAL,(b),((b) . (c1,v)),((b) . (a,v))) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
[((b) . (c1,v)),((b) . (a,v))] is set
(b) . [((b) . (c1,v)),((b) . (a,v))] is set
(b) . ((c1 + a),v) is Element of Funcs (b,REAL)
[(c1 + a),v] is set
(b) . [(c1 + a),v] is set
(REAL,b,multreal,(c1 + a),v) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
dom v is set
(dom v) --> (c1 + a) is Relation-like dom v -defined REAL -valued Function-like constant V14( dom v) set
{(c1 + a)} is non empty trivial V44(1) set
[:(dom v),{(c1 + a)}:] is Relation-like set
K291(((dom v) --> (c1 + a)),v) is Relation-like Function-like set
K291(((dom v) --> (c1 + a)),v) * multreal is Relation-like REAL -valued set
a is non empty set
Funcs (a,REAL) is non empty FUNCTION_DOMAIN of a, REAL
(a) is Relation-like [:(Funcs (a,REAL)),(Funcs (a,REAL)):] -defined Funcs (a,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (a,REAL)),(Funcs (a,REAL)):],(Funcs (a,REAL)):]
[:(Funcs (a,REAL)),(Funcs (a,REAL)):] is Relation-like non empty set
[:[:(Funcs (a,REAL)),(Funcs (a,REAL)):],(Funcs (a,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (a,REAL)),(Funcs (a,REAL)):],(Funcs (a,REAL)):] is non empty set
(a) is Relation-like [:REAL,(Funcs (a,REAL)):] -defined Funcs (a,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (a,REAL)):],(Funcs (a,REAL)):]
[:REAL,(Funcs (a,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (a,REAL)):],(Funcs (a,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (a,REAL)):],(Funcs (a,REAL)):] is non empty V37() set
b is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
[c1,b] is Element of [:REAL,(Funcs (a,REAL)):]
(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,b]) is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
[a,b] is Element of [:REAL,(Funcs (a,REAL)):]
(a,REAL,REAL,(Funcs (a,REAL)),(a),[a,b]) is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
(a,REAL,(a),(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,b]),(a,REAL,REAL,(Funcs (a,REAL)),(a),[a,b])) is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
[(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,b]),(a,REAL,REAL,(Funcs (a,REAL)),(a),[a,b])] is set
(a) . [(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,b]),(a,REAL,REAL,(Funcs (a,REAL)),(a),[a,b])] is set
h is Element of a
(a,REAL,(a),(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,b]),(a,REAL,REAL,(Funcs (a,REAL)),(a),[a,b])) . h is V33() real Element of REAL
(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,b]) . h is V33() real Element of REAL
(a,REAL,REAL,(Funcs (a,REAL)),(a),[a,b]) . h is V33() real Element of REAL
((a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,b]) . h) + ((a,REAL,REAL,(Funcs (a,REAL)),(a),[a,b]) . h) is V33() real Element of REAL
b . h is V33() real Element of REAL
c1 * (b . h) is V33() real Element of REAL
(c1 * (b . h)) + ((a,REAL,REAL,(Funcs (a,REAL)),(a),[a,b]) . h) is V33() real Element of REAL
a * (b . h) is V33() real Element of REAL
(c1 * (b . h)) + (a * (b . h)) is V33() real Element of REAL
(c1 + a) * (b . h) is V33() real Element of REAL
[(c1 + a),b] is Element of [:REAL,(Funcs (a,REAL)):]
(a,REAL,REAL,(Funcs (a,REAL)),(a),[(c1 + a),b]) is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
(a,REAL,REAL,(Funcs (a,REAL)),(a),[(c1 + a),b]) . h is V33() real Element of REAL
c1 is V33() real Element of REAL
a is set
Funcs (a,REAL) is non empty FUNCTION_DOMAIN of a, REAL
(a) is Relation-like [:(Funcs (a,REAL)),(Funcs (a,REAL)):] -defined Funcs (a,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (a,REAL)),(Funcs (a,REAL)):],(Funcs (a,REAL)):]
[:(Funcs (a,REAL)),(Funcs (a,REAL)):] is Relation-like non empty set
[:[:(Funcs (a,REAL)),(Funcs (a,REAL)):],(Funcs (a,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (a,REAL)),(Funcs (a,REAL)):],(Funcs (a,REAL)):] is non empty set
(a) is Relation-like [:REAL,(Funcs (a,REAL)):] -defined Funcs (a,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (a,REAL)):],(Funcs (a,REAL)):]
[:REAL,(Funcs (a,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (a,REAL)):],(Funcs (a,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (a,REAL)):],(Funcs (a,REAL)):] is non empty V37() set
b is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
(a) . (c1,b) is Element of Funcs (a,REAL)
[c1,b] is set
(a) . [c1,b] is set
v is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
(a) . (c1,v) is Element of Funcs (a,REAL)
[c1,v] is set
(a) . [c1,v] is set
(a,REAL,(a),((a) . (c1,b)),((a) . (c1,v))) is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
[((a) . (c1,b)),((a) . (c1,v))] is set
(a) . [((a) . (c1,b)),((a) . (c1,v))] is set
(a,REAL,(a),b,v) is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
[b,v] is set
(a) . [b,v] is set
(a) . (c1,(a,REAL,(a),b,v)) is Element of Funcs (a,REAL)
[c1,(a,REAL,(a),b,v)] is set
(a) . [c1,(a,REAL,(a),b,v)] is set
(REAL,a,multreal,c1,(a,REAL,(a),b,v)) is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
dom (a,REAL,(a),b,v) is set
(dom (a,REAL,(a),b,v)) --> c1 is Relation-like dom (a,REAL,(a),b,v) -defined REAL -valued Function-like constant V14( dom (a,REAL,(a),b,v)) set
{c1} is non empty trivial V44(1) set
[:(dom (a,REAL,(a),b,v)),{c1}:] is Relation-like set
K291(((dom (a,REAL,(a),b,v)) --> c1),(a,REAL,(a),b,v)) is Relation-like Function-like set
K291(((dom (a,REAL,(a),b,v)) --> c1),(a,REAL,(a),b,v)) * multreal is Relation-like REAL -valued set
a is non empty set
Funcs (a,REAL) is non empty FUNCTION_DOMAIN of a, REAL
(a) is Relation-like [:(Funcs (a,REAL)),(Funcs (a,REAL)):] -defined Funcs (a,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (a,REAL)),(Funcs (a,REAL)):],(Funcs (a,REAL)):]
[:(Funcs (a,REAL)),(Funcs (a,REAL)):] is Relation-like non empty set
[:[:(Funcs (a,REAL)),(Funcs (a,REAL)):],(Funcs (a,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (a,REAL)),(Funcs (a,REAL)):],(Funcs (a,REAL)):] is non empty set
(a) is Relation-like [:REAL,(Funcs (a,REAL)):] -defined Funcs (a,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (a,REAL)):],(Funcs (a,REAL)):]
[:REAL,(Funcs (a,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (a,REAL)):],(Funcs (a,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (a,REAL)):],(Funcs (a,REAL)):] is non empty V37() set
b is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
[c1,b] is Element of [:REAL,(Funcs (a,REAL)):]
(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,b]) is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
h is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
[c1,h] is Element of [:REAL,(Funcs (a,REAL)):]
(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,h]) is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
(a,REAL,(a),(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,b]),(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,h])) is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
[(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,b]),(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,h])] is set
(a) . [(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,b]),(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,h])] is set
t is Element of a
(a,REAL,(a),(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,b]),(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,h])) . t is V33() real Element of REAL
(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,b]) . t is V33() real Element of REAL
(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,h]) . t is V33() real Element of REAL
((a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,b]) . t) + ((a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,h]) . t) is V33() real Element of REAL
b . t is V33() real Element of REAL
c1 * (b . t) is V33() real Element of REAL
(c1 * (b . t)) + ((a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,h]) . t) is V33() real Element of REAL
h . t is V33() real Element of REAL
c1 * (h . t) is V33() real Element of REAL
(c1 * (b . t)) + (c1 * (h . t)) is V33() real Element of REAL
(b . t) + (h . t) is V33() real Element of REAL
c1 * ((b . t) + (h . t)) is V33() real Element of REAL
(a,REAL,(a),b,h) is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
[b,h] is set
(a) . [b,h] is set
(a,REAL,(a),b,h) . t is V33() real Element of REAL
c1 * ((a,REAL,(a),b,h) . t) is V33() real Element of REAL
[c1,(a,REAL,(a),b,h)] is Element of [:REAL,(Funcs (a,REAL)):]
(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,(a,REAL,(a),b,h)]) is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
(a,REAL,REAL,(Funcs (a,REAL)),(a),[c1,(a,REAL,(a),b,h)]) . t is V33() real Element of REAL
c1 is set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
a is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
b is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
v is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1,REAL,(c1),b,v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[b,v] is set
(c1) . [b,v] is set
(c1,REAL,(c1),a,(c1,REAL,(c1),b,v)) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[a,(c1,REAL,(c1),b,v)] is set
(c1) . [a,(c1,REAL,(c1),b,v)] is set
(c1,REAL,(c1),a,b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[a,b] is set
(c1) . [a,b] is set
(c1,REAL,(c1),a,v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[a,v] is set
(c1) . [a,v] is set
(c1,REAL,(c1),(c1,REAL,(c1),a,b),(c1,REAL,(c1),a,v)) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[(c1,REAL,(c1),a,b),(c1,REAL,(c1),a,v)] is set
(c1) . [(c1,REAL,(c1),a,b),(c1,REAL,(c1),a,v)] is set
(REAL,c1,addreal,b,v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(b,v) is Relation-like Function-like set
K291(b,v) * addreal is Relation-like REAL -valued set
(REAL,c1,multreal,a,(REAL,c1,addreal,b,v)) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(a,(REAL,c1,addreal,b,v)) is Relation-like Function-like set
K291(a,(REAL,c1,addreal,b,v)) * multreal is Relation-like REAL -valued set
(REAL,c1,multreal,a,b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(a,b) is Relation-like Function-like set
K291(a,b) * multreal is Relation-like REAL -valued set
(REAL,c1,multreal,a,v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(a,v) is Relation-like Function-like set
K291(a,v) * multreal is Relation-like REAL -valued set
(REAL,c1,addreal,(REAL,c1,multreal,a,b),(REAL,c1,multreal,a,v)) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291((REAL,c1,multreal,a,b),(REAL,c1,multreal,a,v)) is Relation-like Function-like set
K291((REAL,c1,multreal,a,b),(REAL,c1,multreal,a,v)) * addreal is Relation-like REAL -valued set
a is Element of c1
(REAL,c1,multreal,a,(REAL,c1,addreal,b,v)) . a is set
(REAL,c1,addreal,(REAL,c1,multreal,a,b),(REAL,c1,multreal,a,v)) . a is set
b is non empty set
Funcs (b,REAL) is non empty FUNCTION_DOMAIN of b, REAL
b is Element of b
a . b is set
(REAL,c1,addreal,b,v) . b is set
multreal . ((a . b),((REAL,c1,addreal,b,v) . b)) is set
[(a . b),((REAL,c1,addreal,b,v) . b)] is set
multreal . [(a . b),((REAL,c1,addreal,b,v) . b)] is set
b . b is set
v . b is set
addreal . ((b . b),(v . b)) is set
[(b . b),(v . b)] is set
addreal . [(b . b),(v . b)] is set
multreal . ((a . b),(addreal . ((b . b),(v . b)))) is set
[(a . b),(addreal . ((b . b),(v . b)))] is set
multreal . [(a . b),(addreal . ((b . b),(v . b)))] is set
h is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
h . b is V33() real Element of REAL
t is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
t . b is V33() real Element of REAL
c9 is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
c9 . b is V33() real Element of REAL
addreal . ((t . b),(c9 . b)) is V33() real Element of REAL
[(t . b),(c9 . b)] is set
addreal . [(t . b),(c9 . b)] is set
(h . b) * (addreal . ((t . b),(c9 . b))) is V33() real Element of REAL
(t . b) + (c9 . b) is V33() real Element of REAL
(h . b) * ((t . b) + (c9 . b)) is V33() real Element of REAL
(h . b) * (t . b) is V33() real Element of REAL
(h . b) * (c9 . b) is V33() real Element of REAL
((h . b) * (t . b)) + ((h . b) * (c9 . b)) is V33() real Element of REAL
multreal . ((h . b),(c9 . b)) is V33() real Element of REAL
[(h . b),(c9 . b)] is set
multreal . [(h . b),(c9 . b)] is set
((h . b) * (t . b)) + (multreal . ((h . b),(c9 . b))) is V33() real Element of REAL
multreal . ((h . b),(t . b)) is V33() real Element of REAL
[(h . b),(t . b)] is set
multreal . [(h . b),(t . b)] is set
(multreal . ((h . b),(t . b))) + (multreal . ((h . b),(c9 . b))) is V33() real Element of REAL
a . a is set
b . a is set
multreal . ((a . a),(b . a)) is set
[(a . a),(b . a)] is set
multreal . [(a . a),(b . a)] is set
v . a is set
multreal . ((a . a),(v . a)) is set
[(a . a),(v . a)] is set
multreal . [(a . a),(v . a)] is set
addreal . ((multreal . ((a . a),(b . a))),(multreal . ((a . a),(v . a)))) is set
[(multreal . ((a . a),(b . a))),(multreal . ((a . a),(v . a)))] is set
addreal . [(multreal . ((a . a),(b . a))),(multreal . ((a . a),(v . a)))] is set
multreal .: (h,v) is Relation-like Function-like set
K291(h,v) is Relation-like Function-like set
K291(h,v) * multreal is Relation-like REAL -valued set
(multreal .: (h,v)) . a is set
addreal . ((multreal . ((a . a),(b . a))),((multreal .: (h,v)) . a)) is set
[(multreal . ((a . a),(b . a))),((multreal .: (h,v)) . a)] is set
addreal . [(multreal . ((a . a),(b . a))),((multreal .: (h,v)) . a)] is set
multreal .: (h,b) is Relation-like Function-like set
K291(h,b) is Relation-like Function-like set
K291(h,b) * multreal is Relation-like REAL -valued set
(multreal .: (h,b)) . a is set
addreal . (((multreal .: (h,b)) . a),((multreal .: (h,v)) . a)) is set
[((multreal .: (h,b)) . a),((multreal .: (h,v)) . a)] is set
addreal . [((multreal .: (h,b)) . a),((multreal .: (h,v)) . a)] is set
(c1,REAL,(c1),a,(REAL,c1,addreal,b,v)) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[a,(REAL,c1,addreal,b,v)] is set
(c1) . [a,(REAL,c1,addreal,b,v)] is set
(c1,REAL,(c1),(REAL,c1,multreal,a,b),(REAL,c1,multreal,a,v)) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[(REAL,c1,multreal,a,b),(REAL,c1,multreal,a,v)] is set
(c1) . [(REAL,c1,multreal,a,b),(REAL,c1,multreal,a,v)] is set
(c1,REAL,(c1),(c1,REAL,(c1),a,b),(REAL,c1,multreal,a,v)) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[(c1,REAL,(c1),a,b),(REAL,c1,multreal,a,v)] is set
(c1) . [(c1,REAL,(c1),a,b),(REAL,c1,multreal,a,v)] is set
c1 is set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like [:REAL,(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:REAL,(Funcs (c1,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty V37() set
a is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
b is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1,REAL,(c1),a,b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[a,b] is set
(c1) . [a,b] is set
a is V33() real Element of REAL
(c1) . (a,a) is Element of Funcs (c1,REAL)
[a,a] is set
(c1) . [a,a] is set
(c1,REAL,(c1),((c1) . (a,a)),b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[((c1) . (a,a)),b] is set
(c1) . [((c1) . (a,a)),b] is set
(c1) . (a,(c1,REAL,(c1),a,b)) is Element of Funcs (c1,REAL)
[a,(c1,REAL,(c1),a,b)] is set
(c1) . [a,(c1,REAL,(c1),a,b)] is set
(REAL,c1,multreal,a,a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
dom a is set
(dom a) --> a is Relation-like dom a -defined REAL -valued Function-like constant V14( dom a) set
{a} is non empty trivial V44(1) set
[:(dom a),{a}:] is Relation-like set
K291(((dom a) --> a),a) is Relation-like Function-like set
K291(((dom a) --> a),a) * multreal is Relation-like REAL -valued set
(c1,REAL,(c1),(REAL,c1,multreal,a,a),b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[(REAL,c1,multreal,a,a),b] is set
(c1) . [(REAL,c1,multreal,a,a),b] is set
(REAL,c1,multreal,(REAL,c1,multreal,a,a),b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291((REAL,c1,multreal,a,a),b) is Relation-like Function-like set
K291((REAL,c1,multreal,a,a),b) * multreal is Relation-like REAL -valued set
(REAL,c1,multreal,a,b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
K291(a,b) is Relation-like Function-like set
K291(a,b) * multreal is Relation-like REAL -valued set
(REAL,c1,multreal,a,(REAL,c1,multreal,a,b)) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
dom (REAL,c1,multreal,a,b) is set
(dom (REAL,c1,multreal,a,b)) --> a is Relation-like dom (REAL,c1,multreal,a,b) -defined REAL -valued Function-like constant V14( dom (REAL,c1,multreal,a,b)) set
[:(dom (REAL,c1,multreal,a,b)),{a}:] is Relation-like set
K291(((dom (REAL,c1,multreal,a,b)) --> a),(REAL,c1,multreal,a,b)) is Relation-like Function-like set
K291(((dom (REAL,c1,multreal,a,b)) --> a),(REAL,c1,multreal,a,b)) * multreal is Relation-like REAL -valued set
(c1) . (a,(REAL,c1,multreal,a,b)) is Element of Funcs (c1,REAL)
[a,(REAL,c1,multreal,a,b)] is set
(c1) . [a,(REAL,c1,multreal,a,b)] is set
c1 is set
a is non empty set
Funcs (a,REAL) is non empty FUNCTION_DOMAIN of a, REAL
b is set
[:a,REAL:] is Relation-like non empty V37() set
bool [:a,REAL:] is non empty V37() set
b is Relation-like a -defined REAL -valued Function-like quasi_total Element of bool [:a,REAL:]
v is set
v is Relation-like a -defined REAL -valued Function-like quasi_total Element of bool [:a,REAL:]
a is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
b is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
h is set
a . h is set
t is set
b . t is set
c1 is set
a is set
b is non empty set
Funcs (b,REAL) is non empty FUNCTION_DOMAIN of b, REAL
(b) is Relation-like [:(Funcs (b,REAL)),(Funcs (b,REAL)):] -defined Funcs (b,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):]
[:(Funcs (b,REAL)),(Funcs (b,REAL)):] is Relation-like non empty set
[:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):] is non empty set
(b) is Relation-like [:REAL,(Funcs (b,REAL)):] -defined Funcs (b,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):]
[:REAL,(Funcs (b,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):] is non empty V37() set
(b) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
b --> 0 is Relation-like b -defined NAT -valued Function-like constant non empty V14(b) quasi_total Element of bool [:b,NAT:]
[:b,NAT:] is Relation-like non empty V37() set
bool [:b,NAT:] is non empty V37() set
[:b,{0}:] is Relation-like non empty set
v is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
a is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
v . a is set
a . a is set
v . c1 is set
a . c1 is set
b is V33() real Element of REAL
[b,v] is Element of [:REAL,(Funcs (b,REAL)):]
(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,v]) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
h is V33() real Element of REAL
[h,a] is Element of [:REAL,(Funcs (b,REAL)):]
(b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a]) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
(b,REAL,(b),(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,v]),(b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a])) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
[(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,v]),(b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a])] is set
(b) . [(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,v]),(b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a])] is set
c9 is Element of b
(b,REAL,(b),(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,v]),(b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a])) . c9 is V33() real Element of REAL
(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,v]) . c9 is V33() real Element of REAL
(b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a]) . c9 is V33() real Element of REAL
((b,REAL,REAL,(Funcs (b,REAL)),(b),[b,v]) . c9) + ((b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a]) . c9) is V33() real Element of REAL
v . c9 is V33() real Element of REAL
b * (v . c9) is V33() real Element of REAL
(b * (v . c9)) + ((b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a]) . c9) is V33() real Element of REAL
h * 1 is V33() real Element of REAL
0 + (h * 1) is V33() real Element of REAL
t is Element of b
(b,REAL,(b),(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,v]),(b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a])) . t is V33() real Element of REAL
(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,v]) . t is V33() real Element of REAL
(b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a]) . t is V33() real Element of REAL
((b,REAL,REAL,(Funcs (b,REAL)),(b),[b,v]) . t) + ((b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a]) . t) is V33() real Element of REAL
v . t is V33() real Element of REAL
b * (v . t) is V33() real Element of REAL
(b * (v . t)) + ((b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a]) . t) is V33() real Element of REAL
h * 0 is V33() real Element of REAL
b + (h * 0) is V33() real Element of REAL
c1 is set
a is set
b is non empty set
Funcs (b,REAL) is non empty FUNCTION_DOMAIN of b, REAL
(b) is Relation-like [:(Funcs (b,REAL)),(Funcs (b,REAL)):] -defined Funcs (b,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):]
[:(Funcs (b,REAL)),(Funcs (b,REAL)):] is Relation-like non empty set
[:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):] is non empty set
(b) is Relation-like [:REAL,(Funcs (b,REAL)):] -defined Funcs (b,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):]
[:REAL,(Funcs (b,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):] is non empty V37() set
(b) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
b --> 0 is Relation-like b -defined NAT -valued Function-like constant non empty V14(b) quasi_total Element of bool [:b,NAT:]
[:b,NAT:] is Relation-like non empty V37() set
bool [:b,NAT:] is non empty V37() set
[:b,{0}:] is Relation-like non empty set
v is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
a is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
b is V33() real Element of REAL
[b,v] is Element of [:REAL,(Funcs (b,REAL)):]
(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,v]) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
h is V33() real Element of REAL
[h,a] is Element of [:REAL,(Funcs (b,REAL)):]
(b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a]) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
(b,REAL,(b),(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,v]),(b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a])) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
[(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,v]),(b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a])] is set
(b) . [(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,v]),(b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a])] is set
c1 is set
a is set
{c1,a} is non empty set
b is non empty set
Funcs (b,REAL) is non empty FUNCTION_DOMAIN of b, REAL
(b) is Relation-like [:(Funcs (b,REAL)),(Funcs (b,REAL)):] -defined Funcs (b,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):]
[:(Funcs (b,REAL)),(Funcs (b,REAL)):] is Relation-like non empty set
[:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):] is non empty set
(b) is Relation-like [:REAL,(Funcs (b,REAL)):] -defined Funcs (b,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):]
[:REAL,(Funcs (b,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):] is non empty V37() set
v is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
a is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
v . a is set
a . a is set
v . c1 is set
a . c1 is set
b is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
h is Element of b
b . h is V33() real Element of REAL
c9 is V33() real Element of REAL
[c9,v] is Element of [:REAL,(Funcs (b,REAL)):]
(b,REAL,REAL,(Funcs (b,REAL)),(b),[c9,v]) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
t is Element of b
b . t is V33() real Element of REAL
b is V33() real Element of REAL
[b,a] is Element of [:REAL,(Funcs (b,REAL)):]
(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,a]) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
(b,REAL,(b),(b,REAL,REAL,(Funcs (b,REAL)),(b),[c9,v]),(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,a])) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
[(b,REAL,REAL,(Funcs (b,REAL)),(b),[c9,v]),(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,a])] is set
(b) . [(b,REAL,REAL,(Funcs (b,REAL)),(b),[c9,v]),(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,a])] is set
x is Element of b
(b,REAL,(b),(b,REAL,REAL,(Funcs (b,REAL)),(b),[c9,v]),(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,a])) . t is V33() real Element of REAL
(b,REAL,REAL,(Funcs (b,REAL)),(b),[c9,v]) . t is V33() real Element of REAL
(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,a]) . t is V33() real Element of REAL
((b,REAL,REAL,(Funcs (b,REAL)),(b),[c9,v]) . t) + ((b,REAL,REAL,(Funcs (b,REAL)),(b),[b,a]) . t) is V33() real Element of REAL
v . t is V33() real Element of REAL
c9 * (v . t) is V33() real Element of REAL
(c9 * (v . t)) + ((b,REAL,REAL,(Funcs (b,REAL)),(b),[b,a]) . t) is V33() real Element of REAL
b * 1 is V33() real Element of REAL
0 + (b * 1) is V33() real Element of REAL
(b,REAL,(b),(b,REAL,REAL,(Funcs (b,REAL)),(b),[c9,v]),(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,a])) . h is V33() real Element of REAL
(b,REAL,REAL,(Funcs (b,REAL)),(b),[c9,v]) . h is V33() real Element of REAL
(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,a]) . h is V33() real Element of REAL
((b,REAL,REAL,(Funcs (b,REAL)),(b),[c9,v]) . h) + ((b,REAL,REAL,(Funcs (b,REAL)),(b),[b,a]) . h) is V33() real Element of REAL
v . h is V33() real Element of REAL
c9 * (v . h) is V33() real Element of REAL
(c9 * (v . h)) + ((b,REAL,REAL,(Funcs (b,REAL)),(b),[b,a]) . h) is V33() real Element of REAL
b * 0 is V33() real Element of REAL
c9 + (b * 0) is V33() real Element of REAL
b . x is V33() real Element of REAL
(b,REAL,(b),(b,REAL,REAL,(Funcs (b,REAL)),(b),[c9,v]),(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,a])) . x is V33() real Element of REAL
c1 is set
a is set
{c1,a} is non empty set
b is non empty set
Funcs (b,REAL) is non empty FUNCTION_DOMAIN of b, REAL
(b) is Relation-like [:(Funcs (b,REAL)),(Funcs (b,REAL)):] -defined Funcs (b,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):]
[:(Funcs (b,REAL)),(Funcs (b,REAL)):] is Relation-like non empty set
[:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):] is non empty set
(b) is Relation-like [:REAL,(Funcs (b,REAL)):] -defined Funcs (b,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):]
[:REAL,(Funcs (b,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):] is non empty V37() set
v is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
a is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
b is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
c1 is set
a is set
{c1,a} is non empty set
b is non empty set
Funcs (b,REAL) is non empty FUNCTION_DOMAIN of b, REAL
(b) is Relation-like [:(Funcs (b,REAL)),(Funcs (b,REAL)):] -defined Funcs (b,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):]
[:(Funcs (b,REAL)),(Funcs (b,REAL)):] is Relation-like non empty set
[:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (b,REAL)),(Funcs (b,REAL)):],(Funcs (b,REAL)):] is non empty set
(b) is Relation-like [:REAL,(Funcs (b,REAL)):] -defined Funcs (b,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):]
[:REAL,(Funcs (b,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (b,REAL)):],(Funcs (b,REAL)):] is non empty V37() set
(b) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
b --> 0 is Relation-like b -defined NAT -valued Function-like constant non empty V14(b) quasi_total Element of bool [:b,NAT:]
[:b,NAT:] is Relation-like non empty V37() set
bool [:b,NAT:] is non empty V37() set
[:b,{0}:] is Relation-like non empty set
v is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
a is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
b is V33() real Element of REAL
[b,v] is Element of [:REAL,(Funcs (b,REAL)):]
(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,v]) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
h is V33() real Element of REAL
[h,a] is Element of [:REAL,(Funcs (b,REAL)):]
(b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a]) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
(b,REAL,(b),(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,v]),(b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a])) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
[(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,v]),(b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a])] is set
(b) . [(b,REAL,REAL,(Funcs (b,REAL)),(b),[b,v]),(b,REAL,REAL,(Funcs (b,REAL)),(b),[h,a])] is set
t is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
c1 is set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like set
bool [:c1,NAT:] is non empty set
[:c1,{0}:] is Relation-like set
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like [:REAL,(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:REAL,(Funcs (c1,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty V37() set
RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is non empty strict RLSStruct
the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is non empty set
b is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
v is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
b + v is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is Relation-like [: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] -defined the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) -valued Function-like quasi_total Element of bool [:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):]
[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty set
[:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty set
bool [:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is non empty set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (b,v) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
[b,v] is set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [b,v] is set
a is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
(b + v) + a is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . ((b + v),a) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
[(b + v),a] is set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [(b + v),a] is set
v + a is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (v,a) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
[v,a] is set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [v,a] is set
b + (v + a) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (b,(v + a)) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
[b,(v + a)] is set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [b,(v + a)] is set
the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is non empty set
b is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
v is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[(- 1),v] is Element of [:REAL,(Funcs (c1,REAL)):]
(c1) . [(- 1),v] is Element of Funcs (c1,REAL)
a is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
b + a is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is Relation-like [: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] -defined the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) -valued Function-like quasi_total Element of bool [:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):]
[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty set
[:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty set
bool [:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is non empty set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (b,a) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
[b,a] is set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [b,a] is set
0. RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is V53( RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)) Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the ZeroF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is non empty set
b is V33() real set
v is V33() real Element of REAL
a is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
b is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
a + b is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is Relation-like [: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] -defined the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) -valued Function-like quasi_total Element of bool [:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):]
[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty set
[:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty set
bool [:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is non empty set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (a,b) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
[a,b] is set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [a,b] is set
v * (a + b) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is Relation-like [:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] -defined the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):]
[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty V37() set
[:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty V37() set
bool [:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is non empty V37() set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (v,(a + b)) is set
[v,(a + b)] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [v,(a + b)] is set
v * a is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (v,a) is set
[v,a] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [v,a] is set
v * b is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (v,b) is set
[v,b] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [v,b] is set
(v * a) + (v * b) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . ((v * a),(v * b)) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
[(v * a),(v * b)] is set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [(v * a),(v * b)] is set
a is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
b is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
a + b is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is Relation-like [: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] -defined the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) -valued Function-like quasi_total Element of bool [:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):]
[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty set
[:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty set
bool [:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is non empty set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (a,b) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
[a,b] is set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [a,b] is set
b * (a + b) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is Relation-like [:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] -defined the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):]
[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty V37() set
[:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty V37() set
bool [:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is non empty V37() set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (b,(a + b)) is set
[b,(a + b)] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [b,(a + b)] is set
b * a is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (b,a) is set
[b,a] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [b,a] is set
b * b is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (b,b) is set
[b,b] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [b,b] is set
(b * a) + (b * b) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . ((b * a),(b * b)) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
[(b * a),(b * b)] is set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [(b * a),(b * b)] is set
b is V33() real set
v is V33() real set
b + v is V33() real set
a is V33() real Element of REAL
b is V33() real Element of REAL
a + b is V33() real Element of REAL
h is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
(a + b) * h is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is Relation-like [:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] -defined the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):]
[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty V37() set
[:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty V37() set
bool [:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is non empty V37() set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . ((a + b),h) is set
[(a + b),h] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [(a + b),h] is set
a * h is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (a,h) is set
[a,h] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [a,h] is set
b * h is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (b,h) is set
[b,h] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [b,h] is set
(a * h) + (b * h) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is Relation-like [: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] -defined the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) -valued Function-like quasi_total Element of bool [:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):]
[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty set
[:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty set
bool [:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is non empty set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . ((a * h),(b * h)) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
[(a * h),(b * h)] is set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [(a * h),(b * h)] is set
h is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
(b + v) * h is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is Relation-like [:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] -defined the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):]
[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty V37() set
[:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty V37() set
bool [:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is non empty V37() set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . ((b + v),h) is set
[(b + v),h] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [(b + v),h] is set
b * h is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (b,h) is set
[b,h] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [b,h] is set
v * h is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (v,h) is set
[v,h] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [v,h] is set
(b * h) + (v * h) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is Relation-like [: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] -defined the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) -valued Function-like quasi_total Element of bool [:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):]
[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty set
[:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty set
bool [:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is non empty set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . ((b * h),(v * h)) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
[(b * h),(v * h)] is set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [(b * h),(v * h)] is set
b is V33() real set
v is V33() real set
b * v is V33() real set
a is V33() real Element of REAL
b is V33() real Element of REAL
a * b is V33() real Element of REAL
h is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
(a * b) * h is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is Relation-like [:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] -defined the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):]
[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty V37() set
[:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty V37() set
bool [:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is non empty V37() set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . ((a * b),h) is set
[(a * b),h] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [(a * b),h] is set
b * h is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (b,h) is set
[b,h] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [b,h] is set
a * (b * h) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (a,(b * h)) is set
[a,(b * h)] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [a,(b * h)] is set
h is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
(b * v) * h is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is Relation-like [:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] -defined the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):]
[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty V37() set
[:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty V37() set
bool [:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is non empty V37() set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . ((b * v),h) is set
[(b * v),h] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [(b * v),h] is set
v * h is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (v,h) is set
[v,h] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [v,h] is set
b * (v * h) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (b,(v * h)) is set
[b,(v * h)] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [b,(v * h)] is set
b is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
1 * b is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is Relation-like [:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] -defined the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):]
[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty V37() set
[:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty V37() set
bool [:[:REAL, the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is non empty V37() set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (1,b) is set
[1,b] is set
the Mult of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [1,b] is set
the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is non empty set
b is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
0. RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is V53( RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)) Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the ZeroF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
b + (0. RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is Relation-like [: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] -defined the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) -valued Function-like quasi_total Element of bool [:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):]
[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty set
[:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty set
bool [:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is non empty set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (b,(0. RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #))) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
[b,(0. RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #))] is set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [b,(0. RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #))] is set
v is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1,REAL,(c1),(c1),v) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[(c1),v] is set
(c1) . [(c1),v] is set
the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is non empty set
b is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
v is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
b + v is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) is Relation-like [: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] -defined the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) -valued Function-like quasi_total Element of bool [:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):]
[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty set
[:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is Relation-like non empty set
bool [:[: the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #), the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):], the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #):] is non empty set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (b,v) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
[b,v] is set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [b,v] is set
v + b is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . (v,b) is Element of the carrier of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #)
[v,b] is set
the addF of RLSStruct(# (Funcs (c1,REAL)),(c1),(c1),(c1) #) . [v,b] is set
{0,1} is non empty Element of bool NAT
({0,1}) is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V126() RLSStruct
Funcs ({0,1},REAL) is non empty FUNCTION_DOMAIN of {0,1}, REAL
({0,1}) is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of Funcs ({0,1},REAL)
{0,1} --> 0 is Relation-like {0,1} -defined NAT -valued Function-like constant non empty V14({0,1}) quasi_total Element of bool [:{0,1},NAT:]
[:{0,1},NAT:] is Relation-like non empty V37() set
bool [:{0,1},NAT:] is non empty V37() set
[:{0,1},{0}:] is Relation-like non empty set
({0,1}) is Relation-like [:(Funcs ({0,1},REAL)),(Funcs ({0,1},REAL)):] -defined Funcs ({0,1},REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs ({0,1},REAL)),(Funcs ({0,1},REAL)):],(Funcs ({0,1},REAL)):]
[:(Funcs ({0,1},REAL)),(Funcs ({0,1},REAL)):] is Relation-like non empty set
[:[:(Funcs ({0,1},REAL)),(Funcs ({0,1},REAL)):],(Funcs ({0,1},REAL)):] is Relation-like non empty set
bool [:[:(Funcs ({0,1},REAL)),(Funcs ({0,1},REAL)):],(Funcs ({0,1},REAL)):] is non empty set
({0,1}) is Relation-like [:REAL,(Funcs ({0,1},REAL)):] -defined Funcs ({0,1},REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs ({0,1},REAL)):],(Funcs ({0,1},REAL)):]
[:REAL,(Funcs ({0,1},REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs ({0,1},REAL)):],(Funcs ({0,1},REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs ({0,1},REAL)):],(Funcs ({0,1},REAL)):] is non empty V37() set
RLSStruct(# (Funcs ({0,1},REAL)),({0,1}),({0,1}),({0,1}) #) is non empty strict RLSStruct
a is non empty left_complementable right_complementable complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V126() RLSStruct
the carrier of a is non empty set
0. a is V53(a) left_complementable right_complementable complementable Element of the carrier of a
the ZeroF of a is left_complementable right_complementable complementable Element of the carrier of a
b is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of Funcs ({0,1},REAL)
v is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of Funcs ({0,1},REAL)
a is left_complementable right_complementable complementable Element of the carrier of a
b is left_complementable right_complementable complementable Element of the carrier of a
h is V33() real Element of REAL
h * a is left_complementable right_complementable complementable Element of the carrier of a
the Mult of a is Relation-like [:REAL, the carrier of a:] -defined the carrier of a -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of a:], the carrier of a:]
[:REAL, the carrier of a:] is Relation-like non empty V37() set
[:[:REAL, the carrier of a:], the carrier of a:] is Relation-like non empty V37() set
bool [:[:REAL, the carrier of a:], the carrier of a:] is non empty V37() set
the Mult of a . (h,a) is set
[h,a] is set
the Mult of a . [h,a] is set
t is V33() real Element of REAL
t * b is left_complementable right_complementable complementable Element of the carrier of a
the Mult of a . (t,b) is set
[t,b] is set
the Mult of a . [t,b] is set
(h * a) + (t * b) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is Relation-like non empty set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is Relation-like non empty set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
the addF of a . ((h * a),(t * b)) is left_complementable right_complementable complementable Element of the carrier of a
[(h * a),(t * b)] is set
the addF of a . [(h * a),(t * b)] is set
h is left_complementable right_complementable complementable Element of the carrier of a
t is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of Funcs ({0,1},REAL)
c9 is V33() real Element of REAL
[c9,b] is Element of [:REAL,(Funcs ({0,1},REAL)):]
({0,1},REAL,REAL,(Funcs ({0,1},REAL)),({0,1}),[c9,b]) is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of Funcs ({0,1},REAL)
b is V33() real Element of REAL
[b,v] is Element of [:REAL,(Funcs ({0,1},REAL)):]
({0,1},REAL,REAL,(Funcs ({0,1},REAL)),({0,1}),[b,v]) is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of Funcs ({0,1},REAL)
({0,1},REAL,({0,1}),({0,1},REAL,REAL,(Funcs ({0,1},REAL)),({0,1}),[c9,b]),({0,1},REAL,REAL,(Funcs ({0,1},REAL)),({0,1}),[b,v])) is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of Funcs ({0,1},REAL)
[({0,1},REAL,REAL,(Funcs ({0,1},REAL)),({0,1}),[c9,b]),({0,1},REAL,REAL,(Funcs ({0,1},REAL)),({0,1}),[b,v])] is set
({0,1}) . [({0,1},REAL,REAL,(Funcs ({0,1},REAL)),({0,1}),[c9,b]),({0,1},REAL,REAL,(Funcs ({0,1},REAL)),({0,1}),[b,v])] is set
c9 * a is left_complementable right_complementable complementable Element of the carrier of a
the Mult of a is Relation-like [:REAL, the carrier of a:] -defined the carrier of a -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of a:], the carrier of a:]
[:REAL, the carrier of a:] is Relation-like non empty V37() set
[:[:REAL, the carrier of a:], the carrier of a:] is Relation-like non empty V37() set
bool [:[:REAL, the carrier of a:], the carrier of a:] is non empty V37() set
the Mult of a . (c9,a) is set
[c9,a] is set
the Mult of a . [c9,a] is set
b * b is left_complementable right_complementable complementable Element of the carrier of a
the Mult of a . (b,b) is set
[b,b] is set
the Mult of a . [b,b] is set
(c9 * a) + (b * b) is left_complementable right_complementable complementable Element of the carrier of a
the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is Relation-like non empty set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is Relation-like non empty set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
the addF of a . ((c9 * a),(b * b)) is left_complementable right_complementable complementable Element of the carrier of a
[(c9 * a),(b * b)] is set
the addF of a . [(c9 * a),(b * b)] is set
c1 is non empty set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 1 is Relation-like non-empty c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like non empty V37() set
bool [:c1,NAT:] is non empty V37() set
[:c1,{1}:] is Relation-like non empty set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,{0}:] is Relation-like non empty set
doubleLoopStr(# (Funcs (c1,REAL)),(c1),(c1),(c1),(c1) #) is non empty strict doubleLoopStr
c1 is non empty set
(c1) is strict doubleLoopStr
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 1 is Relation-like non-empty c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like non empty V37() set
bool [:c1,NAT:] is non empty V37() set
[:c1,{1}:] is Relation-like non empty set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,{0}:] is Relation-like non empty set
doubleLoopStr(# (Funcs (c1,REAL)),(c1),(c1),(c1),(c1) #) is non empty strict doubleLoopStr
c1 is non empty set
(c1) is non empty strict doubleLoopStr
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 1 is Relation-like non-empty c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like non empty V37() set
bool [:c1,NAT:] is non empty V37() set
[:c1,{1}:] is Relation-like non empty set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,{0}:] is Relation-like non empty set
doubleLoopStr(# (Funcs (c1,REAL)),(c1),(c1),(c1),(c1) #) is non empty strict doubleLoopStr
the carrier of (c1) is non empty set
b is Element of the carrier of (c1)
v is Element of the carrier of (c1)
b * v is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the multF of (c1) . (b,v) is Element of the carrier of (c1)
[b,v] is set
the multF of (c1) . [b,v] is set
a is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1,REAL,(c1),(c1),a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[(c1),a] is set
(c1) . [(c1),a] is set
v * b is Element of the carrier of (c1)
the multF of (c1) . (v,b) is Element of the carrier of (c1)
[v,b] is set
the multF of (c1) . [v,b] is set
c1 is non empty set
(c1) is non empty strict doubleLoopStr
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 1 is Relation-like non-empty c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like non empty V37() set
bool [:c1,NAT:] is non empty V37() set
[:c1,{1}:] is Relation-like non empty set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,{0}:] is Relation-like non empty set
doubleLoopStr(# (Funcs (c1,REAL)),(c1),(c1),(c1),(c1) #) is non empty strict doubleLoopStr
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
b is Element of the carrier of (c1)
b * a is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the multF of (c1) . (b,a) is Element of the carrier of (c1)
[b,a] is set
the multF of (c1) . [b,a] is set
v is Element of the carrier of (c1)
a * v is Element of the carrier of (c1)
the multF of (c1) . (a,v) is Element of the carrier of (c1)
[a,v] is set
the multF of (c1) . [a,v] is set
c1 is non empty set
(c1) is non empty strict unital doubleLoopStr
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 1 is Relation-like non-empty c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like non empty V37() set
bool [:c1,NAT:] is non empty V37() set
[:c1,{1}:] is Relation-like non empty set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,{0}:] is Relation-like non empty set
doubleLoopStr(# (Funcs (c1,REAL)),(c1),(c1),(c1),(c1) #) is non empty strict doubleLoopStr
1. (c1) is Element of the carrier of (c1)
the carrier of (c1) is non empty set
the OneF of (c1) is Element of the carrier of (c1)
c1 is non empty set
(c1) is non empty strict unital doubleLoopStr
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 1 is Relation-like non-empty c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like non empty V37() set
bool [:c1,NAT:] is non empty V37() set
[:c1,{1}:] is Relation-like non empty set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,{0}:] is Relation-like non empty set
doubleLoopStr(# (Funcs (c1,REAL)),(c1),(c1),(c1),(c1) #) is non empty strict doubleLoopStr
the carrier of (c1) is non empty set
0. (c1) is V53((c1)) Element of the carrier of (c1)
the ZeroF of (c1) is Element of the carrier of (c1)
1. (c1) is Element of the carrier of (c1)
the OneF of (c1) is Element of the carrier of (c1)
a is Element of the carrier of (c1)
b is Element of the carrier of (c1)
a + b is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the addF of (c1) . (a,b) is Element of the carrier of (c1)
[a,b] is set
the addF of (c1) . [a,b] is set
b + a is Element of the carrier of (c1)
the addF of (c1) . (b,a) is Element of the carrier of (c1)
[b,a] is set
the addF of (c1) . [b,a] is set
v is Element of the carrier of (c1)
(a + b) + v is Element of the carrier of (c1)
the addF of (c1) . ((a + b),v) is Element of the carrier of (c1)
[(a + b),v] is set
the addF of (c1) . [(a + b),v] is set
b + v is Element of the carrier of (c1)
the addF of (c1) . (b,v) is Element of the carrier of (c1)
[b,v] is set
the addF of (c1) . [b,v] is set
a + (b + v) is Element of the carrier of (c1)
the addF of (c1) . (a,(b + v)) is Element of the carrier of (c1)
[a,(b + v)] is set
the addF of (c1) . [a,(b + v)] is set
a + (0. (c1)) is Element of the carrier of (c1)
the addF of (c1) . (a,(0. (c1))) is Element of the carrier of (c1)
[a,(0. (c1))] is set
the addF of (c1) . [a,(0. (c1))] is set
a * b is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
the multF of (c1) . (a,b) is Element of the carrier of (c1)
the multF of (c1) . [a,b] is set
b * a is Element of the carrier of (c1)
the multF of (c1) . (b,a) is Element of the carrier of (c1)
the multF of (c1) . [b,a] is set
(a * b) * v is Element of the carrier of (c1)
the multF of (c1) . ((a * b),v) is Element of the carrier of (c1)
[(a * b),v] is set
the multF of (c1) . [(a * b),v] is set
b * v is Element of the carrier of (c1)
the multF of (c1) . (b,v) is Element of the carrier of (c1)
the multF of (c1) . [b,v] is set
a * (b * v) is Element of the carrier of (c1)
the multF of (c1) . (a,(b * v)) is Element of the carrier of (c1)
[a,(b * v)] is set
the multF of (c1) . [a,(b * v)] is set
a * (1. (c1)) is Element of the carrier of (c1)
the multF of (c1) . (a,(1. (c1))) is Element of the carrier of (c1)
[a,(1. (c1))] is set
the multF of (c1) . [a,(1. (c1))] is set
(1. (c1)) * a is Element of the carrier of (c1)
the multF of (c1) . ((1. (c1)),a) is Element of the carrier of (c1)
[(1. (c1)),a] is set
the multF of (c1) . [(1. (c1)),a] is set
a * (b + v) is Element of the carrier of (c1)
the multF of (c1) . (a,(b + v)) is Element of the carrier of (c1)
the multF of (c1) . [a,(b + v)] is set
a * v is Element of the carrier of (c1)
the multF of (c1) . (a,v) is Element of the carrier of (c1)
[a,v] is set
the multF of (c1) . [a,v] is set
(a * b) + (a * v) is Element of the carrier of (c1)
the addF of (c1) . ((a * b),(a * v)) is Element of the carrier of (c1)
[(a * b),(a * v)] is set
the addF of (c1) . [(a * b),(a * v)] is set
(b + v) * a is Element of the carrier of (c1)
the multF of (c1) . ((b + v),a) is Element of the carrier of (c1)
[(b + v),a] is set
the multF of (c1) . [(b + v),a] is set
v * a is Element of the carrier of (c1)
the multF of (c1) . (v,a) is Element of the carrier of (c1)
[v,a] is set
the multF of (c1) . [v,a] is set
(b * a) + (v * a) is Element of the carrier of (c1)
the addF of (c1) . ((b * a),(v * a)) is Element of the carrier of (c1)
[(b * a),(v * a)] is set
the addF of (c1) . [(b * a),(v * a)] is set
b is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1,REAL,(c1),(c1),b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[(c1),b] is set
(c1) . [(c1),b] is set
(c1) is Relation-like [:REAL,(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:REAL,(Funcs (c1,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty V37() set
[(- 1),b] is Element of [:REAL,(Funcs (c1,REAL)):]
(c1,REAL,REAL,(Funcs (c1,REAL)),(c1),[(- 1),b]) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
t is Element of the carrier of (c1)
a + t is Element of the carrier of (c1)
the addF of (c1) . (a,t) is Element of the carrier of (c1)
[a,t] is set
the addF of (c1) . [a,t] is set
(c1,REAL,(c1),(c1),b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[(c1),b] is set
(c1) . [(c1),b] is set
(b * a) + (a * v) is Element of the carrier of (c1)
the addF of (c1) . ((b * a),(a * v)) is Element of the carrier of (c1)
[(b * a),(a * v)] is set
the addF of (c1) . [(b * a),(a * v)] is set
Trivial-doubleLoopStr is non empty trivial V52() 1 -element strict doubleLoopStr
c1 is non empty trivial V52() 1 -element strict doubleLoopStr
the carrier of c1 is non empty trivial V37() V44(1) set
a is Element of the carrier of c1
b is Element of the carrier of c1
a + b is Element of the carrier of c1
the addF of c1 is Relation-like [: the carrier of c1, the carrier of c1:] -defined the carrier of c1 -valued Function-like quasi_total Element of bool [:[: the carrier of c1, the carrier of c1:], the carrier of c1:]
[: the carrier of c1, the carrier of c1:] is Relation-like non empty set
[:[: the carrier of c1, the carrier of c1:], the carrier of c1:] is Relation-like non empty set
bool [:[: the carrier of c1, the carrier of c1:], the carrier of c1:] is non empty set
the addF of c1 . (a,b) is Element of the carrier of c1
[a,b] is set
the addF of c1 . [a,b] is set
b + a is Element of the carrier of c1
the addF of c1 . (b,a) is Element of the carrier of c1
[b,a] is set
the addF of c1 . [b,a] is set
the carrier of c1 is non empty trivial V37() V44(1) set
a is Element of the carrier of c1
b is Element of the carrier of c1
a + b is Element of the carrier of c1
the addF of c1 is Relation-like [: the carrier of c1, the carrier of c1:] -defined the carrier of c1 -valued Function-like quasi_total Element of bool [:[: the carrier of c1, the carrier of c1:], the carrier of c1:]
[: the carrier of c1, the carrier of c1:] is Relation-like non empty set
[:[: the carrier of c1, the carrier of c1:], the carrier of c1:] is Relation-like non empty set
bool [:[: the carrier of c1, the carrier of c1:], the carrier of c1:] is non empty set
the addF of c1 . (a,b) is Element of the carrier of c1
[a,b] is set
the addF of c1 . [a,b] is set
v is Element of the carrier of c1
(a + b) + v is Element of the carrier of c1
the addF of c1 . ((a + b),v) is Element of the carrier of c1
[(a + b),v] is set
the addF of c1 . [(a + b),v] is set
b + v is Element of the carrier of c1
the addF of c1 . (b,v) is Element of the carrier of c1
[b,v] is set
the addF of c1 . [b,v] is set
a + (b + v) is Element of the carrier of c1
the addF of c1 . (a,(b + v)) is Element of the carrier of c1
[a,(b + v)] is set
the addF of c1 . [a,(b + v)] is set
the carrier of c1 is non empty trivial V37() V44(1) set
a is Element of the carrier of c1
0. c1 is V53(c1) Element of the carrier of c1
the ZeroF of c1 is Element of the carrier of c1
a + (0. c1) is Element of the carrier of c1
the addF of c1 is Relation-like [: the carrier of c1, the carrier of c1:] -defined the carrier of c1 -valued Function-like quasi_total Element of bool [:[: the carrier of c1, the carrier of c1:], the carrier of c1:]
[: the carrier of c1, the carrier of c1:] is Relation-like non empty set
[:[: the carrier of c1, the carrier of c1:], the carrier of c1:] is Relation-like non empty set
bool [:[: the carrier of c1, the carrier of c1:], the carrier of c1:] is non empty set
the addF of c1 . (a,(0. c1)) is Element of the carrier of c1
[a,(0. c1)] is set
the addF of c1 . [a,(0. c1)] is set
the carrier of c1 is non empty trivial V37() V44(1) set
a is Element of the carrier of c1
a + a is Element of the carrier of c1
the addF of c1 is Relation-like [: the carrier of c1, the carrier of c1:] -defined the carrier of c1 -valued Function-like quasi_total Element of bool [:[: the carrier of c1, the carrier of c1:], the carrier of c1:]
[: the carrier of c1, the carrier of c1:] is Relation-like non empty set
[:[: the carrier of c1, the carrier of c1:], the carrier of c1:] is Relation-like non empty set
bool [:[: the carrier of c1, the carrier of c1:], the carrier of c1:] is non empty set
the addF of c1 . (a,a) is Element of the carrier of c1
[a,a] is set
the addF of c1 . [a,a] is set
0. c1 is V53(c1) Element of the carrier of c1
the ZeroF of c1 is Element of the carrier of c1
the carrier of c1 is non empty trivial V37() V44(1) set
a is Element of the carrier of c1
b is Element of the carrier of c1
a * b is Element of the carrier of c1
the multF of c1 is Relation-like [: the carrier of c1, the carrier of c1:] -defined the carrier of c1 -valued Function-like quasi_total Element of bool [:[: the carrier of c1, the carrier of c1:], the carrier of c1:]
[: the carrier of c1, the carrier of c1:] is Relation-like non empty set
[:[: the carrier of c1, the carrier of c1:], the carrier of c1:] is Relation-like non empty set
bool [:[: the carrier of c1, the carrier of c1:], the carrier of c1:] is non empty set
the multF of c1 . (a,b) is Element of the carrier of c1
[a,b] is set
the multF of c1 . [a,b] is set
v is Element of the carrier of c1
(a * b) * v is Element of the carrier of c1
the multF of c1 . ((a * b),v) is Element of the carrier of c1
[(a * b),v] is set
the multF of c1 . [(a * b),v] is set
b * v is Element of the carrier of c1
the multF of c1 . (b,v) is Element of the carrier of c1
[b,v] is set
the multF of c1 . [b,v] is set
a * (b * v) is Element of the carrier of c1
the multF of c1 . (a,(b * v)) is Element of the carrier of c1
[a,(b * v)] is set
the multF of c1 . [a,(b * v)] is set
the carrier of c1 is non empty trivial V37() V44(1) set
a is Element of the carrier of c1
b is Element of the carrier of c1
a * b is Element of the carrier of c1
the multF of c1 is Relation-like [: the carrier of c1, the carrier of c1:] -defined the carrier of c1 -valued Function-like quasi_total Element of bool [:[: the carrier of c1, the carrier of c1:], the carrier of c1:]
[: the carrier of c1, the carrier of c1:] is Relation-like non empty set
[:[: the carrier of c1, the carrier of c1:], the carrier of c1:] is Relation-like non empty set
bool [:[: the carrier of c1, the carrier of c1:], the carrier of c1:] is non empty set
the multF of c1 . (a,b) is Element of the carrier of c1
[a,b] is set
the multF of c1 . [a,b] is set
b * a is Element of the carrier of c1
the multF of c1 . (b,a) is Element of the carrier of c1
[b,a] is set
the multF of c1 . [b,a] is set
the carrier of c1 is non empty trivial V37() V44(1) set
a is Element of the carrier of c1
1. c1 is Element of the carrier of c1
the OneF of c1 is Element of the carrier of c1
a * (1. c1) is Element of the carrier of c1
the multF of c1 is Relation-like [: the carrier of c1, the carrier of c1:] -defined the carrier of c1 -valued Function-like quasi_total Element of bool [:[: the carrier of c1, the carrier of c1:], the carrier of c1:]
[: the carrier of c1, the carrier of c1:] is Relation-like non empty set
[:[: the carrier of c1, the carrier of c1:], the carrier of c1:] is Relation-like non empty set
bool [:[: the carrier of c1, the carrier of c1:], the carrier of c1:] is non empty set
the multF of c1 . (a,(1. c1)) is Element of the carrier of c1
[a,(1. c1)] is set
the multF of c1 . [a,(1. c1)] is set
the carrier of c1 is non empty trivial V37() V44(1) set
a is Element of the carrier of c1
b is Element of the carrier of c1
v is Element of the carrier of c1
b + v is Element of the carrier of c1
the addF of c1 is Relation-like [: the carrier of c1, the carrier of c1:] -defined the carrier of c1 -valued Function-like quasi_total Element of bool [:[: the carrier of c1, the carrier of c1:], the carrier of c1:]
[: the carrier of c1, the carrier of c1:] is Relation-like non empty set
[:[: the carrier of c1, the carrier of c1:], the carrier of c1:] is Relation-like non empty set
bool [:[: the carrier of c1, the carrier of c1:], the carrier of c1:] is non empty set
the addF of c1 . (b,v) is Element of the carrier of c1
[b,v] is set
the addF of c1 . [b,v] is set
a * (b + v) is Element of the carrier of c1
the multF of c1 is Relation-like [: the carrier of c1, the carrier of c1:] -defined the carrier of c1 -valued Function-like quasi_total Element of bool [:[: the carrier of c1, the carrier of c1:], the carrier of c1:]
the multF of c1 . (a,(b + v)) is Element of the carrier of c1
[a,(b + v)] is set
the multF of c1 . [a,(b + v)] is set
a * b is Element of the carrier of c1
the multF of c1 . (a,b) is Element of the carrier of c1
[a,b] is set
the multF of c1 . [a,b] is set
a * v is Element of the carrier of c1
the multF of c1 . (a,v) is Element of the carrier of c1
[a,v] is set
the multF of c1 . [a,v] is set
(a * b) + (a * v) is Element of the carrier of c1
the addF of c1 . ((a * b),(a * v)) is Element of the carrier of c1
[(a * b),(a * v)] is set
the addF of c1 . [(a * b),(a * v)] is set
c1 is non empty set
(c1) is non empty strict unital doubleLoopStr
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 1 is Relation-like non-empty c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like non empty V37() set
bool [:c1,NAT:] is non empty V37() set
[:c1,{1}:] is Relation-like non empty set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,{0}:] is Relation-like non empty set
doubleLoopStr(# (Funcs (c1,REAL)),(c1),(c1),(c1),(c1) #) is non empty strict doubleLoopStr
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
b is Element of the carrier of (c1)
a + b is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the addF of (c1) . (a,b) is Element of the carrier of (c1)
[a,b] is set
the addF of (c1) . [a,b] is set
b + a is Element of the carrier of (c1)
the addF of (c1) . (b,a) is Element of the carrier of (c1)
[b,a] is set
the addF of (c1) . [b,a] is set
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
b is Element of the carrier of (c1)
a + b is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the addF of (c1) . (a,b) is Element of the carrier of (c1)
[a,b] is set
the addF of (c1) . [a,b] is set
v is Element of the carrier of (c1)
(a + b) + v is Element of the carrier of (c1)
the addF of (c1) . ((a + b),v) is Element of the carrier of (c1)
[(a + b),v] is set
the addF of (c1) . [(a + b),v] is set
b + v is Element of the carrier of (c1)
the addF of (c1) . (b,v) is Element of the carrier of (c1)
[b,v] is set
the addF of (c1) . [b,v] is set
a + (b + v) is Element of the carrier of (c1)
the addF of (c1) . (a,(b + v)) is Element of the carrier of (c1)
[a,(b + v)] is set
the addF of (c1) . [a,(b + v)] is set
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
0. (c1) is V53((c1)) Element of the carrier of (c1)
the ZeroF of (c1) is Element of the carrier of (c1)
b is Element of the carrier of (c1)
a + b is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the addF of (c1) . (a,b) is Element of the carrier of (c1)
[a,b] is set
the addF of (c1) . [a,b] is set
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
0. (c1) is V53((c1)) Element of the carrier of (c1)
the ZeroF of (c1) is Element of the carrier of (c1)
a + (0. (c1)) is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the addF of (c1) . (a,(0. (c1))) is Element of the carrier of (c1)
[a,(0. (c1))] is set
the addF of (c1) . [a,(0. (c1))] is set
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
b is Element of the carrier of (c1)
v is Element of the carrier of (c1)
b + v is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the addF of (c1) . (b,v) is Element of the carrier of (c1)
[b,v] is set
the addF of (c1) . [b,v] is set
a * (b + v) is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
the multF of (c1) . (a,(b + v)) is Element of the carrier of (c1)
[a,(b + v)] is set
the multF of (c1) . [a,(b + v)] is set
a * b is Element of the carrier of (c1)
the multF of (c1) . (a,b) is Element of the carrier of (c1)
[a,b] is set
the multF of (c1) . [a,b] is set
a * v is Element of the carrier of (c1)
the multF of (c1) . (a,v) is Element of the carrier of (c1)
[a,v] is set
the multF of (c1) . [a,v] is set
(a * b) + (a * v) is Element of the carrier of (c1)
the addF of (c1) . ((a * b),(a * v)) is Element of the carrier of (c1)
[(a * b),(a * v)] is set
the addF of (c1) . [(a * b),(a * v)] is set
a is Element of the carrier of (c1)
b is Element of the carrier of (c1)
a + b is Element of the carrier of (c1)
the addF of (c1) . (a,b) is Element of the carrier of (c1)
[a,b] is set
the addF of (c1) . [a,b] is set
(a + b) * a is Element of the carrier of (c1)
the multF of (c1) . ((a + b),a) is Element of the carrier of (c1)
[(a + b),a] is set
the multF of (c1) . [(a + b),a] is set
a * a is Element of the carrier of (c1)
the multF of (c1) . (a,a) is Element of the carrier of (c1)
[a,a] is set
the multF of (c1) . [a,a] is set
b * a is Element of the carrier of (c1)
the multF of (c1) . (b,a) is Element of the carrier of (c1)
[b,a] is set
the multF of (c1) . [b,a] is set
(a * a) + (b * a) is Element of the carrier of (c1)
the addF of (c1) . ((a * a),(b * a)) is Element of the carrier of (c1)
[(a * a),(b * a)] is set
the addF of (c1) . [(a * a),(b * a)] is set
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
1. (c1) is Element of the carrier of (c1)
the OneF of (c1) is Element of the carrier of (c1)
a * (1. (c1)) is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the multF of (c1) . (a,(1. (c1))) is Element of the carrier of (c1)
[a,(1. (c1))] is set
the multF of (c1) . [a,(1. (c1))] is set
(1. (c1)) * a is Element of the carrier of (c1)
the multF of (c1) . ((1. (c1)),a) is Element of the carrier of (c1)
[(1. (c1)),a] is set
the multF of (c1) . [(1. (c1)),a] is set
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
b is Element of the carrier of (c1)
a * b is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the multF of (c1) . (a,b) is Element of the carrier of (c1)
[a,b] is set
the multF of (c1) . [a,b] is set
v is Element of the carrier of (c1)
(a * b) * v is Element of the carrier of (c1)
the multF of (c1) . ((a * b),v) is Element of the carrier of (c1)
[(a * b),v] is set
the multF of (c1) . [(a * b),v] is set
b * v is Element of the carrier of (c1)
the multF of (c1) . (b,v) is Element of the carrier of (c1)
[b,v] is set
the multF of (c1) . [b,v] is set
a * (b * v) is Element of the carrier of (c1)
the multF of (c1) . (a,(b * v)) is Element of the carrier of (c1)
[a,(b * v)] is set
the multF of (c1) . [a,(b * v)] is set
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
b is Element of the carrier of (c1)
a * b is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the multF of (c1) . (a,b) is Element of the carrier of (c1)
[a,b] is set
the multF of (c1) . [a,b] is set
b * a is Element of the carrier of (c1)
the multF of (c1) . (b,a) is Element of the carrier of (c1)
[b,a] is set
the multF of (c1) . [b,a] is set
the non empty set is non empty set
[: the non empty set , the non empty set :] is Relation-like non empty set
[:[: the non empty set , the non empty set :], the non empty set :] is Relation-like non empty set
bool [:[: the non empty set , the non empty set :], the non empty set :] is non empty set
the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :]
[:REAL, the non empty set :] is Relation-like non empty V37() set
[:[:REAL, the non empty set :], the non empty set :] is Relation-like non empty V37() set
bool [:[:REAL, the non empty set :], the non empty set :] is non empty V37() set
the Relation-like [:REAL, the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[:REAL, the non empty set :], the non empty set :] is Relation-like [:REAL, the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[:REAL, the non empty set :], the non empty set :]
the Element of the non empty set is Element of the non empty set
( the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like [:REAL, the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[:REAL, the non empty set :], the non empty set :], the Element of the non empty set , the Element of the non empty set ) is () ()
the carrier of ( the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like [:REAL, the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[:REAL, the non empty set :], the non empty set :], the Element of the non empty set , the Element of the non empty set ) is set
c1 is set
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
(c1) is Relation-like [:REAL,(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:REAL,(Funcs (c1,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty V37() set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 1 is Relation-like non-empty c1 -defined NAT -valued Function-like constant V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like set
bool [:c1,NAT:] is non empty set
[:c1,{1}:] is Relation-like set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,{0}:] is Relation-like set
((Funcs (c1,REAL)),(c1),(c1),(c1),(c1),(c1)) is () ()
c1 is non empty set
(c1) is () ()
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
(c1) is Relation-like [:REAL,(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:REAL,(Funcs (c1,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty V37() set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 1 is Relation-like non-empty c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like non empty V37() set
bool [:c1,NAT:] is non empty V37() set
[:c1,{1}:] is Relation-like non empty set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,{0}:] is Relation-like non empty set
((Funcs (c1,REAL)),(c1),(c1),(c1),(c1),(c1)) is () ()
c1 is non empty set
(c1) is non empty () ()
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
(c1) is Relation-like [:REAL,(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:REAL,(Funcs (c1,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty V37() set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 1 is Relation-like non-empty c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like non empty V37() set
bool [:c1,NAT:] is non empty V37() set
[:c1,{1}:] is Relation-like non empty set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,{0}:] is Relation-like non empty set
((Funcs (c1,REAL)),(c1),(c1),(c1),(c1),(c1)) is () ()
the carrier of (c1) is non empty set
b is Element of the carrier of (c1)
v is Element of the carrier of (c1)
b * v is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the multF of (c1) . (b,v) is Element of the carrier of (c1)
[b,v] is set
the multF of (c1) . [b,v] is set
a is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
(c1,REAL,(c1),(c1),a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[(c1),a] is set
(c1) . [(c1),a] is set
v * b is Element of the carrier of (c1)
the multF of (c1) . (v,b) is Element of the carrier of (c1)
[v,b] is set
the multF of (c1) . [v,b] is set
c1 is non empty set
(c1) is non empty () ()
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
(c1) is Relation-like [:REAL,(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:REAL,(Funcs (c1,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty V37() set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 1 is Relation-like non-empty c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like non empty V37() set
bool [:c1,NAT:] is non empty V37() set
[:c1,{1}:] is Relation-like non empty set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,{0}:] is Relation-like non empty set
((Funcs (c1,REAL)),(c1),(c1),(c1),(c1),(c1)) is () ()
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
b is Element of the carrier of (c1)
b * a is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the multF of (c1) . (b,a) is Element of the carrier of (c1)
[b,a] is set
the multF of (c1) . [b,a] is set
v is Element of the carrier of (c1)
a * v is Element of the carrier of (c1)
the multF of (c1) . (a,v) is Element of the carrier of (c1)
[a,v] is set
the multF of (c1) . [a,v] is set
c1 is non empty set
(c1) is non empty unital () ()
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
(c1) is Relation-like [:REAL,(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:REAL,(Funcs (c1,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty V37() set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 1 is Relation-like non-empty c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like non empty V37() set
bool [:c1,NAT:] is non empty V37() set
[:c1,{1}:] is Relation-like non empty set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant non empty V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,{0}:] is Relation-like non empty set
((Funcs (c1,REAL)),(c1),(c1),(c1),(c1),(c1)) is () ()
1. (c1) is Element of the carrier of (c1)
the carrier of (c1) is non empty set
the OneF of (c1) is Element of the carrier of (c1)
c1 is set
(c1) is () ()
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
(c1) is Relation-like [:REAL,(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:REAL,(Funcs (c1,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty V37() set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 1 is Relation-like non-empty c1 -defined NAT -valued Function-like constant V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like set
bool [:c1,NAT:] is non empty set
[:c1,{1}:] is Relation-like set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,{0}:] is Relation-like set
((Funcs (c1,REAL)),(c1),(c1),(c1),(c1),(c1)) is () ()
c1 is set
(c1) is non empty () ()
Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] is Relation-like non empty set
[:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty set
(c1) is Relation-like [:(Funcs (c1,REAL)),(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,REAL)),(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
(c1) is Relation-like [:REAL,(Funcs (c1,REAL)):] -defined Funcs (c1,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):]
[:REAL,(Funcs (c1,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (c1,REAL)):],(Funcs (c1,REAL)):] is non empty V37() set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 1 is Relation-like non-empty c1 -defined NAT -valued Function-like constant V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,NAT:] is Relation-like set
bool [:c1,NAT:] is non empty set
[:c1,{1}:] is Relation-like set
(c1) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
c1 --> 0 is Relation-like c1 -defined NAT -valued Function-like constant V14(c1) quasi_total Element of bool [:c1,NAT:]
[:c1,{0}:] is Relation-like set
((Funcs (c1,REAL)),(c1),(c1),(c1),(c1),(c1)) is () ()
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
b is Element of the carrier of (c1)
a + b is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the addF of (c1) . (a,b) is Element of the carrier of (c1)
[a,b] is set
the addF of (c1) . [a,b] is set
b + a is Element of the carrier of (c1)
the addF of (c1) . (b,a) is Element of the carrier of (c1)
[b,a] is set
the addF of (c1) . [b,a] is set
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
b is Element of the carrier of (c1)
a + b is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the addF of (c1) . (a,b) is Element of the carrier of (c1)
[a,b] is set
the addF of (c1) . [a,b] is set
v is Element of the carrier of (c1)
(a + b) + v is Element of the carrier of (c1)
the addF of (c1) . ((a + b),v) is Element of the carrier of (c1)
[(a + b),v] is set
the addF of (c1) . [(a + b),v] is set
b + v is Element of the carrier of (c1)
the addF of (c1) . (b,v) is Element of the carrier of (c1)
[b,v] is set
the addF of (c1) . [b,v] is set
a + (b + v) is Element of the carrier of (c1)
the addF of (c1) . (a,(b + v)) is Element of the carrier of (c1)
[a,(b + v)] is set
the addF of (c1) . [a,(b + v)] is set
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
0. (c1) is V53((c1)) Element of the carrier of (c1)
the ZeroF of (c1) is Element of the carrier of (c1)
a + (0. (c1)) is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the addF of (c1) . (a,(0. (c1))) is Element of the carrier of (c1)
[a,(0. (c1))] is set
the addF of (c1) . [a,(0. (c1))] is set
(c1) . ((c1),a) is set
[(c1),a] is set
(c1) . [(c1),a] is set
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
b is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)
[(- 1),b] is Element of [:REAL,(Funcs (c1,REAL)):]
(c1) . [(- 1),b] is Element of Funcs (c1,REAL)
v is Element of the carrier of (c1)
a + v is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the addF of (c1) . (a,v) is Element of the carrier of (c1)
[a,v] is set
the addF of (c1) . [a,v] is set
0. (c1) is V53((c1)) Element of the carrier of (c1)
the ZeroF of (c1) is Element of the carrier of (c1)
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
b is Element of the carrier of (c1)
a * b is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the multF of (c1) . (a,b) is Element of the carrier of (c1)
[a,b] is set
the multF of (c1) . [a,b] is set
b * a is Element of the carrier of (c1)
the multF of (c1) . (b,a) is Element of the carrier of (c1)
[b,a] is set
the multF of (c1) . [b,a] is set
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
b is Element of the carrier of (c1)
a * b is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the multF of (c1) . (a,b) is Element of the carrier of (c1)
[a,b] is set
the multF of (c1) . [a,b] is set
v is Element of the carrier of (c1)
(a * b) * v is Element of the carrier of (c1)
the multF of (c1) . ((a * b),v) is Element of the carrier of (c1)
[(a * b),v] is set
the multF of (c1) . [(a * b),v] is set
b * v is Element of the carrier of (c1)
the multF of (c1) . (b,v) is Element of the carrier of (c1)
[b,v] is set
the multF of (c1) . [b,v] is set
a * (b * v) is Element of the carrier of (c1)
the multF of (c1) . (a,(b * v)) is Element of the carrier of (c1)
[a,(b * v)] is set
the multF of (c1) . [a,(b * v)] is set
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
1. (c1) is Element of the carrier of (c1)
the OneF of (c1) is Element of the carrier of (c1)
a * (1. (c1)) is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the multF of (c1) . (a,(1. (c1))) is Element of the carrier of (c1)
[a,(1. (c1))] is set
the multF of (c1) . [a,(1. (c1))] is set
(c1) . ((c1),a) is set
[(c1),a] is set
(c1) . [(c1),a] is set
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
b is Element of the carrier of (c1)
v is Element of the carrier of (c1)
b + v is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the addF of (c1) . (b,v) is Element of the carrier of (c1)
[b,v] is set
the addF of (c1) . [b,v] is set
a * (b + v) is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
the multF of (c1) . (a,(b + v)) is Element of the carrier of (c1)
[a,(b + v)] is set
the multF of (c1) . [a,(b + v)] is set
a * b is Element of the carrier of (c1)
the multF of (c1) . (a,b) is Element of the carrier of (c1)
[a,b] is set
the multF of (c1) . [a,b] is set
a * v is Element of the carrier of (c1)
the multF of (c1) . (a,v) is Element of the carrier of (c1)
[a,v] is set
the multF of (c1) . [a,v] is set
(a * b) + (a * v) is Element of the carrier of (c1)
the addF of (c1) . ((a * b),(a * v)) is Element of the carrier of (c1)
[(a * b),(a * v)] is set
the addF of (c1) . [(a * b),(a * v)] is set
the carrier of (c1) is non empty set
a is Element of the carrier of (c1)
b is Element of the carrier of (c1)
a * b is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the multF of (c1) . (a,b) is Element of the carrier of (c1)
[a,b] is set
the multF of (c1) . [a,b] is set
v is V33() real Element of REAL
v * (a * b) is Element of the carrier of (c1)
the Mult of (c1) is Relation-like [:REAL, the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of (c1):], the carrier of (c1):]
[:REAL, the carrier of (c1):] is Relation-like non empty V37() set
[:[:REAL, the carrier of (c1):], the carrier of (c1):] is Relation-like non empty V37() set
bool [:[:REAL, the carrier of (c1):], the carrier of (c1):] is non empty V37() set
the Mult of (c1) . (v,(a * b)) is set
[v,(a * b)] is set
the Mult of (c1) . [v,(a * b)] is set
v * a is Element of the carrier of (c1)
the Mult of (c1) . (v,a) is set
[v,a] is set
the Mult of (c1) . [v,a] is set
(v * a) * b is Element of the carrier of (c1)
the multF of (c1) . ((v * a),b) is Element of the carrier of (c1)
[(v * a),b] is set
the multF of (c1) . [(v * a),b] is set
the carrier of (c1) is non empty set
a is V33() real set
b is V33() real set
a * b is V33() real set
v is Element of the carrier of (c1)
(a * b) * v is Element of the carrier of (c1)
the Mult of (c1) is Relation-like [:REAL, the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of (c1):], the carrier of (c1):]
[:REAL, the carrier of (c1):] is Relation-like non empty V37() set
[:[:REAL, the carrier of (c1):], the carrier of (c1):] is Relation-like non empty V37() set
bool [:[:REAL, the carrier of (c1):], the carrier of (c1):] is non empty V37() set
the Mult of (c1) . ((a * b),v) is set
[(a * b),v] is set
the Mult of (c1) . [(a * b),v] is set
b * v is Element of the carrier of (c1)
the Mult of (c1) . (b,v) is set
[b,v] is set
the Mult of (c1) . [b,v] is set
a * (b * v) is Element of the carrier of (c1)
the Mult of (c1) . (a,(b * v)) is set
[a,(b * v)] is set
the Mult of (c1) . [a,(b * v)] is set
a is V33() real Element of REAL
b is V33() real Element of REAL
a * b is V33() real Element of REAL
(a * b) * v is Element of the carrier of (c1)
the Mult of (c1) . ((a * b),v) is set
[(a * b),v] is set
the Mult of (c1) . [(a * b),v] is set
b * v is Element of the carrier of (c1)
the Mult of (c1) . (b,v) is set
[b,v] is set
the Mult of (c1) . [b,v] is set
a * (b * v) is Element of the carrier of (c1)
the Mult of (c1) . (a,(b * v)) is set
[a,(b * v)] is set
the Mult of (c1) . [a,(b * v)] is set
the carrier of (c1) is non empty set
a is V33() real set
b is Element of the carrier of (c1)
v is Element of the carrier of (c1)
b + v is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the addF of (c1) . (b,v) is Element of the carrier of (c1)
[b,v] is set
the addF of (c1) . [b,v] is set
a * (b + v) is Element of the carrier of (c1)
the Mult of (c1) is Relation-like [:REAL, the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of (c1):], the carrier of (c1):]
[:REAL, the carrier of (c1):] is Relation-like non empty V37() set
[:[:REAL, the carrier of (c1):], the carrier of (c1):] is Relation-like non empty V37() set
bool [:[:REAL, the carrier of (c1):], the carrier of (c1):] is non empty V37() set
the Mult of (c1) . (a,(b + v)) is set
[a,(b + v)] is set
the Mult of (c1) . [a,(b + v)] is set
a * b is Element of the carrier of (c1)
the Mult of (c1) . (a,b) is set
[a,b] is set
the Mult of (c1) . [a,b] is set
a * v is Element of the carrier of (c1)
the Mult of (c1) . (a,v) is set
[a,v] is set
the Mult of (c1) . [a,v] is set
(a * b) + (a * v) is Element of the carrier of (c1)
the addF of (c1) . ((a * b),(a * v)) is Element of the carrier of (c1)
[(a * b),(a * v)] is set
the addF of (c1) . [(a * b),(a * v)] is set
a is V33() real Element of REAL
a * (b + v) is Element of the carrier of (c1)
the Mult of (c1) . (a,(b + v)) is set
[a,(b + v)] is set
the Mult of (c1) . [a,(b + v)] is set
a * b is Element of the carrier of (c1)
the Mult of (c1) . (a,b) is set
[a,b] is set
the Mult of (c1) . [a,b] is set
a * v is Element of the carrier of (c1)
the Mult of (c1) . (a,v) is set
[a,v] is set
the Mult of (c1) . [a,v] is set
(a * b) + (a * v) is Element of the carrier of (c1)
the addF of (c1) . ((a * b),(a * v)) is Element of the carrier of (c1)
[(a * b),(a * v)] is set
the addF of (c1) . [(a * b),(a * v)] is set
the carrier of (c1) is non empty set
a is V33() real set
b is V33() real set
a + b is V33() real set
v is Element of the carrier of (c1)
(a + b) * v is Element of the carrier of (c1)
the Mult of (c1) is Relation-like [:REAL, the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of (c1):], the carrier of (c1):]
[:REAL, the carrier of (c1):] is Relation-like non empty V37() set
[:[:REAL, the carrier of (c1):], the carrier of (c1):] is Relation-like non empty V37() set
bool [:[:REAL, the carrier of (c1):], the carrier of (c1):] is non empty V37() set
the Mult of (c1) . ((a + b),v) is set
[(a + b),v] is set
the Mult of (c1) . [(a + b),v] is set
a * v is Element of the carrier of (c1)
the Mult of (c1) . (a,v) is set
[a,v] is set
the Mult of (c1) . [a,v] is set
b * v is Element of the carrier of (c1)
the Mult of (c1) . (b,v) is set
[b,v] is set
the Mult of (c1) . [b,v] is set
(a * v) + (b * v) is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is Relation-like non empty set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is Relation-like non empty set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is non empty set
the addF of (c1) . ((a * v),(b * v)) is Element of the carrier of (c1)
[(a * v),(b * v)] is set
the addF of (c1) . [(a * v),(b * v)] is set
a is V33() real Element of REAL
b is V33() real Element of REAL
a + b is V33() real Element of REAL
(a + b) * v is Element of the carrier of (c1)
the Mult of (c1) . ((a + b),v) is set
[(a + b),v] is set
the Mult of (c1) . [(a + b),v] is set
a * v is Element of the carrier of (c1)
the Mult of (c1) . (a,v) is set
[a,v] is set
the Mult of (c1) . [a,v] is set
b * v is Element of the carrier of (c1)
the Mult of (c1) . (b,v) is set
[b,v] is set
the Mult of (c1) . [b,v] is set
(a * v) + (b * v) is Element of the carrier of (c1)
the addF of (c1) . ((a * v),(b * v)) is Element of the carrier of (c1)
[(a * v),(b * v)] is set
the addF of (c1) . [(a * v),(b * v)] is set
({}) is non empty left_complementable right_complementable complementable associative commutative right-distributive right_unital Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V126() () () ()
Funcs ({},REAL) is non empty FUNCTION_DOMAIN of {} , REAL
({}) is Relation-like [:(Funcs ({},REAL)),(Funcs ({},REAL)):] -defined Funcs ({},REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs ({},REAL)),(Funcs ({},REAL)):],(Funcs ({},REAL)):]
[:(Funcs ({},REAL)),(Funcs ({},REAL)):] is Relation-like non empty set
[:[:(Funcs ({},REAL)),(Funcs ({},REAL)):],(Funcs ({},REAL)):] is Relation-like non empty set
bool [:[:(Funcs ({},REAL)),(Funcs ({},REAL)):],(Funcs ({},REAL)):] is non empty set
({}) is Relation-like [:(Funcs ({},REAL)),(Funcs ({},REAL)):] -defined Funcs ({},REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs ({},REAL)),(Funcs ({},REAL)):],(Funcs ({},REAL)):]
({}) is Relation-like [:REAL,(Funcs ({},REAL)):] -defined Funcs ({},REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs ({},REAL)):],(Funcs ({},REAL)):]
[:REAL,(Funcs ({},REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs ({},REAL)):],(Funcs ({},REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs ({},REAL)):],(Funcs ({},REAL)):] is non empty V37() set
({}) is Relation-like non-empty empty-yielding {} -defined REAL -valued Function-like empty quasi_total Function-yielding V25() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real V37() V42() V44( {} ) Element of Funcs ({},REAL)
{} --> 1 is Relation-like non-empty empty-yielding {} -defined NAT -valued Function-like constant empty V14( {} ) quasi_total Function-yielding V25() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real V37() V42() V44( {} ) Element of bool [:{},NAT:]
[:{},NAT:] is Relation-like set
bool [:{},NAT:] is non empty set
[:{},{1}:] is Relation-like set
({}) is Relation-like non-empty empty-yielding {} -defined REAL -valued Function-like empty quasi_total Function-yielding V25() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real V37() V42() V44( {} ) Element of Funcs ({},REAL)
{} --> 0 is Relation-like non-empty empty-yielding {} -defined NAT -valued Function-like constant empty V14( {} ) quasi_total Function-yielding V25() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real V37() V42() V44( {} ) Element of bool [:{},NAT:]
[:{},{0}:] is Relation-like set
((Funcs ({},REAL)),({}),({}),({}),({}),({})) is () ()