:: 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₅ is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V64() V76() set
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₅ is V22() real ext-real Element of REAL
(f ") . c₅ is V22() real ext-real Element of REAL
(Z /* f) . c₅ is V22() real ext-real Element of REAL
((f ") . c₅) * ((Z /* f) . c₅) is V22() real ext-real Element of REAL
f . c₅ is V22() real ext-real Element of REAL
Z . (f . c₅) is V22() real ext-real Element of REAL
((f ") . c₅) * (Z . (f . c₅)) is V22() real ext-real Element of REAL
((f ") . c₅) * 0 is V22() real ext-real Element of REAL
((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₅ 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))
c₅ " 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 /* c₅ 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₅ ") (#) (Z /* c₅) 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 ((c₅ ") (#) (Z /* c₅)) 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))
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₅ is V22() real ext-real Element of REAL
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₅ * L is V22() real ext-real Element of REAL
(c₅ * L) + (f . L) is V22() real ext-real Element of REAL
R * L is V22() real ext-real Element of REAL
(c₅ * L) + (R * L) is V22() real ext-real Element of REAL
c₅ + R is V22() real ext-real Element of REAL
(c₅ + R) * L 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₅ * L is V22() real ext-real Element of REAL
(c₅ * L) - (f . L) is V22() real ext-real Element of REAL
R * L is V22() real ext-real Element of REAL
(c₅ * L) - (R * L) is V22() real ext-real Element of REAL
c₅ - R is V22() real ext-real Element of REAL
(c₅ - R) * L is V22() real ext-real Element of REAL
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₅ is V22() real ext-real Element of REAL
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₅ * R is V22() real ext-real Element of REAL
Z * (c₅ * R) is V22() real ext-real Element of REAL
Z * c₅ is V22() real ext-real Element of REAL
(Z * c₅) * R 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
Z (#) f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
c₅ 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))
c₅ " 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) /* c₅ 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₅ ") (#) ((Z + f) /* c₅) 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 /* c₅ 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 /* c₅ 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 /* c₅) + (f /* c₅) 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₅ ") (#) ((Z /* c₅) + (f /* c₅)) 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₅ ") (#) (Z /* c₅) 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₅ ") (#) (f /* c₅) 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₅ ") (#) (Z /* c₅)) + ((c₅ ") (#) (f /* c₅)) 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 ((c₅ ") (#) (Z /* c₅)) is V22() real ext-real Element of REAL
lim ((c₅ ") (#) (f /* c₅)) is V22() real ext-real Element of REAL
lim ((c₅ ") (#) ((Z + f) /* c₅)) 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
c₅ 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))
c₅ " 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) /* c₅ 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₅ ") (#) ((Z - f) /* c₅) 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 /* c₅ 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 /* c₅ 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 /* c₅) - (f /* c₅) 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 /* c₅) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(- 1) (#) (f /* c₅) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(Z /* c₅) + (- (f /* c₅)) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(c₅ ") (#) ((Z /* c₅) - (f /* c₅)) 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₅ ") (#) (Z /* c₅) 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₅ ") (#) (f /* c₅) 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₅ ") (#) (Z /* c₅)) - ((c₅ ") (#) (f /* c₅)) 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₅ ") (#) (f /* c₅)) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(- 1) (#) ((c₅ ") (#) (f /* c₅)) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
((c₅ ") (#) (Z /* c₅)) + (- ((c₅ ") (#) (f /* c₅))) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
lim ((c₅ ") (#) (Z /* c₅)) is V22() real ext-real Element of REAL
lim ((c₅ ") (#) (f /* c₅)) is V22() real ext-real Element of REAL
lim ((c₅ ") (#) ((Z - f) /* c₅)) is V22() real ext-real Element of REAL
0 - 0 is V22() real ext-real Element of REAL
c₅ 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))
c₅ " 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 /* c₅ 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₅ ") (#) (f /* c₅) 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 /* c₅ 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₅ ") (#) (Z /* c₅) 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₅)) 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 ((c₅ ") (#) (Z /* c₅)) is V22() real ext-real Element of REAL
lim c₅ 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 (c₅ (#) ((c₅ ") (#) (Z /* c₅))) 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 (#) f) /* c₅ 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₅ ") (#) ((Z (#) f) /* c₅) 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 /* c₅) (#) (f /* c₅) 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 /* c₅) (#) (f /* c₅)) /" c₅ 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₅ " is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
((Z /* c₅) (#) (f /* c₅)) (#) (c₅ ") is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
((Z /* c₅) (#) (f /* c₅)) (#) (c₅ ") 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₅ ") 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 /* c₅) (#) (f /* c₅)) (#) (c₅ ")) /" (c₅ (#) (c₅ ")) 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₅ ")) " is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(((Z /* c₅) (#) (f /* c₅)) (#) (c₅ ")) (#) ((c₅ (#) (c₅ ")) ") is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(c₅ ") " 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₅ ") 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 /* c₅) (#) (f /* c₅)) (#) (c₅ ")) (#) (((c₅ ") ") (#) (c₅ ")) 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 /* c₅) (#) ((c₅ ") (#) (f /* c₅)) 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₅ ") (#) (f /* c₅))) 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₅) 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₅ ") (#) (f /* c₅)) 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₅ ") (#) (f /* c₅)) 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 ((c₅ ") (#) (f /* c₅)) is V22() real ext-real Element of REAL
lim ((c₅ ") (#) ((Z (#) f) /* c₅)) is V22() real ext-real Element of REAL
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₅ 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))
c₅ " 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) /* c₅ 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₅ ") (#) ((Z (#) f) /* c₅) 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 /* c₅ 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 /* c₅) 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₅ ") (#) (Z (#) (f /* c₅)) 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₅ ") (#) (f /* c₅) 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 (#) ((c₅ ") (#) (f /* c₅)) 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 ((c₅ ") (#) (f /* c₅)) is V22() real ext-real Element of REAL
lim ((c₅ ") (#) ((Z (#) f) /* c₅)) is V22() real ext-real Element of REAL
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₅ is V22() real ext-real Element of REAL
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₅ is V22() real ext-real Element of REAL
((L . L) ") * ((L . L) * c₅) is V22() real ext-real Element of REAL
(((L . L) ") * ((L . L) * c₅)) * (f . (L . L)) is V22() real ext-real Element of REAL
((L . L) ") * (L . L) is V22() real ext-real Element of REAL
(((L . L) ") * (L . L)) * c₅ is V22() real ext-real Element of REAL
((((L . L) ") * (L . L)) * c₅) * (f . (L . L)) is V22() real ext-real Element of REAL
1 * c₅ is V22() real ext-real Element of REAL
(1 * c₅) * (f . (L . L)) is V22() real ext-real Element of REAL
R * (L . L) is V22() real ext-real Element of REAL
c₅ * (R * (L . L)) is V22() real ext-real Element of REAL
c₅ * R is V22() real ext-real Element of REAL
(c₅ * R) * (L . L) is V22() real ext-real Element of REAL
(c₅ * R) (#) 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))
((c₅ * R) (#) L) . L 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 ") (#) ((Z (#) f) /* L)) is V22() real ext-real Element of REAL
(c₅ * R) * 0 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 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₅ is V22() real ext-real Element of 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))
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₅ * (R . L) is V22() real ext-real Element of REAL
c₅ (#) 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))
(c₅ (#) R) . L is V22() real ext-real Element of REAL
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₅ * 0 is V22() real ext-real Element of REAL
(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₅ is open V57() V58() V59() Neighbourhood of f
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₅ is V22() real ext-real Element of REAL
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₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= f - h & not f + h <= b₁ ) } is set
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₅ * (L11 - f) is V22() real ext-real Element of REAL
(c₅ * (L11 - f)) + (r . (L11 - f)) is V22() real ext-real Element of REAL
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₅ * (n . L11) is V22() real ext-real Element of REAL
r . (n . L11) is V22() real ext-real Element of REAL
(c₅ * (n . L11)) + (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) 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₅ * (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
((c₅ * (n . L11)) / (n . L11)) + ((r . (n . L11)) / (n . L11)) is V22() real ext-real Element of REAL
((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₅ * ((n . L11) / (n . L11)) is V22() real ext-real Element of REAL
c₅ * 1 is V22() real ext-real Element of REAL
c₅ + ((r . (n . L11)) / (n . L11)) is V22() real ext-real Element of REAL
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₅ - R is V22() real ext-real Element of REAL
((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₅ is V22() real ext-real Element of REAL
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₅ is V22() real ext-real Element of REAL
R is open V57() V58() V59() Neighbourhood of c₅
f . c₅ is V22() real ext-real Element of REAL
(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₅) is V22() real ext-real Element of REAL
r - c₅ is V22() real ext-real Element of REAL
L . (r - c₅) is V22() real ext-real Element of REAL
L . (r - c₅) is V22() real ext-real Element of REAL
(L . (r - c₅)) + (L . (r - c₅)) is V22() real ext-real Element of REAL
(f | Z) . r is V22() real ext-real Element of REAL
((f | Z) . r) - ((f | Z) . c₅) is V22() real ext-real Element of REAL
(f . r) - ((f | Z) . c₅) is V22() real ext-real Element of REAL
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₅ is V22() real ext-real Element of REAL
R is open V57() V58() V59() Neighbourhood of c₅
f . c₅ is V22() real ext-real Element of REAL
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₅ is V22() real ext-real Element of REAL
(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₅) is V22() real ext-real Element of REAL
N - c₅ is V22() real ext-real Element of REAL
r . (N - c₅) is V22() real ext-real Element of REAL
x0 . (N - c₅) is V22() real ext-real Element of REAL
(r . (N - c₅)) + (x0 . (N - c₅)) is V22() real ext-real Element of REAL
f . N is V22() real ext-real Element of REAL
(f . N) - (f . c₅) is V22() real ext-real Element of REAL
((f | Z) . N) - (f . c₅) is V22() real ext-real Element of REAL
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₅ is V22() real ext-real set
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₅ is V22() real ext-real Element of REAL
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₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom c₅ is V57() V58() V59() Element of K19(REAL)
R is set
R is set
R is V22() real ext-real Element of REAL
c₅ . R is V22() real ext-real Element of REAL
(Z,R) is V22() real ext-real Element of REAL
R is V22() real ext-real Element of REAL
c₅ . R is V22() real ext-real Element of REAL
(Z,R) is V22() real ext-real Element of REAL
c₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom c₅ is V57() V58() V59() Element of K19(REAL)
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₅ . L is V22() real ext-real Element of REAL
(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₅ 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 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₅ is open V57() V58() V59() Neighbourhood of f
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₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= f - x0 & not f + x0 <= b₁ ) } is set
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() 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)
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 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))
R is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))
p is set
L ^\ N is V1() non-zero V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent ( 0 ) subsequence of L
L /* (L ^\ 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 /* (L ^\ 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))
(L /* (L ^\ N)) + (R /* (L ^\ 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))
(L ^\ 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))
((L /* (L ^\ N)) + (R /* (L ^\ N))) (#) ((L ^\ 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))
lim (((L /* (L ^\ N)) + (R /* (L ^\ N))) (#) ((L ^\ N) ")) is V22() real ext-real Element of REAL
L . 1 is V22() real ext-real Element of REAL
(R /* (L ^\ N)) (#) ((L ^\ 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))
p 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 ^\ N) ") (#) (R /* (L ^\ 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))
lim (((L ^\ N) ") (#) (R /* (L ^\ N))) is V22() real ext-real Element of REAL
s1 is V22() real ext-real set
h 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
M 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 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
p . n is V22() real ext-real Element of REAL
(p . n) - (L . 1) is V22() real ext-real Element of REAL
abs ((p . n) - (L . 1)) is V22() real ext-real Element of REAL
((R /* (L ^\ N)) (#) ((L ^\ N) ")) . n is V22() real ext-real Element of REAL
(L . 1) + (((R /* (L ^\ N)) (#) ((L ^\ N) ")) . n) is V22() real ext-real Element of REAL
((L . 1) + (((R /* (L ^\ N)) (#) ((L ^\ N) ")) . n)) - (L . 1) is V22() real ext-real Element of REAL
abs (((L . 1) + (((R /* (L ^\ N)) (#) ((L ^\ N) ")) . n)) - (L . 1)) is V22() real ext-real Element of REAL
(((L ^\ N) ") (#) (R /* (L ^\ N))) . n is V22() real ext-real Element of REAL
((((L ^\ N) ") (#) (R /* (L ^\ N))) . n) - 0 is V22() real ext-real Element of REAL
abs (((((L ^\ N) ") (#) (R /* (L ^\ N))) . n) - 0) is V22() real ext-real Element of REAL
s1 is V22() real ext-real Element of REAL
s1 * 1 is V22() real ext-real Element of REAL
h 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 ^\ N) . h is V22() real ext-real Element of REAL
(((L /* (L ^\ N)) + (R /* (L ^\ N))) (#) ((L ^\ N) ")) . h is V22() real ext-real Element of REAL
((L /* (L ^\ N)) + (R /* (L ^\ N))) . h is V22() real ext-real Element of REAL
((L ^\ N) ") . h is V22() real ext-real Element of REAL
(((L /* (L ^\ N)) + (R /* (L ^\ N))) . h) * (((L ^\ N) ") . h) is V22() real ext-real Element of REAL
(L /* (L ^\ N)) . h is V22() real ext-real Element of REAL
(R /* (L ^\ N)) . h is V22() real ext-real Element of REAL
((L /* (L ^\ N)) . h) + ((R /* (L ^\ N)) . h) is V22() real ext-real Element of REAL
(((L /* (L ^\ N)) . h) + ((R /* (L ^\ N)) . h)) * (((L ^\ N) ") . h) is V22() real ext-real Element of REAL
((L /* (L ^\ N)) . h) * (((L ^\ N) ") . h) is V22() real ext-real Element of REAL
((R /* (L ^\ N)) . h) * (((L ^\ N) ") . h) is V22() real ext-real Element of REAL
(((L /* (L ^\ N)) . h) * (((L ^\ N) ") . h)) + (((R /* (L ^\ N)) . h) * (((L ^\ N) ") . h)) is V22() real ext-real Element of REAL
((R /* (L ^\ N)) (#) ((L ^\ N) ")) . h is V22() real ext-real Element of REAL
(((L /* (L ^\ N)) . h) * (((L ^\ N) ") . h)) + (((R /* (L ^\ N)) (#) ((L ^\ N) ")) . h) is V22() real ext-real Element of REAL
((L ^\ N) . h) " is V22() real ext-real Element of REAL
((L /* (L ^\ N)) . h) * (((L ^\ N) . h) ") is V22() real ext-real Element of REAL
(((L /* (L ^\ N)) . h) * (((L ^\ N) . h) ")) + (((R /* (L ^\ N)) (#) ((L ^\ N) ")) . h) is V22() real ext-real Element of REAL
L . ((L ^\ N) . h) is V22() real ext-real Element of REAL
(L . ((L ^\ N) . h)) * (((L ^\ N) . h) ") is V22() real ext-real Element of REAL
((L . ((L ^\ N) . h)) * (((L ^\ N) . h) ")) + (((R /* (L ^\ N)) (#) ((L ^\ N) ")) . h) is V22() real ext-real Element of REAL
s1 * ((L ^\ N) . h) is V22() real ext-real Element of REAL
(s1 * ((L ^\ N) . h)) * (((L ^\ N) . h) ") is V22() real ext-real Element of REAL
((s1 * ((L ^\ N) . h)) * (((L ^\ N) . h) ")) + (((R /* (L ^\ N)) (#) ((L ^\ N) ")) . h) is V22() real ext-real Element of REAL
((L ^\ N) . h) * (((L ^\ N) . h) ") is V22() real ext-real Element of REAL
s1 * (((L ^\ N) . h) * (((L ^\ N) . h) ")) is V22() real ext-real Element of REAL
(s1 * (((L ^\ N) . h) * (((L ^\ N) . h) "))) + (((R /* (L ^\ N)) (#) ((L ^\ N) ")) . h) is V22() real ext-real Element of REAL
(s1 * 1) + (((R /* (L ^\ N)) (#) ((L ^\ N) ")) . h) is V22() real ext-real Element of REAL
p . h is V22() real ext-real Element of REAL
p is set
p is set
p 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) . p is V22() real ext-real Element of REAL
Z . (((L + r) ^\ N) . p) is V22() real ext-real Element of REAL
(r ^\ N) . p is V22() real ext-real Element of REAL
Z . ((r ^\ N) . p) is V22() real ext-real Element of REAL
(Z . (((L + r) ^\ N) . p)) - (Z . ((r ^\ N) . p)) is V22() real ext-real Element of REAL
(L ^\ N) . p is V22() real ext-real Element of REAL
L . ((L ^\ N) . p) is V22() real ext-real Element of REAL
R . ((L ^\ N) . p) is V22() real ext-real Element of REAL
(L . ((L ^\ N) . p)) + (R . ((L ^\ N) . p)) is V22() real ext-real Element of REAL
(((L + r) ^\ N) . p) - ((r ^\ N) . p) is V22() real ext-real Element of REAL
(L ^\ 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))
((L ^\ N) + (r ^\ N)) . p is V22() real ext-real Element of REAL
(((L ^\ N) + (r ^\ N)) . p) - ((r ^\ N) . p) is V22() real ext-real Element of REAL
((L ^\ N) . p) + ((r ^\ N) . p) is V22() real ext-real Element of REAL
(((L ^\ N) . p) + ((r ^\ N) . p)) - ((r ^\ N) . p) is V22() real ext-real Element of REAL
Z /* ((L + 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))
Z /* (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))
(Z /* ((L + r) ^\ N)) - (Z /* (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))
- (Z /* (r ^\ N)) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(- 1) (#) (Z /* (r ^\ N)) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(Z /* ((L + r) ^\ N)) + (- (Z /* (r ^\ N))) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
p 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 /* ((L + r) ^\ N)) - (Z /* (r ^\ N))) . p is V22() real ext-real Element of REAL
(Z /* ((L + r) ^\ N)) . p is V22() real ext-real Element of REAL
(Z /* (r ^\ N)) . p is V22() real ext-real Element of REAL
((Z /* ((L + r) ^\ N)) . p) - ((Z /* (r ^\ N)) . p) is V22() real ext-real Element of REAL
((L + r) ^\ N) . p is V22() real ext-real Element of REAL
Z . (((L + r) ^\ N) . p) is V22() real ext-real Element of REAL
(Z . (((L + r) ^\ N) . p)) - ((Z /* (r ^\ N)) . p) is V22() real ext-real Element of REAL
(r ^\ N) . p is V22() real ext-real Element of REAL
Z . ((r ^\ N) . p) is V22() real ext-real Element of REAL
(Z . (((L + r) ^\ N) . p)) - (Z . ((r ^\ N) . p)) is V22() real ext-real Element of REAL
(L ^\ N) . p is V22() real ext-real Element of REAL
L . ((L ^\ N) . p) is V22() real ext-real Element of REAL
R . ((L ^\ N) . p) is V22() real ext-real Element of REAL
(L . ((L ^\ N) . p)) + (R . ((L ^\ N) . p)) is V22() real ext-real Element of REAL
(L /* (L ^\ N)) . p is V22() real ext-real Element of REAL
((L /* (L ^\ N)) . p) + (R . ((L ^\ N) . p)) is V22() real ext-real Element of REAL
(R /* (L ^\ N)) . p is V22() real ext-real Element of REAL
((L /* (L ^\ N)) . p) + ((R /* (L ^\ N)) . p) is V22() real ext-real Element of REAL
((L /* (L ^\ N)) + (R /* (L ^\ N))) . p is V22() real ext-real Element of REAL
(Z /* (L + r)) ^\ N is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of Z /* (L + r)
((Z /* (L + r)) ^\ N) - (Z /* (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))
((Z /* (L + r)) ^\ N) + (- (Z /* (r ^\ N))) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(((Z /* (L + r)) ^\ N) - (Z /* (r ^\ N))) (#) ((L ^\ 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))
(Z /* r) ^\ N is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of Z /* r
((Z /* (L + r)) ^\ N) - ((Z /* 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))
- ((Z /* r) ^\ N) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(- 1) (#) ((Z /* r) ^\ N) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
((Z /* (L + r)) ^\ N) + (- ((Z /* r) ^\ N)) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(((Z /* (L + r)) ^\ N) - ((Z /* r) ^\ N)) (#) ((L ^\ 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))
((Z /* (L + r)) - (Z /* r)) ^\ N is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (Z /* (L + r)) - (Z /* r)
(((Z /* (L + r)) - (Z /* r)) ^\ N) (#) ((L ^\ 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))
(L ") ^\ N is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of L "
(((Z /* (L + r)) - (Z /* r)) ^\ N) (#) ((L ") ^\ 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))
((Z /* (L + r)) - (Z /* r)) (#) (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 /* (L + r)) - (Z /* r)) (#) (L ")) ^\ N is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of ((Z /* (L + r)) - (Z /* r)) (#) (L ")
p is V22() real ext-real Element of REAL
Z . p is V22() real ext-real Element of REAL
(Z . p) - (Z . f) is V22() real ext-real Element of REAL
p - f is V22() real ext-real Element of REAL
L . (p - f) is V22() real ext-real Element of REAL
R . (p - f) is V22() real ext-real Element of REAL
(L . (p - f)) + (R . (p - f)) is V22() real ext-real Element of REAL
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))
(f,Z) is V22() real ext-real Element of REAL
c₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f + c₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f + c₅),Z) is V22() real ext-real Element of REAL
(c₅,Z) is V22() real ext-real Element of REAL
(f,Z) + (c₅,Z) is V22() real ext-real Element of REAL
dom f is V57() V58() V59() Element of K19(REAL)
f . Z is V22() real ext-real Element of REAL
R is open V57() V58() V59() Neighbourhood of Z
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))
dom c₅ is V57() V58() V59() Element of K19(REAL)
c₅ . Z is V22() real ext-real Element of REAL
r is open V57() V58() V59() Neighbourhood of Z
x0 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))
N 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 V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))
L + N is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
L + x0 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is open V57() V58() V59() Neighbourhood of Z
p /\ p is V57() V58() V59() Element of K19(REAL)
(dom f) /\ (dom c₅) is V57() V58() V59() Element of K19(REAL)
dom (f + c₅) is V57() V58() V59() Element of K19(REAL)
s1 is V22() real ext-real Element of REAL
(f + c₅) . s1 is V22() real ext-real Element of REAL
(f + c₅) . Z is V22() real ext-real Element of REAL
((f + c₅) . s1) - ((f + c₅) . Z) is V22() real ext-real Element of REAL
f . s1 is V22() real ext-real Element of REAL
c₅ . s1 is V22() real ext-real Element of REAL
(f . s1) + (c₅ . s1) is V22() real ext-real Element of REAL
((f . s1) + (c₅ . s1)) - ((f + c₅) . Z) is V22() real ext-real Element of REAL
(f . Z) + (c₅ . Z) is V22() real ext-real Element of REAL
((f . s1) + (c₅ . s1)) - ((f . Z) + (c₅ . Z)) is V22() real ext-real Element of REAL
(f . s1) - (f . Z) is V22() real ext-real Element of REAL
(c₅ . s1) - (c₅ . Z) is V22() real ext-real Element of REAL
((f . s1) - (f . Z)) + ((c₅ . s1) - (c₅ . Z)) is V22() real ext-real Element of REAL
s1 - Z is V22() real ext-real Element of REAL
L . (s1 - Z) is V22() real ext-real Element of REAL
L . (s1 - Z) is V22() real ext-real Element of REAL
(L . (s1 - Z)) + (L . (s1 - Z)) is V22() real ext-real Element of REAL
((L . (s1 - Z)) + (L . (s1 - Z))) + ((c₅ . s1) - (c₅ . Z)) is V22() real ext-real Element of REAL
x0 . (s1 - Z) is V22() real ext-real Element of REAL
N . (s1 - Z) is V22() real ext-real Element of REAL
(x0 . (s1 - Z)) + (N . (s1 - Z)) is V22() real ext-real Element of REAL
((L . (s1 - Z)) + (L . (s1 - Z))) + ((x0 . (s1 - Z)) + (N . (s1 - Z))) is V22() real ext-real Element of REAL
(L . (s1 - Z)) + (x0 . (s1 - Z)) is V22() real ext-real Element of REAL
(L . (s1 - Z)) + (N . (s1 - Z)) is V22() real ext-real Element of REAL
((L . (s1 - Z)) + (x0 . (s1 - Z))) + ((L . (s1 - Z)) + (N . (s1 - Z))) 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))
R . (s1 - Z) is V22() real ext-real Element of REAL
(R . (s1 - Z)) + ((L . (s1 - Z)) + (N . (s1 - Z))) 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))
L . (s1 - Z) is V22() real ext-real Element of REAL
(R . (s1 - Z)) + (L . (s1 - Z)) 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
x0 . 1 is V22() real ext-real Element of REAL
(L . 1) + (x0 . 1) is V22() real ext-real Element of REAL
(f,Z) + (x0 . 1) is V22() real ext-real Element of REAL
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))
(f,Z) is V22() real ext-real Element of REAL
c₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f - c₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- c₅ is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
- 1 is V22() real ext-real non positive set
(- 1) (#) c₅ is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
f + (- c₅) is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
((f - c₅),Z) is V22() real ext-real Element of REAL
(c₅,Z) is V22() real ext-real Element of REAL
(f,Z) - (c₅,Z) is V22() real ext-real Element of REAL
dom f is V57() V58() V59() Element of K19(REAL)
f . Z is V22() real ext-real Element of REAL
R is open V57() V58() V59() Neighbourhood of Z
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))
dom c₅ is V57() V58() V59() Element of K19(REAL)
c₅ . Z is V22() real ext-real Element of REAL
r is open V57() V58() V59() Neighbourhood of Z
x0 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))
N 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 V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))
L - N is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- N is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
(- 1) (#) N is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
L + (- N) is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
L - x0 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 ) V6() complex-valued ext-real-valued real-valued set
(- 1) (#) x0 is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
L + (- x0) is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
p is open V57() V58() V59() Neighbourhood of Z
p /\ p is V57() V58() V59() Element of K19(REAL)
(dom f) /\ (dom c₅) is V57() V58() V59() Element of K19(REAL)
dom (f - c₅) is V57() V58() V59() Element of K19(REAL)
s1 is V22() real ext-real Element of REAL
(f - c₅) . s1 is V22() real ext-real Element of REAL
(f - c₅) . Z is V22() real ext-real Element of REAL
((f - c₅) . s1) - ((f - c₅) . Z) is V22() real ext-real Element of REAL
f . s1 is V22() real ext-real Element of REAL
c₅ . s1 is V22() real ext-real Element of REAL
(f . s1) - (c₅ . s1) is V22() real ext-real Element of REAL
((f . s1) - (c₅ . s1)) - ((f - c₅) . Z) is V22() real ext-real Element of REAL
(f . Z) - (c₅ . Z) is V22() real ext-real Element of REAL
((f . s1) - (c₅ . s1)) - ((f . Z) - (c₅ . Z)) is V22() real ext-real Element of REAL
(f . s1) - (f . Z) is V22() real ext-real Element of REAL
(c₅ . s1) - (c₅ . Z) is V22() real ext-real Element of REAL
((f . s1) - (f . Z)) - ((c₅ . s1) - (c₅ . Z)) is V22() real ext-real Element of REAL
s1 - Z is V22() real ext-real Element of REAL
L . (s1 - Z) is V22() real ext-real Element of REAL
L . (s1 - Z) is V22() real ext-real Element of REAL
(L . (s1 - Z)) + (L . (s1 - Z)) is V22() real ext-real Element of REAL
((L . (s1 - Z)) + (L . (s1 - Z))) - ((c₅ . s1) - (c₅ . Z)) is V22() real ext-real Element of REAL
x0 . (s1 - Z) is V22() real ext-real Element of REAL
N . (s1 - Z) is V22() real ext-real Element of REAL
(x0 . (s1 - Z)) + (N . (s1 - Z)) is V22() real ext-real Element of REAL
((L . (s1 - Z)) + (L . (s1 - Z))) - ((x0 . (s1 - Z)) + (N . (s1 - Z))) is V22() real ext-real Element of REAL
(L . (s1 - Z)) - (x0 . (s1 - Z)) is V22() real ext-real Element of REAL
(L . (s1 - Z)) - (N . (s1 - Z)) is V22() real ext-real Element of REAL
((L . (s1 - Z)) - (x0 . (s1 - Z))) + ((L . (s1 - Z)) - (N . (s1 - Z))) 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))
R . (s1 - Z) is V22() real ext-real Element of REAL
(R . (s1 - Z)) + ((L . (s1 - Z)) - (N . (s1 - Z))) 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))
L . (s1 - Z) is V22() real ext-real Element of REAL
(R . (s1 - Z)) + (L . (s1 - Z)) 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
x0 . 1 is V22() real ext-real Element of REAL
(L . 1) - (x0 . 1) is V22() real ext-real Element of REAL
(f,Z) - (x0 . 1) is V22() real ext-real Element of REAL
Z is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
c₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) c₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f (#) c₅),Z) is V22() real ext-real Element of REAL
(c₅,Z) is V22() real ext-real Element of REAL
f * (c₅,Z) is V22() real ext-real Element of REAL
dom c₅ is V57() V58() V59() Element of K19(REAL)
c₅ . Z is V22() real ext-real Element of REAL
R is open V57() V58() V59() Neighbourhood of Z
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))
f (#) L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f (#) c₅) is V57() V58() V59() Element of K19(REAL)
N is V22() real ext-real Element of REAL
(f (#) c₅) . N is V22() real ext-real Element of REAL
(f (#) c₅) . Z is V22() real ext-real Element of REAL
((f (#) c₅) . N) - ((f (#) c₅) . Z) is V22() real ext-real Element of REAL
c₅ . N is V22() real ext-real Element of REAL
f * (c₅ . N) is V22() real ext-real Element of REAL
(f * (c₅ . N)) - ((f (#) c₅) . Z) is V22() real ext-real Element of REAL
f * (c₅ . Z) is V22() real ext-real Element of REAL
(f * (c₅ . N)) - (f * (c₅ . Z)) is V22() real ext-real Element of REAL
(c₅ . N) - (c₅ . Z) is V22() real ext-real Element of REAL
f * ((c₅ . N) - (c₅ . Z)) is V22() real ext-real Element of REAL
N - Z is V22() real ext-real Element of REAL
L . (N - Z) is V22() real ext-real Element of REAL
L . (N - Z) is V22() real ext-real Element of REAL
(L . (N - Z)) + (L . (N - Z)) is V22() real ext-real Element of REAL
f * ((L . (N - Z)) + (L . (N - Z))) is V22() real ext-real Element of REAL
f * (L . (N - Z)) is V22() real ext-real Element of REAL
f * (L . (N - Z)) is V22() real ext-real Element of REAL
(f * (L . (N - Z))) + (f * (L . (N - Z))) is V22() real ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))
x0 . (N - Z) is V22() real ext-real Element of REAL
(x0 . (N - Z)) + (f * (L . (N - Z))) 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))
r . (N - Z) is V22() real ext-real Element of REAL
(x0 . (N - Z)) + (r . (N - Z)) is V22() real ext-real Element of REAL
x0 . 1 is V22() real ext-real Element of REAL
L . 1 is V22() real ext-real Element of REAL
f * (L . 1) is V22() real ext-real Element of REAL
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))
(f,Z) is V22() real ext-real Element of REAL
f . Z is V22() real ext-real Element of REAL
c₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) c₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f (#) c₅),Z) is V22() real ext-real Element of REAL
c₅ . Z is V22() real ext-real Element of REAL
(c₅ . Z) * (f,Z) is V22() real ext-real Element of REAL
(c₅,Z) is V22() real ext-real Element of REAL
(f . Z) * (c₅,Z) is V22() real ext-real Element of REAL
((c₅ . Z) * (f,Z)) + ((f . Z) * (c₅,Z)) is V22() real ext-real Element of REAL
dom f is V57() V58() V59() Element of K19(REAL)
R is open V57() V58() V59() Neighbourhood of Z
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))
dom c₅ is V57() V58() V59() Element of K19(REAL)
r is open V57() V58() V59() Neighbourhood of Z
x0 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))
N 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 V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))
N (#) L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
L (#) N 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 (#) x0 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
L (#) x0 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p 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))
p + R is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
h is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))
h + L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s1 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))
(f . Z) (#) N is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(c₅ . Z) (#) L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(c₅ . Z) (#) L is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
R11 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))
n is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))
R11 + n is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
R13 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))
R13 + s1 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
R15 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))
M is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))
R15 + M 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 Z
N /\ N is V57() V58() V59() Element of K19(REAL)
(dom f) /\ (dom c₅) is V57() V58() V59() Element of K19(REAL)
dom (f (#) c₅) is V57() V58() V59() Element of K19(REAL)
(f . Z) (#) x0 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
L11 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))
L12 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))
L11 + L12 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x is V22() real ext-real Element of REAL
f . x is V22() real ext-real Element of REAL
(f . x) - (f . Z) is V22() real ext-real Element of REAL
((f . x) - (f . Z)) + (f . Z) is V22() real ext-real Element of REAL
x - Z is V22() real ext-real Element of REAL
L . (x - Z) is V22() real ext-real Element of REAL
L . (x - Z) is V22() real ext-real Element of REAL
(L . (x - Z)) + (L . (x - Z)) is V22() real ext-real Element of REAL
((L . (x - Z)) + (L . (x - Z))) + (f . Z) is V22() real ext-real Element of REAL
(f (#) c₅) . x is V22() real ext-real Element of REAL
(f (#) c₅) . Z is V22() real ext-real Element of REAL
((f (#) c₅) . x) - ((f (#) c₅) . Z) is V22() real ext-real Element of REAL
c₅ . x is V22() real ext-real Element of REAL
(f . x) * (c₅ . x) is V22() real ext-real Element of REAL
((f . x) * (c₅ . x)) - ((f (#) c₅) . Z) is V22() real ext-real Element of REAL
(f . x) * (c₅ . Z) is V22() real ext-real Element of REAL
- ((f . x) * (c₅ . Z)) is V22() real ext-real Element of REAL
((f . x) * (c₅ . x)) + (- ((f . x) * (c₅ . Z))) is V22() real ext-real Element of REAL
(((f . x) * (c₅ . x)) + (- ((f . x) * (c₅ . Z)))) + ((f . x) * (c₅ . Z)) is V22() real ext-real Element of REAL
(f . Z) * (c₅ . Z) is V22() real ext-real Element of REAL
((((f . x) * (c₅ . x)) + (- ((f . x) * (c₅ . Z)))) + ((f . x) * (c₅ . Z))) - ((f . Z) * (c₅ . Z)) is V22() real ext-real Element of REAL
(c₅ . x) - (c₅ . Z) is V22() real ext-real Element of REAL
(f . x) * ((c₅ . x) - (c₅ . Z)) is V22() real ext-real Element of REAL
((f . x) - (f . Z)) * (c₅ . Z) is V22() real ext-real Element of REAL
((f . x) * ((c₅ . x) - (c₅ . Z))) + (((f . x) - (f . Z)) * (c₅ . Z)) is V22() real ext-real Element of REAL
((L . (x - Z)) + (L . (x - Z))) * (c₅ . Z) is V22() real ext-real Element of REAL
((f . x) * ((c₅ . x) - (c₅ . Z))) + (((L . (x - Z)) + (L . (x - Z))) * (c₅ . Z)) is V22() real ext-real Element of REAL
(c₅ . Z) * (L . (x - Z)) is V22() real ext-real Element of REAL
(L . (x - Z)) * (c₅ . Z) is V22() real ext-real Element of REAL
((c₅ . Z) * (L . (x - Z))) + ((L . (x - Z)) * (c₅ . Z)) is V22() real ext-real Element of REAL
((f . x) * ((c₅ . x) - (c₅ . Z))) + (((c₅ . Z) * (L . (x - Z))) + ((L . (x - Z)) * (c₅ . Z))) is V22() real ext-real Element of REAL
L11 . (x - Z) is V22() real ext-real Element of REAL
(c₅ . Z) * (L . (x - Z)) is V22() real ext-real Element of REAL
(L11 . (x - Z)) + ((c₅ . Z) * (L . (x - Z))) is V22() real ext-real Element of REAL
((f . x) * ((c₅ . x) - (c₅ . Z))) + ((L11 . (x - Z)) + ((c₅ . Z) * (L . (x - Z)))) is V22() real ext-real Element of REAL
(((L . (x - Z)) + (L . (x - Z))) + (f . Z)) * ((c₅ . x) - (c₅ . Z)) is V22() real ext-real Element of REAL
R11 . (x - Z) is V22() real ext-real Element of REAL
(L11 . (x - Z)) + (R11 . (x - Z)) is V22() real ext-real Element of REAL
((((L . (x - Z)) + (L . (x - Z))) + (f . Z)) * ((c₅ . x) - (c₅ . Z))) + ((L11 . (x - Z)) + (R11 . (x - Z))) is V22() real ext-real Element of REAL
x0 . (x - Z) is V22() real ext-real Element of REAL
N . (x - Z) is V22() real ext-real Element of REAL
(x0 . (x - Z)) + (N . (x - Z)) is V22() real ext-real Element of REAL
(((L . (x - Z)) + (L . (x - Z))) + (f . Z)) * ((x0 . (x - Z)) + (N . (x - Z))) is V22() real ext-real Element of REAL
((((L . (x - Z)) + (L . (x - Z))) + (f . Z)) * ((x0 . (x - Z)) + (N . (x - Z)))) + ((L11 . (x - Z)) + (R11 . (x - Z))) is V22() real ext-real Element of REAL
((L . (x - Z)) + (L . (x - Z))) * ((x0 . (x - Z)) + (N . (x - Z))) is V22() real ext-real Element of REAL
(f . Z) * (x0 . (x - Z)) is V22() real ext-real Element of REAL
(f . Z) * (N . (x - Z)) is V22() real ext-real Element of REAL
((f . Z) * (x0 . (x - Z))) + ((f . Z) * (N . (x - Z))) is V22() real ext-real Element of REAL
(((L . (x - Z)) + (L . (x - Z))) * ((x0 . (x - Z)) + (N . (x - Z)))) + (((f . Z) * (x0 . (x - Z))) + ((f . Z) * (N . (x - Z)))) is V22() real ext-real Element of REAL
((((L . (x - Z)) + (L . (x - Z))) * ((x0 . (x - Z)) + (N . (x - Z)))) + (((f . Z) * (x0 . (x - Z))) + ((f . Z) * (N . (x - Z))))) + ((L11 . (x - Z)) + (R11 . (x - Z))) is V22() real ext-real Element of REAL
L12 . (x - Z) is V22() real ext-real Element of REAL
(L12 . (x - Z)) + ((f . Z) * (N . (x - Z))) is V22() real ext-real Element of REAL
(((L . (x - Z)) + (L . (x - Z))) * ((x0 . (x - Z)) + (N . (x - Z)))) + ((L12 . (x - Z)) + ((f . Z) * (N . (x - Z)))) is V22() real ext-real Element of REAL
((((L . (x - Z)) + (L . (x - Z))) * ((x0 . (x - Z)) + (N . (x - Z)))) + ((L12 . (x - Z)) + ((f . Z) * (N . (x - Z))))) + ((L11 . (x - Z)) + (R11 . (x - Z))) is V22() real ext-real Element of REAL
n . (x - Z) is V22() real ext-real Element of REAL
(L12 . (x - Z)) + (n . (x - Z)) is V22() real ext-real Element of REAL
(((L . (x - Z)) + (L . (x - Z))) * ((x0 . (x - Z)) + (N . (x - Z)))) + ((L12 . (x - Z)) + (n . (x - Z))) is V22() real ext-real Element of REAL
((((L . (x - Z)) + (L . (x - Z))) * ((x0 . (x - Z)) + (N . (x - Z)))) + ((L12 . (x - Z)) + (n . (x - Z)))) + ((L11 . (x - Z)) + (R11 . (x - Z))) is V22() real ext-real Element of REAL
(R11 . (x - Z)) + (n . (x - Z)) is V22() real ext-real Element of REAL
(L11 . (x - Z)) + ((R11 . (x - Z)) + (n . (x - Z))) is V22() real ext-real Element of REAL
(L12 . (x - Z)) + ((L11 . (x - Z)) + ((R11 . (x - Z)) + (n . (x - Z)))) is V22() real ext-real Element of REAL
(((L . (x - Z)) + (L . (x - Z))) * ((x0 . (x - Z)) + (N . (x - Z)))) + ((L12 . (x - Z)) + ((L11 . (x - Z)) + ((R11 . (x - Z)) + (n . (x - Z))))) is V22() real ext-real Element of REAL
R13 . (x - Z) is V22() real ext-real Element of REAL
(L11 . (x - Z)) + (R13 . (x - Z)) is V22() real ext-real Element of REAL
(L12 . (x - Z)) + ((L11 . (x - Z)) + (R13 . (x - Z))) is V22() real ext-real Element of REAL
(((L . (x - Z)) + (L . (x - Z))) * ((x0 . (x - Z)) + (N . (x - Z)))) + ((L12 . (x - Z)) + ((L11 . (x - Z)) + (R13 . (x - Z)))) is V22() real ext-real Element of REAL
(L11 . (x - Z)) + (L12 . (x - Z)) is V22() real ext-real Element of REAL
((L11 . (x - Z)) + (L12 . (x - Z))) + (R13 . (x - Z)) is V22() real ext-real Element of REAL
(((L . (x - Z)) + (L . (x - Z))) * ((x0 . (x - Z)) + (N . (x - Z)))) + (((L11 . (x - Z)) + (L12 . (x - Z))) + (R13 . (x - Z))) is V22() real ext-real Element of REAL
(L . (x - Z)) * (x0 . (x - Z)) is V22() real ext-real Element of REAL
(L . (x - Z)) * (N . (x - Z)) is V22() real ext-real Element of REAL
((L . (x - Z)) * (x0 . (x - Z))) + ((L . (x - Z)) * (N . (x - Z))) is V22() real ext-real Element of REAL
(L . (x - Z)) * ((x0 . (x - Z)) + (N . (x - Z))) is V22() real ext-real Element of REAL
(((L . (x - Z)) * (x0 . (x - Z))) + ((L . (x - Z)) * (N . (x - Z)))) + ((L . (x - Z)) * ((x0 . (x - Z)) + (N . (x - Z)))) 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))
L . (x - Z) is V22() real ext-real Element of REAL
(L . (x - Z)) + (R13 . (x - Z)) is V22() real ext-real Element of REAL
((((L . (x - Z)) * (x0 . (x - Z))) + ((L . (x - Z)) * (N . (x - Z)))) + ((L . (x - Z)) * ((x0 . (x - Z)) + (N . (x - Z))))) + ((L . (x - Z)) + (R13 . (x - Z))) is V22() real ext-real Element of REAL
s1 . (x - Z) is V22() real ext-real Element of REAL
(N . (x - Z)) * (L . (x - Z)) is V22() real ext-real Element of REAL
(s1 . (x - Z)) + ((N . (x - Z)) * (L . (x - Z))) is V22() real ext-real Element of REAL
((s1 . (x - Z)) + ((N . (x - Z)) * (L . (x - Z)))) + ((L . (x - Z)) * ((x0 . (x - Z)) + (N . (x - Z)))) is V22() real ext-real Element of REAL
(((s1 . (x - Z)) + ((N . (x - Z)) * (L . (x - Z)))) + ((L . (x - Z)) * ((x0 . (x - Z)) + (N . (x - Z))))) + ((L . (x - Z)) + (R13 . (x - Z))) is V22() real ext-real Element of REAL
L . (x - Z) is V22() real ext-real Element of REAL
(s1 . (x - Z)) + (L . (x - Z)) is V22() real ext-real Element of REAL
(L . (x - Z)) * (x0 . (x - Z)) is V22() real ext-real Element of REAL
(L . (x - Z)) * (N . (x - Z)) is V22() real ext-real Element of REAL
((L . (x - Z)) * (x0 . (x - Z))) + ((L . (x - Z)) * (N . (x - Z))) is V22() real ext-real Element of REAL
((s1 . (x - Z)) + (L . (x - Z))) + (((L . (x - Z)) * (x0 . (x - Z))) + ((L . (x - Z)) * (N . (x - Z)))) is V22() real ext-real Element of REAL
(((s1 . (x - Z)) + (L . (x - Z))) + (((L . (x - Z)) * (x0 . (x - Z))) + ((L . (x - Z)) * (N . (x - Z))))) + ((L . (x - Z)) + (R13 . (x - Z))) is V22() real ext-real Element of REAL
p . (x - Z) is V22() real ext-real Element of REAL
(p . (x - Z)) + ((L . (x - Z)) * (N . (x - Z))) is V22() real ext-real Element of REAL
((s1 . (x - Z)) + (L . (x - Z))) + ((p . (x - Z)) + ((L . (x - Z)) * (N . (x - Z)))) is V22() real ext-real Element of REAL
(((s1 . (x - Z)) + (L . (x - Z))) + ((p . (x - Z)) + ((L . (x - Z)) * (N . (x - Z))))) + ((L . (x - Z)) + (R13 . (x - Z))) is V22() real ext-real Element of REAL
R . (x - Z) is V22() real ext-real Element of REAL
(p . (x - Z)) + (R . (x - Z)) is V22() real ext-real Element of REAL
((s1 . (x - Z)) + (L . (x - Z))) + ((p . (x - Z)) + (R . (x - Z))) is V22() real ext-real Element of REAL
(((s1 . (x - Z)) + (L . (x - Z))) + ((p . (x - Z)) + (R . (x - Z)))) + ((L . (x - Z)) + (R13 . (x - Z))) is V22() real ext-real Element of REAL
h . (x - Z) is V22() real ext-real Element of REAL
((s1 . (x - Z)) + (L . (x - Z))) + (h . (x - Z)) is V22() real ext-real Element of REAL
(((s1 . (x - Z)) + (L . (x - Z))) + (h . (x - Z))) + ((L . (x - Z)) + (R13 . (x - Z))) is V22() real ext-real Element of REAL
(h . (x - Z)) + (L . (x - Z)) is V22() real ext-real Element of REAL
(s1 . (x - Z)) + ((h . (x - Z)) + (L . (x - Z))) is V22() real ext-real Element of REAL
((s1 . (x - Z)) + ((h . (x - Z)) + (L . (x - Z)))) + ((L . (x - Z)) + (R13 . (x - Z))) is V22() real ext-real Element of REAL
M . (x - Z) is V22() real ext-real Element of REAL
(s1 . (x - Z)) + (M . (x - Z)) is V22() real ext-real Element of REAL
((L . (x - Z)) + (R13 . (x - Z))) + ((s1 . (x - Z)) + (M . (x - Z))) is V22() real ext-real Element of REAL
(R13 . (x - Z)) + (s1 . (x - Z)) is V22() real ext-real Element of REAL
((R13 . (x - Z)) + (s1 . (x - Z))) + (M . (x - Z)) is V22() real ext-real Element of REAL
(L . (x - Z)) + (((R13 . (x - Z)) + (s1 . (x - Z))) + (M . (x - Z))) is V22() real ext-real Element of REAL
R15 . (x - Z) is V22() real ext-real Element of REAL
(R15 . (x - Z)) + (M . (x - Z)) is V22() real ext-real Element of REAL
(L . (x - Z)) + ((R15 . (x - Z)) + (M . (x - Z))) 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))
R . (x - Z) is V22() real ext-real Element of REAL
(L . (x - Z)) + (R . (x - Z)) is V22() real ext-real Element of REAL
L . 1 is V22() real ext-real Element of REAL
L11 . 1 is V22() real ext-real Element of REAL
L12 . 1 is V22() real ext-real Element of REAL
(L11 . 1) + (L12 . 1) is V22() real ext-real Element of REAL
L . 1 is V22() real ext-real Element of REAL
(c₅ . Z) * (L . 1) is V22() real ext-real Element of REAL
((c₅ . Z) * (L . 1)) + (L12 . 1) is V22() real ext-real Element of REAL
x0 . 1 is V22() real ext-real Element of REAL
(f . Z) * (x0 . 1) is V22() real ext-real Element of REAL
((c₅ . Z) * (L . 1)) + ((f . Z) * (x0 . 1)) is V22() real ext-real Element of REAL
((c₅ . Z) * (f,Z)) + ((f . Z) * (x0 . 1)) is V22() real ext-real Element of REAL
Z is open V57() V58() V59() Element of K19(REAL)
id Z is V1() V4( REAL ) V4(Z) V5( REAL ) V5(Z) V6() V7() total 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))
dom f is V57() V58() V59() Element of K19(REAL)
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))
(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
id REAL is V1() V4( REAL ) V5( REAL ) V6() V7() non empty total quasi_total complex-valued ext-real-valued real-valued increasing non-decreasing 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
L . L is V22() real ext-real Element of REAL
1 * L is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
(f | Z) . r is V22() real ext-real Element of REAL
f . r is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
x0 is open V57() V58() V59() Neighbourhood of r
f . r 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))
N is V22() real ext-real Element of REAL
f . N is V22() real ext-real Element of REAL
(f . N) - (f . r) is V22() real ext-real Element of REAL
N - r is V22() real ext-real Element of REAL
L . (N - r) is V22() real ext-real Element of REAL
R . (N - r) is V22() real ext-real Element of REAL
(L . (N - r)) + (R . (N - r)) is V22() real ext-real Element of REAL
N - (f . r) is V22() real ext-real Element of REAL
(L . (N - r)) + 0 is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
(f,Z) . r is V22() real ext-real Element of REAL
x0 is open V57() V58() V59() Neighbourhood of r
f . r is V22() real ext-real Element of REAL
N is open V57() V58() V59() Neighbourhood of r
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 r
L is open V57() V58() V59() Neighbourhood of r
R is V22() real ext-real Element of REAL
f . R is V22() real ext-real Element of REAL
(f . R) - (f . r) is V22() real ext-real Element of REAL
R - r is V22() real ext-real Element of REAL
L . (R - r) is V22() real ext-real Element of REAL
R . (R - r) is V22() real ext-real Element of REAL
(L . (R - r)) + (R . (R - r)) is V22() real ext-real Element of REAL
R - (f . r) is V22() real ext-real Element of REAL
(L . (R - r)) + 0 is V22() real ext-real Element of REAL
(f,r) is V22() real ext-real Element of REAL
L . 1 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))
c₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f + c₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f + c₅) is V57() V58() V59() Element of K19(REAL)
((f + c₅),Z) 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
R is V22() real ext-real Element of REAL
((f + c₅),Z) . R is V22() real ext-real Element of REAL
((f + c₅),R) is V22() real ext-real Element of REAL
(f,R) is V22() real ext-real Element of REAL
(c₅,R) is V22() real ext-real Element of REAL
(f,R) + (c₅,R) is V22() real ext-real Element of REAL
R is V22() real ext-real Element of REAL
((f + c₅),Z) . R is V22() real ext-real Element of REAL
(f,R) is V22() real ext-real Element of REAL
(c₅,R) is V22() real ext-real Element of REAL
(f,R) + (c₅,R) 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))
c₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f - c₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- c₅ is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
- 1 is V22() real ext-real non positive set
(- 1) (#) c₅ is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
f + (- c₅) is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
dom (f - c₅) is V57() V58() V59() Element of K19(REAL)
((f - c₅),Z) 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
R is V22() real ext-real Element of REAL
((f - c₅),Z) . R is V22() real ext-real Element of REAL
((f - c₅),R) is V22() real ext-real Element of REAL
(f,R) is V22() real ext-real Element of REAL
(c₅,R) is V22() real ext-real Element of REAL
(f,R) - (c₅,R) is V22() real ext-real Element of REAL
R is V22() real ext-real Element of REAL
((f - c₅),Z) . R is V22() real ext-real Element of REAL
(f,R) is V22() real ext-real Element of REAL
(c₅,R) is V22() real ext-real Element of REAL
(f,R) - (c₅,R) is V22() real ext-real Element of REAL
Z is V22() real ext-real Element of REAL
f is open V57() V58() V59() Element of K19(REAL)
c₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
Z (#) c₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (Z (#) c₅) is V57() V58() V59() Element of K19(REAL)
((Z (#) c₅),f) 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
R is V22() real ext-real Element of REAL
((Z (#) c₅),f) . R is V22() real ext-real Element of REAL
((Z (#) c₅),R) is V22() real ext-real Element of REAL
(c₅,R) is V22() real ext-real Element of REAL
Z * (c₅,R) is V22() real ext-real Element of REAL
R is V22() real ext-real Element of REAL
((Z (#) c₅),f) . R is V22() real ext-real Element of REAL
(c₅,R) is V22() real ext-real Element of REAL
Z * (c₅,R) 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))
c₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) c₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f (#) c₅) is V57() V58() V59() Element of K19(REAL)
((f (#) c₅),Z) 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
R is V22() real ext-real Element of REAL
((f (#) c₅),Z) . R is V22() real ext-real Element of REAL
((f (#) c₅),R) is V22() real ext-real Element of REAL
c₅ . R is V22() real ext-real Element of REAL
(f,R) is V22() real ext-real Element of REAL
(c₅ . R) * (f,R) is V22() real ext-real Element of REAL
f . R is V22() real ext-real Element of REAL
(c₅,R) is V22() real ext-real Element of REAL
(f . R) * (c₅,R) is V22() real ext-real Element of REAL
((c₅ . R) * (f,R)) + ((f . R) * (c₅,R)) is V22() real ext-real Element of REAL
R is V22() real ext-real Element of REAL
((f (#) c₅),Z) . R is V22() real ext-real Element of REAL
c₅ . R is V22() real ext-real Element of REAL
(f,R) is V22() real ext-real Element of REAL
(c₅ . R) * (f,R) is V22() real ext-real Element of REAL
f . R is V22() real ext-real Element of REAL
(c₅,R) is V22() real ext-real Element of REAL
(f . R) * (c₅,R) is V22() real ext-real Element of REAL
((c₅ . R) * (f,R)) + ((f . R) * (c₅,R)) 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)
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))
(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
Z /\ (dom f) is V57() V58() V59() Element of K19(REAL)
r 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
N is open V57() V58() V59() Neighbourhood of x0
f . x0 is V22() real ext-real Element of 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
(f,x0) is V22() real ext-real Element of REAL
L . 1 is V22() real ext-real Element of REAL
Z is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
c₅ is open V57() V58() V59() Element of K19(REAL)
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)
(R,c₅) 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)
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))
rng L is non empty V57() V58() V59() V73() V74() Element of K19(REAL)
r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V64() V76() set
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))
cf /* 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 ") (#) (cf /* 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 ") (#) (cf /* L)) . r is V22() real ext-real Element of REAL
(L ") . r is V22() real ext-real Element of REAL
(cf /* L) . r is V22() real ext-real Element of REAL
((L ") . r) * ((cf /* L) . r) is V22() real ext-real Element of REAL
L . r is V22() real ext-real Element of REAL
cf . (L . r) is V22() real ext-real Element of REAL
((L ") . r) * (cf . (L . r)) is V22() real ext-real Element of REAL
((L ") . r) * 0 is V22() real ext-real Element of REAL
((L ") (#) (cf /* L)) . 0 is V22() real ext-real Element of REAL
lim ((L ") (#) (cf /* L)) 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))
dom r is V57() V58() V59() Element of K19(REAL)
x0 is V22() real ext-real Element of REAL
r . x0 is V22() real ext-real Element of REAL
Z * x0 is V22() real ext-real Element of REAL
N is V22() real ext-real Element of REAL
L is open V57() V58() V59() Neighbourhood of N
R . N is V22() real ext-real Element of REAL
x0 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
R . R is V22() real ext-real Element of REAL
(R . R) - (R . N) is V22() real ext-real Element of REAL
R - N is V22() real ext-real Element of REAL
x0 . (R - N) is V22() real ext-real Element of REAL
L . (R - N) is V22() real ext-real Element of REAL
(x0 . (R - N)) + (L . (R - N)) is V22() real ext-real Element of REAL
Z * R is V22() real ext-real Element of REAL
(Z * R) + f is V22() real ext-real Element of REAL
((Z * R) + f) - (R . N) is V22() real ext-real Element of REAL
Z * N is V22() real ext-real Element of REAL
(Z * N) + f is V22() real ext-real Element of REAL
((Z * R) + f) - ((Z * N) + f) is V22() real ext-real Element of REAL
Z * (R - N) is V22() real ext-real Element of REAL
(Z * (R - N)) + 0 is V22() real ext-real Element of REAL
(x0 . (R - N)) + 0 is V22() real ext-real Element of REAL
N is V22() real ext-real Element of REAL
(R,c₅) . N is V22() real ext-real Element of REAL
L is open V57() V58() V59() Neighbourhood of N
R . N is V22() real ext-real Element of REAL
R is V22() real ext-real Element of REAL
R . R is V22() real ext-real Element of REAL
(R . R) - (R . N) is V22() real ext-real Element of REAL
R - N is V22() real ext-real Element of REAL
x0 . (R - N) is V22() real ext-real Element of REAL
L . (R - N) is V22() real ext-real Element of REAL
(x0 . (R - N)) + (L . (R - N)) is V22() real ext-real Element of REAL
Z * R is V22() real ext-real Element of REAL
(Z * R) + f is V22() real ext-real Element of REAL
((Z * R) + f) - (R . N) is V22() real ext-real Element of REAL
Z * N is V22() real ext-real Element of REAL
(Z * N) + f is V22() real ext-real Element of REAL
((Z * R) + f) - ((Z * N) + f) is V22() real ext-real Element of REAL
Z * (R - N) is V22() real ext-real Element of REAL
(Z * (R - N)) + 0 is V22() real ext-real Element of REAL
(x0 . (R - N)) + 0 is V22() real ext-real Element of REAL
(R,N) is V22() real ext-real Element of REAL
x0 . 1 is V22() real ext-real Element of REAL
Z * 1 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 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₅ is open V57() V58() V59() Neighbourhood of f
R is V22() real ext-real set
f - R is V22() real ext-real set
f + R is V22() real ext-real set
].(f - R),(f + R).[ is open V57() V58() V59() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= f - R & not f + R <= b₁ ) } is set
NAT --> f is V1() V4( NAT ) V5({f}) V6() constant non empty total T-Sequence-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,{f}))
{f} is non empty V12() V57() V58() V59() V64() V78(1) set
K20(NAT,{f}) is V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() set
K19(K20(NAT,{f})) is non empty V12() V64() V74() set
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))
rng L is non empty V57() V58() V59() Element of K19(REAL)
lim L is V22() real ext-real Element of REAL
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 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 ^\ r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of L
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))
L - 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() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
- 1 is V22() real ext-real non positive set
(- 1) (#) L is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
L + (- L) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
x0 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 x0 is non empty V12() V57() V58() V59() V64() V78(1) Element of K19(REAL)
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) . R is V22() real ext-real Element of REAL
R + 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 + r) is V22() real ext-real Element of REAL
L is set
x0 . 0 is V22() real ext-real Element of REAL
0 + 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 . (0 + r) is V22() real ext-real Element of REAL
L is V22() real ext-real 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
p 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 /* x0 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 /* x0) . p is V22() real ext-real Element of REAL
((Z /* x0) . p) - (Z . f) is V22() real ext-real Element of REAL
abs (((Z /* x0) . p) - (Z . f)) is V22() real ext-real Element of REAL
x0 . p is V22() real ext-real Element of REAL
Z . (x0 . p) is V22() real ext-real Element of REAL
(Z . (x0 . p)) - (Z . f) is V22() real ext-real Element of REAL
abs ((Z . (x0 . p)) - (Z . f)) is V22() real ext-real Element of REAL
p + 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 . (p + r) is V22() real ext-real Element of REAL
Z . (L . (p + r)) is V22() real ext-real Element of REAL
(Z . (L . (p + r))) - (Z . f) is V22() real ext-real Element of REAL
abs ((Z . (L . (p + r))) - (Z . f)) is V22() real ext-real Element of REAL
(Z . f) - (Z . f) is V22() real ext-real Element of REAL
abs ((Z . f) - (Z . f)) is V22() real ext-real Element of REAL
lim L is V22() real ext-real Element of REAL
L . 0 is V22() real ext-real Element of REAL
lim N is V22() real ext-real Element of REAL
f - f is V22() real ext-real set
N ^\ r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of N
lim (N ^\ r) is V22() real ext-real Element of 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
N . L is V22() real ext-real Element of REAL
L . L is V22() real ext-real Element of REAL
L . L is V22() real ext-real Element of REAL
(L . L) - (L . L) is V22() real ext-real Element of 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
(N ^\ r) . L is V22() real ext-real Element of REAL
L + 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
N . (L + 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 + x0 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 + x0) 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 + x0)) - (Z /* x0) 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 /* x0) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(- 1) (#) (Z /* x0) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
(Z /* (L + x0)) + (- (Z /* x0)) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
((Z /* (L + x0)) - (Z /* x0)) + (Z /* x0) 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 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 /* (L + x0)) - (Z /* x0)) + (Z /* x0)) . R is V22() real ext-real Element of REAL
((Z /* (L + x0)) - (Z /* x0)) . R is V22() real ext-real Element of REAL
(Z /* x0) . R is V22() real ext-real Element of REAL
(((Z /* (L + x0)) - (Z /* x0)) . R) + ((Z /* x0) . R) is V22() real ext-real Element of REAL
(Z /* (L + x0)) . R is V22() real ext-real Element of REAL
((Z /* (L + x0)) . R) - ((Z /* x0) . R) is V22() real ext-real Element of REAL
(((Z /* (L + x0)) . R) - ((Z /* x0) . R)) + ((Z /* x0) . R) is V22() real ext-real Element of REAL
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 + x0) . R is V22() real ext-real Element of REAL
(L - L) + 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 - L) + L) ^\ r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (L - L) + L
(((L - L) + L) ^\ r) . R is V22() real ext-real Element of REAL
R + 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 - L) + L) . (R + r) is V22() real ext-real Element of REAL
(L - L) . (R + r) is V22() real ext-real Element of REAL
L . (R + r) is V22() real ext-real Element of REAL
((L - L) . (R + r)) + (L . (R + r)) is V22() real ext-real Element of REAL
L . (R + r) is V22() real ext-real Element of REAL
(L . (R + r)) - (L . (R + r)) is V22() real ext-real Element of REAL
((L . (R + r)) - (L . (R + r))) + (L . (R + r)) is V22() real ext-real Element of REAL
L ^\ r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of L
(L ^\ r) . R is V22() real ext-real Element of 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 /* 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 /* L) ^\ r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of Z /* L
rng (L + x0) is non empty V57() V58() V59() Element of K19(REAL)
R is set
p 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 + x0) . p is V22() real ext-real Element of REAL
(((L - L) + L) ^\ r) . p is V22() real ext-real Element of REAL
p + 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 - L) + L) . (p + r) is V22() real ext-real Element of REAL
(L - L) . (p + r) is V22() real ext-real Element of REAL
L . (p + r) is V22() real ext-real Element of REAL
((L - L) . (p + r)) + (L . (p + r)) is V22() real ext-real Element of REAL
L . (p + r) is V22() real ext-real Element of REAL
(L . (p + r)) - (L . (p + r)) is V22() real ext-real Element of REAL
((L . (p + r)) - (L . (p + r))) + (L . (p + r)) is V22() real ext-real Element of REAL
r + p 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 + p) is V22() real ext-real Element of REAL
((L + x0) . p) - f is V22() real ext-real Element of REAL
abs (((L + x0) . p) - f) 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))
(L ") (#) ((Z /* (L + x0)) - (Z /* x0)) 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 (#) ((L ") (#) ((Z /* (L + x0)) - (Z /* x0))) 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 (#) ((L ") (#) ((Z /* (L + x0)) - (Z /* x0)))) is V22() real ext-real Element of REAL
lim ((L ") (#) ((Z /* (L + x0)) - (Z /* x0))) is V22() real ext-real Element of REAL
0 * (lim ((L ") (#) ((Z /* (L + x0)) - (Z /* x0)))) is V22() real ext-real Element of REAL
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 is V22() real ext-real Element of REAL
(L (#) ((L ") (#) ((Z /* (L + x0)) - (Z /* x0)))) . R is V22() real ext-real Element of REAL
((L ") (#) ((Z /* (L + x0)) - (Z /* x0))) . R is V22() real ext-real Element of REAL
(L . R) * (((L ") (#) ((Z /* (L + x0)) - (Z /* x0))) . R) is V22() real ext-real Element of REAL
(L ") . R is V22() real ext-real Element of REAL
((Z /* (L + x0)) - (Z /* x0)) . R is V22() real ext-real Element of REAL
((L ") . R) * (((Z /* (L + x0)) - (Z /* x0)) . R) is V22() real ext-real Element of REAL
(L . R) * (((L ") . R) * (((Z /* (L + x0)) - (Z /* x0)) . R)) is V22() real ext-real Element of REAL
(L . R) " is V22() real ext-real Element of REAL
((L . R) ") * (((Z /* (L + x0)) - (Z /* x0)) . R) is V22() real ext-real Element of REAL
(L . R) * (((L . R) ") * (((Z /* (L + x0)) - (Z /* x0)) . R)) is V22() real ext-real Element of REAL
(L . R) * ((L . R) ") is V22() real ext-real Element of REAL
((L . R) * ((L . R) ")) * (((Z /* (L + x0)) - (Z /* x0)) . R) is V22() real ext-real Element of REAL
1 * (((Z /* (L + x0)) - (Z /* x0)) . R) is V22() real ext-real Element of REAL
lim (Z /* x0) is V22() real ext-real Element of REAL
lim (((Z /* (L + x0)) - (Z /* x0)) + (Z /* x0)) is V22() real ext-real Element of REAL
0 + (Z . f) is V22() real ext-real Element of REAL
lim (Z /* L) 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))
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₅ is V22() real ext-real set
dom (f | Z) is V57() V58() V59() Element of K19(REAL)
dom (f | Z) is Element of K19(Z)
K19(Z) is set
Z is set
f is open V57() V58() V59() Element of K19(REAL)
c₅ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom c₅ is V57() V58() V59() Element of K19(REAL)
c₅ | f is V1() V4( REAL ) V4(f) 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
c₅ | 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 (c₅ | Z) is Element of K19(Z)
K19(Z) is set
(c₅ | Z) . R is V22() real ext-real Element of REAL
L is open V57() V58() V59() Neighbourhood of R
L is open V57() V58() V59() Neighbourhood of R
r is open V57() V58() V59() Neighbourhood of R
dom (c₅ | f) is V57() V58() V59() Element of K19(REAL)
(c₅ | f) . R is V22() real ext-real Element of REAL
(dom c₅) /\ Z is V57() V58() V59() Element of K19(REAL)
(dom c₅) /\ f is V57() V58() V59() Element of K19(REAL)
dom (c₅ | f) is V57() V58() V59() Element of K19(f)
K19(f) is set
x0 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued () Element of K19(K20(REAL,REAL))
N 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 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
(c₅ | f) . L is V22() real ext-real Element of REAL
((c₅ | f) . L) - ((c₅ | f) . R) is V22() real ext-real Element of REAL
L - R is V22() real ext-real Element of REAL
x0 . (L - R) is V22() real ext-real Element of REAL
N . (L - R) is V22() real ext-real Element of REAL
(x0 . (L - R)) + (N . (L - R)) is V22() real ext-real Element of REAL
(c₅ | Z) . L is V22() real ext-real Element of REAL
((c₅ | Z) . L) - ((c₅ | Z) . R) is V22() real ext-real Element of REAL
c₅ . R is V22() real ext-real Element of REAL
((c₅ | Z) . L) - (c₅ . R) is V22() real ext-real Element of REAL
c₅ . L is V22() real ext-real Element of REAL
(c₅ . L) - (c₅ . R) is V22() real ext-real Element of REAL
(c₅ . L) - ((c₅ | f) . R) is V22() real ext-real Element of REAL
{} REAL is V57() V58() V59() Element of K19(REAL)
Z 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))
K87(Z) is non empty V57() V58() V59() set
lim Z is V22() real ext-real Element of REAL
rng Z is non empty V57() V58() V59() Element of K19(REAL)
[#] REAL is V57() V58() V59() Element of K19(REAL)
([#] REAL) ` is V57() V58() V59() Element of K19(REAL)
REAL \ ([#] REAL) is V57() V58() V59() set
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
c<sub>5</sub> is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
Z is open V57() V58() V59() Element of K19(REAL)
c<sub>5</sub> | 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 c<sub>5</sub> is V57() V58() V59() Element of K19(REAL)
Z /\ (dom c<sub>5</sub>) is V57() V58() V59() Element of K19(REAL)
r is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
the open V57() V58() V59() Neighbourhood of x0 is open V57() V58() V59() Neighbourhood of x0
c<sub>5</sub> . 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
c<sub>5</sub> . L is V22() real ext-real Element of REAL
(c<sub>5</sub> . L) - (c<sub>5</sub> . 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 - (c<sub>5</sub> . 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
the V22() real ext-real Element of REAL is V22() real ext-real Element of REAL
c<sub>5</sub> . the V22() real ext-real Element of REAL is V22() real ext-real Element of REAL
N is open V57() V58() V59() Neighbourhood of the 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 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))
R . 0 is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
(c<sub>5</sub> . the V22() real ext-real Element of REAL ) - (c<sub>5</sub> . the V22() real ext-real Element of REAL ) is V22() real ext-real Element of REAL
the V22() real ext-real Element of REAL - the V22() real ext-real Element of REAL is V22() real ext-real Element of REAL
L . ( the V22() real ext-real Element of REAL - the V22() real ext-real Element of REAL ) is V22() real ext-real Element of REAL
R . ( the V22() real ext-real Element of REAL - the V22() real ext-real Element of REAL ) is V22() real ext-real Element of REAL
(L . ( the V22() real ext-real Element of REAL - the V22() real ext-real Element of REAL )) + (R . ( the V22() real ext-real Element of REAL - the V22() real ext-real Element of REAL )) is V22() real ext-real Element of REAL
p * 0 is V22() real ext-real Element of REAL
(p * 0) + (R . 0) 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))
cs . 1 is V22() real ext-real Element of REAL
h 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))
h " 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 /* h 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))
(h ") (#) (R /* h) 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))
M is V22() real ext-real set
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
((h ") (#) (R /* h)) . n is V22() real ext-real Element of REAL
abs (((h ") (#) (R /* h)) . n) is V22() real ext-real Element of REAL
(h ") . n is V22() real ext-real Element of REAL
(R /* h) . n is V22() real ext-real Element of REAL
((h ") . n) * ((R /* h) . n) is V22() real ext-real Element of REAL
abs (((h ") . n) * ((R /* h) . n)) is V22() real ext-real Element of REAL
h . n is V22() real ext-real Element of REAL
(h . n) " is V22() real ext-real Element of REAL
((h . n) ") * ((R /* h) . n) is V22() real ext-real Element of REAL
abs (((h . n) ") * ((R /* h) . n)) is V22() real ext-real Element of REAL
abs ((R /* h) . n) is V22() real ext-real Element of REAL
abs (R /* h) 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))
(abs (R /* h)) . n is V22() real ext-real Element of REAL
cs . n is V22() real ext-real Element of REAL
abs (h . n) is V22() real ext-real Element of REAL
(abs (h . n)) * (abs (((h . n) ") * ((R /* h) . n))) is V22() real ext-real Element of REAL
M * (abs (h . n)) is V22() real ext-real Element of REAL
(h . n) * (((h . n) ") * ((R /* h) . n)) is V22() real ext-real Element of REAL
abs ((h . n) * (((h . n) ") * ((R /* h) . n))) is V22() real ext-real Element of REAL
(h . n) * ((h . n) ") is V22() real ext-real Element of REAL
((h . n) * ((h . n) ")) * ((R /* h) . n) is V22() real ext-real Element of REAL
abs (((h . n) * ((h . n) ")) * ((R /* h) . n)) is V22() real ext-real Element of REAL
1 * ((R /* h) . n) is V22() real ext-real Element of REAL
abs (1 * ((R /* h) . n)) is V22() real ext-real Element of REAL
abs h is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent Element of K19(K20(NAT,REAL))
(abs h) . n is V22() real ext-real Element of REAL
M * ((abs h) . n) is V22() real ext-real Element of REAL
M (#) (abs h) 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))
(M (#) (abs h)) . n is V22() real ext-real Element of REAL
lim h 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 (abs h) is V22() real ext-real Element of REAL
abs 0 is V22() real ext-real V56() Element of REAL
lim (M (#) (abs h)) is V22() real ext-real Element of REAL
M * 0 is V22() real ext-real Element of REAL
lim cs is V22() real ext-real Element of REAL
lim (abs (R /* h)) is V22() real ext-real Element of REAL
lim (R /* h) is V22() real ext-real Element of REAL
s1 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 s1 is non empty V57() V58() V59() Element of K19(REAL)
dom R is V57() V58() V59() Element of K19(REAL)
lim s1 is V22() real ext-real Element of REAL
R /* s1 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 /* s1) is V22() real ext-real Element of REAL
{} REAL is V57() V58() V59() Element of K19(REAL)
Z 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))
K87(Z) is non empty V57() V58() V59() set
lim Z is V22() real ext-real Element of REAL
rng Z is non empty V57() V58() V59() Element of K19(REAL)
[#] REAL is V57() V58() V59() Element of K19(REAL)
([#] REAL) ` is V57() V58() V59() Element of K19(REAL)
REAL \ ([#] REAL) is V57() V58() V59() set
id REAL is V1() V4( REAL ) V5( REAL ) V6() V7() non empty total quasi_total complex-valued ext-real-valued real-valued increasing non-decreasing Element of K19(K20(REAL,REAL))
f 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 open V57() V58() V59() Element of K19(REAL)
dom f is non empty V57() V58() V59() Element of K19(REAL)
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))
id Z is V1() V4( REAL ) V4(Z) V5( REAL ) V5(Z) V6() V7() total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,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)