REAL is non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V47() V53() V54() set
RAT is non empty V47() V48() V49() V50() V53() V54() set
INT is non empty V47() V48() V49() V50() V51() V53() V54() set
omega is non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below set
K19(omega) is set
K19(NAT) is set
K20(COMPLEX,COMPLEX) is complex-valued set
K19(K20(COMPLEX,COMPLEX)) is set
K20(COMPLEX,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(COMPLEX,REAL)) is set
K20(REAL,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(REAL,REAL)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(K20(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is V5( RAT ) complex-valued ext-real-valued real-valued set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is V5( RAT ) complex-valued ext-real-valued real-valued set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
K20(K20(NAT,NAT),NAT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
K19(K20(K20(NAT,NAT),NAT)) is set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() V52() V53() bounded_below V68() Element of NAT
1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V45() V46() V47() V48() V49() V50() V51() V52() left_end bounded_below Element of NAT
K20(NAT,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V47() V48() V49() V50() V51() V52() V53() bounded_below V68() set
K59(0) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V47() V48() V49() V50() V51() V52() V53() bounded_below V68() set
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
[.p,g.] is V47() V48() V49() V68() closed Element of K19(REAL)
].p,g.[ is V47() V48() V49() non left_end non right_end V68() open Element of K19(REAL)
x1 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom x1 is V47() V48() V49() Element of K19(REAL)
x1 | [.p,g.] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x1 . p is V22() real ext-real Element of REAL
x1 . g is V22() real ext-real Element of REAL
x1 .: [.p,g.] is V47() V48() V49() Element of K19(REAL)
upper_bound (x1 .: [.p,g.]) is V22() real ext-real Element of REAL
lower_bound (x1 .: [.p,g.]) is V22() real ext-real Element of REAL
x2 is V22() real ext-real set
Z is V22() real ext-real set
x1 . x2 is V22() real ext-real Element of REAL
x1 . Z is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( p <= b1 & b1 <= g ) } is set
f3 is V22() real ext-real Element of REAL
x1 . f3 is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
x1 . x is V22() real ext-real Element of REAL
2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V45() V46() V47() V48() V49() V50() V51() V52() left_end bounded_below Element of NAT
g / 2 is V22() real ext-real Element of REAL
K59(2) is non empty V22() real ext-real positive non negative set
K57(g,K59(2)) is V22() real ext-real set
p / 2 is V22() real ext-real Element of REAL
K57(p,K59(2)) is V22() real ext-real set
(g / 2) + (g / 2) is V22() real ext-real Element of REAL
(p / 2) + (g / 2) is V22() real ext-real Element of REAL
(p / 2) + (p / 2) is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= p & not g <= b1 ) } is set
f is V47() V48() V49() open Element of K19(REAL)
x1 | f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x1 `| f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(x1 `| f) . ((p / 2) + (g / 2)) is V22() real ext-real Element of REAL
diff (x1,((p / 2) + (g / 2))) is V22() real ext-real Element of REAL
{p,g} is non empty V47() V48() V49() set
].p,g.[ \/ {p,g} is non empty V47() V48() V49() set
f is V47() V48() V49() open Element of K19(REAL)
f4 is V47() V48() V49() open Neighbourhood of f3
f5 is V22() real ext-real set
f3 - f5 is V22() real ext-real Element of REAL
K58(f5) is V22() real ext-real set
K56(f3,K58(f5)) is V22() real ext-real set
f3 + f5 is V22() real ext-real Element of REAL
].(f3 - f5),(f3 + f5).[ is V47() V48() V49() non left_end non right_end V68() open Element of K19(REAL)
f is V22() real ext-real Element of REAL
2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V45() V46() V47() V48() V49() V50() V51() V52() left_end bounded_below Element of NAT
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))
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
x0 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / (x0 + 2) is V22() real ext-real Element of REAL
K59((x0 + 2)) is non empty V22() real ext-real positive non negative set
K57(f,K59((x0 + 2))) is V22() real ext-real set
x0 . x0 is V22() real ext-real Element of REAL
lim x0 is V22() real ext-real Element of REAL
{f3} is non empty V47() V48() V49() Element of K19(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 V47() V48() V49() Element of K19(REAL)
c is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s3 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
c . s3 is V22() real ext-real Element of REAL
s3 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))
h2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
s3 . h2 is V22() real ext-real Element of REAL
h2 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / (h2 + 2) is V22() real ext-real Element of REAL
K59((h2 + 2)) is non empty V22() real ext-real positive non negative set
K57(f,K59((h2 + 2))) is V22() real ext-real set
- (f / (h2 + 2)) is V22() real ext-real Element of REAL
- f is V22() real ext-real Element of REAL
(- f) / (h2 + 2) is V22() real ext-real Element of REAL
K57((- f),K59((h2 + 2))) is V22() real ext-real set
lim s3 is V22() real ext-real Element of REAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V47() V48() V49() V50() V51() V52() V53() bounded_below V68() Element of REAL
h2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
h2 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / (h2 + 2) is V22() real ext-real Element of REAL
K59((h2 + 2)) is non empty V22() real ext-real positive non negative set
K57(f,K59((h2 + 2))) is V22() real ext-real set
- (f / (h2 + 2)) is V22() real ext-real Element of REAL
s3 . h2 is V22() real ext-real Element of REAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / 1 is V22() real ext-real Element of REAL
K59(1) is non empty V22() real ext-real positive non negative set
K57(f,K59(1)) is V22() real ext-real set
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / (n + 2) is V22() real ext-real Element of REAL
K59((n + 2)) is non empty V22() real ext-real positive non negative set
K57(f,K59((n + 2))) is V22() real ext-real set
f3 - (f / (n + 2)) is V22() real ext-real Element of REAL
K58((f / (n + 2))) is V22() real ext-real set
K56(f3,K58((f / (n + 2)))) is V22() real ext-real set
f3 - f is V22() real ext-real Element of REAL
K58(f) is V22() real ext-real set
K56(f3,K58(f)) is V22() real ext-real set
f3 + f is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= f3 - f & not f3 + f <= b1 ) } is set
h2 is V1() non-zero V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
h2 + 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))
rng (h2 + c) is V47() V48() V49() Element of K19(REAL)
n is set
n1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
(h2 + c) . n1 is V22() real ext-real Element of REAL
h2 . n1 is V22() real ext-real Element of REAL
c . n1 is V22() real ext-real Element of REAL
(h2 . n1) + (c . n1) is V22() real ext-real Element of REAL
n1 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / (n1 + 2) is V22() real ext-real Element of REAL
K59((n1 + 2)) is non empty V22() real ext-real positive non negative set
K57(f,K59((n1 + 2))) is V22() real ext-real set
- (f / (n1 + 2)) is V22() real ext-real Element of REAL
(- (f / (n1 + 2))) + (c . n1) is V22() real ext-real Element of REAL
f3 - (f / (n1 + 2)) is V22() real ext-real Element of REAL
K58((f / (n1 + 2))) is V22() real ext-real set
K56(f3,K58((f / (n1 + 2)))) is V22() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / (n + 2) is V22() real ext-real Element of REAL
K59((n + 2)) is non empty V22() real ext-real positive non negative set
K57(f,K59((n + 2))) is V22() real ext-real set
f3 + (f / (n + 2)) is V22() real ext-real Element of REAL
x0 is V1() non-zero V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
x0 + 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))
rng (x0 + c) is V47() V48() V49() Element of K19(REAL)
n is set
n1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
(x0 + c) . n1 is V22() real ext-real Element of REAL
x0 . n1 is V22() real ext-real Element of REAL
c . n1 is V22() real ext-real Element of REAL
(x0 . n1) + (c . n1) is V22() real ext-real Element of REAL
n1 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / (n1 + 2) is V22() real ext-real Element of REAL
K59((n1 + 2)) is non empty V22() real ext-real positive non negative set
K57(f,K59((n1 + 2))) is V22() real ext-real set
(f / (n1 + 2)) + (c . n1) is V22() real ext-real Element of REAL
f3 + (f / (n1 + 2)) is V22() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / (n + 2) is V22() real ext-real Element of REAL
K59((n + 2)) is non empty V22() real ext-real positive non negative set
K57(f,K59((n + 2))) is V22() real ext-real set
x0 . n is V22() real ext-real Element of REAL
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))
x1 /* (x0 + 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))
x1 /* 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))
(x1 /* (x0 + c)) - (x1 /* 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))
(x0 ") (#) ((x1 /* (x0 + c)) - (x1 /* 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))
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
((x0 ") (#) ((x1 /* (x0 + c)) - (x1 /* c))) . n is V22() real ext-real Element of REAL
x0 . n is V22() real ext-real Element of REAL
(x0 ") . n is V22() real ext-real Element of REAL
(x0 . n) " is V22() real ext-real Element of REAL
(x0 + c) . n is V22() real ext-real Element of REAL
x1 . ((x0 + c) . n) is V22() real ext-real Element of REAL
(x1 . ((x0 + c) . n)) - (x1 . f3) is V22() real ext-real Element of REAL
K58((x1 . f3)) is V22() real ext-real set
K56((x1 . ((x0 + c) . n)),K58((x1 . f3))) is V22() real ext-real set
n1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
(x0 + c) . n1 is V22() real ext-real Element of REAL
rng c is V47() V48() V49() Element of K19(REAL)
((x1 /* (x0 + c)) - (x1 /* c)) . n is V22() real ext-real Element of REAL
((x0 ") . n) * (((x1 /* (x0 + c)) - (x1 /* c)) . n) is V22() real ext-real Element of REAL
(x1 /* (x0 + c)) . n is V22() real ext-real Element of REAL
(x1 /* c) . n is V22() real ext-real Element of REAL
((x1 /* (x0 + c)) . n) - ((x1 /* c) . n) is V22() real ext-real Element of REAL
K58(((x1 /* c) . n)) is V22() real ext-real set
K56(((x1 /* (x0 + c)) . n),K58(((x1 /* c) . n))) is V22() real ext-real set
((x0 ") . n) * (((x1 /* (x0 + c)) . n) - ((x1 /* c) . n)) is V22() real ext-real Element of REAL
(x1 . ((x0 + c) . n)) - ((x1 /* c) . n) is V22() real ext-real Element of REAL
K56((x1 . ((x0 + c) . n)),K58(((x1 /* c) . n))) is V22() real ext-real set
((x0 ") . n) * ((x1 . ((x0 + c) . n)) - ((x1 /* c) . n)) is V22() real ext-real Element of REAL
c . n is V22() real ext-real Element of REAL
x1 . (c . n) is V22() real ext-real Element of REAL
(x1 . ((x0 + c) . n)) - (x1 . (c . n)) is V22() real ext-real Element of REAL
K58((x1 . (c . n))) is V22() real ext-real set
K56((x1 . ((x0 + c) . n)),K58((x1 . (c . n)))) is V22() real ext-real set
((x0 ") . n) * ((x1 . ((x0 + c) . n)) - (x1 . (c . n))) is V22() real ext-real Element of REAL
((x0 ") . n) * ((x1 . ((x0 + c) . n)) - (x1 . f3)) is V22() real ext-real Element of REAL
diff (x1,f3) is V22() real ext-real Element of REAL
lim ((x0 ") (#) ((x1 /* (x0 + c)) - (x1 /* c))) is V22() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / (n + 2) is V22() real ext-real Element of REAL
K59((n + 2)) is non empty V22() real ext-real positive non negative set
K57(f,K59((n + 2))) is V22() real ext-real set
- (f / (n + 2)) is V22() real ext-real Element of REAL
s3 . n is V22() real ext-real Element of REAL
h2 " 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))
x1 /* (h2 + 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))
(x1 /* (h2 + c)) - (x1 /* 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))
(h2 ") (#) ((x1 /* (h2 + c)) - (x1 /* 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))
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
((h2 ") (#) ((x1 /* (h2 + c)) - (x1 /* c))) . n is V22() real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
(h2 + c) . n1 is V22() real ext-real Element of REAL
h2 . n is V22() real ext-real Element of REAL
- (h2 . n) is V22() real ext-real Element of REAL
1 / (- (h2 . n)) is V22() real ext-real Element of REAL
K59((- (h2 . n))) is V22() real ext-real set
K57(1,K59((- (h2 . n)))) is V22() real ext-real set
(h2 ") . n is V22() real ext-real Element of REAL
(h2 . n) " is V22() real ext-real Element of REAL
1 / (h2 . n) is V22() real ext-real Element of REAL
K59((h2 . n)) is V22() real ext-real set
K57(1,K59((h2 . n))) is V22() real ext-real set
- (1 / (h2 . n)) is V22() real ext-real Element of REAL
(h2 + c) . n is V22() real ext-real Element of REAL
x1 . ((h2 + c) . n) is V22() real ext-real Element of REAL
(x1 . ((h2 + c) . n)) - (x1 . f3) is V22() real ext-real Element of REAL
K58((x1 . f3)) is V22() real ext-real set
K56((x1 . ((h2 + c) . n)),K58((x1 . f3))) is V22() real ext-real set
rng c is V47() V48() V49() Element of K19(REAL)
((x1 /* (h2 + c)) - (x1 /* c)) . n is V22() real ext-real Element of REAL
((h2 ") . n) * (((x1 /* (h2 + c)) - (x1 /* c)) . n) is V22() real ext-real Element of REAL
(x1 /* (h2 + c)) . n is V22() real ext-real Element of REAL
(x1 /* c) . n is V22() real ext-real Element of REAL
((x1 /* (h2 + c)) . n) - ((x1 /* c) . n) is V22() real ext-real Element of REAL
K58(((x1 /* c) . n)) is V22() real ext-real set
K56(((x1 /* (h2 + c)) . n),K58(((x1 /* c) . n))) is V22() real ext-real set
((h2 ") . n) * (((x1 /* (h2 + c)) . n) - ((x1 /* c) . n)) is V22() real ext-real Element of REAL
(x1 . ((h2 + c) . n)) - ((x1 /* c) . n) is V22() real ext-real Element of REAL
K56((x1 . ((h2 + c) . n)),K58(((x1 /* c) . n))) is V22() real ext-real set
((h2 ") . n) * ((x1 . ((h2 + c) . n)) - ((x1 /* c) . n)) is V22() real ext-real Element of REAL
c . n is V22() real ext-real Element of REAL
x1 . (c . n) is V22() real ext-real Element of REAL
(x1 . ((h2 + c) . n)) - (x1 . (c . n)) is V22() real ext-real Element of REAL
K58((x1 . (c . n))) is V22() real ext-real set
K56((x1 . ((h2 + c) . n)),K58((x1 . (c . n)))) is V22() real ext-real set
((h2 ") . n) * ((x1 . ((h2 + c) . n)) - (x1 . (c . n))) is V22() real ext-real Element of REAL
((h2 ") . n) * ((x1 . ((h2 + c) . n)) - (x1 . f3)) is V22() real ext-real Element of REAL
lim ((h2 ") (#) ((x1 /* (h2 + c)) - (x1 /* c))) is V22() real ext-real Element of REAL
f4 is V47() V48() V49() open Neighbourhood of x
f5 is V22() real ext-real set
x - f5 is V22() real ext-real Element of REAL
K58(f5) is V22() real ext-real set
K56(x,K58(f5)) is V22() real ext-real set
x + f5 is V22() real ext-real Element of REAL
].(x - f5),(x + f5).[ is V47() V48() V49() non left_end non right_end V68() open Element of K19(REAL)
f is V22() real ext-real Element of REAL
2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V45() V46() V47() V48() V49() V50() V51() V52() left_end bounded_below Element of NAT
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))
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
x0 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / (x0 + 2) is V22() real ext-real Element of REAL
K59((x0 + 2)) is non empty V22() real ext-real positive non negative set
K57(f,K59((x0 + 2))) is V22() real ext-real set
x0 . x0 is V22() real ext-real Element of REAL
lim x0 is V22() real ext-real Element of REAL
{x} is non empty V47() V48() V49() Element of K19(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 V47() V48() V49() Element of K19(REAL)
c is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s3 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
c . s3 is V22() real ext-real Element of REAL
s3 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))
h2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
s3 . h2 is V22() real ext-real Element of REAL
h2 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / (h2 + 2) is V22() real ext-real Element of REAL
K59((h2 + 2)) is non empty V22() real ext-real positive non negative set
K57(f,K59((h2 + 2))) is V22() real ext-real set
- (f / (h2 + 2)) is V22() real ext-real Element of REAL
- f is V22() real ext-real Element of REAL
(- f) / (h2 + 2) is V22() real ext-real Element of REAL
K57((- f),K59((h2 + 2))) is V22() real ext-real set
lim s3 is V22() real ext-real Element of REAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V47() V48() V49() V50() V51() V52() V53() bounded_below V68() Element of REAL
h2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
h2 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / (h2 + 2) is V22() real ext-real Element of REAL
K59((h2 + 2)) is non empty V22() real ext-real positive non negative set
K57(f,K59((h2 + 2))) is V22() real ext-real set
- (f / (h2 + 2)) is V22() real ext-real Element of REAL
s3 . h2 is V22() real ext-real Element of REAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / 1 is V22() real ext-real Element of REAL
K59(1) is non empty V22() real ext-real positive non negative set
K57(f,K59(1)) is V22() real ext-real set
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / (n + 2) is V22() real ext-real Element of REAL
K59((n + 2)) is non empty V22() real ext-real positive non negative set
K57(f,K59((n + 2))) is V22() real ext-real set
x - (f / (n + 2)) is V22() real ext-real Element of REAL
K58((f / (n + 2))) is V22() real ext-real set
K56(x,K58((f / (n + 2)))) is V22() real ext-real set
x - f is V22() real ext-real Element of REAL
K58(f) is V22() real ext-real set
K56(x,K58(f)) is V22() real ext-real set
x + f is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= x - f & not x + f <= b1 ) } is set
h2 is V1() non-zero V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
h2 + 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))
rng (h2 + c) is V47() V48() V49() Element of K19(REAL)
n is set
n1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
(h2 + c) . n1 is V22() real ext-real Element of REAL
h2 . n1 is V22() real ext-real Element of REAL
c . n1 is V22() real ext-real Element of REAL
(h2 . n1) + (c . n1) is V22() real ext-real Element of REAL
n1 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / (n1 + 2) is V22() real ext-real Element of REAL
K59((n1 + 2)) is non empty V22() real ext-real positive non negative set
K57(f,K59((n1 + 2))) is V22() real ext-real set
- (f / (n1 + 2)) is V22() real ext-real Element of REAL
(- (f / (n1 + 2))) + (c . n1) is V22() real ext-real Element of REAL
x - (f / (n1 + 2)) is V22() real ext-real Element of REAL
K58((f / (n1 + 2))) is V22() real ext-real set
K56(x,K58((f / (n1 + 2)))) is V22() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / (n + 2) is V22() real ext-real Element of REAL
K59((n + 2)) is non empty V22() real ext-real positive non negative set
K57(f,K59((n + 2))) is V22() real ext-real set
x + (f / (n + 2)) is V22() real ext-real Element of REAL
x0 is V1() non-zero V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
x0 + 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))
rng (x0 + c) is V47() V48() V49() Element of K19(REAL)
n is set
n1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
(x0 + c) . n1 is V22() real ext-real Element of REAL
x0 . n1 is V22() real ext-real Element of REAL
c . n1 is V22() real ext-real Element of REAL
(x0 . n1) + (c . n1) is V22() real ext-real Element of REAL
n1 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / (n1 + 2) is V22() real ext-real Element of REAL
K59((n1 + 2)) is non empty V22() real ext-real positive non negative set
K57(f,K59((n1 + 2))) is V22() real ext-real set
(f / (n1 + 2)) + (c . n1) is V22() real ext-real Element of REAL
x + (f / (n1 + 2)) is V22() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / (n + 2) is V22() real ext-real Element of REAL
K59((n + 2)) is non empty V22() real ext-real positive non negative set
K57(f,K59((n + 2))) is V22() real ext-real set
x0 . n is V22() real ext-real Element of REAL
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))
x1 /* (x0 + 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))
x1 /* 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))
(x1 /* (x0 + c)) - (x1 /* 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))
(x0 ") (#) ((x1 /* (x0 + c)) - (x1 /* 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))
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
((x0 ") (#) ((x1 /* (x0 + c)) - (x1 /* c))) . n is V22() real ext-real Element of REAL
x0 . n is V22() real ext-real Element of REAL
(x0 ") . n is V22() real ext-real Element of REAL
(x0 . n) " is V22() real ext-real Element of REAL
(x0 + c) . n is V22() real ext-real Element of REAL
f is V47() V48() V49() open Element of K19(REAL)
x1 . ((x0 + c) . n) is V22() real ext-real Element of REAL
(x1 . x) - (x1 . ((x0 + c) . n)) is V22() real ext-real Element of REAL
K58((x1 . ((x0 + c) . n))) is V22() real ext-real set
K56((x1 . x),K58((x1 . ((x0 + c) . n)))) is V22() real ext-real set
- ((x1 . x) - (x1 . ((x0 + c) . n))) is V22() real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
(x0 + c) . n1 is V22() real ext-real Element of REAL
rng c is V47() V48() V49() Element of K19(REAL)
((x1 /* (x0 + c)) - (x1 /* c)) . n is V22() real ext-real Element of REAL
((x0 ") . n) * (((x1 /* (x0 + c)) - (x1 /* c)) . n) is V22() real ext-real Element of REAL
(x1 /* (x0 + c)) . n is V22() real ext-real Element of REAL
(x1 /* c) . n is V22() real ext-real Element of REAL
((x1 /* (x0 + c)) . n) - ((x1 /* c) . n) is V22() real ext-real Element of REAL
K58(((x1 /* c) . n)) is V22() real ext-real set
K56(((x1 /* (x0 + c)) . n),K58(((x1 /* c) . n))) is V22() real ext-real set
((x0 ") . n) * (((x1 /* (x0 + c)) . n) - ((x1 /* c) . n)) is V22() real ext-real Element of REAL
(x1 . ((x0 + c) . n)) - ((x1 /* c) . n) is V22() real ext-real Element of REAL
K56((x1 . ((x0 + c) . n)),K58(((x1 /* c) . n))) is V22() real ext-real set
((x0 ") . n) * ((x1 . ((x0 + c) . n)) - ((x1 /* c) . n)) is V22() real ext-real Element of REAL
c . n is V22() real ext-real Element of REAL
x1 . (c . n) is V22() real ext-real Element of REAL
(x1 . ((x0 + c) . n)) - (x1 . (c . n)) is V22() real ext-real Element of REAL
K58((x1 . (c . n))) is V22() real ext-real set
K56((x1 . ((x0 + c) . n)),K58((x1 . (c . n)))) is V22() real ext-real set
((x0 ") . n) * ((x1 . ((x0 + c) . n)) - (x1 . (c . n))) is V22() real ext-real Element of REAL
(x1 . ((x0 + c) . n)) - (x1 . x) is V22() real ext-real Element of REAL
K58((x1 . x)) is V22() real ext-real set
K56((x1 . ((x0 + c) . n)),K58((x1 . x))) is V22() real ext-real set
((x0 ") . n) * ((x1 . ((x0 + c) . n)) - (x1 . x)) is V22() real ext-real Element of REAL
diff (x1,x) is V22() real ext-real Element of REAL
lim ((x0 ") (#) ((x1 /* (x0 + c)) - (x1 /* c))) is V22() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative Element of REAL
f / (n + 2) is V22() real ext-real Element of REAL
K59((n + 2)) is non empty V22() real ext-real positive non negative set
K57(f,K59((n + 2))) is V22() real ext-real set
- (f / (n + 2)) is V22() real ext-real Element of REAL
s3 . n is V22() real ext-real Element of REAL
h2 " 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))
x1 /* (h2 + 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))
(x1 /* (h2 + c)) - (x1 /* 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))
(h2 ") (#) ((x1 /* (h2 + c)) - (x1 /* 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))
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
((h2 ") (#) ((x1 /* (h2 + c)) - (x1 /* c))) . n is V22() real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V45() V46() V47() V48() V49() V50() V51() V52() bounded_below Element of NAT
(h2 + c) . n1 is V22() real ext-real Element of REAL
h2 . n is V22() real ext-real Element of REAL
- (h2 . n) is V22() real ext-real Element of REAL
1 / (- (h2 . n)) is V22() real ext-real Element of REAL
K59((- (h2 . n))) is V22() real ext-real set
K57(1,K59((- (h2 . n)))) is V22() real ext-real set
(h2 ") . n is V22() real ext-real Element of REAL
(h2 . n) " is V22() real ext-real Element of REAL
1 / (h2 . n) is V22() real ext-real Element of REAL
K59((h2 . n)) is V22() real ext-real set
K57(1,K59((h2 . n))) is V22() real ext-real set
- (1 / (h2 . n)) is V22() real ext-real Element of REAL
(h2 + c) . n is V22() real ext-real Element of REAL
f is V47() V48() V49() open Element of K19(REAL)
x1 . ((h2 + c) . n) is V22() real ext-real Element of REAL
(x1 . x) - (x1 . ((h2 + c) . n)) is V22() real ext-real Element of REAL
K58((x1 . ((h2 + c) . n))) is V22() real ext-real set
K56((x1 . x),K58((x1 . ((h2 + c) . n)))) is V22() real ext-real set
- ((x1 . x) - (x1 . ((h2 + c) . n))) is V22() real ext-real Element of REAL
rng c is V47() V48() V49() Element of K19(REAL)
((x1 /* (h2 + c)) - (x1 /* c)) . n is V22() real ext-real Element of REAL
((h2 ") . n) * (((x1 /* (h2 + c)) - (x1 /* c)) . n) is V22() real ext-real Element of REAL
(x1 /* (h2 + c)) . n is V22() real ext-real Element of REAL
(x1 /* c) . n is V22() real ext-real Element of REAL
((x1 /* (h2 + c)) . n) - ((x1 /* c) . n) is V22() real ext-real Element of REAL
K58(((x1 /* c) . n)) is V22() real ext-real set
K56(((x1 /* (h2 + c)) . n),K58(((x1 /* c) . n))) is V22() real ext-real set
((h2 ") . n) * (((x1 /* (h2 + c)) . n) - ((x1 /* c) . n)) is V22() real ext-real Element of REAL
(x1 . ((h2 + c) . n)) - ((x1 /* c) . n) is V22() real ext-real Element of REAL
K56((x1 . ((h2 + c) . n)),K58(((x1 /* c) . n))) is V22() real ext-real set
((h2 ") . n) * ((x1 . ((h2 + c) . n)) - ((x1 /* c) . n)) is V22() real ext-real Element of REAL
c . n is V22() real ext-real Element of REAL
x1 . (c . n) is V22() real ext-real Element of REAL
(x1 . ((h2 + c) . n)) - (x1 . (c . n)) is V22() real ext-real Element of REAL
K58((x1 . (c . n))) is V22() real ext-real set
K56((x1 . ((h2 + c) . n)),K58((x1 . (c . n)))) is V22() real ext-real set
((h2 ") . n) * ((x1 . ((h2 + c) . n)) - (x1 . (c . n))) is V22() real ext-real Element of REAL
(x1 . ((h2 + c) . n)) - (x1 . x) is V22() real ext-real Element of REAL
K58((x1 . x)) is V22() real ext-real set
K56((x1 . ((h2 + c) . n)),K58((x1 . x))) is V22() real ext-real set
((h2 ") . n) * ((x1 . ((h2 + c) . n)) - (x1 . x)) is V22() real ext-real Element of REAL
lim ((h2 ") (#) ((x1 /* (h2 + c)) - (x1 /* c))) is V22() real ext-real Element of REAL
diff (x1,f3) is V22() real ext-real Element of REAL
diff (x1,x) is V22() real ext-real Element of REAL
diff (x1,f3) is V22() real ext-real Element of REAL
diff (x1,x) is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
p + g is V22() real ext-real Element of REAL
[.p,(p + g).] is V47() V48() V49() V68() closed Element of K19(REAL)
].p,(p + g).[ is V47() V48() V49() non left_end non right_end V68() open 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 V47() V48() V49() Element of K19(REAL)
f | [.p,(p + g).] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f . p is V22() real ext-real Element of REAL
f . (p + g) is V22() real ext-real Element of REAL
x1 is V22() real ext-real Element of REAL
diff (f,x1) is V22() real ext-real Element of REAL
x1 - p is V22() real ext-real Element of REAL
K58(p) is V22() real ext-real set
K56(x1,K58(p)) is V22() real ext-real set
(x1 - p) / g is V22() real ext-real Element of REAL
K59(g) is V22() real ext-real set
K57((x1 - p),K59(g)) is V22() real ext-real set
x2 is V22() real ext-real Element of REAL
x2 * g is V22() real ext-real Element of REAL
p + (x2 * g) is V22() real ext-real Element of REAL
diff (f,(p + (x2 * g))) is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= p & not p + g <= b1 ) } is set
Z is V22() real ext-real Element of REAL
0 / g is V22() real ext-real Element of REAL
K57(0,K59(g)) is V22() real ext-real set
Z is V22() real ext-real Element of REAL
g / g is V22() real ext-real Element of REAL
K57(g,K59(g)) is V22() real ext-real set
(x2 * g) + p is V22() real ext-real Element of REAL
(x1 - p) + p is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
[.p,g.] is V47() V48() V49() V68() closed Element of K19(REAL)
].p,g.[ is V47() V48() V49() non left_end non right_end V68() open Element of K19(REAL)
g - p is V22() real ext-real Element of REAL
K58(p) is V22() real ext-real set
K56(g,K58(p)) is V22() real ext-real set
x1 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom x1 is V47() V48() V49() Element of K19(REAL)
x1 | [.p,g.] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x1 . g is V22() real ext-real Element of REAL
x1 . p is V22() real ext-real Element of REAL
(x1 . g) - (x1 . p) is V22() real ext-real Element of REAL
K58((x1 . p)) is V22() real ext-real set
K56((x1 . g),K58((x1 . p))) is V22() real ext-real set
((x1 . g) - (x1 . p)) / (g - p) is V22() real ext-real Element of REAL
K59((g - p)) is V22() real ext-real set
K57(((x1 . g) - (x1 . p)),K59((g - p))) is V22() real ext-real set
Z is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom Z is V47() V48() V49() Element of K19(REAL)
x1 - Z is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f3 is set
(dom x1) /\ (dom Z) is V47() V48() V49() Element of K19(REAL)
dom (x1 - Z) is V47() V48() V49() Element of K19(REAL)
{p,g} is non empty V47() V48() V49() set
].p,g.[ \/ {p,g} is non empty V47() V48() V49() set
(x1 - Z) . p is V22() real ext-real Element of REAL
Z . p is V22() real ext-real Element of REAL
(x1 . p) - (Z . p) is V22() real ext-real Element of REAL
K58((Z . p)) is V22() real ext-real set
K56((x1 . p),K58((Z . p))) is V22() real ext-real set
p - p is V22() real ext-real Element of REAL
K56(p,K58(p)) is V22() real ext-real set
(((x1 . g) - (x1 . p)) / (g - p)) * (p - p) is V22() real ext-real Element of REAL
(x1 . p) - ((((x1 . g) - (x1 . p)) / (g - p)) * (p - p)) is V22() real ext-real Element of REAL
K58(((((x1 . g) - (x1 . p)) / (g - p)) * (p - p))) is V22() real ext-real set
K56((x1 . p),K58(((((x1 . g) - (x1 . p)) / (g - p)) * (p - p)))) is V22() real ext-real set
f is V47() V48() V49() open Element of K19(REAL)
f3 is V22() real ext-real Element of REAL
Z . f3 is V22() real ext-real Element of REAL
f3 - p is V22() real ext-real Element of REAL
K56(f3,K58(p)) is V22() real ext-real set
(((x1 . g) - (x1 . p)) / (g - p)) * (f3 - p) is V22() real ext-real Element of REAL
(((x1 . g) - (x1 . p)) / (g - p)) * f3 is V22() real ext-real Element of REAL
(((x1 . g) - (x1 . p)) / (g - p)) * p is V22() real ext-real Element of REAL
- ((((x1 . g) - (x1 . p)) / (g - p)) * p) is V22() real ext-real Element of REAL
((((x1 . g) - (x1 . p)) / (g - p)) * f3) + (- ((((x1 . g) - (x1 . p)) / (g - p)) * p)) is V22() real ext-real Element of REAL
f3 is V22() real ext-real set
Z . f3 is V22() real ext-real Element of REAL
f3 - p is V22() real ext-real Element of REAL
K56(f3,K58(p)) is V22() real ext-real set
(((x1 . g) - (x1 . p)) / (g - p)) * (f3 - p) is V22() real ext-real Element of REAL
(((x1 . g) - (x1 . p)) / (g - p)) * f3 is V22() real ext-real Element of REAL
((((x1 . g) - (x1 . p)) / (g - p)) * f3) + (- ((((x1 . g) - (x1 . p)) / (g - p)) * p)) is V22() real ext-real Element of REAL
Z | [.p,g.] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(x1 - Z) | [.p,g.] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(x1 - Z) . g is V22() real ext-real Element of REAL
Z . g is V22() real ext-real Element of REAL
(x1 . g) - (Z . g) is V22() real ext-real Element of REAL
K58((Z . g)) is V22() real ext-real set
K56((x1 . g),K58((Z . g))) is V22() real ext-real set
(((x1 . g) - (x1 . p)) / (g - p)) * (g - p) is V22() real ext-real Element of REAL
(x1 . g) - ((((x1 . g) - (x1 . p)) / (g - p)) * (g - p)) is V22() real ext-real Element of REAL
K58(((((x1 . g) - (x1 . p)) / (g - p)) * (g - p))) is V22() real ext-real set
K56((x1 . g),K58(((((x1 . g) - (x1 . p)) / (g - p)) * (g - p)))) is V22() real ext-real set
(x1 . g) - ((x1 . g) - (x1 . p)) is V22() real ext-real Element of REAL
K58(((x1 . g) - (x1 . p))) is V22() real ext-real set
K56((x1 . g),K58(((x1 . g) - (x1 . p)))) is V22() real ext-real set
f3 is V22() real ext-real Element of REAL
diff ((x1 - Z),f3) is V22() real ext-real Element of REAL
diff (x1,f3) is V22() real ext-real Element of REAL
(x1 - Z) `| f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((x1 - Z) `| f) . f3 is V22() real ext-real Element of REAL
diff (Z,f3) is V22() real ext-real Element of REAL
(diff (x1,f3)) - (diff (Z,f3)) is V22() real ext-real Element of REAL
K58((diff (Z,f3))) is V22() real ext-real set
K56((diff (x1,f3)),K58((diff (Z,f3)))) is V22() real ext-real set
Z `| f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(Z `| f) . f3 is V22() real ext-real Element of REAL
(diff (x1,f3)) - ((Z `| f) . f3) is V22() real ext-real Element of REAL
K58(((Z `| f) . f3)) is V22() real ext-real set
K56((diff (x1,f3)),K58(((Z `| f) . f3))) is V22() real ext-real set
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
p + g is V22() real ext-real Element of REAL
[.p,(p + g).] is V47() V48() V49() V68() closed Element of K19(REAL)
].p,(p + g).[ is V47() V48() V49() non left_end non right_end V68() open 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 V47() V48() V49() Element of K19(REAL)
f | [.p,(p + g).] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f . (p + g) is V22() real ext-real Element of REAL
f . p is V22() real ext-real Element of REAL
(f . (p + g)) - (f . p) is V22() real ext-real Element of REAL
K58((f . p)) is V22() real ext-real set
K56((f . (p + g)),K58((f . p))) is V22() real ext-real set
(p + g) - p is V22() real ext-real Element of REAL
K58(p) is V22() real ext-real set
K56((p + g),K58(p)) is V22() real ext-real set
((f . (p + g)) - (f . p)) / ((p + g) - p) is V22() real ext-real Element of REAL
K59(((p + g) - p)) is V22() real ext-real set
K57(((f . (p + g)) - (f . p)),K59(((p + g) - p))) is V22() real ext-real set
x1 is V22() real ext-real Element of REAL
diff (f,x1) is V22() real ext-real Element of REAL
x1 - p is V22() real ext-real Element of REAL
K56(x1,K58(p)) is V22() real ext-real set
(x1 - p) / g is V22() real ext-real Element of REAL
K59(g) is V22() real ext-real set
K57((x1 - p),K59(g)) is V22() real ext-real set
x2 is V22() real ext-real Element of REAL
x2 * g is V22() real ext-real Element of REAL
p + (x2 * g) is V22() real ext-real Element of REAL
diff (f,(p + (x2 * g))) is V22() real ext-real Element of REAL
g * (diff (f,(p + (x2 * g)))) is V22() real ext-real Element of REAL
(f . p) + (g * (diff (f,(p + (x2 * g))))) is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= p & not p + g <= b1 ) } is set
Z is V22() real ext-real Element of REAL
0 / g is V22() real ext-real Element of REAL
K57(0,K59(g)) is V22() real ext-real set
Z is V22() real ext-real Element of REAL
g / g is V22() real ext-real Element of REAL
K57(g,K59(g)) is V22() real ext-real set
(x2 * g) + p is V22() real ext-real Element of REAL
(x1 - p) + p is V22() real ext-real Element of REAL
g * (diff (f,x1)) is V22() real ext-real Element of REAL
(f . p) + (g * (diff (f,x1))) is V22() real ext-real Element of REAL
(f . p) + ((f . (p + g)) - (f . p)) is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
[.p,g.] is V47() V48() V49() V68() closed Element of K19(REAL)
].p,g.[ is V47() V48() V49() non left_end non right_end V68() open 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 V47() V48() V49() Element of K19(REAL)
f | [.p,g.] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f . g is V22() real ext-real Element of REAL
f . p is V22() real ext-real Element of REAL
(f . g) - (f . p) is V22() real ext-real Element of REAL
K58((f . p)) is V22() real ext-real set
K56((f . g),K58((f . p))) is V22() real ext-real set
x1 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom x1 is V47() V48() V49() Element of K19(REAL)
x1 | [.p,g.] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x1 . g is V22() real ext-real Element of REAL
x1 . p is V22() real ext-real Element of REAL
(x1 . g) - (x1 . p) is V22() real ext-real Element of REAL
K58((x1 . p)) is V22() real ext-real set
K56((x1 . g),K58((x1 . p))) is V22() real ext-real set
x2 is V22() real ext-real Element of REAL
diff (x1,x2) is V22() real ext-real Element of REAL
Z is V22() real ext-real Element of REAL
diff (x1,Z) is V22() real ext-real Element of REAL
((f . g) - (f . p)) * (diff (x1,Z)) is V22() real ext-real Element of REAL
diff (f,Z) is V22() real ext-real Element of REAL
((x1 . g) - (x1 . p)) * (diff (f,Z)) is V22() real ext-real Element of REAL
((f . g) - (f . p)) / ((x1 . g) - (x1 . p)) is V22() real ext-real Element of REAL
K59(((x1 . g) - (x1 . p))) is V22() real ext-real set
K57(((f . g) - (f . p)),K59(((x1 . g) - (x1 . p)))) is V22() real ext-real set
K20([.p,g.],REAL) is complex-valued ext-real-valued real-valued set
K19(K20([.p,g.],REAL)) is set
(x1 . p) * (((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) is V22() real ext-real Element of REAL
(f . p) - ((x1 . p) * (((f . g) - (f . p)) / ((x1 . g) - (x1 . p)))) is V22() real ext-real Element of REAL
K58(((x1 . p) * (((f . g) - (f . p)) / ((x1 . g) - (x1 . p))))) is V22() real ext-real set
K56((f . p),K58(((x1 . p) * (((f . g) - (f . p)) / ((x1 . g) - (x1 . p)))))) is V22() real ext-real set
[.p,g.] --> ((f . p) - ((x1 . p) * (((f . g) - (f . p)) / ((x1 . g) - (x1 . p))))) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x is V1() V4([.p,g.]) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20([.p,g.],REAL))
(((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f3 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) - f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x2 is V47() V48() V49() open Element of K19(REAL)
dom f3 is V47() V48() V49() Element of K19(REAL)
dom ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1) is V47() V48() V49() Element of K19(REAL)
(dom f3) /\ (dom ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) is V47() V48() V49() Element of K19(REAL)
dom (f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) is V47() V48() V49() Element of K19(REAL)
[.p,g.] /\ (dom f3) is V47() V48() V49() Element of K19(REAL)
x0 is V22() real ext-real Element of REAL
f3 . x0 is V22() real ext-real Element of REAL
f3 | [.p,g.] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f3 | ].p,g.[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(dom (f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1))) /\ (dom f) is V47() V48() V49() Element of K19(REAL)
dom ((f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) - f) is V47() V48() V49() Element of K19(REAL)
((f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) - f) . p is V22() real ext-real Element of REAL
(f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) . p is V22() real ext-real Element of REAL
((f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) . p) - (f . p) is V22() real ext-real Element of REAL
K56(((f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) . p),K58((f . p))) is V22() real ext-real set
f3 . p is V22() real ext-real Element of REAL
((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1) . p is V22() real ext-real Element of REAL
(f3 . p) + (((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1) . p) is V22() real ext-real Element of REAL
((f3 . p) + (((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1) . p)) - (f . p) is V22() real ext-real Element of REAL
K56(((f3 . p) + (((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1) . p)),K58((f . p))) is V22() real ext-real set
(((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . p) is V22() real ext-real Element of REAL
(f3 . p) + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . p)) is V22() real ext-real Element of REAL
((f3 . p) + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . p))) - (f . p) is V22() real ext-real Element of REAL
K56(((f3 . p) + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . p))),K58((f . p))) is V22() real ext-real set
(f . p) - ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . p)) is V22() real ext-real Element of REAL
K58(((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . p))) is V22() real ext-real set
K56((f . p),K58(((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . p)))) is V22() real ext-real set
((f . p) - ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . p))) + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . p)) is V22() real ext-real Element of REAL
(((f . p) - ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . p))) + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . p))) - (f . p) is V22() real ext-real Element of REAL
K56((((f . p) - ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . p))) + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . p))),K58((f . p))) is V22() real ext-real set
((f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) - f) . g is V22() real ext-real Element of REAL
(f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) . g is V22() real ext-real Element of REAL
((f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) . g) - (f . g) is V22() real ext-real Element of REAL
K58((f . g)) is V22() real ext-real set
K56(((f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) . g),K58((f . g))) is V22() real ext-real set
f3 . g is V22() real ext-real Element of REAL
((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1) . g is V22() real ext-real Element of REAL
(f3 . g) + (((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1) . g) is V22() real ext-real Element of REAL
((f3 . g) + (((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1) . g)) - (f . g) is V22() real ext-real Element of REAL
K56(((f3 . g) + (((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1) . g)),K58((f . g))) is V22() real ext-real set
(((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . g) is V22() real ext-real Element of REAL
(f3 . g) + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . g)) is V22() real ext-real Element of REAL
((f3 . g) + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . g))) - (f . g) is V22() real ext-real Element of REAL
K56(((f3 . g) + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . g))),K58((f . g))) is V22() real ext-real set
((f . p) - ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . p))) + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . g)) is V22() real ext-real Element of REAL
(((f . p) - ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . p))) + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . g))) - (f . g) is V22() real ext-real Element of REAL
K56((((f . p) - ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . p))) + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (x1 . g))),K58((f . g))) is V22() real ext-real set
- (f . g) is V22() real ext-real Element of REAL
- ((f . g) - (f . p)) is V22() real ext-real Element of REAL
(- ((f . g) - (f . p))) / ((x1 . g) - (x1 . p)) is V22() real ext-real Element of REAL
K57((- ((f . g) - (f . p))),K59(((x1 . g) - (x1 . p)))) is V22() real ext-real set
((- ((f . g) - (f . p))) / ((x1 . g) - (x1 . p))) * ((x1 . g) - (x1 . p)) is V22() real ext-real Element of REAL
(f . p) - (((- ((f . g) - (f . p))) / ((x1 . g) - (x1 . p))) * ((x1 . g) - (x1 . p))) is V22() real ext-real Element of REAL
K58((((- ((f . g) - (f . p))) / ((x1 . g) - (x1 . p))) * ((x1 . g) - (x1 . p)))) is V22() real ext-real set
K56((f . p),K58((((- ((f . g) - (f . p))) / ((x1 . g) - (x1 . p))) * ((x1 . g) - (x1 . p))))) is V22() real ext-real set
(- (f . g)) + ((f . p) - (((- ((f . g) - (f . p))) / ((x1 . g) - (x1 . p))) * ((x1 . g) - (x1 . p)))) is V22() real ext-real Element of REAL
(f . p) - (f . g) is V22() real ext-real Element of REAL
K56((f . p),K58((f . g))) is V22() real ext-real set
(f . p) - ((f . p) - (f . g)) is V22() real ext-real Element of REAL
K58(((f . p) - (f . g))) is V22() real ext-real set
K56((f . p),K58(((f . p) - (f . g)))) is V22() real ext-real set
(- (f . g)) + ((f . p) - ((f . p) - (f . g))) is V22() real ext-real Element of REAL
((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1) | [.p,g.] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) | [.p,g.] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) - f) | [.p,g.] 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
diff (((f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) - f),x0) is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
diff (((f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) - f),x0) is V22() real ext-real Element of REAL
((f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) - f) `| x2 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(((f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) - f) `| x2) . x0 is V22() real ext-real Element of REAL
diff ((f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)),x0) is V22() real ext-real Element of REAL
diff (f,x0) is V22() real ext-real Element of REAL
(diff ((f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)),x0)) - (diff (f,x0)) is V22() real ext-real Element of REAL
K58((diff (f,x0))) is V22() real ext-real set
K56((diff ((f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)),x0)),K58((diff (f,x0)))) is V22() real ext-real set
(f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) `| x2 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) `| x2) . x0 is V22() real ext-real Element of REAL
(((f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) `| x2) . x0) - (diff (f,x0)) is V22() real ext-real Element of REAL
K56((((f3 + ((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1)) `| x2) . x0),K58((diff (f,x0)))) is V22() real ext-real set
diff (f3,x0) is V22() real ext-real Element of REAL
diff (((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1),x0) is V22() real ext-real Element of REAL
(diff (f3,x0)) + (diff (((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1),x0)) is V22() real ext-real Element of REAL
((diff (f3,x0)) + (diff (((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1),x0))) - (diff (f,x0)) is V22() real ext-real Element of REAL
K56(((diff (f3,x0)) + (diff (((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1),x0))),K58((diff (f,x0)))) is V22() real ext-real set
f3 `| x2 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f3 `| x2) . x0 is V22() real ext-real Element of REAL
((f3 `| x2) . x0) + (diff (((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1),x0)) is V22() real ext-real Element of REAL
(((f3 `| x2) . x0) + (diff (((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1),x0))) - (diff (f,x0)) is V22() real ext-real Element of REAL
K56((((f3 `| x2) . x0) + (diff (((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1),x0))),K58((diff (f,x0)))) is V22() real ext-real set
0 + (diff (((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1),x0)) is V22() real ext-real Element of REAL
(0 + (diff (((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1),x0))) - (diff (f,x0)) is V22() real ext-real Element of REAL
K56((0 + (diff (((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1),x0))),K58((diff (f,x0)))) is V22() real ext-real set
((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1) `| x2 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1) `| x2) . x0 is V22() real ext-real Element of REAL
((((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1) `| x2) . x0) - (diff (f,x0)) is V22() real ext-real Element of REAL
K56(((((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) (#) x1) `| x2) . x0),K58((diff (f,x0)))) is V22() real ext-real set
diff (x1,x0) is V22() real ext-real Element of REAL
(((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (diff (x1,x0)) is V22() real ext-real Element of REAL
((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (diff (x1,x0))) - (diff (f,x0)) is V22() real ext-real Element of REAL
K56(((((f . g) - (f . p)) / ((x1 . g) - (x1 . p))) * (diff (x1,x0))),K58((diff (f,x0)))) is V22() real ext-real set
(diff (x1,x0)) * ((f . g) - (f . p)) is V22() real ext-real Element of REAL
((diff (x1,x0)) * ((f . g) - (f . p))) / ((x1 . g) - (x1 . p)) is V22() real ext-real Element of REAL
K57(((diff (x1,x0)) * ((f . g) - (f . p))),K59(((x1 . g) - (x1 . p)))) is V22() real ext-real set
(((diff (x1,x0)) * ((f . g) - (f . p))) / ((x1 . g) - (x1 . p))) * ((x1 . g) - (x1 . p)) is V22() real ext-real Element of REAL
(diff (f,x0)) * ((x1 . g) - (x1 . p)) is V22() real ext-real Element of REAL
((f . g) - (f . p)) * (diff (x1,x0)) is V22() real ext-real Element of REAL
((x1 . g) - (x1 . p)) * (diff (f,x0)) is V22() real ext-real Element of REAL
x2 is V22() real ext-real Element of REAL
diff (x1,x2) is V22() real ext-real Element of REAL
((f . g) - (f . p)) * (diff (x1,x2)) is V22() real ext-real Element of REAL
diff (f,x2) is V22() real ext-real Element of REAL
((x1 . g) - (x1 . p)) * (diff (f,x2)) is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
p + g is V22() real ext-real Element of REAL
[.p,(p + g).] is V47() V48() V49() V68() closed Element of K19(REAL)
].p,(p + g).[ is V47() V48() V49() non left_end non right_end V68() open 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 V47() V48() V49() Element of K19(REAL)
f | [.p,(p + g).] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f . (p + g) is V22() real ext-real Element of REAL
f . p is V22() real ext-real Element of REAL
(f . (p + g)) - (f . p) is V22() real ext-real Element of REAL
K58((f . p)) is V22() real ext-real set
K56((f . (p + g)),K58((f . p))) is V22() real ext-real set
x1 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom x1 is V47() V48() V49() Element of K19(REAL)
x1 | [.p,(p + g).] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x1 . (p + g) is V22() real ext-real Element of REAL
x1 . p is V22() real ext-real Element of REAL
(x1 . (p + g)) - (x1 . p) is V22() real ext-real Element of REAL
K58((x1 . p)) is V22() real ext-real set
K56((x1 . (p + g)),K58((x1 . p))) is V22() real ext-real set
((f . (p + g)) - (f . p)) / ((x1 . (p + g)) - (x1 . p)) is V22() real ext-real Element of REAL
K59(((x1 . (p + g)) - (x1 . p))) is V22() real ext-real set
K57(((f . (p + g)) - (f . p)),K59(((x1 . (p + g)) - (x1 . p)))) is V22() real ext-real set
x2 is V22() real ext-real Element of REAL
diff (x1,x2) is V22() real ext-real Element of REAL
((f . (p + g)) - (f . p)) * (diff (x1,x2)) is V22() real ext-real Element of REAL
diff (f,x2) is V22() real ext-real Element of REAL
((x1 . (p + g)) - (x1 . p)) * (diff (f,x2)) is V22() real ext-real Element of REAL
((f . (p + g)) - (f . p)) / (diff (x1,x2)) is V22() real ext-real Element of REAL
K59((diff (x1,x2))) is V22() real ext-real set
K57(((f . (p + g)) - (f . p)),K59((diff (x1,x2)))) is V22() real ext-real set
(diff (x1,x2)) * (((f . (p + g)) - (f . p)) / (diff (x1,x2))) is V22() real ext-real Element of REAL
(((x1 . (p + g)) - (x1 . p)) * (diff (f,x2))) / (diff (x1,x2)) is V22() real ext-real Element of REAL
K57((((x1 . (p + g)) - (x1 . p)) * (diff (f,x2))),K59((diff (x1,x2)))) is V22() real ext-real set
(diff (f,x2)) / (diff (x1,x2)) is V22() real ext-real Element of REAL
K57((diff (f,x2)),K59((diff (x1,x2)))) is V22() real ext-real set
((x1 . (p + g)) - (x1 . p)) * ((diff (f,x2)) / (diff (x1,x2))) is V22() real ext-real Element of REAL
(((x1 . (p + g)) - (x1 . p)) * ((diff (f,x2)) / (diff (x1,x2)))) / ((x1 . (p + g)) - (x1 . p)) is V22() real ext-real Element of REAL
K57((((x1 . (p + g)) - (x1 . p)) * ((diff (f,x2)) / (diff (x1,x2)))),K59(((x1 . (p + g)) - (x1 . p)))) is V22() real ext-real set
((diff (f,x2)) / (diff (x1,x2))) / ((x1 . (p + g)) - (x1 . p)) is V22() real ext-real Element of REAL
K57(((diff (f,x2)) / (diff (x1,x2))),K59(((x1 . (p + g)) - (x1 . p)))) is V22() real ext-real set
(((diff (f,x2)) / (diff (x1,x2))) / ((x1 . (p + g)) - (x1 . p))) * ((x1 . (p + g)) - (x1 . p)) is V22() real ext-real Element of REAL
x2 - p is V22() real ext-real Element of REAL
K58(p) is V22() real ext-real set
K56(x2,K58(p)) is V22() real ext-real set
(x2 - p) / g is V22() real ext-real Element of REAL
K59(g) is V22() real ext-real set
K57((x2 - p),K59(g)) is V22() real ext-real set
Z is V22() real ext-real Element of REAL
Z * g is V22() real ext-real Element of REAL
p + (Z * g) is V22() real ext-real Element of REAL
diff (f,(p + (Z * g))) is V22() real ext-real Element of REAL
diff (x1,(p + (Z * g))) is V22() real ext-real Element of REAL
(diff (f,(p + (Z * g)))) / (diff (x1,(p + (Z * g)))) is V22() real ext-real Element of REAL
K59((diff (x1,(p + (Z * g))))) is V22() real ext-real set
K57((diff (f,(p + (Z * g)))),K59((diff (x1,(p + (Z * g)))))) is V22() real ext-real set
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= p & not p + g <= b1 ) } is set
x is V22() real ext-real Element of REAL
0 / g is V22() real ext-real Element of REAL
K57(0,K59(g)) is V22() real ext-real set
x is V22() real ext-real Element of REAL
g / g is V22() real ext-real Element of REAL
K57(g,K59(g)) is V22() real ext-real set
(Z * g) + p is V22() real ext-real Element of REAL
(x2 - p) + p is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
].p,g.[ is V47() V48() V49() non left_end non right_end V68() open 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 V47() V48() V49() Element of K19(REAL)
f | ].p,g.[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x1 is V22() real ext-real Element of REAL
].p,g.[ /\ (dom f) is V47() V48() V49() Element of K19(REAL)
x2 is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
x2 - x1 is V22() real ext-real Element of REAL
K58(x1) is V22() real ext-real set
K56(x2,K58(x1)) is V22() real ext-real set
(x2 - x1) " is V22() real ext-real Element of REAL
].x1,x2.[ is V47() V48() V49() non left_end non right_end V68() open Element of K19(REAL)
[.x1,x2.] is V47() V48() V49() V68() closed Element of K19(REAL)
f | [.x1,x2.] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
Z is V47() V48() V49() open Element of K19(REAL)
f . x2 is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
(f . x2) - (f . x1) is V22() real ext-real Element of REAL
K58((f . x1)) is V22() real ext-real set
K56((f . x2),K58((f . x1))) is V22() real ext-real set
((f . x2) - (f . x1)) / (x2 - x1) is V22() real ext-real Element of REAL
K59((x2 - x1)) is V22() real ext-real set
K57(((f . x2) - (f . x1)),K59((x2 - x1))) is V22() real ext-real set
x is V22() real ext-real Element of REAL
diff (f,x) is V22() real ext-real Element of REAL
x1 - x2 is V22() real ext-real Element of REAL
K58(x2) is V22() real ext-real set
K56(x1,K58(x2)) is V22() real ext-real set
(x1 - x2) " is V22() real ext-real Element of REAL
].x2,x1.[ is V47() V48() V49() non left_end non right_end V68() open Element of K19(REAL)
[.x2,x1.] is V47() V48() V49() V68() closed Element of K19(REAL)
f | [.x2,x1.] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
Z is V47() V48() V49() open Element of K19(REAL)
f . x1 is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
(f . x1) - (f . x2) is V22() real ext-real Element of REAL
K58((f . x2)) is V22() real ext-real set
K56((f . x1),K58((f . x2))) is V22() real ext-real set
((f . x1) - (f . x2)) / (x1 - x2) is V22() real ext-real Element of REAL
K59((x1 - x2)) is V22() real ext-real set
K57(((f . x1) - (f . x2)),K59((x1 - x2))) is V22() real ext-real set
x is V22() real ext-real Element of REAL
diff (f,x) is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
].p,g.[ is V47() V48() V49() non left_end non right_end V68() open 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))
x1 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f - x1 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f - x1) | ].p,g.[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
dom x1 is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom x1) is V47() V48() V49() Element of K19(REAL)
dom (f - x1) is V47() V48() V49() Element of K19(REAL)
x2 is V47() V48() V49() open Element of K19(REAL)
Z is V22() real ext-real Element of REAL
diff ((f - x1),Z) is V22() real ext-real Element of REAL
(f - x1) `| x2 is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f - x1) `| x2) . Z is V22() real ext-real Element of REAL
diff (f,Z) is V22() real ext-real Element of REAL
diff (x1,Z) is V22() real ext-real Element of REAL
(diff (f,Z)) - (diff (x1,Z)) is V22() real ext-real Element of REAL
K58((diff (x1,Z))) is V22() real ext-real set
K56((diff (f,Z)),K58((diff (x1,Z)))) is V22() real ext-real set
(diff (f,Z)) - (diff (f,Z)) is V22() real ext-real Element of REAL
K58((diff (f,Z))) is V22() real ext-real set
K56((diff (f,Z)),K58((diff (f,Z)))) is V22() real ext-real set
].p,g.[ /\ (dom (f - x1)) is V47() V48() V49() Element of K19(REAL)
Z is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
f . x is V22() real ext-real Element of REAL
x1 . x is V22() real ext-real Element of REAL
(x1 . x) + Z is V22() real ext-real Element of REAL
(f - x1) . x is V22() real ext-real Element of REAL
(f . x) - (x1 . x) is V22() real ext-real Element of REAL
K58((x1 . x)) is V22() real ext-real set
K56((f . x),K58((x1 . x))) is V22() real ext-real set
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
].p,g.[ is V47() V48() V49() non left_end non right_end V68() open 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 V47() V48() V49() Element of K19(REAL)
f | ].p,g.[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x1 is V22() real ext-real Element of REAL
].p,g.[ /\ (dom f) is V47() V48() V49() Element of K19(REAL)
x2 is V22() real ext-real Element of REAL
x2 - x1 is V22() real ext-real Element of REAL
K58(x1) is V22() real ext-real set
K56(x2,K58(x1)) is V22() real ext-real set
].x1,x2.[ is V47() V48() V49() non left_end non right_end V68() open Element of K19(REAL)
[.x1,x2.] is V47() V48() V49() V68() closed Element of K19(REAL)
f | [.x1,x2.] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
Z is V47() V48() V49() open Element of K19(REAL)
f . x2 is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
(f . x2) - (f . x1) is V22() real ext-real Element of REAL
K58((f . x1)) is V22() real ext-real set
K56((f . x2),K58((f . x1))) is V22() real ext-real set
((f . x2) - (f . x1)) / (x2 - x1) is V22() real ext-real Element of REAL
K59((x2 - x1)) is V22() real ext-real set
K57(((f . x2) - (f . x1)),K59((x2 - x1))) is V22() real ext-real set
x is V22() real ext-real Element of REAL
diff (f,x) is V22() real ext-real Element of REAL
(f . x1) + 0 is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
].p,g.[ is V47() V48() V49() non left_end non right_end V68() open 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 V47() V48() V49() Element of K19(REAL)
f | ].p,g.[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x1 is V22() real ext-real Element of REAL
].p,g.[ /\ (dom f) is V47() V48() V49() Element of K19(REAL)
x2 is V22() real ext-real Element of REAL
x2 - x1 is V22() real ext-real Element of REAL
K58(x1) is V22() real ext-real set
K56(x2,K58(x1)) is V22() real ext-real set
].x1,x2.[ is V47() V48() V49() non left_end non right_end V68() open Element of K19(REAL)
[.x1,x2.] is V47() V48() V49() V68() closed Element of K19(REAL)
f | [.x1,x2.] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
Z is V47() V48() V49() open Element of K19(REAL)
f . x2 is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
(f . x2) - (f . x1) is V22() real ext-real Element of REAL
K58((f . x1)) is V22() real ext-real set
K56((f . x2),K58((f . x1))) is V22() real ext-real set
((f . x2) - (f . x1)) / (x2 - x1) is V22() real ext-real Element of REAL
K59((x2 - x1)) is V22() real ext-real set
K57(((f . x2) - (f . x1)),K59((x2 - x1))) is V22() real ext-real set
x is V22() real ext-real Element of REAL
diff (f,x) is V22() real ext-real Element of REAL
(f . x1) + 0 is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
].p,g.[ is V47() V48() V49() non left_end non right_end V68() open 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 V47() V48() V49() Element of K19(REAL)
f | ].p,g.[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x1 is V22() real ext-real Element of REAL
].p,g.[ /\ (dom f) is V47() V48() V49() Element of K19(REAL)
x2 is V22() real ext-real Element of REAL
x2 - x1 is V22() real ext-real Element of REAL
K58(x1) is V22() real ext-real set
K56(x2,K58(x1)) is V22() real ext-real set
].x1,x2.[ is V47() V48() V49() non left_end non right_end V68() open Element of K19(REAL)
[.x1,x2.] is V47() V48() V49() V68() closed Element of K19(REAL)
f | [.x1,x2.] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
Z is V47() V48() V49() open Element of K19(REAL)
f . x2 is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
(f . x2) - (f . x1) is V22() real ext-real Element of REAL
K58((f . x1)) is V22() real ext-real set
K56((f . x2),K58((f . x1))) is V22() real ext-real set
((f . x2) - (f . x1)) / (x2 - x1) is V22() real ext-real Element of REAL
K59((x2 - x1)) is V22() real ext-real set
K57(((f . x2) - (f . x1)),K59((x2 - x1))) is V22() real ext-real set
x is V22() real ext-real Element of REAL
diff (f,x) is V22() real ext-real Element of REAL
0 * (x2 - x1) is V22() real ext-real Element of REAL
(((f . x2) - (f . x1)) / (x2 - x1)) * (x2 - x1) is V22() real ext-real Element of REAL
(f . x1) + 0 is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
].p,g.[ is V47() V48() V49() non left_end non right_end V68() open 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 V47() V48() V49() Element of K19(REAL)
f | ].p,g.[ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x1 is V22() real ext-real Element of REAL
].p,g.[ /\ (dom f) is V47() V48() V49() Element of K19(REAL)
x2 is V22() real ext-real Element of REAL
x2 - x1 is V22() real ext-real Element of REAL
K58(x1) is V22() real ext-real set
K56(x2,K58(x1)) is V22() real ext-real set
].x1,x2.[ is V47() V48() V49() non left_end non right_end V68() open Element of K19(REAL)
[.x1,x2.] is V47() V48() V49() V68() closed Element of K19(REAL)
f | [.x1,x2.] is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
Z is V47() V48() V49() open Element of K19(REAL)
f . x2 is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
(f . x2) - (f . x1) is V22() real ext-real Element of REAL
K58((f . x1)) is V22() real ext-real set
K56((f . x2),K58((f . x1))) is V22() real ext-real set
((f . x2) - (f . x1)) / (x2 - x1) is V22() real ext-real Element of REAL
K59((x2 - x1)) is V22() real ext-real set
K57(((f . x2) - (f . x1)),K59((x2 - x1))) is V22() real ext-real set
(((f . x2) - (f . x1)) / (x2 - x1)) * (x2 - x1) is V22() real ext-real Element of REAL
0 * (x2 - x1) is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
diff (f,x) is V22() real ext-real Element of REAL
(f . x1) + 0 is V22() real ext-real Element of REAL