:: RFUNCT_2 semantic presentation

REAL is non empty V48() V49() V50() V54() V55() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() Element of bool REAL
bool REAL is set
COMPLEX is non empty V48() V54() V55() set
RAT is non empty V48() V49() V50() V51() V54() V55() set
INT is non empty V48() V49() V50() V51() V52() V54() V55() set
omega is non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() set
bool omega is set
bool NAT is set
[:COMPLEX,COMPLEX:] is complex-valued set
bool [:COMPLEX,COMPLEX:] is set
[:COMPLEX,REAL:] is complex-valued ext-real-valued real-valued set
bool [:COMPLEX,REAL:] is set
{} is set
the Function-like functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real V48() V49() V50() V51() V52() V53() V54() set is Function-like functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real V48() V49() V50() V51() V52() V53() V54() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
{{},1} is set
[:NAT,REAL:] is complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is set
0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
{0} is trivial V48() V49() V50() V51() V52() V53() set
[:NAT,NAT:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:NAT,NAT:] is set
p is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
g is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
g - h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
- h is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
K58(1) is V22() real ext-real set
K58(1) (#) h is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
g + (- h) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
y1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
p . y1 is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
- h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(- h) . y1 is V22() real ext-real Element of REAL
(g . y1) + ((- h) . y1) is V22() real ext-real Element of REAL
h . y1 is V22() real ext-real Element of REAL
- (h . y1) is V22() real ext-real Element of REAL
(g . y1) + (- (h . y1)) is V22() real ext-real Element of REAL
(g . y1) - (h . y1) is V22() real ext-real Element of REAL
y1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
p . y1 is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
h . y1 is V22() real ext-real Element of REAL
(g . y1) - (h . y1) is V22() real ext-real Element of REAL
y1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
p . y1 is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
h . y1 is V22() real ext-real Element of REAL
(g . y1) - (h . y1) is V22() real ext-real Element of REAL
- (h . y1) is V22() real ext-real Element of REAL
(g . y1) + (- (h . y1)) is V22() real ext-real Element of REAL
- h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(- h) . y1 is V22() real ext-real Element of REAL
(g . y1) + ((- h) . y1) is V22() real ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
g is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
p + g is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
p - g is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
- g is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
K58(1) is V22() real ext-real set
K58(1) (#) g is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
p + (- g) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
p (#) g is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
h is Relation-like NAT -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]
(p + g) * h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of p + g
p * h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of p
g * h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of g
(p * h) + (g * h) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(p - g) * h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of p - g
(p * h) - (g * h) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
- (g * h) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
K58(1) (#) (g * h) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(p * h) + (- (g * h)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(p (#) g) * h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of p (#) g
(p * h) (#) (g * h) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
y1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
((p + g) * h) . y1 is V22() real ext-real Element of REAL
h . y1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
(p + g) . (h . y1) is V22() real ext-real Element of REAL
p . (h . y1) is V22() real ext-real Element of REAL
g . (h . y1) is V22() real ext-real Element of REAL
(p . (h . y1)) + (g . (h . y1)) is V22() real ext-real Element of REAL
(p * h) . y1 is V22() real ext-real Element of REAL
((p * h) . y1) + (g . (h . y1)) is V22() real ext-real Element of REAL
(g * h) . y1 is V22() real ext-real Element of REAL
((p * h) . y1) + ((g * h) . y1) is V22() real ext-real Element of REAL
((p * h) + (g * h)) . y1 is V22() real ext-real Element of REAL
y1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
((p - g) * h) . y1 is V22() real ext-real Element of REAL
h . y1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
(p - g) . (h . y1) is V22() real ext-real Element of REAL
p . (h . y1) is V22() real ext-real Element of REAL
g . (h . y1) is V22() real ext-real Element of REAL
(p . (h . y1)) - (g . (h . y1)) is V22() real ext-real Element of REAL
(p * h) . y1 is V22() real ext-real Element of REAL
((p * h) . y1) - (g . (h . y1)) is V22() real ext-real Element of REAL
(g * h) . y1 is V22() real ext-real Element of REAL
((p * h) . y1) - ((g * h) . y1) is V22() real ext-real Element of REAL
((p * h) - (g * h)) . y1 is V22() real ext-real Element of REAL
y1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
((p (#) g) * h) . y1 is V22() real ext-real Element of REAL
h . y1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
(p (#) g) . (h . y1) is V22() real ext-real Element of REAL
p . (h . y1) is V22() real ext-real Element of REAL
g . (h . y1) is V22() real ext-real Element of REAL
(p . (h . y1)) * (g . (h . y1)) is V22() real ext-real Element of REAL
(p * h) . y1 is V22() real ext-real Element of REAL
((p * h) . y1) * (g . (h . y1)) is V22() real ext-real Element of REAL
(g * h) . y1 is V22() real ext-real Element of REAL
((p * h) . y1) * ((g * h) . y1) is V22() real ext-real Element of REAL
((p * h) (#) (g * h)) . y1 is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
g is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
p (#) g is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
h is Relation-like NAT -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]
(p (#) g) * h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of p (#) g
g * h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of g
p (#) (g * h) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
y1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
((p (#) g) * h) . y1 is V22() real ext-real Element of REAL
h . y1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
(p (#) g) . (h . y1) is V22() real ext-real Element of REAL
g . (h . y1) is V22() real ext-real Element of REAL
p * (g . (h . y1)) is V22() real ext-real Element of REAL
(g * h) . y1 is V22() real ext-real Element of REAL
p * ((g * h) . y1) is V22() real ext-real Element of REAL
(p (#) (g * h)) . y1 is V22() real ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
- p is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
K58(1) is V22() real ext-real set
K58(1) (#) p is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
abs p is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
g is Relation-like NAT -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]
(- p) * g is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of - p
p * g is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of p
- (p * g) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
K58(1) (#) (p * g) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(abs p) * g is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of abs p
abs (p * g) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
- 1 is V22() real ext-real Element of REAL
(- 1) (#) p is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
((- 1) (#) p) * g is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (- 1) (#) p
(- 1) (#) (p * g) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
((abs p) * g) . h is V22() real ext-real Element of REAL
g . h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
(abs p) . (g . h) is V22() real ext-real Element of REAL
p . (g . h) is V22() real ext-real Element of REAL
abs (p . (g . h)) is V22() real ext-real Element of REAL
(p * g) . h is V22() real ext-real Element of REAL
abs ((p * g) . h) is V22() real ext-real Element of REAL
(abs (p * g)) . h is V22() real ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
p " is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
g is Relation-like NAT -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]
p * g is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of p
(p * g) " is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(p ") * g is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of p "
h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
((p * g) ") . h is V22() real ext-real Element of REAL
(p * g) . h is V22() real ext-real Element of REAL
((p * g) . h) " is V22() real ext-real Element of REAL
g . h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
p . (g . h) is V22() real ext-real Element of REAL
(p . (g . h)) " is V22() real ext-real Element of REAL
(p ") . (g . h) is V22() real ext-real Element of REAL
((p ") * g) . h is V22() real ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
g is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
p /" g is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
g " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
p (#) (g ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
h is Relation-like NAT -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]
(p /" g) * h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of p /" g
p * h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of p
g * h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of g
(p * h) /" (g * h) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(g * h) " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(p * h) (#) ((g * h) ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
g " is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
p (#) (g ") is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(p (#) (g ")) * h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of p (#) (g ")
(g ") * h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of g "
(p * h) (#) ((g ") * h) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(g * h) " is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(p * h) (#) ((g * h) ") is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
p is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim p is V22() real ext-real Element of REAL
- p is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
K58(1) is V22() real ext-real set
K58(1) (#) p is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
(- p) . h is V22() real ext-real Element of REAL
p . h is V22() real ext-real Element of REAL
- (p . h) is V22() real ext-real Element of REAL
- 0 is V22() real ext-real Element of REAL
lim (- p) is V22() real ext-real Element of REAL
- (lim p) is V22() real ext-real Element of REAL
p is non empty set
[:p,REAL:] is complex-valued ext-real-valued real-valued set
bool [:p,REAL:] is set
[:NAT,p:] is set
bool [:NAT,p:] is set
g is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
dom g is Element of bool p
bool p is set
h is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
dom h is Element of bool p
(dom g) /\ (dom h) is Element of bool p
g + h is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
g - h is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
- h is Relation-like p -defined Function-like complex-valued ext-real-valued real-valued set
K58(1) is V22() real ext-real set
K58(1) (#) h is Relation-like p -defined Function-like complex-valued ext-real-valued real-valued set
g + (- h) is Relation-like p -defined Function-like complex-valued ext-real-valued real-valued set
g (#) h is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
y1 is Relation-like NAT -defined p -valued Function-like non empty total quasi_total Element of bool [:NAT,p:]
rng y1 is Element of bool p
(g + h) /* y1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
g /* y1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
h /* y1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(g /* y1) + (h /* y1) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(g - h) /* y1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(g /* y1) - (h /* y1) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
- (h /* y1) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
K58(1) (#) (h /* y1) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(g /* y1) + (- (h /* y1)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(g (#) h) /* y1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(g /* y1) (#) (h /* y1) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
dom (g + h) is Element of bool p
y2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
y1 . y2 is Element of p
((g + h) /* y1) . y2 is V22() real ext-real Element of REAL
(g + h) . (y1 . y2) is V22() real ext-real Element of REAL
g . (y1 . y2) is V22() real ext-real Element of REAL
h . (y1 . y2) is V22() real ext-real Element of REAL
(g . (y1 . y2)) + (h . (y1 . y2)) is V22() real ext-real Element of REAL
(g /* y1) . y2 is V22() real ext-real Element of REAL
((g /* y1) . y2) + (h . (y1 . y2)) is V22() real ext-real Element of REAL
(h /* y1) . y2 is V22() real ext-real Element of REAL
((g /* y1) . y2) + ((h /* y1) . y2) is V22() real ext-real Element of REAL
dom (g - h) is Element of bool p
y2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
y1 . y2 is Element of p
((g - h) /* y1) . y2 is V22() real ext-real Element of REAL
(g - h) . (y1 . y2) is V22() real ext-real Element of REAL
g . (y1 . y2) is V22() real ext-real Element of REAL
h . (y1 . y2) is V22() real ext-real Element of REAL
(g . (y1 . y2)) - (h . (y1 . y2)) is V22() real ext-real Element of REAL
(g /* y1) . y2 is V22() real ext-real Element of REAL
((g /* y1) . y2) - (h . (y1 . y2)) is V22() real ext-real Element of REAL
(h /* y1) . y2 is V22() real ext-real Element of REAL
((g /* y1) . y2) - ((h /* y1) . y2) is V22() real ext-real Element of REAL
dom (g (#) h) is Element of bool p
y2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
((g (#) h) /* y1) . y2 is V22() real ext-real Element of REAL
y1 . y2 is Element of p
(g (#) h) . (y1 . y2) is V22() real ext-real Element of REAL
g . (y1 . y2) is V22() real ext-real Element of REAL
h . (y1 . y2) is V22() real ext-real Element of REAL
(g . (y1 . y2)) * (h . (y1 . y2)) is V22() real ext-real Element of REAL
(g /* y1) . y2 is V22() real ext-real Element of REAL
((g /* y1) . y2) * (h . (y1 . y2)) is V22() real ext-real Element of REAL
(h /* y1) . y2 is V22() real ext-real Element of REAL
((g /* y1) . y2) * ((h /* y1) . y2) is V22() real ext-real Element of REAL
p is non empty set
[:p,REAL:] is complex-valued ext-real-valued real-valued set
bool [:p,REAL:] is set
[:NAT,p:] is set
bool [:NAT,p:] is set
g is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
dom g is Element of bool p
bool p is set
h is Relation-like NAT -defined p -valued Function-like non empty total quasi_total Element of bool [:NAT,p:]
rng h is Element of bool p
g /* h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
y1 is V22() real ext-real set
y1 (#) g is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
(y1 (#) g) /* h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
y1 (#) (g /* h) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
dom (y1 (#) g) is Element of bool p
y2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
h . y2 is Element of p
((y1 (#) g) /* h) . y2 is V22() real ext-real Element of REAL
(y1 (#) g) . (h . y2) is V22() real ext-real Element of REAL
g . (h . y2) is V22() real ext-real Element of REAL
y1 * (g . (h . y2)) is V22() real ext-real Element of REAL
(g /* h) . y2 is V22() real ext-real Element of REAL
y1 * ((g /* h) . y2) is V22() real ext-real Element of REAL
p is non empty set
[:p,REAL:] is complex-valued ext-real-valued real-valued set
bool [:p,REAL:] is set
[:NAT,p:] is set
bool [:NAT,p:] is set
g is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
dom g is Element of bool p
bool p is set
abs g is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
- g is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
K58(1) is V22() real ext-real set
K58(1) (#) g is Relation-like p -defined Function-like complex-valued ext-real-valued real-valued set
h is Relation-like NAT -defined p -valued Function-like non empty total quasi_total Element of bool [:NAT,p:]
rng h is Element of bool p
g /* h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
abs (g /* h) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(abs g) /* h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
- (g /* h) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
K58(1) (#) (g /* h) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- g) /* h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
dom (abs g) is Element of bool p
y1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
(abs (g /* h)) . y1 is V22() real ext-real Element of REAL
(g /* h) . y1 is V22() real ext-real Element of REAL
abs ((g /* h) . y1) is V22() real ext-real Element of REAL
h . y1 is Element of p
g . (h . y1) is V22() real ext-real Element of REAL
abs (g . (h . y1)) is V22() real ext-real Element of REAL
(abs g) . (h . y1) is V22() real ext-real Element of REAL
((abs g) /* h) . y1 is V22() real ext-real Element of REAL
- 1 is V22() real ext-real Element of REAL
(- 1) (#) (g /* h) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(- 1) (#) g is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
((- 1) (#) g) /* h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
p is non empty set
[:p,REAL:] is complex-valued ext-real-valued real-valued set
bool [:p,REAL:] is set
[:NAT,p:] is set
bool [:NAT,p:] is set
g is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
g ^ is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
dom (g ^) is Element of bool p
bool p is set
h is Relation-like NAT -defined p -valued Function-like non empty total quasi_total Element of bool [:NAT,p:]
rng h is Element of bool p
g /* h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
dom g is Element of bool p
{0} is trivial V48() V49() V50() V51() V52() V53() Element of bool REAL
g " {0} is Element of bool p
(dom g) \ (g " {0}) is Element of bool p
y1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
(g /* h) . y1 is V22() real ext-real Element of REAL
h . y1 is Element of p
g . (h . y1) is V22() real ext-real Element of REAL
p is non empty set
[:p,REAL:] is complex-valued ext-real-valued real-valued set
bool [:p,REAL:] is set
[:NAT,p:] is set
bool [:NAT,p:] is set
g is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
g ^ is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
dom (g ^) is Element of bool p
bool p is set
h is Relation-like NAT -defined p -valued Function-like non empty total quasi_total Element of bool [:NAT,p:]
rng h is Element of bool p
(g ^) /* h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
g /* h is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(g /* h) " is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
dom g is Element of bool p
{0} is trivial V48() V49() V50() V51() V52() V53() Element of bool REAL
g " {0} is Element of bool p
(dom g) \ (g " {0}) is Element of bool p
y1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
h . y1 is Element of p
((g ^) /* h) . y1 is V22() real ext-real Element of REAL
(g ^) . (h . y1) is V22() real ext-real Element of REAL
g . (h . y1) is V22() real ext-real Element of REAL
(g . (h . y1)) " is V22() real ext-real Element of REAL
(g /* h) . y1 is V22() real ext-real Element of REAL
((g /* h) . y1) " is V22() real ext-real Element of REAL
((g /* h) ") . y1 is V22() real ext-real Element of REAL
p is non empty set
[:p,REAL:] is complex-valued ext-real-valued real-valued set
bool [:p,REAL:] is set
[:NAT,p:] is set
bool [:NAT,p:] is set
g is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
h is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
g + h is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
g - h is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
- h is Relation-like p -defined Function-like complex-valued ext-real-valued real-valued set
K58(1) is V22() real ext-real set
K58(1) (#) h is Relation-like p -defined Function-like complex-valued ext-real-valued real-valued set
g + (- h) is Relation-like p -defined Function-like complex-valued ext-real-valued real-valued set
g (#) h is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
y1 is Relation-like NAT -defined p -valued Function-like non empty total quasi_total Element of bool [:NAT,p:]
(g + h) /* y1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
g /* y1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
h /* y1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(g /* y1) + (h /* y1) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(g - h) /* y1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(g /* y1) - (h /* y1) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
- (h /* y1) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
K58(1) (#) (h /* y1) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(g /* y1) + (- (h /* y1)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(g (#) h) /* y1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(g /* y1) (#) (h /* y1) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
dom (g + h) is Element of bool p
bool p is set
dom g is Element of bool p
dom h is Element of bool p
(dom g) /\ (dom h) is Element of bool p
rng y1 is Element of bool p
p is V22() real ext-real Element of REAL
g is non empty set
[:g,REAL:] is complex-valued ext-real-valued real-valued set
bool [:g,REAL:] is set
[:NAT,g:] is set
bool [:NAT,g:] is set
h is Relation-like g -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:g,REAL:]
p (#) h is Relation-like g -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:g,REAL:]
y1 is Relation-like NAT -defined g -valued Function-like non empty total quasi_total Element of bool [:NAT,g:]
(p (#) h) /* y1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
h /* y1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
p (#) (h /* y1) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
dom h is Element of bool g
bool g is set
rng y1 is Element of bool g
p is set
g is non empty set
[:g,REAL:] is complex-valued ext-real-valued real-valued set
bool [:g,REAL:] is set
[:NAT,g:] is set
bool [:NAT,g:] is set
h is Relation-like g -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:g,REAL:]
h | p is Relation-like g -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:g,REAL:]
dom (h | p) is Element of bool g
bool g is set
abs h is Relation-like g -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:g,REAL:]
(abs h) | p is Relation-like g -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:g,REAL:]
y1 is Relation-like NAT -defined g -valued Function-like non empty total quasi_total Element of bool [:NAT,g:]
rng y1 is Element of bool g
(h | p) /* y1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
abs ((h | p) /* y1) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
((abs h) | p) /* y1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
dom h is Element of bool g
(dom h) /\ p is Element of bool g
dom (abs h) is Element of bool g
(dom (abs h)) /\ p is Element of bool g
dom ((abs h) | p) is Element of bool g
y2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
y1 . y2 is Element of g
(abs ((h | p) /* y1)) . y2 is V22() real ext-real Element of REAL
((h | p) /* y1) . y2 is V22() real ext-real Element of REAL
abs (((h | p) /* y1) . y2) is V22() real ext-real Element of REAL
(h | p) . (y1 . y2) is V22() real ext-real Element of REAL
abs ((h | p) . (y1 . y2)) is V22() real ext-real Element of REAL
h . (y1 . y2) is V22() real ext-real Element of REAL
abs (h . (y1 . y2)) is V22() real ext-real Element of REAL
(abs h) . (y1 . y2) is V22() real ext-real Element of REAL
((abs h) | p) . (y1 . y2) is V22() real ext-real Element of REAL
(((abs h) | p) /* y1) . y2 is V22() real ext-real Element of REAL
{0} is trivial V48() V49() V50() V51() V52() V53() Element of bool REAL
p is set
g is non empty set
[:g,REAL:] is complex-valued ext-real-valued real-valued set
bool [:g,REAL:] is set
[:NAT,g:] is set
bool [:NAT,g:] is set
h is Relation-like g -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:g,REAL:]
h | p is Relation-like g -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:g,REAL:]
dom (h | p) is Element of bool g
bool g is set
h " {0} is Element of bool g
h ^ is Relation-like g -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:g,REAL:]
(h ^) | p is Relation-like g -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:g,REAL:]
y1 is Relation-like NAT -defined g -valued Function-like non empty total quasi_total Element of bool [:NAT,g:]
rng y1 is Element of bool g
((h ^) | p) /* y1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(h | p) /* y1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
((h | p) /* y1) " is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
y2 is set
dom h is Element of bool g
(dom h) /\ p is Element of bool g
(dom h) \ (h " {0}) is Element of bool g
dom (h ^) is Element of bool g
(dom (h ^)) /\ p is Element of bool g
dom ((h ^) | p) is Element of bool g
y2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() Element of NAT
y1 . y2 is Element of g
(((h ^) | p) /* y1) . y2 is V22() real ext-real Element of REAL
((h ^) | p) . (y1 . y2) is V22() real ext-real Element of REAL
(h ^) . (y1 . y2) is V22() real ext-real Element of REAL
h . (y1 . y2) is V22() real ext-real Element of REAL
(h . (y1 . y2)) " is V22() real ext-real Element of REAL
(h | p) . (y1 . y2) is V22() real ext-real Element of REAL
((h | p) . (y1 . y2)) " is V22() real ext-real Element of REAL
((h | p) /* y1) . y2 is V22() real ext-real Element of REAL
(((h | p) /* y1) . y2) " is V22() real ext-real Element of REAL
(((h | p) /* y1) ") . y2 is V22() real ext-real Element of REAL
g is Relation-like Function-like one-to-one set
p is set
g | p is Relation-like Function-like set
p is set
g is Relation-like Function-like one-to-one set
g | p is Relation-like Function-like one-to-one set
(g | p) " is Relation-like Function-like one-to-one set
g " is Relation-like Function-like one-to-one set
g .: p is set
(g ") | (g .: p) is Relation-like Function-like one-to-one set
y1 is set
dom ((g | p) ") is set
dom ((g ") | (g .: p)) is set
h is Relation-like Function-like one-to-one set
rng h is set
dom (g | p) is set
y2 is set
(g | p) . y2 is set
g . y2 is set
dom g is set
(dom g) /\ p is set
rng g is set
dom (g ") is set
(dom (g ")) /\ (g .: p) is set
dom (g ") is set
(dom (g ")) /\ (g .: p) is set
dom g is set
y2 is set
g . y2 is set
(dom g) /\ p is set
dom (g | p) is set
(g | p) . y2 is set
h is Relation-like Function-like one-to-one set
rng h is set
h " is Relation-like Function-like one-to-one set
dom (h ") is set
y1 is set
((g | p) ") . y1 is set
((g ") | (g .: p)) . y1 is set
y2 is set
g . y2 is set
r2 is set
(g | p) . r2 is set
g . r2 is set
(h ") . y1 is set
(g ") . y1 is set
(g ") . (g . y2) is set
p is non empty set
[:p,REAL:] is complex-valued ext-real-valued real-valued set
bool [:p,REAL:] is set
g is Relation-like p -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:p,REAL:]
rng g is V48() V49() V50() Element of bool REAL
upper_bound (rng g) is V22() real ext-real Element of REAL
lower_bound (rng g) is V22() real ext-real Element of REAL
dom g is Element of bool p
bool p is set
h is set
y1 is set
g . h is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
p is set
g is non empty set
[:g,REAL:] is complex-valued ext-real-valued real-valued set
bool [:g,REAL:] is set
h is Relation-like g -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:g,REAL:]
h .: p is V48() V49() V50() Element of bool REAL
upper_bound (h .: p) is V22() real ext-real Element of REAL
lower_bound (h .: p) is V22() real ext-real Element of REAL
h | p is Relation-like g -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:g,REAL:]
rng (h | p) is V48() V49() V50() Element of bool REAL
[:REAL,REAL:] is complex-valued ext-real-valued real-valued set
bool [:REAL,REAL:] is set
p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom p is V48() V49() V50() Element of bool REAL
g is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
p . h is V22() real ext-real Element of REAL
p . g is V22() real ext-real Element of REAL
g is ext-real set
dom p is set
p . g is V22() real ext-real set
h is ext-real set
p . h is V22() real ext-real set
g is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
p . g is V22() real ext-real Element of REAL
p . h is V22() real ext-real Element of REAL
g is ext-real set
dom p is set
p . g is V22() real ext-real set
h is ext-real set
p . h is V22() real ext-real set
g is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
p . g is V22() real ext-real Element of REAL
p . h is V22() real ext-real Element of REAL
g is ext-real set
dom p is set
p . g is V22() real ext-real set
h is ext-real set
p . h is V22() real ext-real set
g is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
p . h is V22() real ext-real Element of REAL
p . g is V22() real ext-real Element of REAL
g is ext-real set
dom p is set
p . g is V22() real ext-real set
h is ext-real set
p . h is V22() real ext-real set
p is set
g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom g is V48() V49() V50() Element of bool REAL
p /\ (dom g) is V48() V49() V50() Element of bool REAL
h is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
dom (g | p) is V48() V49() V50() Element of bool REAL
(g | p) . y1 is V22() real ext-real Element of REAL
(g | p) . h is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
dom (g | p) is V48() V49() V50() Element of bool REAL
(g | p) . h is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
(g | p) . y1 is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
p is set
g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom g is V48() V49() V50() Element of bool REAL
p /\ (dom g) is V48() V49() V50() Element of bool REAL
h is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
dom (g | p) is V48() V49() V50() Element of bool REAL
(g | p) . y1 is V22() real ext-real Element of REAL
(g | p) . h is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
dom (g | p) is V48() V49() V50() Element of bool REAL
(g | p) . h is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
(g | p) . y1 is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
p is set
g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom g is V48() V49() V50() Element of bool REAL
p /\ (dom g) is V48() V49() V50() Element of bool REAL
h is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
dom (g | p) is V48() V49() V50() Element of bool REAL
(g | p) . y1 is V22() real ext-real Element of REAL
(g | p) . h is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
dom (g | p) is V48() V49() V50() Element of bool REAL
(g | p) . h is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
(g | p) . y1 is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
p is set
g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom g is V48() V49() V50() Element of bool REAL
p /\ (dom g) is V48() V49() V50() Element of bool REAL
h is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
dom (g | p) is V48() V49() V50() Element of bool REAL
(g | p) . y1 is V22() real ext-real Element of REAL
(g | p) . h is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
dom (g | p) is V48() V49() V50() Element of bool REAL
(g | p) . h is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
(g | p) . y1 is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
p is set
g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom g is V48() V49() V50() Element of bool REAL
p /\ (dom g) is V48() V49() V50() Element of bool REAL
h is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
dom (g | p) is V48() V49() V50() Element of bool REAL
(g | p) . h is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
(g | p) . y1 is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
p is set
g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom g is V48() V49() V50() Element of bool REAL
p /\ (dom g) is V48() V49() V50() Element of bool REAL
h is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
dom (g | p) is V48() V49() V50() Element of bool REAL
(g | p) . h is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
(g | p) . y1 is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g is set
dom p is set
h is set
p . g is V22() real ext-real set
p . h is V22() real ext-real set
dom p is V48() V49() V50() Element of bool REAL
y2 is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
p . y1 is V22() real ext-real Element of REAL
p . y2 is V22() real ext-real Element of REAL
p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g is V22() real ext-real Element of REAL
dom p is V48() V49() V50() Element of bool REAL
p . g is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
p . h is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
dom p is V48() V49() V50() Element of bool REAL
p . g is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
p . h is V22() real ext-real Element of REAL
p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued increasing non-decreasing () Element of bool [:REAL,REAL:]
g is set
p | g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h is V22() real ext-real Element of REAL
dom (p | g) is V48() V49() V50() Element of bool REAL
y1 is V22() real ext-real Element of REAL
p . h is V22() real ext-real Element of REAL
(p | g) . h is V22() real ext-real Element of REAL
p . y1 is V22() real ext-real Element of REAL
(p | g) . y1 is V22() real ext-real Element of REAL
dom p is V48() V49() V50() Element of bool REAL
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued decreasing non-increasing () Element of bool [:REAL,REAL:]
g is set
p | g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h is V22() real ext-real Element of REAL
dom (p | g) is V48() V49() V50() Element of bool REAL
y1 is V22() real ext-real Element of REAL
p . h is V22() real ext-real Element of REAL
(p | g) . h is V22() real ext-real Element of REAL
p . y1 is V22() real ext-real Element of REAL
(p | g) . y1 is V22() real ext-real Element of REAL
dom p is V48() V49() V50() Element of bool REAL
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued non-decreasing () Element of bool [:REAL,REAL:]
g is set
p | g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h is V22() real ext-real Element of REAL
dom (p | g) is V48() V49() V50() Element of bool REAL
y1 is V22() real ext-real Element of REAL
p . h is V22() real ext-real Element of REAL
(p | g) . h is V22() real ext-real Element of REAL
p . y1 is V22() real ext-real Element of REAL
(p | g) . y1 is V22() real ext-real Element of REAL
dom p is V48() V49() V50() Element of bool REAL
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
p is set
g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom g is V48() V49() V50() Element of bool REAL
g | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
p /\ (dom g) is V48() V49() V50() Element of bool REAL
h is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
p is set
g is set
p /\ g is set
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | (p /\ g) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom h is V48() V49() V50() Element of bool REAL
(p /\ g) /\ (dom h) is V48() V49() V50() Element of bool REAL
dom h is V48() V49() V50() Element of bool REAL
(p /\ g) /\ (dom h) is V48() V49() V50() Element of bool REAL
the V22() real ext-real Element of (p /\ g) /\ (dom h) is V22() real ext-real Element of (p /\ g) /\ (dom h)
y2 is V22() real ext-real Element of REAL
h . y2 is V22() real ext-real Element of REAL
r2 is V22() real ext-real Element of REAL
g /\ (dom h) is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
h . r2 is V22() real ext-real Element of REAL
h . r2 is V22() real ext-real Element of REAL
h . r2 is V22() real ext-real Element of REAL
h . r2 is V22() real ext-real Element of REAL
r2 is V22() real ext-real Element of REAL
r2 is V22() real ext-real Element of REAL
h . r2 is V22() real ext-real Element of REAL
r2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
(p /\ g) /\ (dom h) is V48() V49() V50() Element of bool REAL
p is set
g is set
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom h is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
g /\ (dom h) is V48() V49() V50() Element of bool REAL
y1 is V22() real ext-real Element of REAL
y2 is V22() real ext-real Element of REAL
h . y2 is V22() real ext-real Element of REAL
h . y1 is V22() real ext-real Element of REAL
p is set
g is set
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom h is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
g /\ (dom h) is V48() V49() V50() Element of bool REAL
y1 is V22() real ext-real Element of REAL
y2 is V22() real ext-real Element of REAL
h . y1 is V22() real ext-real Element of REAL
h . y2 is V22() real ext-real Element of REAL
p is set
g is set
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom h is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
g /\ (dom h) is V48() V49() V50() Element of bool REAL
y1 is V22() real ext-real Element of REAL
y2 is V22() real ext-real Element of REAL
h . y1 is V22() real ext-real Element of REAL
h . y2 is V22() real ext-real Element of REAL
p is set
g is set
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom h is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
g /\ (dom h) is V48() V49() V50() Element of bool REAL
y1 is V22() real ext-real Element of REAL
y2 is V22() real ext-real Element of REAL
h . y2 is V22() real ext-real Element of REAL
h . y1 is V22() real ext-real Element of REAL
p is set
g is V22() real ext-real Element of REAL
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g (#) h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(g (#) h) | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 is V22() real ext-real Element of REAL
dom (g (#) h) is V48() V49() V50() Element of bool REAL
p /\ (dom (g (#) h)) is V48() V49() V50() Element of bool REAL
y2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
h . y2 is V22() real ext-real Element of REAL
h . y1 is V22() real ext-real Element of REAL
g * (h . y2) is V22() real ext-real Element of REAL
g * (h . y1) is V22() real ext-real Element of REAL
(g (#) h) . y1 is V22() real ext-real Element of REAL
(g (#) h) . y2 is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
dom (g (#) h) is V48() V49() V50() Element of bool REAL
p /\ (dom (g (#) h)) is V48() V49() V50() Element of bool REAL
h . y1 is V22() real ext-real Element of REAL
g * (h . y1) is V22() real ext-real Element of REAL
(g (#) h) . y1 is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
dom (g (#) h) is V48() V49() V50() Element of bool REAL
p /\ (dom (g (#) h)) is V48() V49() V50() Element of bool REAL
y2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
h . y2 is V22() real ext-real Element of REAL
h . y1 is V22() real ext-real Element of REAL
g * (h . y1) is V22() real ext-real Element of REAL
g * (h . y2) is V22() real ext-real Element of REAL
(g (#) h) . y2 is V22() real ext-real Element of REAL
(g (#) h) . y1 is V22() real ext-real Element of REAL
p is set
g is V22() real ext-real Element of REAL
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g (#) h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(g (#) h) | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 is V22() real ext-real Element of REAL
dom (g (#) h) is V48() V49() V50() Element of bool REAL
p /\ (dom (g (#) h)) is V48() V49() V50() Element of bool REAL
y2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
h . y1 is V22() real ext-real Element of REAL
h . y2 is V22() real ext-real Element of REAL
g * (h . y1) is V22() real ext-real Element of REAL
g * (h . y2) is V22() real ext-real Element of REAL
(g (#) h) . y2 is V22() real ext-real Element of REAL
(g (#) h) . y1 is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
dom (g (#) h) is V48() V49() V50() Element of bool REAL
p /\ (dom (g (#) h)) is V48() V49() V50() Element of bool REAL
y2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
h . y1 is V22() real ext-real Element of REAL
h . y2 is V22() real ext-real Element of REAL
g * (h . y2) is V22() real ext-real Element of REAL
g * (h . y1) is V22() real ext-real Element of REAL
(g (#) h) . y1 is V22() real ext-real Element of REAL
(g (#) h) . y2 is V22() real ext-real Element of REAL
p is set
g is V22() real ext-real Element of REAL
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g (#) h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(g (#) h) | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 is V22() real ext-real Element of REAL
dom (g (#) h) is V48() V49() V50() Element of bool REAL
p /\ (dom (g (#) h)) is V48() V49() V50() Element of bool REAL
y2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
h . y1 is V22() real ext-real Element of REAL
h . y2 is V22() real ext-real Element of REAL
g * (h . y1) is V22() real ext-real Element of REAL
(h . y2) * g is V22() real ext-real Element of REAL
(g (#) h) . y1 is V22() real ext-real Element of REAL
g * (h . y2) is V22() real ext-real Element of REAL
(g (#) h) . y2 is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
dom (g (#) h) is V48() V49() V50() Element of bool REAL
p /\ (dom (g (#) h)) is V48() V49() V50() Element of bool REAL
y2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
h . y1 is V22() real ext-real Element of REAL
h . y2 is V22() real ext-real Element of REAL
g * (h . y2) is V22() real ext-real Element of REAL
g * (h . y1) is V22() real ext-real Element of REAL
(g (#) h) . y2 is V22() real ext-real Element of REAL
(g (#) h) . y1 is V22() real ext-real Element of REAL
p is set
g is V22() real ext-real Element of REAL
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g (#) h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(g (#) h) | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 is V22() real ext-real Element of REAL
dom (g (#) h) is V48() V49() V50() Element of bool REAL
p /\ (dom (g (#) h)) is V48() V49() V50() Element of bool REAL
y2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
h . y2 is V22() real ext-real Element of REAL
h . y1 is V22() real ext-real Element of REAL
g * (h . y2) is V22() real ext-real Element of REAL
(h . y1) * g is V22() real ext-real Element of REAL
(g (#) h) . y2 is V22() real ext-real Element of REAL
g * (h . y1) is V22() real ext-real Element of REAL
(g (#) h) . y1 is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
dom (g (#) h) is V48() V49() V50() Element of bool REAL
p /\ (dom (g (#) h)) is V48() V49() V50() Element of bool REAL
y2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
h . y2 is V22() real ext-real Element of REAL
h . y1 is V22() real ext-real Element of REAL
g * (h . y1) is V22() real ext-real Element of REAL
g * (h . y2) is V22() real ext-real Element of REAL
(g (#) h) . y1 is V22() real ext-real Element of REAL
(g (#) h) . y2 is V22() real ext-real Element of REAL
p is set
g is set
p /\ g is set
h is V22() real ext-real Element of REAL
y1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom y1 is V48() V49() V50() Element of bool REAL
p /\ (dom y1) is V48() V49() V50() Element of bool REAL
y2 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 + y2 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (y1 + y2) is V48() V49() V50() Element of bool REAL
(p /\ g) /\ (dom (y1 + y2)) is V48() V49() V50() Element of bool REAL
dom y2 is V48() V49() V50() Element of bool REAL
g /\ (dom y2) is V48() V49() V50() Element of bool REAL
(dom y1) /\ (dom y2) is V48() V49() V50() Element of bool REAL
p is set
g is set
p /\ g is set
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 | g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h + y1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(h + y1) | (p /\ g) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y2 is V22() real ext-real Element of REAL
dom (h + y1) is V48() V49() V50() Element of bool REAL
(p /\ g) /\ (dom (h + y1)) is V48() V49() V50() Element of bool REAL
r2 is V22() real ext-real Element of REAL
dom y1 is V48() V49() V50() Element of bool REAL
g /\ (dom y1) is V48() V49() V50() Element of bool REAL
y1 . r2 is V22() real ext-real Element of REAL
y1 . y2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
h . r2 is V22() real ext-real Element of REAL
h . y2 is V22() real ext-real Element of REAL
(h . r2) + (y1 . r2) is V22() real ext-real Element of REAL
(h . y2) + (y1 . y2) is V22() real ext-real Element of REAL
(h + y1) . y2 is V22() real ext-real Element of REAL
(h + y1) . r2 is V22() real ext-real Element of REAL
y2 is V22() real ext-real Element of REAL
dom (h + y1) is V48() V49() V50() Element of bool REAL
(p /\ g) /\ (dom (h + y1)) is V48() V49() V50() Element of bool REAL
r2 is V22() real ext-real Element of REAL
dom y1 is V48() V49() V50() Element of bool REAL
g /\ (dom y1) is V48() V49() V50() Element of bool REAL
y1 . y2 is V22() real ext-real Element of REAL
y1 . r2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
h . y2 is V22() real ext-real Element of REAL
h . r2 is V22() real ext-real Element of REAL
(h . y2) + (y1 . y2) is V22() real ext-real Element of REAL
(h . r2) + (y1 . r2) is V22() real ext-real Element of REAL
(h + y1) . r2 is V22() real ext-real Element of REAL
(h + y1) . y2 is V22() real ext-real Element of REAL
y2 is V22() real ext-real Element of REAL
dom (h + y1) is V48() V49() V50() Element of bool REAL
(p /\ g) /\ (dom (h + y1)) is V48() V49() V50() Element of bool REAL
r2 is V22() real ext-real Element of REAL
dom y1 is V48() V49() V50() Element of bool REAL
g /\ (dom y1) is V48() V49() V50() Element of bool REAL
y1 . y2 is V22() real ext-real Element of REAL
y1 . r2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
h . y2 is V22() real ext-real Element of REAL
h . r2 is V22() real ext-real Element of REAL
(h . y2) + (y1 . y2) is V22() real ext-real Element of REAL
(h . r2) + (y1 . r2) is V22() real ext-real Element of REAL
(h + y1) . y2 is V22() real ext-real Element of REAL
(h + y1) . r2 is V22() real ext-real Element of REAL
y2 is V22() real ext-real Element of REAL
dom (h + y1) is V48() V49() V50() Element of bool REAL
(p /\ g) /\ (dom (h + y1)) is V48() V49() V50() Element of bool REAL
r2 is V22() real ext-real Element of REAL
dom y1 is V48() V49() V50() Element of bool REAL
g /\ (dom y1) is V48() V49() V50() Element of bool REAL
y1 . r2 is V22() real ext-real Element of REAL
y1 . y2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
h . r2 is V22() real ext-real Element of REAL
h . y2 is V22() real ext-real Element of REAL
(h . r2) + (y1 . r2) is V22() real ext-real Element of REAL
(h . y2) + (y1 . y2) is V22() real ext-real Element of REAL
(h + y1) . r2 is V22() real ext-real Element of REAL
(h + y1) . y2 is V22() real ext-real Element of REAL
p is set
g is set
p /\ g is set
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 | g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h + y1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(h + y1) | (p /\ g) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom y1 is V48() V49() V50() Element of bool REAL
g /\ (dom y1) is V48() V49() V50() Element of bool REAL
y2 is V22() real ext-real Element of REAL
r2 is V22() real ext-real Element of REAL
dom (h + y1) is V48() V49() V50() Element of bool REAL
(p /\ g) /\ (dom (h + y1)) is V48() V49() V50() Element of bool REAL
r2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
h . r2 is V22() real ext-real Element of REAL
h . r2 is V22() real ext-real Element of REAL
(h . r2) + y2 is V22() real ext-real Element of REAL
(h . r2) + y2 is V22() real ext-real Element of REAL
y1 . r2 is V22() real ext-real Element of REAL
(h . r2) + (y1 . r2) is V22() real ext-real Element of REAL
y1 . r2 is V22() real ext-real Element of REAL
(h . r2) + (y1 . r2) is V22() real ext-real Element of REAL
(h + y1) . r2 is V22() real ext-real Element of REAL
(h + y1) . r2 is V22() real ext-real Element of REAL
dom y1 is V48() V49() V50() Element of bool REAL
g /\ (dom y1) is V48() V49() V50() Element of bool REAL
y2 is V22() real ext-real Element of REAL
r2 is V22() real ext-real Element of REAL
dom (h + y1) is V48() V49() V50() Element of bool REAL
(p /\ g) /\ (dom (h + y1)) is V48() V49() V50() Element of bool REAL
r2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
h . r2 is V22() real ext-real Element of REAL
h . r2 is V22() real ext-real Element of REAL
(h . r2) + y2 is V22() real ext-real Element of REAL
(h . r2) + y2 is V22() real ext-real Element of REAL
y1 . r2 is V22() real ext-real Element of REAL
(h . r2) + (y1 . r2) is V22() real ext-real Element of REAL
y1 . r2 is V22() real ext-real Element of REAL
(h . r2) + (y1 . r2) is V22() real ext-real Element of REAL
(h + y1) . r2 is V22() real ext-real Element of REAL
(h + y1) . r2 is V22() real ext-real Element of REAL
p is set
g is set
p /\ g is set
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 | g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h + y1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(h + y1) | (p /\ g) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y2 is V22() real ext-real Element of REAL
dom (h + y1) is V48() V49() V50() Element of bool REAL
(p /\ g) /\ (dom (h + y1)) is V48() V49() V50() Element of bool REAL
r2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
dom y1 is V48() V49() V50() Element of bool REAL
(dom h) /\ (dom y1) is V48() V49() V50() Element of bool REAL
g /\ (dom y1) is V48() V49() V50() Element of bool REAL
y1 . y2 is V22() real ext-real Element of REAL
y1 . r2 is V22() real ext-real Element of REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
h . r2 is V22() real ext-real Element of REAL
h . y2 is V22() real ext-real Element of REAL
(h . r2) + (y1 . r2) is V22() real ext-real Element of REAL
(h . y2) + (y1 . y2) is V22() real ext-real Element of REAL
(h + y1) . y2 is V22() real ext-real Element of REAL
(h + y1) . r2 is V22() real ext-real Element of REAL
p is set
g is set
p /\ g is set
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 | g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h + y1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(h + y1) | (p /\ g) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y2 is V22() real ext-real Element of REAL
dom (h + y1) is V48() V49() V50() Element of bool REAL
(p /\ g) /\ (dom (h + y1)) is V48() V49() V50() Element of bool REAL
r2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
dom y1 is V48() V49() V50() Element of bool REAL
(dom h) /\ (dom y1) is V48() V49() V50() Element of bool REAL
g /\ (dom y1) is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
y1 . r2 is V22() real ext-real Element of REAL
y1 . y2 is V22() real ext-real Element of REAL
h . r2 is V22() real ext-real Element of REAL
h . y2 is V22() real ext-real Element of REAL
(h . r2) + (y1 . r2) is V22() real ext-real Element of REAL
(h . y2) + (y1 . y2) is V22() real ext-real Element of REAL
(h + y1) . r2 is V22() real ext-real Element of REAL
(h + y1) . y2 is V22() real ext-real Element of REAL
p is set
g is set
p /\ g is set
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 | g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h + y1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(h + y1) | (p /\ g) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y2 is V22() real ext-real Element of REAL
dom (h + y1) is V48() V49() V50() Element of bool REAL
(p /\ g) /\ (dom (h + y1)) is V48() V49() V50() Element of bool REAL
r2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
dom y1 is V48() V49() V50() Element of bool REAL
(dom h) /\ (dom y1) is V48() V49() V50() Element of bool REAL
g /\ (dom y1) is V48() V49() V50() Element of bool REAL
y1 . r2 is V22() real ext-real Element of REAL
y1 . y2 is V22() real ext-real Element of REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
h . y2 is V22() real ext-real Element of REAL
h . r2 is V22() real ext-real Element of REAL
(h . y2) + (y1 . y2) is V22() real ext-real Element of REAL
(h . r2) + (y1 . r2) is V22() real ext-real Element of REAL
(h + y1) . r2 is V22() real ext-real Element of REAL
(h + y1) . y2 is V22() real ext-real Element of REAL
p is set
g is set
p /\ g is set
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 | g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h + y1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(h + y1) | (p /\ g) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y2 is V22() real ext-real Element of REAL
dom (h + y1) is V48() V49() V50() Element of bool REAL
(p /\ g) /\ (dom (h + y1)) is V48() V49() V50() Element of bool REAL
r2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
dom y1 is V48() V49() V50() Element of bool REAL
(dom h) /\ (dom y1) is V48() V49() V50() Element of bool REAL
g /\ (dom y1) is V48() V49() V50() Element of bool REAL
p /\ (dom h) is V48() V49() V50() Element of bool REAL
y1 . r2 is V22() real ext-real Element of REAL
y1 . y2 is V22() real ext-real Element of REAL
h . y2 is V22() real ext-real Element of REAL
h . r2 is V22() real ext-real Element of REAL
(h . y2) + (y1 . y2) is V22() real ext-real Element of REAL
(h . r2) + (y1 . r2) is V22() real ext-real Element of REAL
(h + y1) . y2 is V22() real ext-real Element of REAL
(h + y1) . r2 is V22() real ext-real Element of REAL
p is set
{p} is trivial set
g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g | {p} is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h is V22() real ext-real Element of REAL
dom g is V48() V49() V50() Element of bool REAL
{p} /\ (dom g) is V48() V49() V50() Element of bool REAL
y1 is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
p is set
{p} is trivial set
g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g | {p} is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h is V22() real ext-real Element of REAL
dom g is V48() V49() V50() Element of bool REAL
{p} /\ (dom g) is V48() V49() V50() Element of bool REAL
y1 is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
p is set
{p} is trivial set
g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g | {p} is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h is V22() real ext-real Element of REAL
dom g is V48() V49() V50() Element of bool REAL
{p} /\ (dom g) is V48() V49() V50() Element of bool REAL
y1 is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
p is set
{p} is trivial set
g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g | {p} is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h is V22() real ext-real Element of REAL
dom g is V48() V49() V50() Element of bool REAL
{p} /\ (dom g) is V48() V49() V50() Element of bool REAL
y1 is V22() real ext-real Element of REAL
g . y1 is V22() real ext-real Element of REAL
g . h is V22() real ext-real Element of REAL
p is V48() V49() V50() Element of bool REAL
id p is Relation-like REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(id p) | p is Relation-like REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g is V22() real ext-real Element of REAL
dom (id p) is V48() V49() V50() Element of bool REAL
p /\ (dom (id p)) is V48() V49() V50() Element of bool REAL
h is V22() real ext-real Element of REAL
(id p) . g is V22() real ext-real Element of REAL
(id p) . h is V22() real ext-real Element of REAL
p is set
g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
K58(1) is V22() real ext-real set
K58(1) (#) g is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- g) | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- 1 is V22() real ext-real Element of REAL
(- 1) (#) g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((- 1) (#) g) | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
p is set
g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
g | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
K58(1) is V22() real ext-real set
K58(1) (#) g is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- g) | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- 1 is V22() real ext-real Element of REAL
(- 1) (#) g is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
((- 1) (#) g) | p is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
[.p,g.] is V48() V49() V50() Element of bool REAL
h is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | [.p,g.] is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
y1 is V22() real ext-real Element of REAL
dom (h | [.p,g.]) is V48() V49() V50() Element of bool REAL
y2 is V22() real ext-real Element of REAL
(h | [.p,g.]) . y1 is V22() real ext-real Element of REAL
(h | [.p,g.]) . y2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
[.p,g.] /\ (dom h) is V48() V49() V50() Element of bool REAL
h . y1 is V22() real ext-real Element of REAL
h . y2 is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
dom (h | [.p,g.]) is V48() V49() V50() Element of bool REAL
y2 is V22() real ext-real Element of REAL
(h | [.p,g.]) . y1 is V22() real ext-real Element of REAL
(h | [.p,g.]) . y2 is V22() real ext-real Element of REAL
dom h is V48() V49() V50() Element of bool REAL
[.p,g.] /\ (dom h) is V48() V49() V50() Element of bool REAL
h . y1 is V22() real ext-real Element of REAL
h . y2 is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
[.p,g.] is V48() V49() V50() Element of bool REAL
h is Relation-like REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | [.p,g.] is Relation-like REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(h | [.p,g.]) " is Relation-like REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h .: [.p,g.] is V48() V49() V50() Element of bool REAL
((h | [.p,g.]) ") | (h .: [.p,g.]) is Relation-like REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((h | [.p,g.]) ") is V48() V49() V50() Element of bool REAL
(h .: [.p,g.]) /\ (dom ((h | [.p,g.]) ")) is V48() V49() V50() Element of bool REAL
y1 is V22() real ext-real Element of REAL
y2 is V22() real ext-real Element of REAL
((h | [.p,g.]) ") . y2 is V22() real ext-real Element of REAL
((h | [.p,g.]) ") . y1 is V22() real ext-real Element of REAL
rng (h | [.p,g.]) is V48() V49() V50() Element of bool REAL
(h | [.p,g.]) | [.p,g.] is Relation-like REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(h | [.p,g.]) . (((h | [.p,g.]) ") . y2) is V22() real ext-real Element of REAL
dom (h | [.p,g.]) is V48() V49() V50() Element of bool REAL
dom ((h | [.p,g.]) | [.p,g.]) is V48() V49() V50() Element of bool REAL
[.p,g.] /\ (dom (h | [.p,g.])) is V48() V49() V50() Element of bool REAL
(h | [.p,g.]) . (((h | [.p,g.]) ") . y1) is V22() real ext-real Element of REAL
(h | [.p,g.]) . (((h | [.p,g.]) ") . y2) is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
[.p,g.] is V48() V49() V50() Element of bool REAL
h is Relation-like REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h | [.p,g.] is Relation-like REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(h | [.p,g.]) " is Relation-like REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
h .: [.p,g.] is V48() V49() V50() Element of bool REAL
((h | [.p,g.]) ") | (h .: [.p,g.]) is Relation-like REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom ((h | [.p,g.]) ") is V48() V49() V50() Element of bool REAL
(h .: [.p,g.]) /\ (dom ((h | [.p,g.]) ")) is V48() V49() V50() Element of bool REAL
y1 is V22() real ext-real Element of REAL
y2 is V22() real ext-real Element of REAL
((h | [.p,g.]) ") . y1 is V22() real ext-real Element of REAL
((h | [.p,g.]) ") . y2 is V22() real ext-real Element of REAL
rng (h | [.p,g.]) is V48() V49() V50() Element of bool REAL
(h | [.p,g.]) | [.p,g.] is Relation-like REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(h | [.p,g.]) . (((h | [.p,g.]) ") . y2) is V22() real ext-real Element of REAL
dom (h | [.p,g.]) is V48() V49() V50() Element of bool REAL
dom ((h | [.p,g.]) | [.p,g.]) is V48() V49() V50() Element of bool REAL
[.p,g.] /\ (dom (h | [.p,g.])) is V48() V49() V50() Element of bool REAL
(h | [.p,g.]) . (((h | [.p,g.]) ") . y1) is V22() real ext-real Element of REAL
(h | [.p,g.]) . (((h | [.p,g.]) ") . y2) is V22() real ext-real Element of REAL