:: FUNCSDOM semantic presentation

REAL is non empty V37() set

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

bool is non empty V37() set

bool is non empty V37() set

bool is non empty V37() set

bool is non empty V37() set

bool is non empty V37() set

bool is non empty V37() set

bool is non empty V37() set

bool is non empty V37() set

bool is non empty V37() set

bool NAT is non empty V37() set
bool NAT is non empty V37() set

{{},1} is non empty set

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)):]

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:]

b .: (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

b [;] (v,a) is Relation-like Function-like set
dom a is 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)):]

(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)

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)):]

(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)

(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)):]

(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)

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)):]

(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)

(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

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

{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 . (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

{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

bool [:c1,NAT:] is non empty set
is non empty trivial V44(1) set

Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL

bool [:c1,REAL:] is non empty set
c1 is 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

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

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

(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)

(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

(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)

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

Funcs (c1,REAL) is non empty FUNCTION_DOMAIN of c1, REAL

[:c1,NAT:] is Relation-like non empty V37() set
bool [:c1,NAT:] is non empty V37() set
[:c1,:] is Relation-like non empty set

[: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

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

{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

{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

(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)

(REAL,c1,addreal,b,a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,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,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)

(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)
(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)
(REAL,c1,addreal,a,b) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,REAL)

(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)
(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)
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,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)

(REAL,c1,multreal,b,a) is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of Funcs (c1,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,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)

(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)

(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

bool [:c1,NAT:] is non empty set
[:c1,{1}:] is Relation-like set

(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,NAT:] is Relation-like non empty V37() set
bool [:b,NAT:] is non empty V37() set
[:b,{1}:] is Relation-like non empty set

(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

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

(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,NAT:] is Relation-like non empty V37() set
bool [:b,NAT:] is non empty V37() set
[:b,:] is Relation-like non empty set

(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

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

[(- 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

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,NAT:] is Relation-like non empty V37() set
bool [:b,NAT:] is non empty V37() set
[:b,:] 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

(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 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

(b) . (1,v) is Element of Funcs (b,REAL)
[1,v] is set
(b) . [1,v] is set

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

(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

dom v is 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)

{(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

[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

(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

{(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

[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

(a) . (c1,b) is Element of Funcs (a,REAL)
[c1,b] is set
(a) . [c1,b] is set

(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

[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)

[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)):]