:: FDIFF_1 semantic presentation

REAL is non empty V12() V57() V58() V59() V63() V64() V74() set

NAT is non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() Element of K19(REAL)

K19(REAL) is non empty V12() V64() V74() set

COMPLEX is non empty V12() V57() V63() V64() V74() set

K20(REAL,REAL) is V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() set

K19(K20(REAL,REAL)) is non empty V12() V64() V74() set

RAT is non empty V12() V57() V58() V59() V60() V63() V64() V74() set

INT is non empty V12() V57() V58() V59() V60() V61() V63() V64() V74() set

K20(COMPLEX,COMPLEX) is V1() non empty V12() complex-valued V64() V74() set

K19(K20(COMPLEX,COMPLEX)) is non empty V12() V64() V74() set

K20(K20(COMPLEX,COMPLEX),COMPLEX) is V1() non empty V12() complex-valued V64() V74() set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is non empty V12() V64() V74() set

K20(K20(REAL,REAL),REAL) is V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() set

K19(K20(K20(REAL,REAL),REAL)) is non empty V12() V64() V74() set

K20(RAT,RAT) is V1() V5( RAT ) non empty V12() complex-valued ext-real-valued real-valued V64() V74() set

K19(K20(RAT,RAT)) is non empty V12() V64() V74() set

K20(K20(RAT,RAT),RAT) is V1() V5( RAT ) non empty V12() complex-valued ext-real-valued real-valued V64() V74() set

K19(K20(K20(RAT,RAT),RAT)) is non empty V12() V64() V74() set

K20(INT,INT) is V1() V5( RAT ) V5( INT ) non empty V12() complex-valued ext-real-valued real-valued V64() V74() set

K19(K20(INT,INT)) is non empty V12() V64() V74() set

K20(K20(INT,INT),INT) is V1() V5( RAT ) V5( INT ) non empty V12() complex-valued ext-real-valued real-valued V64() V74() set

K19(K20(K20(INT,INT),INT)) is non empty V12() V64() V74() set

K20(NAT,NAT) is V1() V5( RAT ) V5( INT ) non empty V12() complex-valued ext-real-valued real-valued natural-valued V64() V74() set

K20(K20(NAT,NAT),NAT) is V1() V5( RAT ) V5( INT ) non empty V12() complex-valued ext-real-valued real-valued natural-valued V64() V74() set

K19(K20(K20(NAT,NAT),NAT)) is non empty V12() V64() V74() set

omega is non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() set

K19(omega) is non empty V12() V64() V74() set

K19(NAT) is non empty V12() V64() V74() set

{} is set

the V1() non-zero V3() V5( RAT ) V6() V7() constant V9() empty V12() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Function-yielding V50() V57() V58() V59() V60() V61() V62() V63() V64() V65() V68() V76() V78( {} ) set is V1() non-zero V3() V5( RAT ) V6() V7() constant V9() empty V12() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Function-yielding V50() V57() V58() V59() V60() V61() V62() V63() V64() V65() V68() V76() V78( {} ) set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

K20(NAT,REAL) is V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() set

K19(K20(NAT,REAL)) is non empty V12() V64() V74() set

cs is V57() V58() V59() Element of K19(REAL)

cf is set

Z is set

cf is V22() real ext-real Element of REAL

cs is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

cf is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

cf + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

(cf + 1) " is non empty V22() real ext-real positive non negative Element of REAL

1 / (cf + 1) is V22() real ext-real non negative Element of REAL

cs . cf is V22() real ext-real Element of REAL

lim cs is V22() real ext-real Element of REAL

cs is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ( 0 ) Element of K19(K20(NAT,REAL))

lim cs is V22() real ext-real Element of REAL

cs is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

NAT --> 0 is V1() V4( REAL ) V4( NAT ) V5( NAT ) V5( RAT ) V5( INT ) V6() constant non empty total T-Sequence-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(REAL,NAT))

K20(REAL,NAT) is V1() V5( RAT ) V5( INT ) non empty V12() complex-valued ext-real-valued real-valued natural-valued V64() V74() set

K19(K20(REAL,NAT)) is non empty V12() V64() V74() set

REAL --> 0 is V1() V4( REAL ) V5( NAT ) V5( RAT ) V5( INT ) V6() constant non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(REAL,NAT))

cf is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

Z is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

dom Z is non empty V57() V58() V59() Element of K19(REAL)

f is V1() non-zero V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent ( 0 ) Element of K19(K20(NAT,REAL))

rng f is non empty V57() V58() V59() V73() V74() Element of K19(REAL)

c

f " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

Z /* f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(f ") (#) (Z /* f) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((f ") (#) (Z /* f)) . c

(f ") . c

(Z /* f) . c

((f ") . c

f . c

Z . (f . c

((f ") . c

((f ") . c

((f ") (#) (Z /* f)) . 0 is V22() real ext-real Element of REAL

lim ((f ") (#) (Z /* f)) is V22() real ext-real Element of REAL

f is V1() non-zero V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent ( 0 ) Element of K19(K20(NAT,REAL))

f " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

Z /* f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(f ") (#) (Z /* f) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

c

c

Z /* c

(c

lim ((c

Z is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

dom Z is V57() V58() V59() Element of K19(REAL)

f is set

f is V22() real ext-real Element of REAL

Z . f is V22() real ext-real Element of REAL

1 * f is V22() real ext-real Element of REAL

Z is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

Z + f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

Z - f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

- f is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set

- 1 is V22() real ext-real non positive set

(- 1) (#) f is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set

Z + (- f) is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set

c

R is V22() real ext-real Element of REAL

L is V22() real ext-real Element of REAL

(Z + f) . L is V22() real ext-real Element of REAL

Z . L is V22() real ext-real Element of REAL

f . L is V22() real ext-real Element of REAL

(Z . L) + (f . L) is V22() real ext-real Element of REAL

c

(c

R * L is V22() real ext-real Element of REAL

(c

c

(c

L is V22() real ext-real Element of REAL

(Z - f) . L is V22() real ext-real Element of REAL

Z . L is V22() real ext-real Element of REAL

f . L is V22() real ext-real Element of REAL

(Z . L) - (f . L) is V22() real ext-real Element of REAL

c

(c

R * L is V22() real ext-real Element of REAL

(c

c

(c

Z is V22() real ext-real Element of REAL

f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

Z (#) f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

c

R is V22() real ext-real Element of REAL

(Z (#) f) . R is V22() real ext-real Element of REAL

f . R is V22() real ext-real Element of REAL

Z * (f . R) is V22() real ext-real Element of REAL

c

Z * (c

Z * c

(Z * c

Z is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

Z + f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

Z - f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

- f is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set

- 1 is V22() real ext-real non positive set

(- 1) (#) f is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set

Z + (- f) is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set

Z (#) f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

c

c

(Z + f) /* c

(c

Z /* c

f /* c

(Z /* c

(c

(c

(c

((c

lim ((c

lim ((c

lim ((c

0 + 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

c

c

(Z - f) /* c

(c

Z /* c

f /* c

(Z /* c

- (f /* c

(- 1) (#) (f /* c

(Z /* c

(c

(c

(c

((c

- ((c

(- 1) (#) ((c

((c

lim ((c

lim ((c

lim ((c

0 - 0 is V22() real ext-real Element of REAL

c

c

f /* c

(c

Z /* c

(c

c

lim ((c

lim c

lim (c

0 * 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

(Z (#) f) /* c

(c

(Z /* c

((Z /* c

c

((Z /* c

((Z /* c

c

(((Z /* c

(c

(((Z /* c

(c

((c

(((Z /* c

(Z /* c

(c

(c

((c

(c

lim ((c

lim ((c

Z is V22() real ext-real Element of REAL

f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

Z (#) f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

c

c

(Z (#) f) /* c

(c

f /* c

Z (#) (f /* c

(c

(c

Z (#) ((c

lim ((c

lim ((c

Z * 0 is V22() real ext-real Element of REAL

Z is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

Z (#) f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

c

R is V22() real ext-real Element of REAL

L is V1() non-zero V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent ( 0 ) Element of K19(K20(NAT,REAL))

L is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

L . L is V22() real ext-real Element of REAL

L " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(Z (#) f) /* L is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(L ") (#) ((Z (#) f) /* L) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((L ") (#) ((Z (#) f) /* L)) . L is V22() real ext-real Element of REAL

(L ") . L is V22() real ext-real Element of REAL

((Z (#) f) /* L) . L is V22() real ext-real Element of REAL

((L ") . L) * (((Z (#) f) /* L) . L) is V22() real ext-real Element of REAL

(Z (#) f) . (L . L) is V22() real ext-real Element of REAL

((L ") . L) * ((Z (#) f) . (L . L)) is V22() real ext-real Element of REAL

Z . (L . L) is V22() real ext-real Element of REAL

f . (L . L) is V22() real ext-real Element of REAL

(Z . (L . L)) * (f . (L . L)) is V22() real ext-real Element of REAL

((L ") . L) * ((Z . (L . L)) * (f . (L . L))) is V22() real ext-real Element of REAL

((L ") . L) * (Z . (L . L)) is V22() real ext-real Element of REAL

(((L ") . L) * (Z . (L . L))) * (f . (L . L)) is V22() real ext-real Element of REAL

(L . L) " is V22() real ext-real Element of REAL

((L . L) ") * (Z . (L . L)) is V22() real ext-real Element of REAL

(((L . L) ") * (Z . (L . L))) * (f . (L . L)) is V22() real ext-real Element of REAL

(L . L) * c

((L . L) ") * ((L . L) * c

(((L . L) ") * ((L . L) * c

((L . L) ") * (L . L) is V22() real ext-real Element of REAL

(((L . L) ") * (L . L)) * c

((((L . L) ") * (L . L)) * c

1 * c

(1 * c

R * (L . L) is V22() real ext-real Element of REAL

c

c

(c

(c

((c

lim L is V1() non-zero V3() V5( RAT ) V6() V7() constant V9() empty V12() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Function-yielding V50() V57() V58() V59() V60() V61() V62() V63() V64() V65() V68() V76() V78( {} ) Element of REAL

lim ((L ") (#) ((Z (#) f) /* L)) is V22() real ext-real Element of REAL

(c

L is V1() non-zero V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent ( 0 ) Element of K19(K20(NAT,REAL))

L " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(Z (#) f) /* L is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(L ") (#) ((Z (#) f) /* L) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

L is V1() non-zero V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent ( 0 ) Element of K19(K20(NAT,REAL))

L " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(Z (#) f) /* L is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(L ") (#) ((Z (#) f) /* L) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim ((L ") (#) ((Z (#) f) /* L)) is V22() real ext-real Element of REAL

Z is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

Z (#) f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

f (#) Z is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

c

R is V1() non-zero V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent ( 0 ) Element of K19(K20(NAT,REAL))

R " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

Z /* R is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(R ") (#) (Z /* R) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

f /* R is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

L is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

(f /* R) . L is V22() real ext-real Element of REAL

R . L is V22() real ext-real Element of REAL

f . (R . L) is V22() real ext-real Element of REAL

c

c

(c

lim R is V1() non-zero V3() V5( RAT ) V6() V7() constant V9() empty V12() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Function-yielding V50() V57() V58() V59() V60() V61() V62() V63() V64() V65() V68() V76() V78( {} ) Element of REAL

lim (f /* R) is V22() real ext-real Element of REAL

c

(Z (#) f) /* R is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(R ") (#) ((Z (#) f) /* R) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(Z /* R) (#) (f /* R) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(R ") (#) ((Z /* R) (#) (f /* R)) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((R ") (#) (Z /* R)) (#) (f /* R) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim ((R ") (#) (Z /* R)) is V22() real ext-real Element of REAL

lim ((R ") (#) ((Z (#) f) /* R)) is V22() real ext-real Element of REAL

0 * 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

Z is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

f is V22() real ext-real set

dom Z is V57() V58() V59() Element of K19(REAL)

Z . f is V22() real ext-real Element of REAL

c

R is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

R is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

L is V22() real ext-real Element of REAL

R . 1 is V22() real ext-real Element of REAL

L * 1 is V22() real ext-real Element of REAL

c

R is V22() real ext-real Element of REAL

L is open V57() V58() V59() Neighbourhood of f

L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

L . 1 is V22() real ext-real Element of REAL

r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

L is open V57() V58() V59() Neighbourhood of f

L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

L . 1 is V22() real ext-real Element of REAL

r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

L . 1 is V22() real ext-real Element of REAL

r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

x0 is V22() real ext-real Element of REAL

N is open V57() V58() V59() Neighbourhood of f

L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

L . 1 is V22() real ext-real Element of REAL

R is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

N is open V57() V58() V59() Neighbourhood of f

L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

L . 1 is V22() real ext-real Element of REAL

R is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

L . 1 is V22() real ext-real Element of REAL

R is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

p is V22() real ext-real Element of REAL

s1 is open V57() V58() V59() Neighbourhood of f

h is V22() real ext-real set

f - h is V22() real ext-real set

f + h is V22() real ext-real set

].(f - h),(f + h).[ is open V57() V58() V59() Element of K19(REAL)

{ b

2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

M is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

h / (n + 2) is V22() real ext-real Element of REAL

M . n is V22() real ext-real Element of REAL

lim M is V22() real ext-real Element of REAL

n is V1() non-zero V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent ( 0 ) Element of K19(K20(NAT,REAL))

L11 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

n . L11 is V22() real ext-real Element of REAL

L11 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

h / (L11 + 2) is V22() real ext-real Element of REAL

f + (h / (L11 + 2)) is V22() real ext-real Element of REAL

(f + (h / (L11 + 2))) - f is V22() real ext-real Element of REAL

L11 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

(L11 + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

h / 1 is V22() real ext-real Element of REAL

- h is V22() real ext-real set

f + (- h) is V22() real ext-real set

p * 1 is V22() real ext-real Element of REAL

x0 * 1 is V22() real ext-real Element of REAL

L11 is V22() real ext-real Element of REAL

Z . L11 is V22() real ext-real Element of REAL

(Z . L11) - (Z . f) is V22() real ext-real Element of REAL

L11 - f is V22() real ext-real Element of REAL

L . (L11 - f) is V22() real ext-real Element of REAL

r . (L11 - f) is V22() real ext-real Element of REAL

(L . (L11 - f)) + (r . (L11 - f)) is V22() real ext-real Element of REAL

L . (L11 - f) is V22() real ext-real Element of REAL

R . (L11 - f) is V22() real ext-real Element of REAL

(L . (L11 - f)) + (R . (L11 - f)) is V22() real ext-real Element of REAL

x0 * (L11 - f) is V22() real ext-real Element of REAL

(x0 * (L11 - f)) + (r . (L11 - f)) is V22() real ext-real Element of REAL

c

(c

R * (L11 - f) is V22() real ext-real Element of REAL

(R * (L11 - f)) + (R . (L11 - f)) is V22() real ext-real Element of REAL

dom R is V57() V58() V59() Element of K19(REAL)

rng n is non empty V57() V58() V59() V73() V74() Element of K19(REAL)

dom r is V57() V58() V59() Element of K19(REAL)

L11 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V64() V76() set

n . L11 is V22() real ext-real Element of REAL

c

r . (n . L11) is V22() real ext-real Element of REAL

(c

R * (n . L11) is V22() real ext-real Element of REAL

R . (n . L11) is V22() real ext-real Element of REAL

(R * (n . L11)) + (R . (n . L11)) is V22() real ext-real Element of REAL

R11 is V22() real ext-real Element of REAL

R11 - f is V22() real ext-real Element of REAL

(c

(r . (n . L11)) / (n . L11) is V22() real ext-real Element of REAL

((c

((R * (n . L11)) + (R . (n . L11))) / (n . L11) is V22() real ext-real Element of REAL

(n . L11) " is V22() real ext-real Element of REAL

(r . (n . L11)) * ((n . L11) ") is V22() real ext-real Element of REAL

n " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(n ") . L11 is V22() real ext-real Element of REAL

(r . (n . L11)) * ((n ") . L11) is V22() real ext-real Element of REAL

r /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(r /* n) . L11 is V22() real ext-real Element of REAL

((r /* n) . L11) * ((n ") . L11) is V22() real ext-real Element of REAL

(n ") (#) (r /* n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((n ") (#) (r /* n)) . L11 is V22() real ext-real Element of REAL

(R . (n . L11)) / (n . L11) is V22() real ext-real Element of REAL

(R . (n . L11)) * ((n . L11) ") is V22() real ext-real Element of REAL

(R . (n . L11)) * ((n ") . L11) is V22() real ext-real Element of REAL

R /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(R /* n) . L11 is V22() real ext-real Element of REAL

((R /* n) . L11) * ((n ") . L11) is V22() real ext-real Element of REAL

(n ") (#) (R /* n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((n ") (#) (R /* n)) . L11 is V22() real ext-real Element of REAL

(R * (n . L11)) / (n . L11) is V22() real ext-real Element of REAL

(n . L11) / (n . L11) is V22() real ext-real Element of REAL

R * ((n . L11) / (n . L11)) is V22() real ext-real Element of REAL

R * 1 is V22() real ext-real Element of REAL

c

c

c

R + ((R . (n . L11)) / (n . L11)) is V22() real ext-real Element of REAL

(((n ") (#) (R /* n)) . L11) - (((n ") (#) (r /* n)) . L11) is V22() real ext-real Element of REAL

R + ((((n ") (#) (R /* n)) . L11) - (((n ") (#) (r /* n)) . L11)) is V22() real ext-real Element of REAL

c

((n ") (#) (R /* n)) - ((n ") (#) (r /* n)) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

- ((n ") (#) (r /* n)) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set

- 1 is V22() real ext-real non positive set

(- 1) (#) ((n ") (#) (r /* n)) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set

((n ") (#) (R /* n)) + (- ((n ") (#) (r /* n))) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set

(((n ") (#) (R /* n)) - ((n ") (#) (r /* n))) . L11 is V22() real ext-real Element of REAL

(((n ") (#) (R /* n)) - ((n ") (#) (r /* n))) . 1 is V22() real ext-real Element of REAL

lim (((n ") (#) (R /* n)) - ((n ") (#) (r /* n))) is V22() real ext-real Element of REAL

lim ((n ") (#) (R /* n)) is V22() real ext-real Element of REAL

lim ((n ") (#) (r /* n)) is V22() real ext-real Element of REAL

0 - 0 is V22() real ext-real Element of REAL

Z is set

f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

dom f is V57() V58() V59() Element of K19(REAL)

Z is open V57() V58() V59() Element of K19(REAL)

f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

dom f is V57() V58() V59() Element of K19(REAL)

c

f | Z is V1() V4( REAL ) V4(Z) V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

dom (f | Z) is V57() V58() V59() Element of K19(Z)

K19(Z) is set

(f | Z) . c

R is open V57() V58() V59() Neighbourhood of c

f . c

(dom f) /\ Z is V57() V58() V59() Element of K19(REAL)

L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

r is V22() real ext-real Element of REAL

f . r is V22() real ext-real Element of REAL

(f . r) - (f . c

r - c

L . (r - c

L . (r - c

(L . (r - c

(f | Z) . r is V22() real ext-real Element of REAL

((f | Z) . r) - ((f | Z) . c

(f . r) - ((f | Z) . c

f | Z is V1() V4( REAL ) V4(Z) V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

c

R is open V57() V58() V59() Neighbourhood of c

f . c

L is open V57() V58() V59() Neighbourhood of c

L is open V57() V58() V59() Neighbourhood of c

dom (f | Z) is V57() V58() V59() Element of K19(REAL)

(f | Z) . c

(dom f) /\ Z is V57() V58() V59() Element of K19(REAL)

dom (f | Z) is V57() V58() V59() Element of K19(Z)

K19(Z) is set

r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

x0 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

x0 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

N is V22() real ext-real Element of REAL

(f | Z) . N is V22() real ext-real Element of REAL

((f | Z) . N) - ((f | Z) . c

N - c

r . (N - c

x0 . (N - c

(r . (N - c

f . N is V22() real ext-real Element of REAL

(f . N) - (f . c

((f | Z) . N) - (f . c

Z is V57() V58() V59() Element of K19(REAL)

f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

c

f | Z is V1() V4( REAL ) V4(Z) V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

dom (f | Z) is V57() V58() V59() Element of K19(Z)

K19(Z) is set

(f | Z) . c

R is open V57() V58() V59() Neighbourhood of c

L is open V57() V58() V59() Neighbourhood of c

Z is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

f is set

c

dom c

R is set

R is set

R is V22() real ext-real Element of REAL

c

(Z,R) is V22() real ext-real Element of REAL

R is V22() real ext-real Element of REAL

c

(Z,R) is V22() real ext-real Element of REAL

c

dom c

R is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

dom R is V57() V58() V59() Element of K19(REAL)

L is V22() real ext-real Element of REAL

c

(Z,L) is V22() real ext-real Element of REAL

R . L is V22() real ext-real Element of REAL

Z is open V57() V58() V59() Element of K19(REAL)

f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

dom f is V57() V58() V59() Element of K19(REAL)

rng f is V57() V58() V59() Element of K19(REAL)

(f,Z) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

cf is V1() V4( REAL ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

dom cf is non empty V57() V58() V59() Element of K19(REAL)

R is V1() non-zero V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent ( 0 ) Element of K19(K20(NAT,REAL))

rng R is non empty V57() V58() V59() V73() V74() Element of K19(REAL)

L is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V64() V76() set

R " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

cf /* R is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(R ") (#) (cf /* R) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

((R ") (#) (cf /* R)) . L is V22() real ext-real Element of REAL

(R ") . L is V22() real ext-real Element of REAL

(cf /* R) . L is V22() real ext-real Element of REAL

((R ") . L) * ((cf /* R) . L) is V22() real ext-real Element of REAL

R . L is V22() real ext-real Element of REAL

cf . (R . L) is V22() real ext-real Element of REAL

((R ") . L) * (cf . (R . L)) is V22() real ext-real Element of REAL

((R ") . L) * 0 is V22() real ext-real Element of REAL

((R ") (#) (cf /* R)) . 0 is V22() real ext-real Element of REAL

lim ((R ") (#) (cf /* R)) is V22() real ext-real Element of REAL

L is V22() real ext-real Element of REAL

cf . L is V22() real ext-real Element of REAL

0 * L is V22() real ext-real Element of REAL

r is V22() real ext-real Element of REAL

{r} is non empty V12() V57() V58() V59() V64() V78(1) set

x0 is V22() real ext-real Element of REAL

f . x0 is V22() real ext-real Element of REAL

x0 is V22() real ext-real Element of REAL

N is open V57() V58() V59() Neighbourhood of x0

f . x0 is V22() real ext-real Element of REAL

L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

R is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

L is V22() real ext-real Element of REAL

f . L is V22() real ext-real Element of REAL

(f . L) - (f . x0) is V22() real ext-real Element of REAL

L - x0 is V22() real ext-real Element of REAL

L . (L - x0) is V22() real ext-real Element of REAL

R . (L - x0) is V22() real ext-real Element of REAL

(L . (L - x0)) + (R . (L - x0)) is V22() real ext-real Element of REAL

r - (f . x0) is V22() real ext-real Element of REAL

r - r is V22() real ext-real Element of REAL

(L . (L - x0)) + 0 is V22() real ext-real Element of REAL

x0 is V22() real ext-real Element of REAL

(f,Z) . x0 is V22() real ext-real Element of REAL

f . x0 is V22() real ext-real Element of REAL

N is open V57() V58() V59() Neighbourhood of x0

L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

R is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))

N is open V57() V58() V59() Neighbourhood of x0

L is V22() real ext-real Element of REAL

f . L is V22() real ext-real Element of REAL

(f . L) - (f . x0) is V22() real ext-real Element of REAL

L - x0 is V22() real ext-real Element of REAL

L . (L - x0) is V22() real ext-real Element of REAL

R . (L - x0) is V22() real ext-real Element of REAL

(L . (L - x0)) + (R . (L - x0)) is V22() real ext-real Element of REAL

r - (f . x0) is V22() real ext-real Element of REAL

r - r is V22() real ext-real Element of REAL

(L . (L - x0)) + 0 is V22() real ext-real Element of REAL

(f,x0) is V22() real ext-real Element of REAL

L . 1 is V22() real ext-real Element of REAL

Z is V1() non-zero V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent ( 0 ) Element of K19(K20(NAT,REAL))

f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

Z ^\ f is V1() non-zero V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent subsequence of Z

lim Z is V1() non-zero V3() V5( RAT ) V6() V7() constant V9() empty V12() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Function-yielding V50() V57() V58() V59() V60() V61() V62() V63() V64() V65() V68() V76() V78( {} ) Element of REAL

lim (Z ^\ f) is V22() real ext-real Element of REAL

c

Z is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))

dom Z is V57() V58() V59() Element of K19(REAL)

f is V22() real ext-real set

{f} is non empty V12() V57() V58() V59() V64() V78(1) set

(Z,f) is V22() real ext-real Element of REAL

c

Z . f is V22() real ext-real Element of REAL

R is open V57() V58() V59() Neighbourhood of f

L is open V57() V58() V59() Neighbourhood of f

L is V1() non-zero V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent ( 0 ) Element of K19(K20(NAT,REAL))

L " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

r is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total complex-valued ext-real-valued real-valued convergent Element of K19(K20(NAT,REAL))

rng r is non empty V12() V57() V58() V59() V64() V78(1) Element of K19(REAL)

L + r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

rng (L + r) is non empty V57() V58() V59() Element of K19(REAL)

Z /* (L + r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

Z /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

(Z /* (L + r)) - (Z /* r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

- (Z /* r) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set

- 1 is V22() real ext-real non positive set

(- 1) (#) (Z /* r) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set

(Z /* (L + r)) + (- (Z /* r)) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set

(L ") (#) ((Z /* (L + r)) - (Z /* r)) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim ((L ") (#) ((Z /* (L + r)) - (Z /* r))) is V22() real ext-real Element of REAL

x0 is V22() real ext-real set

f - x0 is V22() real ext-real set

f + x0 is V22() real ext-real set

].(f - x0),(f + x0).[ is open V57() V58() V59() Element of K19(REAL)

{ b

f + 0 is V22() real ext-real Element of REAL

f - 0 is V22() real ext-real Element of REAL

N is set

lim r is V22() real ext-real Element of REAL

lim L is V1() non-zero V3() V5( RAT ) V6() V7() constant V9() empty V12() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Function-yielding V50() V57() V58() V59() V60() V61() V62() V63() V64() V65() V68() V76() V78( {} ) Element of REAL

lim (L + r) is V22() real ext-real Element of REAL

0 + f is V22() real ext-real Element of REAL

N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

r ^\ N is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total complex-valued ext-real-valued real-valued convergent subsequence of r

rng (r ^\ N) is non empty V12() V57() V58() V59() V64() V78(1) Element of K19(REAL)

(L + r) ^\ N is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of L + r

rng ((L + r) ^\ N) is non empty V57() V58() V59() Element of K19(REAL)

L is set

L is set

R is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

((L + r) ^\ N) . R is V22() real ext-real Element of REAL

N + 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

N + R is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

(L + r) . (N + R) is V22() real ext-real Element of REAL

((L + r) . (N + R)) - f is V22() real ext-real Element of REAL

abs (((L + r) . (N + R)) - f) is V22() real ext-real Element of REAL

R + N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() Element of NAT

(L + r) . (R + N) is V22() real ext-real Element of REAL

((L + r) . (R + N)) - f is V22() real ext-real Element of REAL

(((L + r) ^\ N) . R) - f is V22() real ext-real Element of REAL

- x0 is V22() real ext-real set

f + (- x0) is V22() real ext-real set

N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56()