:: FUNCSDOM semantic presentation

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:]
c₁ is set
a is non empty set
Funcs (c₁,a) is non empty FUNCTION_DOMAIN of c₁,a
[:(Funcs (c₁,a)),(Funcs (c₁,a)):] is Relation-like non empty set
[:[:(Funcs (c₁,a)),(Funcs (c₁,a)):],(Funcs (c₁,a)):] is Relation-like non empty set
bool [:[:(Funcs (c₁,a)),(Funcs (c₁,a)):],(Funcs (c₁,a)):] is non empty set
b is Relation-like [:(Funcs (c₁,a)),(Funcs (c₁,a)):] -defined Funcs (c₁,a) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,a)),(Funcs (c₁,a)):],(Funcs (c₁,a)):]
v is Relation-like c₁ -defined a -valued Function-like quasi_total Element of Funcs (c₁,a)
a is Relation-like c₁ -defined a -valued Function-like quasi_total Element of Funcs (c₁,a)
b . (v,a) is set
[v,a] is set
b . [v,a] is set
b is Element of Funcs (c₁,a)
h is Element of Funcs (c₁,a)
b . (b,h) is Element of Funcs (c₁,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
c₁ is non empty set
a is non empty set
Funcs (c₁,a) is non empty FUNCTION_DOMAIN of c₁,a
[:[:b,v:],(Funcs (c₁,a)):] is Relation-like non empty set
bool [:[:b,v:],(Funcs (c₁,a)):] is non empty set
a is Relation-like [:b,v:] -defined Funcs (c₁,a) -valued Function-like quasi_total Element of bool [:[:b,v:],(Funcs (c₁,a)):]
b is Element of [:b,v:]
a . b is set
a . b is Element of Funcs (c₁,a)
c₁ is non empty set
[:c₁,c₁:] is Relation-like non empty set
[:[:c₁,c₁:],c₁:] is Relation-like non empty set
bool [:[:c₁,c₁:],c₁:] is non empty set
a is set
[:a,c₁:] is Relation-like set
bool [:a,c₁:] is non empty set
b is Relation-like [:c₁,c₁:] -defined c₁ -valued Function-like quasi_total Element of bool [:[:c₁,c₁:],c₁:]
v is Relation-like a -defined c₁ -valued Function-like quasi_total Element of bool [:a,c₁:]
a is Relation-like a -defined c₁ -valued Function-like quasi_total Element of bool [:a,c₁:]
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 c₁ -valued set
Funcs (a,c₁) is non empty FUNCTION_DOMAIN of a,c₁
b .: (v,a) is Relation-like a -defined c₁ -valued Function-like quasi_total Element of bool [:a,c₁:]
c₁ is non empty set
[:c₁,c₁:] is Relation-like non empty set
[:[:c₁,c₁:],c₁:] is Relation-like non empty set
bool [:[:c₁,c₁:],c₁:] is non empty set
a is set
[:a,c₁:] is Relation-like set
bool [:a,c₁:] is non empty set
b is Relation-like [:c₁,c₁:] -defined c₁ -valued Function-like quasi_total Element of bool [:[:c₁,c₁:],c₁:]
v is Element of c₁
a is Relation-like a -defined c₁ -valued Function-like quasi_total Element of bool [:a,c₁:]
b [;] (v,a) is Relation-like Function-like set
dom a is set
(dom a) --> v is Relation-like dom a -defined c₁ -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 c₁ -valued set
Funcs (a,c₁) is non empty FUNCTION_DOMAIN of a,c₁
b [;] (v,a) is Relation-like a -defined c₁ -valued Function-like quasi_total Element of bool [:a,c₁:]
c₁ is set
Funcs (c₁,REAL) is non empty FUNCTION_DOMAIN of c₁, REAL
[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] is Relation-like non empty set
[:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is non empty set
a is Relation-like [:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
b is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
v is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
(c₁,REAL,a,b,v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[b,v] is set
a . [b,v] is set
(REAL,c₁,addreal,b,v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,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 (c₁,REAL)),(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
b is Relation-like [:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
v is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
a is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
(c₁,REAL,a,v,a) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[v,a] is set
a . [v,a] is set
(REAL,c₁,addreal,v,a) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
K291(v,a) is Relation-like Function-like set
K291(v,a) * addreal is Relation-like REAL -valued set
(c₁,REAL,b,v,a) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
b . [v,a] is set
c₁ is set
Funcs (c₁,REAL) is non empty FUNCTION_DOMAIN of c₁, REAL
[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] is Relation-like non empty set
[:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is non empty set
a is Relation-like [:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
b is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
v is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
(c₁,REAL,a,b,v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[b,v] is set
a . [b,v] is set
(REAL,c₁,multreal,b,v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,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 (c₁,REAL)),(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
b is Relation-like [:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
v is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
a is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
(c₁,REAL,a,v,a) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[v,a] is set
a . [v,a] is set
(REAL,c₁,multreal,v,a) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
K291(v,a) is Relation-like Function-like set
K291(v,a) * multreal is Relation-like REAL -valued set
(c₁,REAL,b,v,a) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
b . [v,a] is set
c₁ is set
Funcs (c₁,REAL) is non empty FUNCTION_DOMAIN of c₁, REAL
[:REAL,(Funcs (c₁,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is non empty V37() set
a is Relation-like [:REAL,(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
b is V33() real Element of REAL
v is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
a . (b,v) is Element of Funcs (c₁,REAL)
[b,v] is set
a . [b,v] is set
(REAL,c₁,multreal,b,v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,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 (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
b is Relation-like [:REAL,(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
v is V33() real Element of REAL
a is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
a . (v,a) is Element of Funcs (c₁,REAL)
[v,a] is set
a . [v,a] is set
(REAL,c₁,multreal,v,a) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,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 (c₁,REAL)
b . [v,a] is set
c₁ 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
c₁ --> 0 is Relation-like c₁ -defined NAT -valued Function-like constant V14(c₁) quasi_total Element of bool [:c₁,NAT:]
[:c₁,NAT:] is Relation-like set
bool [:c₁,NAT:] is non empty set
{0} is non empty trivial V44(1) set
[:c₁,{0}:] is Relation-like set
Funcs (c₁,REAL) is non empty FUNCTION_DOMAIN of c₁, REAL
[:c₁,REAL:] is Relation-like set
bool [:c₁,REAL:] is non empty set
c₁ is set
c₁ --> 1 is Relation-like non-empty c₁ -defined NAT -valued Function-like constant V14(c₁) quasi_total Element of bool [:c₁,NAT:]
[:c₁,NAT:] is Relation-like set
bool [:c₁,NAT:] is non empty set
{1} is non empty trivial V44(1) set
[:c₁,{1}:] is Relation-like set
Funcs (c₁,REAL) is non empty FUNCTION_DOMAIN of c₁, REAL
[:c₁,REAL:] is Relation-like set
bool [:c₁,REAL:] is non empty set
c₁ is non empty set
a is non empty set
[:c₁,a:] is Relation-like non empty set
bool [:c₁,a:] is non empty set
b is Element of c₁
v is Relation-like c₁ -defined a -valued Function-like quasi_total Element of bool [:c₁,a:]
dom v is set
c₁ is non empty set
Funcs (c₁,REAL) is non empty FUNCTION_DOMAIN of c₁, REAL
(c₁) is Relation-like [:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] is Relation-like non empty set
[:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is non empty set
a is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
b is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
v is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
(c₁,REAL,(c₁),b,v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[b,v] is set
(c₁) . [b,v] is set
a is Element of c₁
(REAL,c₁,addreal,b,v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
K291(b,v) is Relation-like Function-like set
K291(b,v) * addreal is Relation-like REAL -valued set
dom (REAL,c₁,addreal,b,v) is set
(c₁,REAL,(c₁),b,v) . a is V33() real Element of REAL
(REAL,c₁,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 c₁
a . a is V33() real Element of REAL
(REAL,c₁,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 c₁
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 c₁
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
c₁ is non empty set
Funcs (c₁,REAL) is non empty FUNCTION_DOMAIN of c₁, REAL
(c₁) is Relation-like [:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] is Relation-like non empty set
[:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is non empty set
a is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
b is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
v is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
(c₁,REAL,(c₁),b,v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[b,v] is set
(c₁) . [b,v] is set
a is Element of c₁
(REAL,c₁,multreal,b,v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
K291(b,v) is Relation-like Function-like set
K291(b,v) * multreal is Relation-like REAL -valued set
dom (REAL,c₁,multreal,b,v) is set
(c₁,REAL,(c₁),b,v) . a is V33() real Element of REAL
(REAL,c₁,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 c₁
a . a is V33() real Element of REAL
(REAL,c₁,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 c₁
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 c₁
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
c₁ is non empty set
(c₁) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
Funcs (c₁,REAL) is non empty FUNCTION_DOMAIN of c₁, REAL
c₁ --> 0 is Relation-like c₁ -defined NAT -valued Function-like constant non empty V14(c₁) quasi_total Element of bool [:c₁,NAT:]
[:c₁,NAT:] is Relation-like non empty V37() set
bool [:c₁,NAT:] is non empty V37() set
[:c₁,{0}:] is Relation-like non empty set
(c₁) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
c₁ --> 1 is Relation-like non-empty c₁ -defined NAT -valued Function-like constant non empty V14(c₁) quasi_total Element of bool [:c₁,NAT:]
[:c₁,{1}:] is Relation-like non empty set
the Element of c₁ is Element of c₁
(c₁) . the Element of c₁ is V33() real Element of REAL
c₁ is non empty set
Funcs (c₁,REAL) is non empty FUNCTION_DOMAIN of c₁, REAL
(c₁) is Relation-like [:REAL,(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
[:REAL,(Funcs (c₁,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is non empty V37() set
a is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
b is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
v is V33() real Element of REAL
[v,b] is Element of [:REAL,(Funcs (c₁,REAL)):]
(c₁,REAL,REAL,(Funcs (c₁,REAL)),(c₁),[v,b]) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
a is Element of c₁
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
(c₁) . (v,b) is Element of Funcs (c₁,REAL)
[v,b] is set
(c₁) . [v,b] is set
(REAL,c₁,multreal,v,b) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,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,c₁,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 c₁
a . a is V33() real Element of REAL
(c₁,REAL,REAL,(Funcs (c₁,REAL)),(c₁),[v,b]) . a is V33() real Element of REAL
(REAL,c₁,multreal,v,b) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,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
(c₁) . (v,b) is Element of Funcs (c₁,REAL)
[v,b] is set
(c₁) . [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
(c₁) . (v,b) is Element of Funcs (c₁,REAL)
[v,b] is set
(c₁) . [v,b] is set
a is Element of c₁
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
c₁ is set
Funcs (c₁,REAL) is non empty FUNCTION_DOMAIN of c₁, REAL
(c₁) is Relation-like [:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] is Relation-like non empty set
[:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is non empty set
a is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
b is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
(c₁,REAL,(c₁),a,b) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[a,b] is set
(c₁) . [a,b] is set
(c₁,REAL,(c₁),b,a) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[b,a] is set
(c₁) . [b,a] is set
(REAL,c₁,addreal,a,b) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
K291(a,b) is Relation-like Function-like set
K291(a,b) * addreal is Relation-like REAL -valued set
(REAL,c₁,addreal,b,a) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
K291(b,a) is Relation-like Function-like set
K291(b,a) * addreal is Relation-like REAL -valued set
c₁ is set
Funcs (c₁,REAL) is non empty FUNCTION_DOMAIN of c₁, REAL
(c₁) is Relation-like [:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] is Relation-like non empty set
[:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is non empty set
a is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
b is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
v is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
(c₁,REAL,(c₁),b,v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[b,v] is set
(c₁) . [b,v] is set
(c₁,REAL,(c₁),a,(c₁,REAL,(c₁),b,v)) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[a,(c₁,REAL,(c₁),b,v)] is set
(c₁) . [a,(c₁,REAL,(c₁),b,v)] is set
(c₁,REAL,(c₁),a,b) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[a,b] is set
(c₁) . [a,b] is set
(c₁,REAL,(c₁),(c₁,REAL,(c₁),a,b),v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[(c₁,REAL,(c₁),a,b),v] is set
(c₁) . [(c₁,REAL,(c₁),a,b),v] is set
(REAL,c₁,addreal,b,v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
K291(b,v) is Relation-like Function-like set
K291(b,v) * addreal is Relation-like REAL -valued set
(c₁,REAL,(c₁),a,(REAL,c₁,addreal,b,v)) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[a,(REAL,c₁,addreal,b,v)] is set
(c₁) . [a,(REAL,c₁,addreal,b,v)] is set
(REAL,c₁,addreal,a,(REAL,c₁,addreal,b,v)) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
K291(a,(REAL,c₁,addreal,b,v)) is Relation-like Function-like set
K291(a,(REAL,c₁,addreal,b,v)) * addreal is Relation-like REAL -valued set
(REAL,c₁,addreal,a,b) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
K291(a,b) is Relation-like Function-like set
K291(a,b) * addreal is Relation-like REAL -valued set
(REAL,c₁,addreal,(REAL,c₁,addreal,a,b),v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
K291((REAL,c₁,addreal,a,b),v) is Relation-like Function-like set
K291((REAL,c₁,addreal,a,b),v) * addreal is Relation-like REAL -valued set
(c₁,REAL,(c₁),(REAL,c₁,addreal,a,b),v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[(REAL,c₁,addreal,a,b),v] is set
(c₁) . [(REAL,c₁,addreal,a,b),v] is set
c₁ is set
Funcs (c₁,REAL) is non empty FUNCTION_DOMAIN of c₁, REAL
(c₁) is Relation-like [:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] is Relation-like non empty set
[:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is non empty set
a is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
b is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
(c₁,REAL,(c₁),a,b) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[a,b] is set
(c₁) . [a,b] is set
(c₁,REAL,(c₁),b,a) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[b,a] is set
(c₁) . [b,a] is set
(REAL,c₁,multreal,a,b) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
K291(a,b) is Relation-like Function-like set
K291(a,b) * multreal is Relation-like REAL -valued set
(REAL,c₁,multreal,b,a) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
K291(b,a) is Relation-like Function-like set
K291(b,a) * multreal is Relation-like REAL -valued set
c₁ is set
Funcs (c₁,REAL) is non empty FUNCTION_DOMAIN of c₁, REAL
(c₁) is Relation-like [:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] is Relation-like non empty set
[:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is non empty set
a is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
b is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
v is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
(c₁,REAL,(c₁),b,v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[b,v] is set
(c₁) . [b,v] is set
(c₁,REAL,(c₁),a,(c₁,REAL,(c₁),b,v)) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[a,(c₁,REAL,(c₁),b,v)] is set
(c₁) . [a,(c₁,REAL,(c₁),b,v)] is set
(c₁,REAL,(c₁),a,b) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[a,b] is set
(c₁) . [a,b] is set
(c₁,REAL,(c₁),(c₁,REAL,(c₁),a,b),v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[(c₁,REAL,(c₁),a,b),v] is set
(c₁) . [(c₁,REAL,(c₁),a,b),v] is set
(REAL,c₁,multreal,b,v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
K291(b,v) is Relation-like Function-like set
K291(b,v) * multreal is Relation-like REAL -valued set
(c₁,REAL,(c₁),a,(REAL,c₁,multreal,b,v)) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[a,(REAL,c₁,multreal,b,v)] is set
(c₁) . [a,(REAL,c₁,multreal,b,v)] is set
(REAL,c₁,multreal,a,(REAL,c₁,multreal,b,v)) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
K291(a,(REAL,c₁,multreal,b,v)) is Relation-like Function-like set
K291(a,(REAL,c₁,multreal,b,v)) * multreal is Relation-like REAL -valued set
(REAL,c₁,multreal,a,b) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
K291(a,b) is Relation-like Function-like set
K291(a,b) * multreal is Relation-like REAL -valued set
(REAL,c₁,multreal,(REAL,c₁,multreal,a,b),v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
K291((REAL,c₁,multreal,a,b),v) is Relation-like Function-like set
K291((REAL,c₁,multreal,a,b),v) * multreal is Relation-like REAL -valued set
(c₁,REAL,(c₁),(REAL,c₁,multreal,a,b),v) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[(REAL,c₁,multreal,a,b),v] is set
(c₁) . [(REAL,c₁,multreal,a,b),v] is set
c₁ is set
Funcs (c₁,REAL) is non empty FUNCTION_DOMAIN of c₁, REAL
(c₁) is Relation-like [:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] is Relation-like non empty set
[:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is non empty set
(c₁) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
c₁ --> 1 is Relation-like non-empty c₁ -defined NAT -valued Function-like constant V14(c₁) quasi_total Element of bool [:c₁,NAT:]
[:c₁,NAT:] is Relation-like set
bool [:c₁,NAT:] is non empty set
[:c₁,{1}:] is Relation-like set
a is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
(c₁,REAL,(c₁),(c₁),a) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[(c₁),a] is set
(c₁) . [(c₁),a] is set
(REAL,c₁,multreal,(c₁),a) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
K291((c₁),a) is Relation-like Function-like set
K291((c₁),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
c₁ is set
Funcs (c₁,REAL) is non empty FUNCTION_DOMAIN of c₁, REAL
(c₁) is Relation-like [:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] is Relation-like non empty set
[:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is non empty set
(c₁) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
c₁ --> 0 is Relation-like c₁ -defined NAT -valued Function-like constant V14(c₁) quasi_total Element of bool [:c₁,NAT:]
[:c₁,NAT:] is Relation-like set
bool [:c₁,NAT:] is non empty set
[:c₁,{0}:] is Relation-like set
a is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
(c₁,REAL,(c₁),(c₁),a) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[(c₁),a] is set
(c₁) . [(c₁),a] is set
(REAL,c₁,addreal,(c₁),a) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
K291((c₁),a) is Relation-like Function-like set
K291((c₁),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
c₁ is set
Funcs (c₁,REAL) is non empty FUNCTION_DOMAIN of c₁, REAL
(c₁) is Relation-like [:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):] is Relation-like non empty set
[:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is Relation-like non empty set
bool [:[:(Funcs (c₁,REAL)),(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is non empty set
[:REAL,(Funcs (c₁,REAL)):] is Relation-like non empty V37() set
(c₁) is Relation-like [:REAL,(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
[:[:REAL,(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is non empty V37() set
(c₁) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
c₁ --> 0 is Relation-like c₁ -defined NAT -valued Function-like constant V14(c₁) quasi_total Element of bool [:c₁,NAT:]
[:c₁,NAT:] is Relation-like set
bool [:c₁,NAT:] is non empty set
[:c₁,{0}:] is Relation-like set
a is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[(- 1),a] is Element of [:REAL,(Funcs (c₁,REAL)):]
(c₁) . [(- 1),a] is Element of Funcs (c₁,REAL)
(c₁,REAL,(c₁),a,((c₁) . [(- 1),a])) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
[a,((c₁) . [(- 1),a])] is set
(c₁) . [a,((c₁) . [(- 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
c₁ is set
Funcs (c₁,REAL) is non empty FUNCTION_DOMAIN of c₁, REAL
(c₁) is Relation-like [:REAL,(Funcs (c₁,REAL)):] -defined Funcs (c₁,REAL) -valued Function-like quasi_total Element of bool [:[:REAL,(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):]
[:REAL,(Funcs (c₁,REAL)):] is Relation-like non empty V37() set
[:[:REAL,(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is Relation-like non empty V37() set
bool [:[:REAL,(Funcs (c₁,REAL)):],(Funcs (c₁,REAL)):] is non empty V37() set
a is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,REAL)
(c₁) . (1,a) is Element of Funcs (c₁,REAL)
[1,a] is set
(c₁) . [1,a] is set
(REAL,c₁,multreal,1,a) is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of Funcs (c₁,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
c₁ is V33() real Element of REAL
a is V33() real Element of REAL
c₁ * 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) . (c₁,((b) . (a,v))) is Element of Funcs (b,REAL)
[c₁,((b) . (a,v))] is set
(b) . [c₁,((b) . (a,v))] is set
(b) . ((c₁ * a),v) is Element of Funcs (b,REAL)
[(c₁ * a),v] is set
(b) . [(c₁ * 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,c₁,(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)) --> c₁ is Relation-like dom (REAL,b,multreal,a,v) -defined REAL -valued Function-like constant V14( dom (REAL,b,multreal,a,v)) set
{c₁} is non empty trivial V44(1) set
[:(dom (REAL,b,multreal,a,v)),{c₁}:] is Relation-like set
K291(((dom (REAL,b,multreal,a,v)) --> c₁),(REAL,b,multreal,a,v)) is Relation-like Function-like set
K291(((dom (REAL,b,multreal,a,v)) --> c₁),(REAL,b,multreal,a,v)) * multreal is Relation-like REAL -valued set
(REAL,b,multreal,(c₁ * a),v) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
(dom v) --> (c₁ * a) is Relation-like dom v -defined REAL -valued Function-like constant V14( dom v) set
{(c₁ * a)} is non empty trivial V44(1) set
[:(dom v),{(c₁ * a)}:] is Relation-like set
K291(((dom v) --> (c₁ * a)),v) is Relation-like Function-like set
K291(((dom v) --> (c₁ * 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)
[c₁,(a,REAL,REAL,(Funcs (a,REAL)),(a),[a,b])] is Element of [:REAL,(Funcs (a,REAL)):]
(a,REAL,REAL,(Funcs (a,REAL)),(a),[c₁,(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),[c₁,(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
c₁ * ((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
c₁ * (a * (b . h)) is V33() real Element of REAL
(c₁ * a) * (b . h) is V33() real Element of REAL
[(c₁ * a),b] is Element of [:REAL,(Funcs (a,REAL)):]
(a,REAL,REAL,(Funcs (a,REAL)),(a),[(c₁ * 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),[(c₁ * a),b]) . h is V33() real Element of REAL
c₁ is V33() real Element of REAL
a is V33() real Element of REAL
c₁ + 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) . (c₁,v) is Element of Funcs (b,REAL)
[c₁,v] is set
(b) . [c₁,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) . (c₁,v)),((b) . (a,v))) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
[((b) . (c₁,v)),((b) . (a,v))] is set
(b) . [((b) . (c₁,v)),((b) . (a,v))] is set
(b) . ((c₁ + a),v) is Element of Funcs (b,REAL)
[(c₁ + a),v] is set
(b) . [(c₁ + a),v] is set
(REAL,b,multreal,(c₁ + a),v) is Relation-like b -defined REAL -valued Function-like quasi_total Element of Funcs (b,REAL)
dom v is set
(dom v) --> (c₁ + a) is Relation-like dom v -defined REAL -valued Function-like constant V14( dom v) set
{(c₁ + a)} is non empty trivial V44(1) set
[:(dom v),{(c₁ + a)}:] is Relation-like set
K291(((dom v) --> (c₁ + a)),v) is Relation-like Function-like set
K291(((dom v) --> (c₁ + 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)
[c₁,b] is Element of [:REAL,(Funcs (a,REAL)):]
(a,REAL,REAL,(Funcs (a,REAL)),(a),[c₁,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),[c₁,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),[c₁,b]),(a,REAL,REAL,(Funcs (a,REAL)),(a),[a,b])] is set
(a) . [(a,REAL,REAL,(Funcs (a,REAL)),(a),[c₁,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),[c₁,b]),(a,REAL,REAL,(Funcs (a,REAL)),(a),[a,b])) . h is V33() real Element of REAL
(a,REAL,REAL,(Funcs (a,REAL)),(a),[c₁,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),[c₁,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
c₁ * (b . h) is V33() real Element of REAL
(c₁ * (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
(c₁ * (b . h)) + (a * (b . h)) is V33() real Element of REAL
(c₁ + a) * (b . h) is V33() real Element of REAL
[(c₁ + a),b] is Element of [:REAL,(Funcs (a,REAL)):]
(a,REAL,REAL,(Funcs (a,REAL)),(a),[(c₁ + 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),[(c₁ + a),b]) . h is V33() real Element of REAL
c₁ 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) . (c₁,b) is Element of Funcs (a,REAL)
[c₁,b] is set
(a) . [c₁,b] is set
v is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
(a) . (c₁,v) is Element of Funcs (a,REAL)
[c₁,v] is set
(a) . [c₁,v] is set
(a,REAL,(a),((a) . (c₁,b)),((a) . (c₁,v))) is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
[((a) . (c₁,b)),((a) . (c₁,v))] is set
(a) . [((a) . (c₁,b)),((a) . (c₁,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) . (c₁,(a,REAL,(a),b,v)) is Element of Funcs (a,REAL)
[c₁,(a,REAL,(a),b,v)] is set
(a) . [c₁,(a,REAL,(a),b,v)] is set
(REAL,a,multreal,c₁,(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)) --> c₁ is Relation-like dom (a,REAL,(a),b,v) -defined REAL -valued Function-like constant V14( dom (a,REAL,(a),b,v)) set
{c₁} is non empty trivial V44(1) set
[:(dom (a,REAL,(a),b,v)),{c₁}:] is Relation-like set
K291(((dom (a,REAL,(a),b,v)) --> c₁),(a,REAL,(a),b,v)) is Relation-like Function-like set
K291(((dom (a,REAL,(a),b,v)) --> c₁),(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)
[c₁,b] is Element of [:REAL,(Funcs (a,REAL)):]
(a,REAL,REAL,(Funcs (a,REAL)),(a),[c₁,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)
[c₁,h] is Element of [:REAL,(Funcs (a,REAL)):]
(a,REAL,REAL,(Funcs (a,REAL)),(a),[c₁,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),[c₁,b]),(a,REAL,REAL,(Funcs (a,REAL)),(a),[c₁,h])) is Relation-like a -defined REAL -valued Function-like quasi_total Element of Funcs (a,REAL)
[(a,REAL,REAL,(Funcs (a,REAL)),(a),[c₁,b]),(a,REAL,REAL,(Funcs (a,REAL)),(a),[c₁,h])] is set
(a) . [(a,REAL,REAL,(Funcs (a,REAL)),(a),[c₁,b]),(a,REAL,REAL,(Funcs (a,REAL)),(a),[c₁,h])] is set
t is Element of a
(a,REAL,(a),(a,REAL,REAL,(Funcs (a,REAL)),(a),[c₁,b]),(a,REAL,REAL,(Funcs (a,REAL)),(a),[c₁,h])) . t is V33() real Element of REAL
(a,REAL,REAL,(Funcs (a,REAL)),(a),[c₁,b]) . t is V33() real Element of REAL
(a,REAL,REAL,(Funcs (a,REAL)),(a),[c₁,h]) . t is V33() real Element of REAL
((a,REAL,REAL,(Funcs (a,REAL)),(a),[c₁,b]) . t) + ((a,REAL,REAL,(Funcs (a,REAL)),(a),[c₁,h]) . t) is V33() real Element of REAL
b . t is V33() real Element of REAL
c₁ * (b . t) is V33() real Element of REAL
(c₁ * (b . t)) + ((a,REAL,REAL,(Funcs (a,REAL)),(a),[c₁,h]) . t) is V33() real Element of REAL
h . t is V33() real Element of REAL
c₁ * (h . t) is V33() real Element of REAL
(c₁ * (b . t)) + (c₁ * (h . t)) is V33() real Element of REAL
(b . t) + (h . t) is V33() real Element of REAL
c₁ * ((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
c₁ * ((a,REAL,(a),b,h) . t) is V33() real Element of REAL
[c₁,(a,REAL,(a),b,h)] is Element of [:REAL,(Funcs (a,REAL)):]