:: CFCONT_1 semantic presentation

REAL is non empty V47() V59() V60() V61() V65() set
NAT is non empty V18() V19() V20() V59() V60() V61() V62() V63() V64() V65() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V47() V59() V65() set
NAT is non empty V18() V19() V20() V59() V60() V61() V62() V63() V64() V65() set
K19(NAT) is set
K19(NAT) is set
RAT is non empty V47() V59() V60() V61() V62() V65() set
INT is non empty V47() V59() V60() V61() V62() V63() V65() set
K20(NAT,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is set
K20(NAT,COMPLEX) is complex-valued set
K19(K20(NAT,COMPLEX)) is set
1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
0 is Function-like functional empty ext-real non negative V18() V19() V20() V22() V23() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
|.0.| is ext-real V25() real V58() Element of REAL
K20(NAT,NAT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
K19(K20(NAT,NAT)) is set
0c is Function-like functional empty ext-real non negative V18() V19() V20() V22() V23() V24() V25() real V59() V60() V61() V62() V63() V64() V65() Element of COMPLEX
1r is V25() Element of COMPLEX
- 1r is V25() Element of COMPLEX
2 is non empty ext-real positive non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
{0} is non empty V59() V60() V61() V62() V63() V64() set
{} is Function-like functional empty ext-real non negative V18() V19() V20() V22() V23() V24() V25() real V59() V60() V61() V62() V63() V64() V65() set
K19(COMPLEX) is set
K20(COMPLEX,COMPLEX) is complex-valued set
K19(K20(COMPLEX,COMPLEX)) is set
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f - g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- g is V1() V4( NAT ) Function-like total complex-valued set
K63(1) is ext-real non positive V25() real set
K63(1) (#) g is V1() V4( NAT ) Function-like total complex-valued set
f + (- g) is V1() V4( NAT ) Function-like total complex-valued set
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y . s2 is V25() Element of COMPLEX
f . s2 is V25() Element of COMPLEX
- g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(- g) . s2 is V25() Element of COMPLEX
(f . s2) + ((- g) . s2) is V25() Element of COMPLEX
g . s2 is V25() Element of COMPLEX
- (g . s2) is V25() Element of COMPLEX
(f . s2) + (- (g . s2)) is V25() Element of COMPLEX
(f . s2) - (g . s2) is V25() Element of COMPLEX
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y . s2 is V25() Element of COMPLEX
f . s2 is V25() Element of COMPLEX
g . s2 is V25() Element of COMPLEX
(f . s2) - (g . s2) is V25() Element of COMPLEX
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y . s2 is V25() Element of COMPLEX
f . s2 is V25() Element of COMPLEX
g . s2 is V25() Element of COMPLEX
(f . s2) - (g . s2) is V25() Element of COMPLEX
- (g . s2) is V25() Element of COMPLEX
(f . s2) + (- (g . s2)) is V25() Element of COMPLEX
- g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(- g) . s2 is V25() Element of COMPLEX
(f . s2) + ((- g) . s2) is V25() Element of COMPLEX
f + (- g) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f + (- g)) . s2 is V25() Element of COMPLEX
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Y + f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Y - f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- f is V1() V4( NAT ) Function-like total complex-valued set
K63(1) is ext-real non positive V25() real set
K63(1) (#) f is V1() V4( NAT ) Function-like total complex-valued set
Y + (- f) is V1() V4( NAT ) Function-like total complex-valued set
Y (#) f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g is V1() V4( NAT ) V5( NAT ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
(Y + f) * g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Y * g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f * g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(Y * g) + (f * g) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(Y - f) * g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(Y * g) - (f * g) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- (f * g) is V1() V4( NAT ) Function-like total complex-valued set
K63(1) (#) (f * g) is V1() V4( NAT ) Function-like total complex-valued set
(Y * g) + (- (f * g)) is V1() V4( NAT ) Function-like total complex-valued set
(Y (#) f) * g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(Y * g) (#) (f * g) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((Y + f) * g) . s2 is V25() Element of COMPLEX
g . s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Y + f) . (g . s2) is V25() Element of COMPLEX
Y . (g . s2) is V25() Element of COMPLEX
f . (g . s2) is V25() Element of COMPLEX
(Y . (g . s2)) + (f . (g . s2)) is V25() Element of COMPLEX
(Y * g) . s2 is V25() Element of COMPLEX
((Y * g) . s2) + (f . (g . s2)) is V25() Element of COMPLEX
(f * g) . s2 is V25() Element of COMPLEX
((Y * g) . s2) + ((f * g) . s2) is V25() Element of COMPLEX
((Y * g) + (f * g)) . s2 is V25() Element of COMPLEX
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((Y - f) * g) . s2 is V25() Element of COMPLEX
g . s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Y - f) . (g . s2) is V25() Element of COMPLEX
Y . (g . s2) is V25() Element of COMPLEX
f . (g . s2) is V25() Element of COMPLEX
(Y . (g . s2)) - (f . (g . s2)) is V25() Element of COMPLEX
(Y * g) . s2 is V25() Element of COMPLEX
((Y * g) . s2) - (f . (g . s2)) is V25() Element of COMPLEX
(f * g) . s2 is V25() Element of COMPLEX
((Y * g) . s2) - ((f * g) . s2) is V25() Element of COMPLEX
((Y * g) - (f * g)) . s2 is V25() Element of COMPLEX
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((Y (#) f) * g) . s2 is V25() Element of COMPLEX
g . s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Y (#) f) . (g . s2) is V25() Element of COMPLEX
Y . (g . s2) is V25() Element of COMPLEX
f . (g . s2) is V25() Element of COMPLEX
(Y . (g . s2)) * (f . (g . s2)) is V25() Element of COMPLEX
(Y * g) . s2 is V25() Element of COMPLEX
((Y * g) . s2) * (f . (g . s2)) is V25() Element of COMPLEX
(f * g) . s2 is V25() Element of COMPLEX
((Y * g) . s2) * ((f * g) . s2) is V25() Element of COMPLEX
((Y * g) (#) (f * g)) . s2 is V25() Element of COMPLEX
Y is V25() Element of COMPLEX
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Y (#) f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g is V1() V4( NAT ) V5( NAT ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
(Y (#) f) * g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f * g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Y (#) (f * g) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((Y (#) f) * g) . s2 is V25() Element of COMPLEX
g . s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Y (#) f) . (g . s2) is V25() Element of COMPLEX
f . (g . s2) is V25() Element of COMPLEX
Y * (f . (g . s2)) is V25() Element of COMPLEX
(f * g) . s2 is V25() Element of COMPLEX
Y * ((f * g) . s2) is V25() Element of COMPLEX
(Y (#) (f * g)) . s2 is V25() Element of COMPLEX
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
K63(1) is ext-real non positive V25() real set
K63(1) (#) Y is V1() V4( NAT ) Function-like total complex-valued set
|.Y.| is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( NAT ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
(- Y) * f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Y * f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- (Y * f) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
K63(1) (#) (Y * f) is V1() V4( NAT ) Function-like total complex-valued set
|.Y.| * f is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of |.Y.|
|.(Y * f).| is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1r) (#) Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((- 1r) (#) Y) * f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) (Y * f) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(|.Y.| * f) . g is ext-real V25() real Element of REAL
f . g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
|.Y.| . (f . g) is ext-real V25() real Element of REAL
Y . (f . g) is V25() Element of COMPLEX
|.(Y . (f . g)).| is ext-real V25() real Element of REAL
(Y * f) . g is V25() Element of COMPLEX
|.((Y * f) . g).| is ext-real V25() real Element of REAL
|.(Y * f).| . g is ext-real V25() real Element of REAL
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Y " is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f is V1() V4( NAT ) V5( NAT ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
Y * f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(Y * f) " is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(Y ") * f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((Y * f) ") . g is V25() Element of COMPLEX
(Y * f) . g is V25() Element of COMPLEX
((Y * f) . g) " is V25() Element of COMPLEX
f . g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y . (f . g) is V25() Element of COMPLEX
(Y . (f . g)) " is V25() Element of COMPLEX
(Y ") . (f . g) is V25() Element of COMPLEX
((Y ") * f) . g is V25() Element of COMPLEX
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Y /" f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f " is V1() V4( NAT ) Function-like total complex-valued set
Y (#) (f ") is V1() V4( NAT ) Function-like total complex-valued set
g is V1() V4( NAT ) V5( NAT ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
(Y /" f) * g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Y * g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f * g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(Y * g) /" (f * g) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f * g) " is V1() V4( NAT ) Function-like total complex-valued set
(Y * g) (#) ((f * g) ") is V1() V4( NAT ) Function-like total complex-valued set
f " is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f ") * g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(Y * g) (#) ((f ") * g) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng Y is V59() Element of K19(COMPLEX)
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom f is V59() Element of K19(COMPLEX)
f /* Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom g is V59() Element of K19(COMPLEX)
(dom f) /\ (dom g) is V59() Element of K19(COMPLEX)
f + g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
(f + g) /* Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g /* Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /* Y) + (g /* Y) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f - g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
- g is V1() V4( COMPLEX ) Function-like complex-valued set
K63(1) is ext-real non positive V25() real set
K63(1) (#) g is V1() V4( COMPLEX ) Function-like complex-valued set
f + (- g) is V1() V4( COMPLEX ) Function-like complex-valued set
(f - g) /* Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /* Y) - (g /* Y) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- (g /* Y) is V1() V4( NAT ) Function-like total complex-valued set
K63(1) (#) (g /* Y) is V1() V4( NAT ) Function-like total complex-valued set
(f /* Y) + (- (g /* Y)) is V1() V4( NAT ) Function-like total complex-valued set
f (#) g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
(f (#) g) /* Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /* Y) (#) (g /* Y) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
dom (f + g) is V59() Element of K19(COMPLEX)
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y . s2 is V25() Element of COMPLEX
((f + g) /* Y) . s2 is V25() Element of COMPLEX
(f + g) /. (Y . s2) is V25() Element of COMPLEX
f /. (Y . s2) is V25() Element of COMPLEX
g /. (Y . s2) is V25() Element of COMPLEX
(f /. (Y . s2)) + (g /. (Y . s2)) is V25() Element of COMPLEX
(f /* Y) . s2 is V25() Element of COMPLEX
((f /* Y) . s2) + (g /. (Y . s2)) is V25() Element of COMPLEX
(g /* Y) . s2 is V25() Element of COMPLEX
((f /* Y) . s2) + ((g /* Y) . s2) is V25() Element of COMPLEX
((f /* Y) + (g /* Y)) . s2 is V25() Element of COMPLEX
dom (f - g) is V59() Element of K19(COMPLEX)
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y . s2 is V25() Element of COMPLEX
((f - g) /* Y) . s2 is V25() Element of COMPLEX
(f - g) /. (Y . s2) is V25() Element of COMPLEX
f /. (Y . s2) is V25() Element of COMPLEX
g /. (Y . s2) is V25() Element of COMPLEX
(f /. (Y . s2)) - (g /. (Y . s2)) is V25() Element of COMPLEX
(f /* Y) . s2 is V25() Element of COMPLEX
((f /* Y) . s2) - (g /. (Y . s2)) is V25() Element of COMPLEX
(g /* Y) . s2 is V25() Element of COMPLEX
((f /* Y) . s2) - ((g /* Y) . s2) is V25() Element of COMPLEX
dom (f (#) g) is V59() Element of K19(COMPLEX)
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y . s2 is V25() Element of COMPLEX
((f (#) g) /* Y) . s2 is V25() Element of COMPLEX
(f (#) g) /. (Y . s2) is V25() Element of COMPLEX
f /. (Y . s2) is V25() Element of COMPLEX
g /. (Y . s2) is V25() Element of COMPLEX
(f /. (Y . s2)) * (g /. (Y . s2)) is V25() Element of COMPLEX
(f /* Y) . s2 is V25() Element of COMPLEX
((f /* Y) . s2) * (g /. (Y . s2)) is V25() Element of COMPLEX
(g /* Y) . s2 is V25() Element of COMPLEX
((f /* Y) . s2) * ((g /* Y) . s2) is V25() Element of COMPLEX
((f /* Y) (#) (g /* Y)) . s2 is V25() Element of COMPLEX
Y is V25() Element of COMPLEX
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng f is V59() Element of K19(COMPLEX)
g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom g is V59() Element of K19(COMPLEX)
Y (#) g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
(Y (#) g) /* f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g /* f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Y (#) (g /* f) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
dom (Y (#) g) is V59() Element of K19(COMPLEX)
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f . s2 is V25() Element of COMPLEX
((Y (#) g) /* f) . s2 is V25() Element of COMPLEX
(Y (#) g) /. (f . s2) is V25() Element of COMPLEX
g /. (f . s2) is V25() Element of COMPLEX
Y * (g /. (f . s2)) is V25() Element of COMPLEX
(g /* f) . s2 is V25() Element of COMPLEX
Y * ((g /* f) . s2) is V25() Element of COMPLEX
(Y (#) (g /* f)) . s2 is V25() Element of COMPLEX
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng Y is V59() Element of K19(COMPLEX)
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom f is V59() Element of K19(COMPLEX)
f /* Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- (f /* Y) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
K63(1) is ext-real non positive V25() real set
K63(1) (#) (f /* Y) is V1() V4( NAT ) Function-like total complex-valued set
- f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
K63(1) (#) f is V1() V4( COMPLEX ) Function-like complex-valued set
(- f) /* Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) (f /* Y) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1r) (#) f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
((- 1r) (#) f) /* Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng Y is V59() Element of K19(COMPLEX)
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f ^ is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom (f ^) is V59() Element of K19(COMPLEX)
f /* Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
dom f is V59() Element of K19(COMPLEX)
{0c} is non empty V59() V60() V61() V62() V63() V64() set
f " {0c} is V59() Element of K19(COMPLEX)
(dom f) \ (f " {0c}) is V59() Element of K19(COMPLEX)
g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(f /* Y) . g is V25() Element of COMPLEX
Y . g is V25() Element of COMPLEX
f /. (Y . g) is V25() Element of COMPLEX
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng Y is V59() Element of K19(COMPLEX)
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f ^ is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom (f ^) is V59() Element of K19(COMPLEX)
(f ^) /* Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f /* Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /* Y) " is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
dom f is V59() Element of K19(COMPLEX)
{0c} is non empty V59() V60() V61() V62() V63() V64() set
f " {0c} is V59() Element of K19(COMPLEX)
(dom f) \ (f " {0c}) is V59() Element of K19(COMPLEX)
g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y . g is V25() Element of COMPLEX
((f ^) /* Y) . g is V25() Element of COMPLEX
(f ^) /. (Y . g) is V25() Element of COMPLEX
f /. (Y . g) is V25() Element of COMPLEX
(f /. (Y . g)) " is V25() Element of COMPLEX
(f /* Y) . g is V25() Element of COMPLEX
((f /* Y) . g) " is V25() Element of COMPLEX
((f /* Y) ") . g is V25() Element of COMPLEX
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng Y is V59() Element of K19(COMPLEX)
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom f is V59() Element of K19(COMPLEX)
f /* Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g is V1() V4( NAT ) V5( NAT ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
(f /* Y) * g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Re ((f /* Y) * g) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Y * g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f /* (Y * g) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Re (f /* (Y * g)) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (Y * g) is V59() Element of K19(COMPLEX)
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Re ((f /* Y) * g)) . s2 is ext-real V25() real Element of REAL
((f /* Y) * g) . s2 is V25() Element of COMPLEX
Re (((f /* Y) * g) . s2) is ext-real V25() real Element of REAL
g . s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(f /* Y) . (g . s2) is V25() Element of COMPLEX
Re ((f /* Y) . (g . s2)) is ext-real V25() real Element of REAL
Y . (g . s2) is V25() Element of COMPLEX
f /. (Y . (g . s2)) is V25() Element of COMPLEX
Re (f /. (Y . (g . s2))) is ext-real V25() real Element of REAL
(Y * g) . s2 is V25() Element of COMPLEX
f /. ((Y * g) . s2) is V25() Element of COMPLEX
Re (f /. ((Y * g) . s2)) is ext-real V25() real Element of REAL
(f /* (Y * g)) . s2 is V25() Element of COMPLEX
Re ((f /* (Y * g)) . s2) is ext-real V25() real Element of REAL
(Re (f /* (Y * g))) . s2 is ext-real V25() real Element of REAL
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng Y is V59() Element of K19(COMPLEX)
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom f is V59() Element of K19(COMPLEX)
f /* Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g is V1() V4( NAT ) V5( NAT ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
(f /* Y) * g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Im ((f /* Y) * g) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Y * g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f /* (Y * g) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Im (f /* (Y * g)) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (Y * g) is V59() Element of K19(COMPLEX)
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Im ((f /* Y) * g)) . s2 is ext-real V25() real Element of REAL
((f /* Y) * g) . s2 is V25() Element of COMPLEX
Im (((f /* Y) * g) . s2) is ext-real V25() real Element of REAL
g . s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(f /* Y) . (g . s2) is V25() Element of COMPLEX
Im ((f /* Y) . (g . s2)) is ext-real V25() real Element of REAL
Y . (g . s2) is V25() Element of COMPLEX
f /. (Y . (g . s2)) is V25() Element of COMPLEX
Im (f /. (Y . (g . s2))) is ext-real V25() real Element of REAL
(Y * g) . s2 is V25() Element of COMPLEX
f /. ((Y * g) . s2) is V25() Element of COMPLEX
Im (f /. ((Y * g) . s2)) is ext-real V25() real Element of REAL
(f /* (Y * g)) . s2 is V25() Element of COMPLEX
Im ((f /* (Y * g)) . s2) is ext-real V25() real Element of REAL
(Im (f /* (Y * g))) . s2 is ext-real V25() real Element of REAL
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f /* Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f + g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
(f + g) /* Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g /* Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /* Y) + (g /* Y) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f - g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
- g is V1() V4( COMPLEX ) Function-like complex-valued set
K63(1) is ext-real non positive V25() real set
K63(1) (#) g is V1() V4( COMPLEX ) Function-like complex-valued set
f + (- g) is V1() V4( COMPLEX ) Function-like complex-valued set
(f - g) /* Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /* Y) - (g /* Y) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- (g /* Y) is V1() V4( NAT ) Function-like total complex-valued set
K63(1) (#) (g /* Y) is V1() V4( NAT ) Function-like total complex-valued set
(f /* Y) + (- (g /* Y)) is V1() V4( NAT ) Function-like total complex-valued set
f (#) g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
(f (#) g) /* Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /* Y) (#) (g /* Y) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
dom (f + g) is V59() Element of K19(COMPLEX)
dom f is V59() Element of K19(COMPLEX)
dom g is V59() Element of K19(COMPLEX)
(dom f) /\ (dom g) is V59() Element of K19(COMPLEX)
rng Y is V59() Element of K19(COMPLEX)
Y is V25() Element of COMPLEX
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
Y (#) g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
(Y (#) g) /* f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g /* f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Y (#) (g /* f) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
dom g is V59() Element of K19(COMPLEX)
rng f is V59() Element of K19(COMPLEX)
Y is set
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng f is V59() Element of K19(COMPLEX)
g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
g | Y is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom (g | Y) is V59() Element of K19(COMPLEX)
g " {0} is V59() Element of K19(COMPLEX)
g ^ is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
(g ^) | Y is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
((g ^) | Y) /* f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(g | Y) /* f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((g | Y) /* f) " is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
s2 is set
dom g is V59() Element of K19(COMPLEX)
(dom g) /\ Y is V59() Element of K19(COMPLEX)
{0c} is non empty V59() V60() V61() V62() V63() V64() set
g " {0c} is V59() Element of K19(COMPLEX)
(dom g) \ (g " {0c}) is V59() Element of K19(COMPLEX)
dom (g ^) is V59() Element of K19(COMPLEX)
(dom (g ^)) /\ Y is V59() Element of K19(COMPLEX)
dom ((g ^) | Y) is V59() Element of K19(COMPLEX)
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f . s2 is V25() Element of COMPLEX
(((g ^) | Y) /* f) . s2 is V25() Element of COMPLEX
((g ^) | Y) /. (f . s2) is V25() Element of COMPLEX
(g ^) /. (f . s2) is V25() Element of COMPLEX
g /. (f . s2) is V25() Element of COMPLEX
(g /. (f . s2)) " is V25() Element of COMPLEX
(g | Y) /. (f . s2) is V25() Element of COMPLEX
((g | Y) /. (f . s2)) " is V25() Element of COMPLEX
((g | Y) /* f) . s2 is V25() Element of COMPLEX
(((g | Y) /* f) . s2) " is V25() Element of COMPLEX
(((g | Y) /* f) ") . s2 is V25() Element of COMPLEX
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g is V25() Element of COMPLEX
s2 is V25() Element of COMPLEX
q2 is ext-real V25() real Element of REAL
n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y . x2 is V25() set
K65((Y . x2),s2) is set
|.K65((Y . x2),s2).| is ext-real V25() real Element of REAL
p is V1() V4( NAT ) V5( NAT ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
f * p is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
p . x2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y . x2 is V25() Element of COMPLEX
f . (p . x2) is V25() Element of COMPLEX
(Y . x2) - s2 is V25() Element of COMPLEX
|.((Y . x2) - s2).| is ext-real V25() real Element of REAL
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim Y is V25() Element of COMPLEX
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim f is V25() Element of COMPLEX
g is V1() V4( NAT ) V5( NAT ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
f * g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
s2 is ext-real V25() real Element of REAL
q2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g . s is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y . s is V25() Element of COMPLEX
f . (g . s) is V25() Element of COMPLEX
(Y . s) - (lim f) is V25() Element of COMPLEX
|.((Y . s) - (lim f)).| is ext-real V25() real Element of REAL
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g is V25() Element of COMPLEX
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
q2 is V25() Element of COMPLEX
n is ext-real V25() real Element of REAL
s is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
p is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y . p is V25() Element of COMPLEX
(Y . p) - g is V25() Element of COMPLEX
|.((Y . p) - g).| is ext-real V25() real Element of REAL
f . p is V25() Element of COMPLEX
(f . p) - q2 is V25() Element of COMPLEX
|.((f . p) - q2).| is ext-real V25() real Element of REAL
x2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
p is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f . p is V25() Element of COMPLEX
Y . p is V25() Element of COMPLEX
(f . p) - q2 is V25() Element of COMPLEX
|.((f . p) - q2).| is ext-real V25() real Element of REAL
x2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
p is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim Y is V25() Element of COMPLEX
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim f is V25() Element of COMPLEX
g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s2 is ext-real V25() real Element of REAL
q2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y . s is V25() Element of COMPLEX
(Y . s) - (lim Y) is V25() Element of COMPLEX
|.((Y . s) - (lim Y)).| is ext-real V25() real Element of REAL
f . s is V25() Element of COMPLEX
(f . s) - (lim Y) is V25() Element of COMPLEX
|.((f . s) - (lim Y)).| is ext-real V25() real Element of REAL
n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f . s is V25() Element of COMPLEX
Y . s is V25() Element of COMPLEX
(f . s) - (lim Y) is V25() Element of COMPLEX
|.((f . s) - (lim Y)).| is ext-real V25() real Element of REAL
n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Y is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f ^\ Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued subsequence of f
lim (f ^\ Y) is V25() Element of COMPLEX
lim f is V25() Element of COMPLEX
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f ^\ g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued subsequence of f
g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f ^\ g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued subsequence of f
s2 is V25() Element of COMPLEX
q2 is V25() Element of COMPLEX
n is ext-real V25() real Element of REAL
s is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s + g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
p is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f . p is V25() set
K65((f . p),q2) is set
|.K65((f . p),q2).| is ext-real V25() real Element of REAL
n is ext-real non negative V18() V19() V20() V24() V25() real set
(s + g) + n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
p - g is ext-real V25() real Element of REAL
k is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s + k is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(s + k) + g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
- g is ext-real non positive V25() real Element of REAL
((s + k) + g) + (- g) is ext-real V25() real Element of REAL
m is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
m + g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y . m is V25() Element of COMPLEX
(Y . m) - s2 is V25() Element of COMPLEX
|.((Y . m) - s2).| is ext-real V25() real Element of REAL
f . p is V25() Element of COMPLEX
(f . p) - q2 is V25() Element of COMPLEX
|.((f . p) - q2).| is ext-real V25() real Element of REAL
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim Y is V25() Element of COMPLEX
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim f is V25() Element of COMPLEX
g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f ^\ g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued subsequence of f
g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f ^\ g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued subsequence of f
s2 is ext-real V25() real Element of REAL
q2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
q2 + g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 is ext-real non negative V18() V19() V20() V24() V25() real set
(q2 + g) + x2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s - g is ext-real V25() real Element of REAL
p is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
q2 + p is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(q2 + p) + g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
- g is ext-real non positive V25() real Element of REAL
((q2 + p) + g) + (- g) is ext-real V25() real Element of REAL
n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y . n is V25() Element of COMPLEX
(Y . n) - (lim Y) is V25() Element of COMPLEX
|.((Y . n) - (lim Y)).| is ext-real V25() real Element of REAL
f . s is V25() Element of COMPLEX
(f . s) - (lim Y) is V25() Element of COMPLEX
|.((f . s) - (lim Y)).| is ext-real V25() real Element of REAL
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f ^\ s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued subsequence of f
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim Y is V25() Element of COMPLEX
|.(lim Y).| is ext-real V25() real Element of REAL
|.(lim Y).| / 2 is ext-real V25() real Element of REAL
f is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y ^\ g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued subsequence of Y
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
0 + g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s2 + g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y . (s2 + g) is V25() Element of COMPLEX
|.(Y . (s2 + g)).| is ext-real V25() real Element of REAL
(Y ^\ g) . s2 is V25() Element of COMPLEX
|.((Y ^\ g) . s2).| is ext-real V25() real Element of REAL
0 / 2 is ext-real non negative V25() real Element of REAL
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim Y is V25() Element of COMPLEX
f is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y ^\ f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued subsequence of Y
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f is V25() Element of COMPLEX
g is V25() Element of COMPLEX
s2 is ext-real V25() real Element of REAL
q2 is Function-like functional empty ext-real non negative V18() V19() V20() V22() V23() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y . n is V25() set
K65((Y . n),g) is set
|.K65((Y . n),g).| is ext-real V25() real Element of REAL
Y . n is V25() Element of COMPLEX
(Y . n) - g is V25() Element of COMPLEX
|.((Y . n) - g).| is ext-real V25() real Element of REAL
f - g is V25() Element of COMPLEX
|.(f - g).| is ext-real V25() real Element of REAL
Y is V25() Element of COMPLEX
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng f is V59() Element of K19(COMPLEX)
lim f is V25() Element of COMPLEX
g is V25() Element of COMPLEX
{g} is non empty V59() set
s2 is V25() Element of COMPLEX
q2 is ext-real V25() real Element of REAL
n is Function-like functional empty ext-real non negative V18() V19() V20() V22() V23() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
s is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
dom f is V59() V60() V61() V62() V63() V64() Element of K19(NAT)
f . s is V25() Element of COMPLEX
(f . s) - Y is V25() Element of COMPLEX
|.((f . s) - Y).| is ext-real V25() real Element of REAL
q2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f . q2 is V25() Element of COMPLEX
g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f . g is V25() Element of COMPLEX
g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f . g is V25() Element of COMPLEX
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f . s2 is V25() Element of COMPLEX
g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f . g is V25() Element of COMPLEX
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim Y is V25() Element of COMPLEX
f is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y . f is V25() Element of COMPLEX
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim Y is V25() Element of COMPLEX
(lim Y) " is V25() Element of COMPLEX
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f " is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim (f ") is V25() Element of COMPLEX
lim f is V25() Element of COMPLEX
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Y . 0 is V25() Element of COMPLEX
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Y + f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim (Y + f) is V25() Element of COMPLEX
lim f is V25() Element of COMPLEX
(Y . 0) + (lim f) is V25() Element of COMPLEX
Y - f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- f is V1() V4( NAT ) Function-like total complex-valued set
K63(1) is ext-real non positive V25() real set
K63(1) (#) f is V1() V4( NAT ) Function-like total complex-valued set
Y + (- f) is V1() V4( NAT ) Function-like total complex-valued set
lim (Y - f) is V25() Element of COMPLEX
(Y . 0) - (lim f) is V25() Element of COMPLEX
f - Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- Y is V1() V4( NAT ) Function-like total complex-valued set
K63(1) (#) Y is V1() V4( NAT ) Function-like total complex-valued set
f + (- Y) is V1() V4( NAT ) Function-like total complex-valued set
lim (f - Y) is V25() Element of COMPLEX
(lim f) - (Y . 0) is V25() Element of COMPLEX
Y (#) f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim (Y (#) f) is V25() Element of COMPLEX
(Y . 0) * (lim f) is V25() Element of COMPLEX
lim Y is V25() Element of COMPLEX
(lim Y) + (lim f) is V25() Element of COMPLEX
(lim Y) - (lim f) is V25() Element of COMPLEX
(lim f) - (lim Y) is V25() Element of COMPLEX
(lim Y) * (lim f) is V25() Element of COMPLEX
Y is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f . g is V25() Element of COMPLEX
Y is V25() Element of COMPLEX
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom f is V59() Element of K19(COMPLEX)
f /. Y is V25() Element of COMPLEX
g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng g is V59() Element of K19(COMPLEX)
lim g is V25() Element of COMPLEX
f /* g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim (f /* g) is V25() Element of COMPLEX
g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng g is V59() Element of K19(COMPLEX)
lim g is V25() Element of COMPLEX
f /* g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim (f /* g) is V25() Element of COMPLEX
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g ^\ s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued subsequence of g
q2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(g ^\ s2) . q2 is V25() Element of COMPLEX
q2 + s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g . (q2 + s2) is V25() Element of COMPLEX
f /* (g ^\ s2) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /* g) ^\ s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued subsequence of f /* g
rng (g ^\ s2) is V59() Element of K19(COMPLEX)
q2 is ext-real V25() real Element of REAL
n is Function-like functional empty ext-real non negative V18() V19() V20() V22() V23() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
s is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(f /* (g ^\ s2)) . s is V25() Element of COMPLEX
((f /* (g ^\ s2)) . s) - (f /. Y) is V25() Element of COMPLEX
|.(((f /* (g ^\ s2)) . s) - (f /. Y)).| is ext-real V25() real Element of REAL
(g ^\ s2) . s is V25() Element of COMPLEX
f /. ((g ^\ s2) . s) is V25() Element of COMPLEX
(f /. ((g ^\ s2) . s)) - (f /. Y) is V25() Element of COMPLEX
|.((f /. ((g ^\ s2) . s)) - (f /. Y)).| is ext-real V25() real Element of REAL
(f /. Y) - (f /. Y) is V25() Element of COMPLEX
|.((f /. Y) - (f /. Y)).| is ext-real V25() real Element of REAL
lim ((f /* g) ^\ s2) is V25() Element of COMPLEX
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g . s2 is V25() Element of COMPLEX
s2 is ext-real non negative V18() V19() V20() V24() V25() real set
g . s2 is V25() set
n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g . s is V25() Element of COMPLEX
x2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g . x2 is V25() Element of COMPLEX
n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g . x2 is V25() Element of COMPLEX
x2 is ext-real non negative V18() V19() V20() V24() V25() real set
g . x2 is V25() Element of COMPLEX
p is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g . n is V25() Element of COMPLEX
k is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g . k is V25() Element of COMPLEX
q2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is V1() V4( NAT ) V5( NAT ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(NAT,NAT))
n . 0 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n . s is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
rng n is V59() V60() V61() V62() V63() V64() Element of K19(NAT)
dom n is V59() V60() V61() V62() V63() V64() Element of K19(NAT)
s is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
x2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s . x2 is ext-real V25() real Element of REAL
rng s is V59() V60() V61() Element of K19(REAL)
x2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s . x2 is ext-real V25() real Element of REAL
x2 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s . (x2 + 1) is ext-real V25() real Element of REAL
x2 is V1() V4( NAT ) V5( NAT ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
g * x2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim (g * x2) is V25() Element of COMPLEX
p is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g . p is V25() set
p is ext-real non negative V18() V19() V20() V24() V25() real set
g . p is V25() set
g . s2 is V25() Element of COMPLEX
x2 . 0 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is ext-real non negative V18() V19() V20() V24() V25() real set
g . n is V25() Element of COMPLEX
k is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 . k is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is ext-real non negative V18() V19() V20() V24() V25() real set
g . n is V25() Element of COMPLEX
k is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g . k is V25() Element of COMPLEX
m is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 . m is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
l is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 . l is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
m is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 . m is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 . k is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 . k is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 . (k + 1) is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g . (x2 . (k + 1)) is V25() Element of COMPLEX
m is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 . m is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
p is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(g * x2) . p is V25() Element of COMPLEX
p + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(g * x2) . (p + 1) is V25() Element of COMPLEX
x2 . p is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 . (p + 1) is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g . k is V25() Element of COMPLEX
m is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g . m is V25() Element of COMPLEX
g . (x2 . (p + 1)) is V25() Element of COMPLEX
(g * x2) . 0 is V25() Element of COMPLEX
rng (g * x2) is V59() Element of K19(COMPLEX)
f /* (g * x2) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim (f /* (g * x2)) is V25() Element of COMPLEX
p is ext-real V25() real Element of REAL
n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 . n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
k is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
m is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g . m is V25() Element of COMPLEX
(f /* g) . m is V25() Element of COMPLEX
((f /* g) . m) - (f /. Y) is V25() Element of COMPLEX
|.(((f /* g) . m) - (f /. Y)).| is ext-real V25() real Element of REAL
(f /. Y) - (f /. Y) is V25() Element of COMPLEX
|.((f /. Y) - (f /. Y)).| is ext-real V25() real Element of REAL
g . m is V25() Element of COMPLEX
l is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 . l is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(f /* (g * x2)) . l is V25() Element of COMPLEX
((f /* (g * x2)) . l) - (f /. Y) is V25() Element of COMPLEX
|.(((f /* (g * x2)) . l) - (f /. Y)).| is ext-real V25() real Element of REAL
(g * x2) . l is V25() Element of COMPLEX
f /. ((g * x2) . l) is V25() Element of COMPLEX
(f /. ((g * x2) . l)) - (f /. Y) is V25() Element of COMPLEX
|.((f /. ((g * x2) . l)) - (f /. Y)).| is ext-real V25() real Element of REAL
f /. (g . m) is V25() Element of COMPLEX
(f /. (g . m)) - (f /. Y) is V25() Element of COMPLEX
|.((f /. (g . m)) - (f /. Y)).| is ext-real V25() real Element of REAL
(f /* g) . m is V25() Element of COMPLEX
((f /* g) . m) - (f /. Y) is V25() Element of COMPLEX
|.(((f /* g) . m) - (f /. Y)).| is ext-real V25() real Element of REAL
g . m is V25() Element of COMPLEX
(f /* g) . m is V25() Element of COMPLEX
((f /* g) . m) - (f /. Y) is V25() Element of COMPLEX
|.(((f /* g) . m) - (f /. Y)).| is ext-real V25() real Element of REAL
(f /* g) . m is V25() Element of COMPLEX
((f /* g) . m) - (f /. Y) is V25() Element of COMPLEX
|.(((f /* g) . m) - (f /. Y)).| is ext-real V25() real Element of REAL
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Y is V25() Element of COMPLEX
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom f is V59() Element of K19(COMPLEX)
f /. Y is V25() Element of COMPLEX
g is ext-real V25() real Element of REAL
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s2 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
1 / (s2 + 1) is ext-real non negative V25() real Element of REAL
(s2 + 1) " is ext-real positive non negative V25() real Element of REAL
q2 is V25() Element of COMPLEX
q2 - Y is V25() Element of COMPLEX
|.(q2 - Y).| is ext-real V25() real Element of REAL
f /. q2 is V25() Element of COMPLEX
(f /. q2) - (f /. Y) is V25() Element of COMPLEX
|.((f /. q2) - (f /. Y)).| is ext-real V25() real Element of REAL
s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng s2 is V59() Element of K19(COMPLEX)
q2 is set
n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s2 . n is V25() Element of COMPLEX
q2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s2 . q2 is V25() Element of COMPLEX
f /. (s2 . q2) is V25() Element of COMPLEX
(f /. (s2 . q2)) - (f /. Y) is V25() Element of COMPLEX
|.((f /. (s2 . q2)) - (f /. Y)).| is ext-real V25() real Element of REAL
f /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /* s2) . q2 is V25() Element of COMPLEX
((f /* s2) . q2) - (f /. Y) is V25() Element of COMPLEX
|.(((f /* s2) . q2) - (f /. Y)).| is ext-real V25() real Element of REAL
q2 is ext-real V25() real Element of REAL
q2 " is ext-real V25() real Element of REAL
n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(q2 ") + 0 is ext-real V25() real Element of REAL
1 / (q2 ") is ext-real V25() real Element of REAL
1 / (n + 1) is ext-real non negative V25() real Element of REAL
s is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
1 / (x2 + 1) is ext-real non negative V25() real Element of REAL
1 / (s + 1) is ext-real non negative V25() real Element of REAL
s2 . x2 is V25() Element of COMPLEX
(s2 . x2) - Y is V25() Element of COMPLEX
|.((s2 . x2) - Y).| is ext-real V25() real Element of REAL
lim s2 is V25() Element of COMPLEX
lim (f /* s2) is V25() Element of COMPLEX
q2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(f /* s2) . q2 is V25() Element of COMPLEX
((f /* s2) . q2) - (f /. Y) is V25() Element of COMPLEX
|.(((f /* s2) . q2) - (f /. Y)).| is ext-real V25() real Element of REAL
g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng g is V59() Element of K19(COMPLEX)
lim g is V25() Element of COMPLEX
s2 is ext-real V25() real Element of REAL
q2 is ext-real V25() real Element of REAL
n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
x2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g . x2 is V25() Element of COMPLEX
(g . x2) - Y is V25() Element of COMPLEX
|.((g . x2) - Y).| is ext-real V25() real Element of REAL
f /. (g . x2) is V25() Element of COMPLEX
(f /. (g . x2)) - (f /. Y) is V25() Element of COMPLEX
|.((f /. (g . x2)) - (f /. Y)).| is ext-real V25() real Element of REAL
f /* g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /* g) . x2 is V25() Element of COMPLEX
((f /* g) . x2) - (f /. Y) is V25() Element of COMPLEX
|.(((f /* g) . x2) - (f /. Y)).| is ext-real V25() real Element of REAL
lim (f /* g) is V25() Element of COMPLEX
Y is V25() Element of COMPLEX
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f + g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f - g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
- g is V1() V4( COMPLEX ) Function-like complex-valued set
K63(1) is ext-real non positive V25() real set
K63(1) (#) g is V1() V4( COMPLEX ) Function-like complex-valued set
f + (- g) is V1() V4( COMPLEX ) Function-like complex-valued set
f (#) g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom f is V59() Element of K19(COMPLEX)
dom g is V59() Element of K19(COMPLEX)
(dom f) /\ (dom g) is V59() Element of K19(COMPLEX)
dom (f + g) is V59() Element of K19(COMPLEX)
s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng s2 is V59() Element of K19(COMPLEX)
lim s2 is V25() Element of COMPLEX
g /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /* s2) + (g /* s2) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f + g) /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f /. Y is V25() Element of COMPLEX
lim (f /* s2) is V25() Element of COMPLEX
g /. Y is V25() Element of COMPLEX
lim (g /* s2) is V25() Element of COMPLEX
(f + g) /. Y is V25() Element of COMPLEX
(f /. Y) + (g /. Y) is V25() Element of COMPLEX
lim ((f /* s2) + (g /* s2)) is V25() Element of COMPLEX
lim ((f + g) /* s2) is V25() Element of COMPLEX
dom (f - g) is V59() Element of K19(COMPLEX)
s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng s2 is V59() Element of K19(COMPLEX)
lim s2 is V25() Element of COMPLEX
g /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /* s2) - (g /* s2) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- (g /* s2) is V1() V4( NAT ) Function-like total complex-valued set
K63(1) (#) (g /* s2) is V1() V4( NAT ) Function-like total complex-valued set
(f /* s2) + (- (g /* s2)) is V1() V4( NAT ) Function-like total complex-valued set
(f - g) /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim (f /* s2) is V25() Element of COMPLEX
lim (g /* s2) is V25() Element of COMPLEX
(f - g) /. Y is V25() Element of COMPLEX
(f /. Y) - (g /. Y) is V25() Element of COMPLEX
lim ((f /* s2) - (g /* s2)) is V25() Element of COMPLEX
lim ((f - g) /* s2) is V25() Element of COMPLEX
dom (f (#) g) is V59() Element of K19(COMPLEX)
(f (#) g) /. Y is V25() Element of COMPLEX
s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng s2 is V59() Element of K19(COMPLEX)
lim s2 is V25() Element of COMPLEX
(f (#) g) /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((f (#) g) /* s2) is V25() Element of COMPLEX
g /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /* s2) (#) (g /* s2) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim (f /* s2) is V25() Element of COMPLEX
lim (g /* s2) is V25() Element of COMPLEX
(f /. Y) * (g /. Y) is V25() Element of COMPLEX
lim ((f /* s2) (#) (g /* s2)) is V25() Element of COMPLEX
Y is V25() Element of COMPLEX
f is V25() Element of COMPLEX
g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f (#) g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom g is V59() Element of K19(COMPLEX)
dom (f (#) g) is V59() Element of K19(COMPLEX)
(f (#) g) /. Y is V25() Element of COMPLEX
s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng s2 is V59() Element of K19(COMPLEX)
lim s2 is V25() Element of COMPLEX
(f (#) g) /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((f (#) g) /* s2) is V25() Element of COMPLEX
g /. Y is V25() Element of COMPLEX
g /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim (g /* s2) is V25() Element of COMPLEX
f (#) (g /* s2) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f * (g /. Y) is V25() Element of COMPLEX
lim (f (#) (g /* s2)) is V25() Element of COMPLEX
Y is V25() Element of COMPLEX
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
- f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
K63(1) is ext-real non positive V25() real set
K63(1) (#) f is V1() V4( COMPLEX ) Function-like complex-valued set
(- 1r) (#) f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
Y is V25() Element of COMPLEX
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f /. Y is V25() Element of COMPLEX
f ^ is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
{0c} is non empty V59() V60() V61() V62() V63() V64() set
f " {0c} is V59() Element of K19(COMPLEX)
dom f is V59() Element of K19(COMPLEX)
(dom f) \ (f " {0c}) is V59() Element of K19(COMPLEX)
dom (f ^) is V59() Element of K19(COMPLEX)
(f ^) /. Y is V25() Element of COMPLEX
g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng g is V59() Element of K19(COMPLEX)
lim g is V25() Element of COMPLEX
(f ^) /* g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((f ^) /* g) is V25() Element of COMPLEX
f /* g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim (f /* g) is V25() Element of COMPLEX
(f /* g) " is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /. Y) " is V25() Element of COMPLEX
lim ((f /* g) ") is V25() Element of COMPLEX
Y is V25() Element of COMPLEX
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f /. Y is V25() Element of COMPLEX
g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
g / f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f ^ is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
g (#) (f ^) is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
Y is set
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom f is V59() Element of K19(COMPLEX)
g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng g is V59() Element of K19(COMPLEX)
lim g is V25() Element of COMPLEX
f | Y is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom (f | Y) is V59() Element of K19(COMPLEX)
(dom f) /\ Y is V59() Element of K19(COMPLEX)
s2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g . s2 is V25() Element of COMPLEX
(f | Y) /* g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((f | Y) /* g) . s2 is V25() Element of COMPLEX
(f | Y) /. (g . s2) is V25() Element of COMPLEX
f /. (g . s2) is V25() Element of COMPLEX
f /* g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /* g) . s2 is V25() Element of COMPLEX
f /. (lim g) is V25() Element of COMPLEX
(f | Y) /. (lim g) is V25() Element of COMPLEX
lim (f /* g) is V25() Element of COMPLEX
g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng g is V59() Element of K19(COMPLEX)
lim g is V25() Element of COMPLEX
f /* g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f /. (lim g) is V25() Element of COMPLEX
lim (f /* g) is V25() Element of COMPLEX
f | Y is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom (f | Y) is V59() Element of K19(COMPLEX)
(dom f) /\ Y is V59() Element of K19(COMPLEX)
g is V25() Element of COMPLEX
s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng s2 is V59() Element of K19(COMPLEX)
lim s2 is V25() Element of COMPLEX
q2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s2 . q2 is V25() Element of COMPLEX
(f | Y) /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((f | Y) /* s2) . q2 is V25() Element of COMPLEX
(f | Y) /. (s2 . q2) is V25() Element of COMPLEX
f /. (s2 . q2) is V25() Element of COMPLEX
f /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /* s2) . q2 is V25() Element of COMPLEX
(f | Y) /. (lim s2) is V25() Element of COMPLEX
f /. (lim s2) is V25() Element of COMPLEX
lim ((f | Y) /* s2) is V25() Element of COMPLEX
(f | Y) /. g is V25() Element of COMPLEX
Y is set
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom f is V59() Element of K19(COMPLEX)
g is V25() Element of COMPLEX
f /. g is V25() Element of COMPLEX
s2 is ext-real V25() real Element of REAL
f | Y is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom (f | Y) is V59() Element of K19(COMPLEX)
(f | Y) /. g is V25() Element of COMPLEX
q2 is ext-real V25() real Element of REAL
n is V25() Element of COMPLEX
n - g is V25() Element of COMPLEX
|.(n - g).| is ext-real V25() real Element of REAL
f /. n is V25() Element of COMPLEX
(f /. n) - (f /. g) is V25() Element of COMPLEX
|.((f /. n) - (f /. g)).| is ext-real V25() real Element of REAL
(dom f) /\ Y is V59() Element of K19(COMPLEX)
(f | Y) /. n is V25() Element of COMPLEX
((f | Y) /. n) - (f /. g) is V25() Element of COMPLEX
|.(((f | Y) /. n) - (f /. g)).| is ext-real V25() real Element of REAL
((f | Y) /. n) - ((f | Y) /. g) is V25() Element of COMPLEX
|.(((f | Y) /. n) - ((f | Y) /. g)).| is ext-real V25() real Element of REAL
f | Y is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom (f | Y) is V59() Element of K19(COMPLEX)
(dom f) /\ Y is V59() Element of K19(COMPLEX)
g is V25() Element of COMPLEX
(f | Y) /. g is V25() Element of COMPLEX
s2 is ext-real V25() real Element of REAL
f /. g is V25() Element of COMPLEX
q2 is ext-real V25() real Element of REAL
n is V25() Element of COMPLEX
n - g is V25() Element of COMPLEX
|.(n - g).| is ext-real V25() real Element of REAL
(f | Y) /. n is V25() Element of COMPLEX
((f | Y) /. n) - ((f | Y) /. g) is V25() Element of COMPLEX
|.(((f | Y) /. n) - ((f | Y) /. g)).| is ext-real V25() real Element of REAL
((f | Y) /. n) - (f /. g) is V25() Element of COMPLEX
|.(((f | Y) /. n) - (f /. g)).| is ext-real V25() real Element of REAL
f /. n is V25() Element of COMPLEX
(f /. n) - (f /. g) is V25() Element of COMPLEX
|.((f /. n) - (f /. g)).| is ext-real V25() real Element of REAL
Y is set
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f | Y is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom f is V59() Element of K19(COMPLEX)
(dom f) /\ Y is V59() Element of K19(COMPLEX)
dom (f | Y) is V59() Element of K19(COMPLEX)
(f | Y) | Y is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
g is V25() Element of COMPLEX
dom (f | Y) is V59() Element of K19(COMPLEX)
dom f is V59() Element of K19(COMPLEX)
(dom f) /\ Y is V59() Element of K19(COMPLEX)
g is V25() Element of COMPLEX
(f | Y) | Y is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
Y is set
f is set
g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom g is V59() Element of K19(COMPLEX)
g | f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
s2 is V25() Element of COMPLEX
g | Y is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
(dom g) /\ f is V59() Element of K19(COMPLEX)
(dom g) /\ Y is V59() Element of K19(COMPLEX)
dom (g | f) is V59() Element of K19(COMPLEX)
dom (g | Y) is V59() Element of K19(COMPLEX)
(g | f) /. s2 is V25() Element of COMPLEX
(g | Y) /. s2 is V25() Element of COMPLEX
g /. s2 is V25() Element of COMPLEX
q2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng q2 is V59() Element of K19(COMPLEX)
lim q2 is V25() Element of COMPLEX
(g | f) /* q2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((g | f) /* q2) is V25() Element of COMPLEX
n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
q2 . n is V25() Element of COMPLEX
(g | Y) /* q2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((g | Y) /* q2) . n is V25() Element of COMPLEX
(g | Y) /. (q2 . n) is V25() Element of COMPLEX
g /. (q2 . n) is V25() Element of COMPLEX
(g | f) /. (q2 . n) is V25() Element of COMPLEX
((g | f) /* q2) . n is V25() Element of COMPLEX
lim ((g | Y) /* q2) is V25() Element of COMPLEX
Y is V25() Element of COMPLEX
{Y} is non empty V59() set
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom f is V59() Element of K19(COMPLEX)
g is set
f | {Y} is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
g is V25() Element of COMPLEX
(dom f) /\ {Y} is V59() Element of K19(COMPLEX)
dom (f | {Y}) is V59() Element of K19(COMPLEX)
(f | {Y}) /. g is V25() Element of COMPLEX
s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng s2 is V59() Element of K19(COMPLEX)
lim s2 is V25() Element of COMPLEX
(f | {Y}) /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((f | {Y}) /* s2) is V25() Element of COMPLEX
q2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s2 . q2 is V25() Element of COMPLEX
q2 is ext-real V25() real Element of REAL
n is Function-like functional empty ext-real non negative V18() V19() V20() V22() V23() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT
s is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
((f | {Y}) /* s2) . s is V25() Element of COMPLEX
(((f | {Y}) /* s2) . s) - ((f | {Y}) /. g) is V25() Element of COMPLEX
|.((((f | {Y}) /* s2) . s) - ((f | {Y}) /. g)).| is ext-real V25() real Element of REAL
s2 . s is V25() Element of COMPLEX
(f | {Y}) /. (s2 . s) is V25() Element of COMPLEX
(f | {Y}) /. Y is V25() Element of COMPLEX
((f | {Y}) /. (s2 . s)) - ((f | {Y}) /. Y) is V25() Element of COMPLEX
|.(((f | {Y}) /. (s2 . s)) - ((f | {Y}) /. Y)).| is ext-real V25() real Element of REAL
((f | {Y}) /. Y) - ((f | {Y}) /. Y) is V25() Element of COMPLEX
|.(((f | {Y}) /. Y) - ((f | {Y}) /. Y)).| is ext-real V25() real Element of REAL
Y is set
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f + g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f - g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
- g is V1() V4( COMPLEX ) Function-like complex-valued set
K63(1) is ext-real non positive V25() real set
K63(1) (#) g is V1() V4( COMPLEX ) Function-like complex-valued set
f + (- g) is V1() V4( COMPLEX ) Function-like complex-valued set
f (#) g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom f is V59() Element of K19(COMPLEX)
dom g is V59() Element of K19(COMPLEX)
(dom f) /\ (dom g) is V59() Element of K19(COMPLEX)
dom (f + g) is V59() Element of K19(COMPLEX)
s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng s2 is V59() Element of K19(COMPLEX)
lim s2 is V25() Element of COMPLEX
f /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /* s2) + (g /* s2) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f /. (lim s2) is V25() Element of COMPLEX
lim (f /* s2) is V25() Element of COMPLEX
g /. (lim s2) is V25() Element of COMPLEX
lim (g /* s2) is V25() Element of COMPLEX
(f + g) /. (lim s2) is V25() Element of COMPLEX
(lim (f /* s2)) + (lim (g /* s2)) is V25() Element of COMPLEX
lim ((f /* s2) + (g /* s2)) is V25() Element of COMPLEX
(f + g) /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((f + g) /* s2) is V25() Element of COMPLEX
dom (f - g) is V59() Element of K19(COMPLEX)
s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng s2 is V59() Element of K19(COMPLEX)
lim s2 is V25() Element of COMPLEX
f /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /* s2) - (g /* s2) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
- (g /* s2) is V1() V4( NAT ) Function-like total complex-valued set
K63(1) (#) (g /* s2) is V1() V4( NAT ) Function-like total complex-valued set
(f /* s2) + (- (g /* s2)) is V1() V4( NAT ) Function-like total complex-valued set
f /. (lim s2) is V25() Element of COMPLEX
lim (f /* s2) is V25() Element of COMPLEX
g /. (lim s2) is V25() Element of COMPLEX
lim (g /* s2) is V25() Element of COMPLEX
(f - g) /. (lim s2) is V25() Element of COMPLEX
(lim (f /* s2)) - (lim (g /* s2)) is V25() Element of COMPLEX
lim ((f /* s2) - (g /* s2)) is V25() Element of COMPLEX
(f - g) /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((f - g) /* s2) is V25() Element of COMPLEX
dom (f (#) g) is V59() Element of K19(COMPLEX)
s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng s2 is V59() Element of K19(COMPLEX)
lim s2 is V25() Element of COMPLEX
f /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(f /* s2) (#) (g /* s2) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
f /. (lim s2) is V25() Element of COMPLEX
lim (f /* s2) is V25() Element of COMPLEX
g /. (lim s2) is V25() Element of COMPLEX
lim (g /* s2) is V25() Element of COMPLEX
(f (#) g) /. (lim s2) is V25() Element of COMPLEX
(lim (f /* s2)) * (lim (g /* s2)) is V25() Element of COMPLEX
lim ((f /* s2) (#) (g /* s2)) is V25() Element of COMPLEX
(f (#) g) /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((f (#) g) /* s2) is V25() Element of COMPLEX
Y is set
f is set
Y /\ f is set
g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
s2 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
g + s2 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
g - s2 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
- s2 is V1() V4( COMPLEX ) Function-like complex-valued set
K63(1) is ext-real non positive V25() real set
K63(1) (#) s2 is V1() V4( COMPLEX ) Function-like complex-valued set
g + (- s2) is V1() V4( COMPLEX ) Function-like complex-valued set
g (#) s2 is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
Y is V25() Element of COMPLEX
f is set
g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
Y (#) g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom g is V59() Element of K19(COMPLEX)
dom (Y (#) g) is V59() Element of K19(COMPLEX)
s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng s2 is V59() Element of K19(COMPLEX)
lim s2 is V25() Element of COMPLEX
g /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Y (#) (g /* s2) is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
g /. (lim s2) is V25() Element of COMPLEX
lim (g /* s2) is V25() Element of COMPLEX
(Y (#) g) /. (lim s2) is V25() Element of COMPLEX
Y * (lim (g /* s2)) is V25() Element of COMPLEX
lim (Y (#) (g /* s2)) is V25() Element of COMPLEX
(Y (#) g) /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((Y (#) g) /* s2) is V25() Element of COMPLEX
Y is set
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
- f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
K63(1) is ext-real non positive V25() real set
K63(1) (#) f is V1() V4( COMPLEX ) Function-like complex-valued set
(- 1r) (#) f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
Y is set
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f " {0} is V59() Element of K19(COMPLEX)
f ^ is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom (f ^) is V59() Element of K19(COMPLEX)
dom f is V59() Element of K19(COMPLEX)
(dom f) \ {} is V59() Element of K19(COMPLEX)
(f ^) | Y is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
g is V25() Element of COMPLEX
f | Y is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
(dom (f ^)) /\ Y is V59() Element of K19(COMPLEX)
dom ((f ^) | Y) is V59() Element of K19(COMPLEX)
s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng s2 is V59() Element of K19(COMPLEX)
lim s2 is V25() Element of COMPLEX
dom (f | Y) is V59() Element of K19(COMPLEX)
(f | Y) /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
q2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s2 . q2 is V25() Element of COMPLEX
(dom f) /\ Y is V59() Element of K19(COMPLEX)
f /. (s2 . q2) is V25() Element of COMPLEX
{0c} is non empty V59() V60() V61() V62() V63() V64() set
((f | Y) /* s2) . q2 is V25() Element of COMPLEX
(f | Y) /. (s2 . q2) is V25() Element of COMPLEX
(f | Y) /. g is V25() Element of COMPLEX
f /. g is V25() Element of COMPLEX
q2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
s2 . q2 is V25() Element of COMPLEX
((f ^) | Y) /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(((f ^) | Y) /* s2) . q2 is V25() Element of COMPLEX
((f ^) | Y) /. (s2 . q2) is V25() Element of COMPLEX
(f ^) /. (s2 . q2) is V25() Element of COMPLEX
f /. (s2 . q2) is V25() Element of COMPLEX
(f /. (s2 . q2)) " is V25() Element of COMPLEX
(f | Y) /. (s2 . q2) is V25() Element of COMPLEX
((f | Y) /. (s2 . q2)) " is V25() Element of COMPLEX
((f | Y) /* s2) . q2 is V25() Element of COMPLEX
(((f | Y) /* s2) . q2) " is V25() Element of COMPLEX
((f | Y) /* s2) " is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(((f | Y) /* s2) ") . q2 is V25() Element of COMPLEX
lim ((f | Y) /* s2) is V25() Element of COMPLEX
lim (((f ^) | Y) /* s2) is V25() Element of COMPLEX
((f | Y) /. g) " is V25() Element of COMPLEX
(f /. g) " is V25() Element of COMPLEX
(f ^) /. g is V25() Element of COMPLEX
((f ^) | Y) /. g is V25() Element of COMPLEX
Y is set
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f | Y is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
(f | Y) " {0} is V59() Element of K19(COMPLEX)
f ^ is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
(f | Y) ^ is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
(f ^) | Y is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
Y is set
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f " {0} is V59() Element of K19(COMPLEX)
g is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
g / f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
f ^ is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
g (#) (f ^) is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
Y is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom Y is V59() Element of K19(COMPLEX)
f is V25() Element of COMPLEX
f is V25() Element of COMPLEX
Y /. f is V25() Element of COMPLEX
(Y /. f) + 0c is V25() Element of COMPLEX
f + 0c is V25() Element of COMPLEX
Y /. (f + 0c) is V25() Element of COMPLEX
Y /. 0c is V25() Element of COMPLEX
(Y /. f) + (Y /. 0c) is V25() Element of COMPLEX
g is V25() Element of COMPLEX
- g is V25() Element of COMPLEX
g + (- g) is V25() Element of COMPLEX
Y /. (g + (- g)) is V25() Element of COMPLEX
Y /. g is V25() Element of COMPLEX
Y /. (- g) is V25() Element of COMPLEX
(Y /. g) + (Y /. (- g)) is V25() Element of COMPLEX
- (Y /. g) is V25() Element of COMPLEX
g is V25() Element of COMPLEX
s2 is V25() Element of COMPLEX
g - s2 is V25() Element of COMPLEX
Y /. (g - s2) is V25() Element of COMPLEX
- s2 is V25() Element of COMPLEX
g + (- s2) is V25() Element of COMPLEX
Y /. (g + (- s2)) is V25() Element of COMPLEX
Y /. g is V25() Element of COMPLEX
Y /. (- s2) is V25() Element of COMPLEX
(Y /. g) + (Y /. (- s2)) is V25() Element of COMPLEX
Y /. s2 is V25() Element of COMPLEX
- (Y /. s2) is V25() Element of COMPLEX
(Y /. g) + (- (Y /. s2)) is V25() Element of COMPLEX
(Y /. g) - (Y /. s2) is V25() Element of COMPLEX
g is V25() Element of COMPLEX
s2 is ext-real V25() real Element of REAL
g - f is V25() Element of COMPLEX
n is ext-real V25() real Element of REAL
s is ext-real V25() real Element of REAL
x2 is V25() Element of COMPLEX
x2 - g is V25() Element of COMPLEX
|.(x2 - g).| is ext-real V25() real Element of REAL
x2 - (g - f) is V25() Element of COMPLEX
(x2 - (g - f)) - f is V25() Element of COMPLEX
|.((x2 - (g - f)) - f).| is ext-real V25() real Element of REAL
(g - f) + f is V25() Element of COMPLEX
Y /. x2 is V25() Element of COMPLEX
Y /. g is V25() Element of COMPLEX
(Y /. x2) - (Y /. g) is V25() Element of COMPLEX
|.((Y /. x2) - (Y /. g)).| is ext-real V25() real Element of REAL
Y /. (g - f) is V25() Element of COMPLEX
(Y /. (g - f)) + (Y /. f) is V25() Element of COMPLEX
(Y /. x2) - ((Y /. (g - f)) + (Y /. f)) is V25() Element of COMPLEX
|.((Y /. x2) - ((Y /. (g - f)) + (Y /. f))).| is ext-real V25() real Element of REAL
(Y /. x2) - (Y /. (g - f)) is V25() Element of COMPLEX
((Y /. x2) - (Y /. (g - f))) - (Y /. f) is V25() Element of COMPLEX
|.(((Y /. x2) - (Y /. (g - f))) - (Y /. f)).| is ext-real V25() real Element of REAL
Y /. (x2 - (g - f)) is V25() Element of COMPLEX
(Y /. (x2 - (g - f))) - (Y /. f) is V25() Element of COMPLEX
|.((Y /. (x2 - (g - f))) - (Y /. f)).| is ext-real V25() real Element of REAL
Y is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom Y is V59() Element of K19(COMPLEX)
rng Y is V59() Element of K19(COMPLEX)
f is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng f is V59() Element of K19(COMPLEX)
g is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
f . g is V25() set
f . g is V25() Element of COMPLEX
s2 is V25() Element of COMPLEX
Y . s2 is V25() set
Y /. s2 is V25() Element of COMPLEX
g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
s2 is set
rng g is V59() Element of K19(COMPLEX)
q2 is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g . q2 is V25() Element of COMPLEX
s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim s2 is V25() Element of COMPLEX
Y /* s2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
rng s2 is V59() Element of K19(COMPLEX)
n is ext-real non negative V18() V19() V20() V24() V25() real V45() V58() V59() V60() V61() V62() V63() V64() Element of NAT
g . n is V25() Element of COMPLEX
Y /. (g . n) is V25() Element of COMPLEX
f . n is V25() Element of COMPLEX
Y /* g is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(Y /* g) . n is V25() Element of COMPLEX
Y | (dom Y) is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
Y /. (lim s2) is V25() Element of COMPLEX
lim (Y /* s2) is V25() Element of COMPLEX
Y . (lim s2) is V25() set
q2 is V1() V4( NAT ) V5( COMPLEX ) Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
lim q2 is V25() Element of COMPLEX
Y is V59() Element of K19(COMPLEX)
f is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom f is V59() Element of K19(COMPLEX)
f .: Y is V59() Element of K19(COMPLEX)
f | Y is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
dom (f | Y) is V59() Element of K19(COMPLEX)
(dom f) /\ Y is V59() Element of K19(COMPLEX)
(f | Y) | Y is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like complex-valued Element of K19(K20(COMPLEX,COMPLEX))
g is V25() Element of COMPLEX
rng (f | Y) is V59() Element of K19(COMPLEX)