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