REAL is non empty V56() V57() V58() V62() V63() set
NAT is V56() V57() V58() V59() V60() V61() V62() Element of K10(REAL)
K10(REAL) is non empty set
COMPLEX is non empty V56() V62() V63() set
RAT is non empty V56() V57() V58() V59() V62() V63() set
INT is non empty V56() V57() V58() V59() V60() V62() V63() set
K11(COMPLEX,COMPLEX) is non empty V46() set
K10(K11(COMPLEX,COMPLEX)) is non empty set
K11(K11(COMPLEX,COMPLEX),COMPLEX) is non empty V46() set
K10(K11(K11(COMPLEX,COMPLEX),COMPLEX)) is non empty set
K11(REAL,REAL) is non empty V46() V47() V48() set
K10(K11(REAL,REAL)) is non empty set
K11(K11(REAL,REAL),REAL) is non empty V46() V47() V48() set
K10(K11(K11(REAL,REAL),REAL)) is non empty set
K11(RAT,RAT) is non empty V11( RAT ) V46() V47() V48() set
K10(K11(RAT,RAT)) is non empty set
K11(K11(RAT,RAT),RAT) is non empty V11( RAT ) V46() V47() V48() set
K10(K11(K11(RAT,RAT),RAT)) is non empty set
K11(INT,INT) is non empty V11( RAT ) V11( INT ) V46() V47() V48() set
K10(K11(INT,INT)) is non empty set
K11(K11(INT,INT),INT) is non empty V11( RAT ) V11( INT ) V46() V47() V48() set
K10(K11(K11(INT,INT),INT)) is non empty set
K11(NAT,NAT) is V11( RAT ) V11( INT ) V46() V47() V48() V49() set
K11(K11(NAT,NAT),NAT) is V11( RAT ) V11( INT ) V46() V47() V48() V49() set
K10(K11(K11(NAT,NAT),NAT)) is non empty set
NAT is V56() V57() V58() V59() V60() V61() V62() set
K10(NAT) is non empty set
K10(NAT) is non empty set
K11(COMPLEX,REAL) is non empty V46() V47() V48() set
K10(K11(COMPLEX,REAL)) is non empty set
1 is non empty V38() V39() V40() V41() V42() V43() V44() V45() V56() V57() V58() V59() V60() V61() Element of NAT
0 is empty V12() V15() V38() V39() V40() V41() V42() V43() V44() V45() V56() V57() V58() V59() V60() V61() V62() Element of NAT
the empty V12() V15() V56() V57() V58() V59() V60() V61() V62() set is empty V12() V15() V56() V57() V58() V59() V60() V61() V62() set
{} is empty V12() V15() V56() V57() V58() V59() V60() V61() V62() set
2 is non empty V38() V39() V40() V41() V42() V43() V44() V45() V56() V57() V58() V59() V60() V61() Element of NAT
n is V38() V39() V40() V41() V44() V45() V56() V57() V58() V59() V60() V61() Element of NAT
COMPLEX n is non empty V15() V83() M13( COMPLEX )
K343(n,COMPLEX) is non empty V15() V83() M13( COMPLEX )
K342(COMPLEX) is V15() V83() M13( COMPLEX )
{ b1 where b1 is V7() V10( NAT ) V11( COMPLEX ) V12() V81() Element of K342(COMPLEX) : K324(b1) = n } is set
ComplexOpenSets n is Element of K10(K10((COMPLEX n)))
K10((COMPLEX n)) is non empty set
K10(K10((COMPLEX n))) is non empty set
{ b1 where b1 is V15() Element of K10((COMPLEX n)) : b1 is open } is set
TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is non empty strict TopStruct
P is V15() Element of K10((COMPLEX n))
the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is set
the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is Element of K10(K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #)))
K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #)) is non empty set
K10(K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #))) is non empty set
A is Element of K10(K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #)))
union A is Element of K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #))
z1 is V15() Element of K10((COMPLEX n))
z1 is V15() Element of K10((COMPLEX n))
A is Element of K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #))
z1 is Element of K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #))
A /\ z1 is Element of K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #))
d is V15() Element of K10((COMPLEX n))
K1 is V15() Element of K10((COMPLEX n))
K2 is V15() Element of K10((COMPLEX n))
n is V38() V39() V40() V41() V44() V45() V56() V57() V58() V59() V60() V61() Element of NAT
(n) is strict TopSpace-like TopStruct
COMPLEX n is non empty V15() V83() M13( COMPLEX )
K343(n,COMPLEX) is non empty V15() V83() M13( COMPLEX )
{ b1 where b1 is V7() V10( NAT ) V11( COMPLEX ) V12() V81() Element of K342(COMPLEX) : K324(b1) = n } is set
ComplexOpenSets n is Element of K10(K10((COMPLEX n)))
K10((COMPLEX n)) is non empty set
K10(K10((COMPLEX n))) is non empty set
{ b1 where b1 is V15() Element of K10((COMPLEX n)) : b1 is open } is set
TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is non empty strict TopStruct
n is V38() V39() V40() V41() V44() V45() V56() V57() V58() V59() V60() V61() Element of NAT
(n) is non empty strict TopSpace-like TopStruct
COMPLEX n is non empty V15() V83() M13( COMPLEX )
K343(n,COMPLEX) is non empty V15() V83() M13( COMPLEX )
{ b1 where b1 is V7() V10( NAT ) V11( COMPLEX ) V12() V81() Element of K342(COMPLEX) : K324(b1) = n } is set
ComplexOpenSets n is Element of K10(K10((COMPLEX n)))
K10((COMPLEX n)) is non empty set
K10(K10((COMPLEX n))) is non empty set
{ b1 where b1 is V15() Element of K10((COMPLEX n)) : b1 is open } is set
TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is non empty strict TopStruct
the topology of (n) is non empty Element of K10(K10( the carrier of (n)))
the carrier of (n) is set
K10( the carrier of (n)) is non empty set
K10(K10( the carrier of (n))) is non empty set
n is V38() V39() V40() V41() V44() V45() V56() V57() V58() V59() V60() V61() Element of NAT
(n) is non empty strict TopSpace-like TopStruct
COMPLEX n is non empty V15() V83() M13( COMPLEX )
K343(n,COMPLEX) is non empty V15() V83() M13( COMPLEX )
{ b1 where b1 is V7() V10( NAT ) V11( COMPLEX ) V12() V81() Element of K342(COMPLEX) : K324(b1) = n } is set
ComplexOpenSets n is Element of K10(K10((COMPLEX n)))
K10((COMPLEX n)) is non empty set
K10(K10((COMPLEX n))) is non empty set
{ b1 where b1 is V15() Element of K10((COMPLEX n)) : b1 is open } is set
TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is non empty strict TopStruct
the carrier of (n) is set
n is V38() V39() V40() V41() V44() V45() V56() V57() V58() V59() V60() V61() Element of NAT
(n) is non empty strict TopSpace-like TopStruct
COMPLEX n is non empty V15() V83() M13( COMPLEX )
K343(n,COMPLEX) is non empty V15() V83() M13( COMPLEX )
{ b1 where b1 is V7() V10( NAT ) V11( COMPLEX ) V12() V81() Element of K342(COMPLEX) : K324(b1) = n } is set
ComplexOpenSets n is Element of K10(K10((COMPLEX n)))
K10((COMPLEX n)) is non empty set
K10(K10((COMPLEX n))) is non empty set
{ b1 where b1 is V15() Element of K10((COMPLEX n)) : b1 is open } is set
TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is non empty strict TopStruct
the carrier of (n) is set
p is Element of the carrier of (n)
n is V38() V39() V40() V41() V44() V45() V56() V57() V58() V59() V60() V61() Element of NAT
(n) is non empty strict TopSpace-like TopStruct
COMPLEX n is non empty V15() V83() M13( COMPLEX )
K343(n,COMPLEX) is non empty V15() V83() M13( COMPLEX )
{ b1 where b1 is V7() V10( NAT ) V11( COMPLEX ) V12() V81() Element of K342(COMPLEX) : K324(b1) = n } is set
ComplexOpenSets n is Element of K10(K10((COMPLEX n)))
K10((COMPLEX n)) is non empty set
K10(K10((COMPLEX n))) is non empty set
{ b1 where b1 is V15() Element of K10((COMPLEX n)) : b1 is open } is set
TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is non empty strict TopStruct
the carrier of (n) is set
K10( the carrier of (n)) is non empty set
p is Element of K10( the carrier of (n))
P is V15() Element of K10((COMPLEX n))
the topology of (n) is non empty Element of K10(K10( the carrier of (n)))
K10(K10( the carrier of (n))) is non empty set
n is V38() V39() V40() V41() V44() V45() V56() V57() V58() V59() V60() V61() Element of NAT
(n) is non empty strict TopSpace-like TopStruct
COMPLEX n is non empty V15() V83() M13( COMPLEX )
K343(n,COMPLEX) is non empty V15() V83() M13( COMPLEX )
{ b1 where b1 is V7() V10( NAT ) V11( COMPLEX ) V12() V81() Element of K342(COMPLEX) : K324(b1) = n } is set
ComplexOpenSets n is Element of K10(K10((COMPLEX n)))
K10((COMPLEX n)) is non empty set
K10(K10((COMPLEX n))) is non empty set
{ b1 where b1 is V15() Element of K10((COMPLEX n)) : b1 is open } is set
TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is non empty strict TopStruct
the carrier of (n) is set
K10( the carrier of (n)) is non empty set
p is Element of K10( the carrier of (n))
P is V15() Element of K10((COMPLEX n))
[#] (n) is closed Element of K10( the carrier of (n))
([#] (n)) \ p is Element of K10( the carrier of (n))
P ` is V15() Element of K10((COMPLEX n))
(COMPLEX n) \ P is set
n is V38() V39() V40() V41() V44() V45() V56() V57() V58() V59() V60() V61() Element of NAT
(n) is non empty strict TopSpace-like TopStruct
COMPLEX n is non empty V15() V83() M13( COMPLEX )
K343(n,COMPLEX) is non empty V15() V83() M13( COMPLEX )
{ b1 where b1 is V7() V10( NAT ) V11( COMPLEX ) V12() V81() Element of K342(COMPLEX) : K324(b1) = n } is set
ComplexOpenSets n is Element of K10(K10((COMPLEX n)))
K10((COMPLEX n)) is non empty set
K10(K10((COMPLEX n))) is non empty set
{ b1 where b1 is V15() Element of K10((COMPLEX n)) : b1 is open } is set
TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is non empty strict TopStruct
the carrier of (n) is set
p is Element of the carrier of (n)
K10( the carrier of (n)) is non empty set
P is Element of the carrier of (n)
A is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() Element of COMPLEX n
z1 is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() Element of COMPLEX n
A - z1 is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() Element of COMPLEX n
K198() is non empty V7() V10(K11(COMPLEX,COMPLEX)) V11( COMPLEX ) V12() V17(K11(COMPLEX,COMPLEX)) V21(K11(COMPLEX,COMPLEX), COMPLEX ) V46() Element of K10(K11(K11(COMPLEX,COMPLEX),COMPLEX))
K197() is non empty V7() V10(K11(COMPLEX,COMPLEX)) V11( COMPLEX ) V12() V17(K11(COMPLEX,COMPLEX)) V21(K11(COMPLEX,COMPLEX), COMPLEX ) V24( COMPLEX ) V25( COMPLEX ) V31( COMPLEX ) V46() Element of K10(K11(K11(COMPLEX,COMPLEX),COMPLEX))
K51(COMPLEX) is non empty V7() V10( COMPLEX ) V11( COMPLEX ) V12() V13() V17( COMPLEX ) V21( COMPLEX , COMPLEX ) V46() Element of K10(K11(COMPLEX,COMPLEX))
K195() is non empty V7() V10( COMPLEX ) V11( COMPLEX ) V12() V17( COMPLEX ) V21( COMPLEX , COMPLEX ) V46() Element of K10(K11(COMPLEX,COMPLEX))
K399(COMPLEX,K197(),K51(COMPLEX),K195()) is non empty V7() V10(K11(COMPLEX,COMPLEX)) V11( COMPLEX ) V12() V17(K11(COMPLEX,COMPLEX)) V21(K11(COMPLEX,COMPLEX), COMPLEX ) V46() Element of K10(K11(K11(COMPLEX,COMPLEX),COMPLEX))
K393(COMPLEX,COMPLEX,COMPLEX,K198(),A,z1) is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() M12( COMPLEX )
- z1 is V7() V10( NAT ) V12() V46() V81() set
K396(COMPLEX,COMPLEX,z1,K195()) is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() M12( COMPLEX )
- 1 is V39() V40() V41() V42() set
K272(z1,(- 1)) is V7() V10( NAT ) V12() V46() V81() set
K353((- 1)) is non empty V7() V10( COMPLEX ) V11( COMPLEX ) V12() V17( COMPLEX ) V21( COMPLEX , COMPLEX ) V46() Element of K10(K11(COMPLEX,COMPLEX))
K199() is non empty V7() V10(K11(COMPLEX,COMPLEX)) V11( COMPLEX ) V12() V17(K11(COMPLEX,COMPLEX)) V21(K11(COMPLEX,COMPLEX), COMPLEX ) V24( COMPLEX ) V25( COMPLEX ) V31( COMPLEX ) V46() Element of K10(K11(K11(COMPLEX,COMPLEX),COMPLEX))
K379(K199(),(- 1),K51(COMPLEX)) is set
K396(COMPLEX,COMPLEX,z1,K353((- 1))) is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() M12( COMPLEX )
A + (- z1) is V7() V10( NAT ) V12() V46() V81() set
|.(A - z1).| is V39() V40() V41() Element of REAL
abs (A - z1) is V7() V10( NAT ) V11( REAL ) V12() V46() V47() V48() V81() M12( REAL )
abscomplex is non empty V7() V10( COMPLEX ) V11( REAL ) V12() V17( COMPLEX ) V21( COMPLEX , REAL ) V46() V47() V48() Element of K10(K11(COMPLEX,REAL))
K396(COMPLEX,REAL,(A - z1),abscomplex) is V7() V10( NAT ) V11( REAL ) V12() V46() V47() V48() V81() M12( REAL )
K411((abs (A - z1))) is V7() V10( NAT ) V11( REAL ) V12() V46() V47() V48() V81() M12( REAL )
K266((abs (A - z1)),(abs (A - z1))) is V7() V10( NAT ) V12() V46() V47() V48() V81() set
K417(K411((abs (A - z1)))) is V39() V40() V41() Element of REAL
K162(K417(K411((abs (A - z1))))) is V39() V40() V41() Element of REAL
|.(A - z1).| / 2 is V39() V40() V41() Element of REAL
Ball (A,(|.(A - z1).| / 2)) is V15() Element of K10((COMPLEX n))
{ b1 where b1 is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() Element of COMPLEX n : |.(b1 - A).| < |.(A - z1).| / 2 } is set
Ball (z1,(|.(A - z1).| / 2)) is V15() Element of K10((COMPLEX n))
{ b1 where b1 is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() Element of COMPLEX n : |.(b1 - z1).| < |.(A - z1).| / 2 } is set
K1 is Element of K10( the carrier of (n))
K2 is Element of K10( the carrier of (n))
K1 /\ K2 is Element of K10( the carrier of (n))
(Ball (A,(|.(A - z1).| / 2))) /\ (Ball (z1,(|.(A - z1).| / 2))) is V15() Element of K10((COMPLEX n))
x is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() Element of COMPLEX n
z1 - x is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() Element of COMPLEX n
K393(COMPLEX,COMPLEX,COMPLEX,K198(),z1,x) is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() M12( COMPLEX )
- x is V7() V10( NAT ) V12() V46() V81() set
K396(COMPLEX,COMPLEX,x,K195()) is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() M12( COMPLEX )
K272(x,(- 1)) is V7() V10( NAT ) V12() V46() V81() set
K396(COMPLEX,COMPLEX,x,K353((- 1))) is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() M12( COMPLEX )
z1 + (- x) is V7() V10( NAT ) V12() V46() V81() set
|.(z1 - x).| is V39() V40() V41() Element of REAL
abs (z1 - x) is V7() V10( NAT ) V11( REAL ) V12() V46() V47() V48() V81() M12( REAL )
K396(COMPLEX,REAL,(z1 - x),abscomplex) is V7() V10( NAT ) V11( REAL ) V12() V46() V47() V48() V81() M12( REAL )
K411((abs (z1 - x))) is V7() V10( NAT ) V11( REAL ) V12() V46() V47() V48() V81() M12( REAL )
K266((abs (z1 - x)),(abs (z1 - x))) is V7() V10( NAT ) V12() V46() V47() V48() V81() set
K417(K411((abs (z1 - x)))) is V39() V40() V41() Element of REAL
K162(K417(K411((abs (z1 - x))))) is V39() V40() V41() Element of REAL
A - x is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() Element of COMPLEX n
K393(COMPLEX,COMPLEX,COMPLEX,K198(),A,x) is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() M12( COMPLEX )
A + (- x) is V7() V10( NAT ) V12() V46() V81() set
|.(A - x).| is V39() V40() V41() Element of REAL
abs (A - x) is V7() V10( NAT ) V11( REAL ) V12() V46() V47() V48() V81() M12( REAL )
K396(COMPLEX,REAL,(A - x),abscomplex) is V7() V10( NAT ) V11( REAL ) V12() V46() V47() V48() V81() M12( REAL )
K411((abs (A - x))) is V7() V10( NAT ) V11( REAL ) V12() V46() V47() V48() V81() M12( REAL )
K266((abs (A - x)),(abs (A - x))) is V7() V10( NAT ) V12() V46() V47() V48() V81() set
K417(K411((abs (A - x)))) is V39() V40() V41() Element of REAL
K162(K417(K411((abs (A - x))))) is V39() V40() V41() Element of REAL
(|.(A - z1).| / 2) + (|.(A - z1).| / 2) is V39() V40() V41() Element of REAL
|.(A - x).| + |.(z1 - x).| is V39() V40() V41() Element of REAL
x - z1 is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() Element of COMPLEX n
K393(COMPLEX,COMPLEX,COMPLEX,K198(),x,z1) is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() M12( COMPLEX )
x + (- z1) is V7() V10( NAT ) V12() V46() V81() set
|.(x - z1).| is V39() V40() V41() Element of REAL
abs (x - z1) is V7() V10( NAT ) V11( REAL ) V12() V46() V47() V48() V81() M12( REAL )
K396(COMPLEX,REAL,(x - z1),abscomplex) is V7() V10( NAT ) V11( REAL ) V12() V46() V47() V48() V81() M12( REAL )
K411((abs (x - z1))) is V7() V10( NAT ) V11( REAL ) V12() V46() V47() V48() V81() M12( REAL )
K266((abs (x - z1)),(abs (x - z1))) is V7() V10( NAT ) V12() V46() V47() V48() V81() set
K417(K411((abs (x - z1)))) is V39() V40() V41() Element of REAL
K162(K417(K411((abs (x - z1))))) is V39() V40() V41() Element of REAL
|.(A - x).| + |.(x - z1).| is V39() V40() V41() Element of REAL
n is V38() V39() V40() V41() V44() V45() V56() V57() V58() V59() V60() V61() Element of NAT
(n) is non empty strict TopSpace-like TopStruct
COMPLEX n is non empty V15() V83() M13( COMPLEX )
K343(n,COMPLEX) is non empty V15() V83() M13( COMPLEX )
{ b1 where b1 is V7() V10( NAT ) V11( COMPLEX ) V12() V81() Element of K342(COMPLEX) : K324(b1) = n } is set
ComplexOpenSets n is Element of K10(K10((COMPLEX n)))
K10((COMPLEX n)) is non empty set
K10(K10((COMPLEX n))) is non empty set
{ b1 where b1 is V15() Element of K10((COMPLEX n)) : b1 is open } is set
TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is non empty strict TopStruct
the carrier of (n) is set
K10( the carrier of (n)) is non empty set
p is Element of the carrier of (n)
P is Element of K10( the carrier of (n))
P ` is Element of K10( the carrier of (n))
the carrier of (n) \ P is set
z1 is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() Element of COMPLEX n
A is V15() Element of K10((COMPLEX n))
dist (z1,A) is V39() V40() V41() Element of REAL
(dist (z1,A)) / 2 is V39() V40() V41() Element of REAL
Ball (z1,((dist (z1,A)) / 2)) is V15() Element of K10((COMPLEX n))
{ b1 where b1 is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() Element of COMPLEX n : |.(b1 - z1).| < (dist (z1,A)) / 2 } is set
Ball (A,((dist (z1,A)) / 2)) is V15() Element of K10((COMPLEX n))
{ b1 where b1 is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() Element of COMPLEX n : dist (b1,A) < (dist (z1,A)) / 2 } is set
K1 is Element of K10( the carrier of (n))
K2 is Element of K10( the carrier of (n))
K1 /\ K2 is Element of K10( the carrier of (n))
(Ball (z1,((dist (z1,A)) / 2))) /\ (Ball (A,((dist (z1,A)) / 2))) is V15() Element of K10((COMPLEX n))
x is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() Element of COMPLEX n
dist (x,A) is V39() V40() V41() Element of REAL
z1 - x is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() Element of COMPLEX n
K198() is non empty V7() V10(K11(COMPLEX,COMPLEX)) V11( COMPLEX ) V12() V17(K11(COMPLEX,COMPLEX)) V21(K11(COMPLEX,COMPLEX), COMPLEX ) V46() Element of K10(K11(K11(COMPLEX,COMPLEX),COMPLEX))
K197() is non empty V7() V10(K11(COMPLEX,COMPLEX)) V11( COMPLEX ) V12() V17(K11(COMPLEX,COMPLEX)) V21(K11(COMPLEX,COMPLEX), COMPLEX ) V24( COMPLEX ) V25( COMPLEX ) V31( COMPLEX ) V46() Element of K10(K11(K11(COMPLEX,COMPLEX),COMPLEX))
K51(COMPLEX) is non empty V7() V10( COMPLEX ) V11( COMPLEX ) V12() V13() V17( COMPLEX ) V21( COMPLEX , COMPLEX ) V46() Element of K10(K11(COMPLEX,COMPLEX))
K195() is non empty V7() V10( COMPLEX ) V11( COMPLEX ) V12() V17( COMPLEX ) V21( COMPLEX , COMPLEX ) V46() Element of K10(K11(COMPLEX,COMPLEX))
K399(COMPLEX,K197(),K51(COMPLEX),K195()) is non empty V7() V10(K11(COMPLEX,COMPLEX)) V11( COMPLEX ) V12() V17(K11(COMPLEX,COMPLEX)) V21(K11(COMPLEX,COMPLEX), COMPLEX ) V46() Element of K10(K11(K11(COMPLEX,COMPLEX),COMPLEX))
K393(COMPLEX,COMPLEX,COMPLEX,K198(),z1,x) is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() M12( COMPLEX )
- x is V7() V10( NAT ) V12() V46() V81() set
K396(COMPLEX,COMPLEX,x,K195()) is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() M12( COMPLEX )
- 1 is V39() V40() V41() V42() set
K272(x,(- 1)) is V7() V10( NAT ) V12() V46() V81() set
K353((- 1)) is non empty V7() V10( COMPLEX ) V11( COMPLEX ) V12() V17( COMPLEX ) V21( COMPLEX , COMPLEX ) V46() Element of K10(K11(COMPLEX,COMPLEX))
K199() is non empty V7() V10(K11(COMPLEX,COMPLEX)) V11( COMPLEX ) V12() V17(K11(COMPLEX,COMPLEX)) V21(K11(COMPLEX,COMPLEX), COMPLEX ) V24( COMPLEX ) V25( COMPLEX ) V31( COMPLEX ) V46() Element of K10(K11(K11(COMPLEX,COMPLEX),COMPLEX))
K379(K199(),(- 1),K51(COMPLEX)) is set
K396(COMPLEX,COMPLEX,x,K353((- 1))) is V7() V10( NAT ) V11( COMPLEX ) V12() V46() V81() M12( COMPLEX )
z1 + (- x) is V7() V10( NAT ) V12() V46() V81() set
|.(z1 - x).| is V39() V40() V41() Element of REAL
abs (z1 - x) is V7() V10( NAT ) V11( REAL ) V12() V46() V47() V48() V81() M12( REAL )
abscomplex is non empty V7() V10( COMPLEX ) V11( REAL ) V12() V17( COMPLEX ) V21( COMPLEX , REAL ) V46() V47() V48() Element of K10(K11(COMPLEX,REAL))
K396(COMPLEX,REAL,(z1 - x),abscomplex) is V7() V10( NAT ) V11( REAL ) V12() V46() V47() V48() V81() M12( REAL )
K411((abs (z1 - x))) is V7() V10( NAT ) V11( REAL ) V12() V46() V47() V48() V81() M12( REAL )
K266((abs (z1 - x)),(abs (z1 - x))) is V7() V10( NAT ) V12() V46() V47() V48() V81() set
K417(K411((abs (z1 - x)))) is V39() V40() V41() Element of REAL
K162(K417(K411((abs (z1 - x))))) is V39() V40() V41() Element of REAL
((dist (z1,A)) / 2) + ((dist (z1,A)) / 2) is V39() V40() V41() Element of REAL
|.(z1 - x).| + (dist (x,A)) is V39() V40() V41() Element of REAL