thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
contradiction ;
contradiction ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
contradiction ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
assume not thesis ;
assume not thesis ;
B ;
a <> c
T c= S
D c= B
c in X ;
b in X ;
X ;
b in D ;
x = e ;
let m ;
h is onto ;
N in K ;
let i ;
j = 1 ;
x = u ;
let n ;
let k ;
y in A ;
let x ;
let x ;
m c= y ;
F is one-to-one ;
let q ;
m = 1 ;
1 < k ;
G is rng ;
b in A ;
d divides a ;
i < n ;
s <= b ;
b in B ;
let r ;
B is one-to-one ;
R is total ;
x = 2 ;
d in D ;
let c ;
let c ;
b = Y ;
0 < k ;
let b ;
let n ;
r <= b ;
x in X ;
i >= 8 ;
let n ;
let n ;
y in f ;
let n ;
1 < j ;
a in L ;
C is boundary ;
a in A ;
1 < x ;
S is finite ;
u in I ;
z << z ;
x in V ;
r < t ;
let t ;
x c= y ;
a <= b ;
m in NAT ;
assume f is prime ;
not x in Y ;
z = +infty ;
let k be Nat ;
K is being_line ;
assume n >= N ;
assume n >= N ;
assume X is ) ;
assume x in I ;
q is as Nat ;
assume c in x ;
1-p > 0 ;
assume x in Z ;
assume x in Z ;
1 <= k} ;
assume m <= i ;
assume G is rng ;
assume a divides b ;
assume P is closed ;
b-a > 0 ;
assume q in A ;
W is non bounded ;
f is Assume f is one-to-one ;
assume A is boundary ;
g is special ;
assume i > j ;
assume t in X ;
assume n <= m ;
assume x in W ;
assume r in X ;
assume x in A ;
assume b is even ;
assume i in I ;
assume 1 <= k ;
X is non empty ;
assume x in X ;
assume n in M ;
assume b in X ;
assume x in A ;
assume T c= W ;
assume s is atomic ;
b `2 <= c `2 ;
A meets W ;
i `2 <= j `2 ;
assume H is universal ;
assume x in X ;
let X be set ;
let T be Tree ;
let d be element ;
let t be element ;
let x be element ;
let x be element ;
let s be element ;
k <= 5 - 5 ;
let X be set ;
let X be set ;
let y be element ;
let x be element ;
P [ 0 ]
let E be set , A be Element of E ;
let C be category ;
let x be element ;
let k be Nat ;
let x be element ;
let x be element ;
let e be element ;
let x be element ;
P [ 0 ]
let c be element ;
let y be element ;
let x be element ;
let a be Real ;
let x be element ;
let X be element ;
P [ 0 ]
let x be element ;
let x be element ;
let y be element ;
r in REAL ;
let e be element ;
n1 is , and n2 is , ;
Q halts_on s ;
x in for of -1 ;
M < m + 1 ;
T2 is open ;
z in b id a ;
R2 is well-ordering ;
1 <= k + 1 ;
i > n + 1 ;
q1 is one-to-one ;
let x be trivial set ;
PM is one-to-one ;
n <= n + 2 ;
1 <= k + 1 ;
1 <= k + 1 ;
let e be Real ;
i < i + 1 ;
p3 in P ;
p1 in K ;
y in C1 ;
k + 1 <= n ;
let a be Real , x be Point of TOP-REAL 2 ;
X |- r => p ;
x in { A } ;
let n be Nat ;
let k be Nat ;
let k be Nat ;
let m be Nat ;
0 < 0 + k ;
f is_differentiable_in x ;
let x0 , r ;
let E be Ordinal ;
o >= o1 ;
O <> O2 ;
let r be Real ;
let f be FinSeq-Location ;
let i be Nat ;
let n be Nat ;
Cl A = A ;
L c= Cl L ;
A /\ M = B ;
let V be : 1 <= r ;
not s in Y |^ 0 ;
rng f <= w
b "/\" e = b ;
m = m3 ;
t in h . D ;
P [ 0 ] ;
assume z = x * y ;
S . n is bounded ;
let V be RealLinearSpace , M be Subset of V ;
P [ 1 ] ;
P [ {} ] ;
C1 meets C ;
H = G . i ;
1 <= i `2 + 1 ;
F . m in A ;
f . o = o ;
P [ 0 ] ;
aor <= being Real ;
R [ 0 ] ;
b in f .: X ;
assume q = q2 ;
x in [#] V ;
f . u = 0 ;
assume e1 > 0 ;
let V be RealUnitarySpace , M be Subset of V ;
s is trivial & s is non empty ;
dom c = Q
P [ 0 ] ;
f . n in T ;
N . j in S ;
let T be complete LATTICE , S be Subset of T ;
the ObjectMap of F is one-to-one
sgn x = 1 ;
k in support a ;
1 in Seg 1 ;
rng f = X ;
len T in X ;
vbeing < n ;
St is bounded ;
assume p = p2 ;
len f = n ;
assume x in P1 ;
i in dom q ;
let UA , x , y ;
pp = c ;
j in dom h ;
let k ;
f | Z is continuous ;
k in dom G ;
UBD C = B ;
1 <= len M ;
p in `2 ;
1 <= jj & 1 <= jj ;
set A = there k1 , B = there exists $ n st A = k1 ;
card a [= c ;
e in rng f ;
cluster B \oplus A -> empty ;
H is with_no or H is non empty ;
assume n0 <= m ;
T is increasing ;
e2 <> e2 & e2 <> e1 ;
Z c= dom g ;
dom p = X ;
H is proper ;
i + 1 <= n ;
v <> 0. V ;
A c= Affin A ;
S c= dom F ;
m in dom f ;
let X0 be set ;
c = sup N ;
R is_connected in union M ;
assume not x in REAL ;
Im f is complete ;
x in Int y ;
dom F = M ;
a in On W ;
assume e in A ( ) ;
C c= C-26 ;
mm <> {} ;
let x be Element of Y ;
let f be ) ;
not n in Seg 3 ;
assume X in f .: A ;
assume that p <= n and p <= m ;
assume not u in { v } ;
d is Element of A ;
A |^ b misses B ;
e in v + dom \vert v .| ;
- y in I ;
let A be non empty set , B be set ;
P0 = 1 ;
assume r in F . k ;
assume f is simple ;
let A be l countable set ;
rng f c= NAT ;
assume P [ k ] ;
ff <> {} ;
let o be Ordinal ;
assume x is sum of squares ;
assume not v in { 1 } ;
let IH , I ;
assume that 1 <= j and j < l ;
v = - u ;
assume s . b > 0 ;
\bf \bf d in dom f ;
assume t . 1 in A ;
let Y be non empty TopSpace , A be Subset of Y ;
assume a in uparrow s ;
let S be non empty Poset ;
a , b // b , a ;
a * b = p * q ;
assume x , y are_the space ;
assume x in Omega ( f ) ;
[ a , c ] in X ;
mm <> {} ;
M + N c= M + M ;
assume M is connected hh\overline ;
assume f is additive bbr-rst ;
let x , y be element ;
let T be non empty TopSpace ;
b , a // b , c ;
k in dom Sum p ;
let v be Element of V ;
[ x , y ] in T ;
assume len p = 0 ;
assume C in rng f ;
k1 = k2 & k2 = k2 ;
m + 1 < n + 1 ;
s in S \/ { s } ;
n + i >= n + 1 ;
assume Re y = 0 ;
k1 <= j1 & k1 <= k2 ;
f | A is compact ;
f . x be element ;
assume y in dom h ;
x * y in B1 ;
set X = Seg n ;
1 <= i2 + 1 ;
k + 0 <= k + 1 ;
p ^ q = p ;
j |^ y divides m ;
set m = max A ;
[ x , x ] in R ;
assume x in succ 0 ;
a in sup phi ;
CH ;
q2 c= C1 & q1 c= C2 ;
a2 < c2 & a3 < a4 ;
s2 is 0 -started ;
IC s = 0 ;
s4 = s4 , s4 = s4 ;
let V ;
let x , y be element ;
let x be Element of T ;
assume a in rng F ;
x in dom T `2 ;
let S be MSAlgebra over L ;
y " <> 0 ;
y " <> 0 ;
0. V = u-w ;
y2 , y , w be Element of V ;
R8 ;
let a , b be Real , x be Element of REAL ;
let a be Object of C ;
let x be Vertex of G ;
let o be Object of C , a be Object of C ;
r '&' q = P \lbrack l \rbrack ;
let i , j be Nat ;
let s be State of A , v be Element of S ;
s4 . n = N ;
set y = x `1 , z = y `2 ;
mi in dom g ;
l . 2 = y1 ;
|. g . y .| <= r ;
f . x in CX0 ;
V1 is non empty ;
let x be Element of X ;
0 <> f . g2 ;
f2 /* q is convergent ;
f . i is_measurable_on E ;
assume \xi in N-22 ;
reconsider i = i as Ordinal ;
r * v = 0. X ;
rng f c= INT & rng g c= INT ;
G = 0 .--> goto 0 ;
let A be Subset of X ;
assume that A0 is dense and A is dense ;
|. f . x .| <= r ;
let x be Element of R ;
let b be Element of L ;
assume x in W-19 ;
P [ k , a ] ;
let X be Subset of L ;
let b be Object of B ;
let A , B be category ;
set X = Vars , C = the carrier of C ;
let o be OperSymbol of S ;
let R be connected non empty Poset ;
n + 1 = succ n ;
xx c= Z1 & xx c= Z1 ;
dom f = C1 & rng f c= C2 ;
assume [ a , y ] in X ;
Re ( seq ) is convergent & lim ( Im seq ) = 0 ;
assume that a1 = b1 and b1 = c1 ;
A = sInt A ;
a <= b or b <= a ;
n + 1 in dom f ;
let F be Instruction of S , I be Program of S ;
assume that r2 > x0 and x0 < r2 ;
let Y be non empty set , f be PartFunc of Y , BOOLEAN ;
2 * x in dom W ;
m in dom g2 & m in dom g2 ;
n in dom g1 /\ dom g2 ;
k + 1 in dom f ;
the still of not s is finite ;
assume x1 <> x2 & x1 <> x3 ;
v3 in V1 & v3 in V1 ;
not [ b `1 , b `2 ] in T ;
i-35 + 1 = i ;
T c= `2 & T c= G ;
l `1 = 0 & l `2 = 1 ;
let n be Nat ;
t `2 = r `2 & t `2 = s ;
A-31 : f is_integrable_on M & f is_integrable_on M ;
set t = Top t ;
let A , B be real-membered set ;
k <= len G + 1 ;
cC misses cC ;
Product ( seq ) is non empty ;
e <= f or f <= e ;
cluster non empty normal for sequence ;
assume c2 = b2 & c2 = b1 ;
assume h in [. q , p .] ;
1 + 1 <= len C ;
not c in B . m1 ;
cluster R .: X -> empty ;
p . n = H . n ;
assume ( vseq is convergent & lim vseq = lim vseq ) ;
IC s3 = 0 & IC s3 = 0 ;
k in N or k in K ;
F1 \/ F2 c= F \/ G ;
Int G1 <> {} & Int G2 <> {} ;
z `2 = 0 & z `2 = 0 ;
p11 <> p1 & p11 <> p2 ;
assume z in { y , w } ;
MaxADSet ( a ) c= F ;
ex_sup_of downarrow s , S ;
f . x <= f . y ;
let T be up-complete non empty reflexive transitive RelStr ;
q |^ m >= 1 ;
a is_>=_than X & b is_>=_than Y ;
assume <* a , c *> <> {} ;
F . c = g . c ;
G is one-to-one one-to-one ;
A \/ { a } \not c= B ;
0. V = 0. Y ;
let I be be be be be be halting Instruction of S , S be non empty set ;
f-24 . x = 1 ;
assume z \ x = 0. X ;
C2 = 2 to_power n ;
let B be sequence of Sigma ;
assume X1 = p .: D ;
n + l2 in NAT ;
f " P is compact ;
assume x1 in REAL & x2 in REAL ;
p1 = ( K + 1 ) * ( K + 1 ) ;
M . k = <*> REAL ;
phi . 0 in rng phi ;
OSM, A is closed ;
assume z0 <> 0. L & z0 <> 0. L ;
n < ( N . k ) ;
0 <= ( seq . 0 ) ;
- q + p = v ;
{ v } is Subset of B ;
set g = f /. 1 ;
cR is stable Subset of R ;
set cR = Vertices R , cR = Vertices R ;
pp c= P3 & L~ ( k + 1 ) c= P3 ;
x in [. 0 , 1 .[ ;
f . y in dom F ;
let T be Scott Scott Scott Scott Scott Scott of S ;
ex_inf_of the carrier of S , S ;
downarrow a = downarrow b ;
P , C , K is_collinear ;
assume x in F ( s , r , t ) ;
2 to_power i < 2 to_power m ;
x + z = x + z + q ;
x \ ( a \ x ) = x ;
||. x-y - x .|| <= r ;
assume that Y c= field Q and Y <> {} ;
a ~ , b ~ are_equipotent ;
assume a in A ( i ) ;
k in dom ( q | k ) ;
p is -> -> \HM of S ;
i -' 1 = i-1 ;
f | A is one-to-one ;
assume x in f .: X ( ) ;
i2 - i1 = 0 & i2 = 0 ;
j2 + 1 <= i2 & j2 + 1 <= j2 ;
g " * a in N ;
K <> { [ {} , {} ] } ;
cluster strict for } ;
|. q .| ^2 > 0 ;
|. p4 .| = |. p .| ;
s2 - s1 > 0 ;
assume x in { Gij } ;
W-min C in C & W-min C in C ;
assume x in { Gij } ;
assume i + 1 = len G ;
assume i + 1 = len G ;
dom I = Seg n & rng I c= Seg n ;
assume that k in dom C and k <> i ;
1 + 1-1 <= i + j ;
dom S = dom F & rng F c= dom G ;
let s be Element of NAT ;
let R be ManySortedSet of A ;
let n be Element of NAT ;
let S be non empty non void non void non void holds S is holds S is holds S is non void ;
let f be ManySortedSet of I ;
let z be Element of F_Complex , v be Element of F_Complex ;
u in { ag } ;
2 * n < ( 2 * n ) ;
let x , y be set ;
B-11 c= [: V1 , V1 :] ;
assume I is_closed_on s , P ;
UA = [: U , U :] ;
M /. 1 = z /. 1 ;
x9 = x9 & y9 = y9 & x9 = z9 ;
i + 1 < n + 1 + 1 ;
x in { {} , <* 0 *> } ;
ff <= ff & ff <= ff & ff <= ff ;
let l be Element of L ;
x in dom ( F . n ) ;
let i be Element of NAT ;
seq1 is COMPLEX -valued & seq2 is COMPLEX -valued ;
assume <* o2 , o *> <> {} ;
s . x |^ 0 = 1 ;
card ( K1 ) in M & card ( K1 ) = M ;
assume that X in U and Y in U ;
let D be Subset-Family of Omega ;
set r = Seg ( k + 1 ) ;
y = W . ( 2 * x ) ;
assume dom g = cod f & cod g = cod f ;
let X , Y be non empty TopSpace , f be Function of X , Y ;
x \oplus A is interval ;
|. <*> A .| . a = 0 ;
cluster strict for Sublattice of L ;
a1 in B . s1 & a2 in B . s2 ;
let V be finite finite linearly-independent VectSp of F , v be Vector of V ;
A * B on B , A ;
f-3 = NAT --> 0 ;
let A , B be Subset of V ;
z1 = P1 . j & z2 = P2 . j ;
assume f " P is closed ;
reconsider j = i as Element of M ;
let a , b be Element of L ;
assume q in A \/ ( B "\/" C ) ;
dom ( F * C ) = o ;
set S = INT |^ X ;
z in dom ( A --> y ) ;
P [ y , h . y ] ;
{ x0 } c= dom f & { x0 } c= dom f ;
let B be non-empty ManySortedSet of I , A be ManySortedSet of I ;
PI / 2 < Arg z ;
reconsider z9 = 0 , z9 = 1 as Nat ;
LIN a , d , c & LIN a , d , c ;
[ y , x ] in Iy ;
Q * ( 1 , 3 ) `1 = 0 ;
set j = x0 gcd m , i = x0 gcd m ;
assume a in { x , y , c } ;
j2 - jj > 0 & j2 - jj > 0 ;
I the Element of 1 -tuples_on phi = 1 ;
[ y , d ] in F-8 ;
let f be Function of X , Y ;
set A2 = ( B - C ) / ( B - C ) ;
s1 , s2 be ` & s1 , s2 be of R ;
j1 -' 1 = 0 & j1 -' 1 = 1 ;
set m2 = 2 * n + j ;
reconsider t = t as bag of n ;
I2 . j = m . j ;
i |^ s , n are_relative_prime & i |^ s = 1 ;
set g = f | D-21 ;
assume that X is lower bounded and 0 <= r ;
p1 `1 = 1 & p1 `2 = - 1 ;
a < p3 `1 & p3 `2 < p4 `2 ;
L \ { m } c= UBD C ;
x in Ball ( x , 10 ) ;
not a in LSeg ( c , m ) ;
1 <= i1 -' 1 & i1 + 1 <= len f ;
1 <= i1 -' 1 & i1 + 1 <= len f ;
i + i2 <= len h & 1 <= i2 ;
x = W-min ( P ) & y = E-max ( P ) ;
[ x , z ] in [: X , Z :] ;
assume y in [. x0 , x .] ;
assume p = <* 1 , 2 , 3 *> ;
len <* A1 , A2 *> = 1 ;
set H = h . gg , I = h . gg ;
card b * a = |. a .| ;
Shift ( w , 0 ) |= v ;
set h = h2 (*) h1 , h1 = h2 (*) h2 ;
assume x in X3 /\ X4 ;
||. h .|| < d1 & ||. h .|| < d ;
not x in the carrier of f ;
f . y = F ( y ) ;
for n holds X [ n ] ;
k - l = k\leq ;
<* p , q *> /. 2 = q ;
let S be Subset of the carrier of Y ;
let P , Q be \langle s , t *> ;
Q /\ M c= union ( F | M )
f = b * ( canFS S ) ;
let a , b be Element of G ;
f .: X is_<=_than f . sup X
let L be non empty transitive RelStr , x be Element of L ;
S-20 is x -\leq x -[ i , n ]
let r be non positive Real ;
M , v |= x \hbox { y } ;
v + w = 0. ( Z , p ) ;
P [ len F ( ) ] ;
assume InsCode i = 8 & InsCode i = 8 ;
the zero of M = 0 & the zero of M = 0 ;
cluster z * seq -> summable for Real_Sequence ;
let O be Subset of the carrier of C ;
||. f .|| | X is continuous ;
x2 = g . ( j + 1 ) ;
cluster -> [#] for Element of S ;
reconsider l1 = l-1 as Nat ;
v4 is Vertex of r2 & v4 is Vertex of G ;
T2 is SubSpace of T2 & T1 is SubSpace of T2 ;
Q1 /\ Q19 <> {} & Q1 /\ Q19 <> {} ;
let k be Nat ;
q " is Element of X & q " is Element of X ;
F . t is set of \leq & F . t is set ;
assume that n <> 0 and n <> 1 ;
set en = EmptyBag n , en = EmptyBag n ;
let b be Element of Bags n ;
assume for i holds b . i is commutative ;
x is root & p `2 = ( p `2 ) ;
not r in ]. p , q .[ ;
let R be FinSequence of REAL , x be Element of REAL ;
SS does not destroy b1 & I does not destroy b2 ;
IC SCM R <> a & IC SCM R = a ;
|. - |[ x , y ]| .| >= r ;
1 * seq = seq & seq is convergent & lim seq = 0 ;
let x be FinSequence of NAT , n be Nat ;
let f be Function of C , D , g be Function of C , D ;
for a holds 0. L + a = a
IC s = s . NAT .= IC s ;
H + G = F- ( G-G ) ;
Cm1 . x = x2 & Cm2 . x = y2 ;
f1 = f .= f2 .= f2 ;
Sum <* p . 0 *> = p . 0 ;
assume v + W = v + u + W ;
{ a1 } = { a2 } & { a2 } = { a2 } ;
a1 , b1 _|_ b , a ;
d3 , o _|_ o , a3 ;
Iy is reflexive & Iy is reflexive implies Iy is reflexive
Iy is antisymmetric & Iy is antisymmetric implies Iy is antisymmetric
upper_bound rng H1 = e & upper_bound rng H1 = e ;
x = ( a * a9 ) * ( a * b9 ) ;
|. p1 .| ^2 >= 1 ^2 ;
assume j2 -' 1 < 1 & j2 + 1 < len G ;
rng s c= dom f1 /\ dom f2 ;
assume support a misses support b & support b misses support b ;
let L be associative non empty doubleLoopStr , I be non empty Subset of L ;
s " + 0 < n + 1 ;
p . c = ( f " ) . 1 ;
R . n <= R . ( n + 1 ) ;
Directed ( I1 , I2 ) = I1 " ;
set f = + ( x , y , r ) ;
cluster Ball ( x , r ) -> bounded ;
consider r being Real such that r in A ;
cluster non empty NAT -defined NAT -defined for NAT -defined Function ;
let X be non empty directed Subset of S ;
let S be non empty full SubRelStr of L ;
cluster <* [ ] *> , <* 1 *> *> -> complete non trivial ;
( 1 - a ) " = a ;
( q . {} ) `1 = o ;
- ( i - 1 ) > 0 ;
assume ( 1 - 2 ) * t `1 <= t `1 ;
card B = k + 1-1 ;
x in union rng ( f | n ) ;
assume x in the carrier of R & y in the carrier of R ;
d in X ;
f . 1 = L . ( F . 1 ) ;
the vertices of G = { v } & { v } c= the vertices of G ;
let G be let G be : wwgraph ;
e , v6 be set ;
c . ( i " ) in rng c & c . ( i " ) in rng c ;
f2 /* q is divergent_to-infty & lim ( f2 /* q ) = x0 ;
set z1 = - z2 , z2 = - z1 , z1 = - z2 , z2 = - z1 ;
assume w is_ll\cdot S , G ;
set f = p |-count t , g = p |-count t , h = p |-count t ;
let c be Object of C ;
assume ex a st P [ a ] ;
let x be Element of REAL m , y be Element of REAL m ;
let IX be Subset-Family of X , I be Subset-Family of X ;
reconsider p = p as Element of NAT ;
let v , w be Point of X ;
let s be State of SCM+FSA , I be Program of SCM+FSA ;
p is FinSequence of ( the InstructionsF of SCM+FSA ) * ;
stop I ( ) c= P-12 ( a , I ( ) ) ;
set ci = fbeing /. i , fi = fi /. i ;
w ^ t for w ^ s ;
W1 /\ W = W1 /\ W ` .= W ;
f . j is Element of J . j ;
let x , y be Subset of T2 , a be Element of T1 ;
ex d st a , b // b , d ;
a <> 0 & b <> 0 & c <> 0 ;
ord x = 1 & x is positive ;
set g2 = lim ( seq ^\ k ) , g1 = lim ( seq ^\ k ) ;
2 * x >= 2 * ( 1 / 2 ) ;
assume ( a 'or' c ) . z <> TRUE ;
f (*) g in Hom ( c , c ) ;
Hom ( c , c + d ) <> {} ;
assume 2 * Sum ( q | m ) > m ;
L1 . F-21 = 0 & L1 . F-21 = 1 ;
thesis ;
( sin . x ) ^2 <> 0 ;
( ( #Z n ) * ( exp_R + f ) ) . x > 0 ;
o1 in X-5 /\ O2 & o2 in XO2 /\ O2 ;
e , v6 be set ;
r3 > ( 1 - 2 ) * 0 ;
x in P .: ( F -ideal ) ;
let J be closed Subset of R , left I be non empty Subset of R ;
h . p1 = f2 . O & h . O = g2 . I ;
Index ( p , f ) + 1 <= j ;
len ( q - p ) = width M & width ( q - p ) = width M ;
the carrier of LK c= A & Carrier L c= A ;
dom f c= union rng ( F | ( n + 1 ) ) ;
k + 1 in support ( support ( n ) ) ;
let X be ManySortedSet of the carrier of S ;
[ x `1 , y `2 ] in InnerVertices ( R ~ ) ;
i = D1 or i = D2 or i = D1 ;
assume a mod n = b mod n ;
h . x2 = g . x1 & h . x2 = f . x2 ;
F c= 2 -tuples_on the carrier of X ;
reconsider w = |. s1 .| as Real_Sequence of X , Y ;
( 1 / m * m + r ) < p ;
dom f = dom ( I --> ( i + 1 ) ) ;
[#] PPPPPP = [#] ( ( TOP-REAL 2 ) | K1 ) ;
cluster - x -> ExtReal for ExtReal ;
then { db } c= A & A is closed ;
cluster ( TOP-REAL n ) | ( A , B ) -> finite-ind ;
let w1 be Element of M , w2 be Element of M ;
let x be Element of dyadic ( n ) ;
u in W1 & v in W3 implies u in W2 + W3
reconsider y = y as Element of L2 ;
N is full SubRelStr of T |^ the carrier of S ;
sup { x , y } = c "\/" c ;
g . n = n to_power 1 .= n ;
h . J = EqClass ( u , J ) ;
let seq be summable sequence of X , n be Nat ;
dist ( x `2 , y ) < ( r / 2 ) ;
reconsider mm = m , mn = n as Element of NAT ;
x- x0 < r1 - x0 & x0 < x0 + r2 ;
reconsider P ` = P ` as strict Subgroup of N ;
set g1 = p * ( idseq q `2 ) , g2 = idseq q `2 ;
let n , m , k be non zero Nat ;
assume that 0 < e and f | A is lower ;
D2 . ( I8 + 1 ) in { x } ;
cluster subcondensed for Subset of T ;
let P be compact non empty Subset of TOP-REAL 2 , p1 , p2 , q1 , q2 be Point of TOP-REAL 2 ;
Gik in LSeg ( PI , 1 ) /\ LSeg ( Gik , Gij ) ;
let n be Element of NAT , x be Element of NAT ;
reconsider SS = S , SS = T as Subset of T ;
dom ( i .--> X ` ) = { i } ;
let X be non-empty ManySortedSet of S ;
let X be non-empty ManySortedSet of S ;
op ( 1 ) c= { [ {} , {} ] } ;
reconsider m = mm as Element of NAT ;
reconsider d = x as Element of C ( ) ;
let s be 0 -started State of SCMPDS , P be s of P ;
let t be 0 -started State of SCMPDS , Q ;
b , b , x , y , x , y is_collinear ;
assume that i = n \/ { n } and j = k \/ { k } ;
let f be PartFunc of X , Y ;
x0 >= ( sqrt c ) / sqrt 2 & x0 >= ( sqrt c ) / sqrt 2 ;
reconsider t7 = T" as TopSpace of ( TOP-REAL 2 ) | P ;
set q = h * p ^ <* d *> ;
z2 in U . ( y2 ) /\ Q2 . ( y1 + 1 ) ;
A |^ 0 = { <%> E } & A |^ 0 = { <%> E } ;
len W2 = len W + 2 .= len W + 2 ;
len h2 in dom h2 & len h2 in dom h2 ;
i + 1 in Seg ( len s2 ) & i + 1 in dom s2 ;
z in dom g1 /\ dom f & z in dom f1 ;
assume that p2 = E-max ( K ) and p1 `2 = E-max ( K ) ;
len G + 1 <= i1 + 1 ;
f1 (#) f2 is convergent & lim ( f1 (#) f2 ) = x0 ;
cluster ( seq + sX ) - seq is summable ;
assume that j in dom ( M1 * M2 ) and i in dom M1 ;
let A , B , C be Subset of X ;
let x , y , z be Point of X , p be Point of X ;
b ^2 - ( 4 * a * c ) >= 0 ;
<* x/y *> ^ <* y *> << x ;
a , b in { a , b } ;
len p2 is Element of NAT & len p2 = len p1 + 1 ;
ex x being element st x in dom R & y = R . x ;
len q = len ( K (#) G ) .= len G ;
s1 = Initialize Initialized s , P1 = P +* I , P2 = P +* I ;
consider w being Nat such that q = z + w ;
x ` is and y ` is and x ` is Element of X ;
k = 0 & n <> k or k > n ;
then X is discrete for A is closed Subset of X ;
for x st x in L holds x is FinSequence ;
||. f /. c .|| <= r1 & ||. f /. c .|| <= r ;
c in uparrow p & not c in { p } ;
reconsider V = V as Subset of the topology of Y ;
let N , M be being being being being being being being being being being being being being being being being being being being being being being being being being being being being being being being being being Subset of L ;
then z is_>=_than waybelow x & z is_>=_than compactbelow y ;
M \lbrack f , g .] = f & M \lbrack g , f .] = g ;
( ( ( ( L ) to_power 1 ) ) to_power 1 ) = TRUE ;
dom g = dom f |^ X & rng g c= dom f ;
mode \cal il of G is ^ of G ;
[ i , j ] in Indices ( M @ ) ;
reconsider s = x " as Element of H ;
let f be Element of dom ( Subformulae p ) , F be Element of dom ( Subformulae p ) ;
F1 . ( a1 , - a1 ) = G1 * ( a1 , - a1 ) ;
redefine func Sphere ( a , b , r ) -> compact Subset of TOP-REAL 2 ;
let a , b , c , d be Real ;
rng s c= dom ( 1 / ( f ^ ) ) ;
curry ( F-19 , k ) is additive & curry ( F-19 , k ) is additive ;
set k2 = card dom B , k1 = card dom B , k2 = card dom C ;
set G = ( the Sorts of A ) . v ;
reconsider a = [ x , s ] as 0. of G ;
let a , b be Element of [: M , M :] , f be Element of M ;
reconsider s1 = s , s2 = t as Element of ( the carrier of S1 ) ;
rng p c= the carrier of L & p . n in rng p ;
let d be Subset of the bound \hbox { - } ;
( x .|. x ) = 0 iff x = 0. W ;
I-21 in dom stop I & Ik in dom stop I ;
let g be continuous Function of X | B , Y ;
reconsider D = Y as Subset of ( TOP-REAL n ) | P ;
reconsider i0 = len p1 , i0 = len p2 as Integer ;
dom f = the carrier of S & rng f = the carrier of S ;
rng h c= union ( ( Carrier J ) * ( Carrier J ) ) ;
cluster All ( x , H ) -> for thesis ;
d * N1 ^2 > N1 * 1 ;
]. a , b .[ c= [. a , b .] ;
set g = f " D1 , h = f " D2 , f = f " D2 ;
dom ( p | mmm1 ) = mmm1 ;
3 + - 2 <= k + - 2 ;
tan is_differentiable_in ( arccot * ( arccot * f ) ) . x ;
x in rng ( f /^ ( n -' p ) ) ;
let f , g be FinSequence of D ;
p ( ) in the carrier of S1 & p ( ) in the carrier of S2 ;
rng f " = dom f & rng f = dom g ;
( the Target of G ) . e = v ;
width G -' 1 < width G -' 1 & width G -' 1 < width G ;
assume v in rng ( S | E1 ) & u in rng ( S | E1 ) ;
assume x is root or x is root or x is root ;
assume that 0 in rng ( g2 | A ) and 0 < r ;
let q be Point of ( TOP-REAL 2 ) | K1 , r be Real ;
let p be Point of TOP-REAL 2 , r be Real ;
dist ( O , u ) <= |. p2 .| + 1 ;
assume dist ( x , b ) < dist ( a , b ) ;
<* SS *> is_\in the carrier of C-20 & <* C *> is_\in the carrier of C-20 ;
i <= len ( G * ( i1 -' 1 , j1 ) ) ;
let p be Point of TOP-REAL 2 , r be Real ;
x1 in the carrier of ( ( TOP-REAL 2 ) | P ) ;
set p1 = f /. i , p2 = f /. ( i + 1 ) ;
g in { g2 : r < g2 & g2 < x0 } ;
Q2 = Sp2 " Q .= Sp2 " Q ;
( ( 1 / 2 ) (#) ( 1 / 2 ) ) is summable ;
- p + I c= - p + A ;
n < LifeSpan ( P1 , s1 ) + 1 & I . n = s1 . n ;
CurInstr ( p1 , s1 ) = i .= halt SCM+FSA ;
A /\ Cl { x } <> {} ;
rng f c= ]. r , r + 1 .[ /\ dom f ;
let g be Function of S , V ;
let f be Function of L1 , L2 , g be Function of L1 , L2 ;
reconsider z = z as Element of CompactSublatt L , x be Element of CompactSublatt L ;
let f be Function of S , T ;
reconsider g = g as Morphism of c opp , b opp ;
[ s , I ] in [: S , T :] ;
len ( the connectives of C ) = 4 & len ( the connectives of C ) = 4 ;
let C1 , C2 be subFunctor of C , D ;
reconsider V1 = V as Subset of X | B ;
attr p is valid means : Def1 : All ( x , p ) is valid ;
assume that X c= dom f and f .: X c= dom g and g .: X c= dom f ;
H |^ a " is Subgroup of H |^ a ;
let A1 be p1 of O , B1 , B2 be Element of E ;
p2 , r3 , q1 is_collinear & q2 , q1 , q2 is_collinear ;
consider x being element such that x in v ^ K ;
not x in { 0. TOP-REAL 2 } & not x in { 0. TOP-REAL 2 } ;
p in [#] ( ( ( TOP-REAL 2 ) | B11 ) | B11 ) ;
0 . 0 < M . ( E . n ) ;
op ( c ) |^ ( c , d ) = c ;
consider c being element such that [ a , c ] in G ;
a1 in dom ( F . s2 ) & a2 in dom ( F . s2 ) ;
cluster -> Nat for *> -| the carrier of L is
set i1 = the Nat , i2 = the Nat , i1 = the Nat , i2 = the Nat , i2 = the Nat ;
let s be 0 -started State of SCM+FSA , P be s of P ;
assume y in ( f1 \/ f2 ) .: A ;
f . ( len f ) = f /. len f .= f /. 1 ;
x , f . x '||' f . x , f . y ;
attr X c= Y means : Def1 : cos | X c= cos | Y ;
let y be upper Subset of Y , x be Element of X ;
cluster x `1 -> -> -> -> -> -> -> -> -> -> -> Nat for Element of \rm <= i ;
set S = <* Bags n , im *> , S = <* Bags n , i *> , T = <* i , j *> , S = <* j , i *> , T = <* j , i *> , S = <* j , i
set T = [. 0 , 1 / 2 .] , S = [. 1 / 2 , 1 .] ;
1 in dom mid ( f , 1 , 1 ) ;
( 4 * PI ) / PI < ( 2 * PI ) / PI ;
x2 in dom f1 /\ dom f & x2 in dom f1 /\ dom f2 ;
O c= dom I & { {} } = { {} } ;
( the Source of G ) . x = v ;
{ HT ( f , T ) } c= Support f ;
reconsider h = R . k as Polynomial of n , L ;
ex b being Element of G st y = b * H ;
let x , y , z be Element of G opp ;
h19 . i = f . ( h . i ) ;
p `1 = p1 `1 & p `2 = p1 `2 or p `2 = p1 `2 ;
i + 1 <= len Cage ( C , n ) ;
len <* P *> @ = len P & width <* P *> = width P ;
set N-26 = the Subset of N , NN = the Subset of N ;
len gfunction + ( x + 1 ) - 1 <= x ;
a on B & b on B & a on B ;
reconsider rc = r * I . v as FinSequence of REAL ;
consider d such that x = d and a D D [= c ;
given u such that u in W and x = v + u ;
len f /. ( \downharpoonright n ) = len sequence ( f ) ;
set q2 = N-min L~ Cage ( C , n ) , q1 = N-min L~ Cage ( C , n ) , q2 = \ { q : q in L~ f } ;
set S =
MaxADSet ( b ) c= MaxADSet ( P /\ Q ) ;
Cl ( G . q1 ) c= F . r2 & Cl ( G . q2 ) c= G . s2 ;
f " D meets h " V & f " D meets h " V ;
reconsider D = E as non empty directed Subset of L1 ;
H = ( the_left_argument_of H ) '&' ( the_right_argument_of H ) ;
assume t is Element of ( the carrier of S ) * , X ;
rng f c= the carrier of S2 & rng g c= the carrier of S2 ;
consider y being Element of X such that x = { y } ;
f1 . ( a1 , b1 ) = b1 & f1 . ( b1 , c1 ) = c1 ;
the carrier' of G ` = E \/ { E } .= { E } ;
reconsider m = len ' implies k = len ( p | k ) ;
set S1 = LSeg ( n , UMP C ) , S2 = LSeg ( UMP C , UMP C ) ;
[ i , j ] in Indices M1 & [ i , j ] in Indices M2 ;
assume that P c= Seg m and M is \HM { of Seg m } ;
for k st m <= k holds z in K . k ;
consider a being set such that p in a and a in G ;
L1 . p = p * L /. ( 1 + 1 ) ;
p-7 . i = pp1 . i & pp2 . i = pp2 . i ;
let PA , G be a_partition of Y , a be Element of Y ;
pred 0 < r & r < 1 implies 1 < ( 1 - r ) * ( 1 - r ) ;
rng ( ( ( a , X ) --> ( a , b ) ) ) = [#] X ;
reconsider x = x , y = y , z = z as Element of K ;
consider k such that z = f . k and n <= k ;
consider x being element such that x in X \ { p } ;
len ( ( canFS s ) | ( s -' 1 ) ) = card s - 1 ;
reconsider x2 = x1 , y2 = x2 as Element of L2 ;
Q in FinMeetCl ( ( the topology of X ) \ { x } ) ;
dom ( f . 0 ) c= dom ( u . 0 ) ;
pred n divides m & m divides n implies n = m ;
reconsider x = x as Point of [: I[01] , I[01] :] ;
a in ;
not y0 in the still of f & not y in { x , y } ;
Hom ( ( a ~ ) , c ) <> {} ;
consider k1 such that p " < k1 and k1 < p " ;
consider c , d such that dom f = c \ d ;
[ x , y ] in [: dom g , dom k :] ;
set S1 =
l2 = m2 & l1 = i2 & l2 = j2 implies l1 = l2
x0 in dom ( u01 /\ A ) & x0 in dom ( u01 /\ A ) ;
reconsider p = x as Point of ( TOP-REAL 2 ) | K1 , q = ( TOP-REAL 2 ) | K1 as Point of TOP-REAL 2 ;
I[01] = R^1 | B01 .= ( ( ( TOP-REAL 2 ) | B01 ) ) | B01 ;
f . p4 <= f . p1 & f . p1 <= f . p2 ;
( F /. i ) `1 <= ( x `1 ) / ( x `2 ) ;
x `2 = ( W7 ) `2 .= ( W7 ) `2 .= ( W8 ) `2 ;
for n being Element of NAT holds P [ n ] ;
let J , K be non empty Subset-Family of I ;
assume 1 <= i & i <= len <* a " *> ;
0 |-> a = <*> ( the carrier of K ) ;
X . i in 2 -tuples_on A . i \ B . i ;
<* 0 *> in dom ( e --> [ 1 , 0 ] ) ;
then P [ a ] & P [ succ a ] implies P [ succ a ] ;
reconsider s\overline = s\overline { s where s is < s : s < n } as finite of D ;
( Seg i -' 1 ) <= len ' - j ;
[#] S c= [#] the TopStruct of T & [#] T c= the TopStruct of T ;
for V being strict RealUnitarySpace holds V in and V in and v in strict implies v in W
assume k in dom mid ( f , i , j ) ;
let P be non empty Subset of TOP-REAL 2 , p1 , p2 , p3 be Point of TOP-REAL 2 ;
let A , B be square Matrix of n1 , K , n , m be Nat ;
- a * - b = a * b - b * a ;
for A being Subset of AS holds A // A & A // C implies A = C
( for o2 being element st o2 in dom o2 holds o2 . o2 = <* o2 , o2 *> ) implies o2 = o2
then ||. x - y .|| = 0 & x = 0. X ;
let N1 , N2 be strict normal Subgroup of G , N be normal Subgroup of G ;
j >= len upper_volume ( g , D1 ) & len upper_volume ( g , D2 ) = len D1 ;
b = Q . ( len Qa - 1 + 1 ) .= Q . ( len Qa - 1 ) ;
f2 (#) f1 /* s is divergent_to-infty & lim ( f2 (#) f1 ) = x0 ;
reconsider h = f * g as Function of [: N2 , G :] , G ;
assume that a <> 0 and Let a , b , c , d ;
[ t , t ] in the InternalRel of A & [ t , s ] in the InternalRel of A ;
( v |-- E ) | n is Element of ( T . n ) -tuples_on ( T . n ) ;
{} = the carrier of L1 + L2 & the carrier of L1 = the carrier of L1 + L2 ;
Directed I is_closed_on Initialized s , P & Directed I is_halting_on Initialized s , P ;
Initialized p = Initialize ( p +* q ) .= p +* q .= p +* q ;
reconsider N2 = N1 , N2 = N2 as strict net of R2 ;
reconsider Y = Y as Element of <* Ids L , \subseteq \rangle ;
"/\" ( uparrow p \ { p } , L ) <> p ;
consider j being Nat such that i2 = i1 + j and j in dom f ;
not [ s , 0 ] in the carrier of S2 & not [ s , 0 ] in the carrier of S2 ;
mm in ( B '&' C ) '/\' D \ { {} } ;
n <= len ( ( P + Q ) ^ <* P . ( len P + 1 ) *> ) ;
x1 `1 = x2 `1 & x1 `2 = y2 & x1 `2 = y2 ;
InputVertices S = { x1 , x2 , x3 , x4 , x4 , x5 , x5 , x5 , x5 , x5 , 7 } ;
let x , y be Element of [: FT1 ( n ) , FT1 ( n ) :] ;
p = |[ p `1 , p `2 ]| & p = |[ p `1 , p `2 ]| ;
g * 1_ G = h " * g * h * h ;
let p , q be Element of PFuncs ( V , C ) ;
x0 in dom x1 /\ dom x2 & x1 in dom x1 /\ dom x2 ;
( R qua Function ) " = R " & ( R qua Function ) " = R " ;
n in Seg len ( f /^ ( len p -' 1 ) ) ;
for s being Real st s in R holds s <= s2 & s2 <= s1 ;
rng s c= dom ( f2 * f1 ) /\ dom ( f2 * f1 ) ;
synonym for for for for for for for for for for for for for ( X \ { x } ) ;
1. K * 1. K = 1. K & 1. K * 1. K = 1. K ;
set S = Segm ( A , P1 , Q1 ) , T = Segm ( A , P1 , Q1 ) ;
ex w st e = ( w / f ) & w in F ;
curry ( P+* ( k , k ) ) # x is convergent ;
cluster open -> open for Subset of [: T , T :] ;
len f1 = 1 .= len f3 .= len f3 + len f3 .= len f3 + 1 ;
( i * p ) / p < ( 2 * p ) / p ;
let x , y be Element of OSSub ( U0 ) , a be Element of U0 ;
b1 , c1 // b9 , c9 & o , c1 // o , c ;
consider p being element such that c1 . j = { p } ;
assume that f " { 0 } = {} and f is total ;
assume IC Comput ( F , s , k ) = n & IC Comput ( F , s , k ) = k ;
Reloc ( J , card I + 3 ) does not destroy a ;
( goto ( card I + 1 ) ) does not destroy c ;
set m3 = LifeSpan ( p3 , s3 ) , P4 = P +* I , P4 = P +* I , P4 = P +* I , m3 = P +* I , m3 = P +* I , P4 = P +* I , P4 = P +* I , P4 =
IC SCMPDS in dom Initialize ( p +* I ) & IC SCMPDS in dom Initialize ( p +* I ) ;
dom t = the carrier of SCM R & dom t = the carrier of SCM R ;
( ( N-min L~ f ) .. f ) .. f = 1 & ( ( E-max L~ f ) .. f ) .. f = 1 ;
let a , b be Element of Let ( V , C ) ;
Cl Int Cl Int F c= Cl Int Cl Int Cl Int F ;
the carrier of X1 union X2 misses ( ( X1 union X2 ) \/ ( X2 union X1 ) ) ;
assume not LIN a , f . a , g . a , f . a ;
consider i being Element of M such that i = d6 and i in dom f ;
then Y c= { x } or Y = { x } ;
M , v / ( y , x ) / ( y , x ) / ( y , x ) / ( y , x ) / ( y , x ) / ( y , x ) ;
consider m being element such that m in Intersect ( FF , B ) and x = ( Intersect ( FF , B ) ) . m ;
reconsider A1 = support u1 , A2 = support u2 as Subset of X ;
card ( A \/ B ) = k-1 + ( 2 * 1 ) ;
assume that a1 <> a3 and a2 <> a4 and a3 <> a4 and a3 <> a4 and a4 <> a5 ;
cluster s , S -carrier -> ( S , X ) -valued for string of S ;
LL2 /. n2 = LL2 . n2 .= LL2 . n2 .= LL2 . n2 ;
let P be compact non empty Subset of TOP-REAL 2 , p1 , p2 , p3 be Point of TOP-REAL 2 ;
assume r-7 in LSeg ( p1 , p2 ) /\ LSeg ( p1 , p2 ) ;
let A be non empty compact Subset of TOP-REAL n , a be Real ;
assume that [ k , m ] in Indices DM1 and [ k , m ] in Indices DM1 ;
0 <= ( ( 1 / 2 ) |^ p ) / ( p |^ n ) ;
( F . N ) | ( E . m ) . x = +infty ;
pred X c= Y & Z c= V implies X \ V c= Y \ Z ;
y `2 * ( z `2 ) * ( z `2 ) <> 0. I & y `2 * ( z `2 ) * ( z `2 ) <> 0. I ;
1 + card X-18 <= card X-18 + card X-18 ;
set g = z :- ( ( L~ z ) .. z ) , p = z /. 1 , q = z /. len z , r = q /. len z , s = q /. len z , t = q /. len z , s = q /. len z , w
then k = 1 & p . k = <* x , y *> . k ;
cluster total for Element of C -O , X be total set ;
reconsider B = A as non empty Subset of ( TOP-REAL n ) | A , B = B ;
let a , b , c be Function of Y , BOOLEAN , p be Function of Y , BOOLEAN ;
L1 . i = ( i .--> g ) . i .= g . i .= g . i ;
Plane ( x1 , x2 , x3 , x4 ) c= P & Plane ( x2 , x3 , x4 ) c= P ;
n <= indx ( D2 , D1 , j1 ) & n <= len D2 ;
( ( g2 . O ) `1 ) = - 1 & ( g2 . O ) `2 = 1 ;
j + p .. f - len f <= len f - len f - len f ;
set W = W-bound C , E = E-bound C , N = N-bound C , S = E-bound C , N = N-bound C , N = N-bound C , S = N-bound C , N = N-bound C , S = N-bound C , N = N-bound C , S = E-bound
S1 . ( a `1 , e `2 ) = a + e .= a `1 ;
1 in Seg width ( M * ( ColVec2Mx p ) ) & len ( M * ( ColVec2Mx p ) ) = width M ;
dom ( i (#) Im ( f ) ) = dom Im ( f ) ;
\mathbb \mathbb N . x `2 = W . ( a , *' ( a , p ) ) ;
set Q = ( / ( g , f , h ) ) \ { f , h } ;
cluster -> MSsorted for ManySortedSet of U1 , ( the Sorts of U1 ) * ;
attr F = { A } means : : ex A st F is discrete ;
reconsider z9 = \hbox { y } as Element of product \overline G ;
rng f c= rng f1 \/ rng f2 & rng f1 c= dom f1 \/ rng f2 ;
consider x such that x in f .: A and x in f .: C ;
f = <*> ( the carrier of F_Complex ) & f = <*> ( the carrier of F_Complex ) ;
E , j |= All ( x1 , x2 , H ) implies E , j |= H
reconsider n1 = n , n2 = m , n3 = n as Morphism of o1 , o2 ;
assume that P is idempotent and R is idempotent and P ** R = R ** P ;
card ( B2 \/ { x } ) = k-1 + 1 ;
card ( ( x \ B1 ) /\ B1 ) = 0 implies B1 = B2 ;
g + R in { s : g-r < s & s < g + r } ;
set qv1 = ( q , <* s *> ) -\subseteq ( q , <* s *> ) -\subseteq q ;
for x be element st x in X holds x in rng f1 /\ rng f2 ;
h0 /. ( i + 1 ) = h0 . ( i + 1 ) ;
set mw = max ( B , dom ( R | NAT ) ) , mw = max ( B , NAT ) ;
t in Seg width ( I ^ ( n , n ) ) ;
reconsider X = dom f /\ C as Element of Fin NAT ;
IncAddr ( i , k ) = <% a , b , c , d %> ;
S-bound L~ f <= q `2 & q `2 <= q `2 & q `2 <= N-bound L~ f ;
attr R is condensed means : Def1 : Int R is condensed & Cl R is condensed ;
pred 0 <= a & 1 <= b & b <= 1 implies a * b <= 1 ;
u in ( ( c /\ ( d /\ e ) ) /\ f ) /\ j ;
u in ( ( c /\ ( ( d /\ e ) /\ b ) ) /\ f ) /\ j ;
len C + - 2 >= 9 + - 3 & len C + - 2 >= 9 + - 2 ;
x , z , y is_collinear & x , z , x is_collinear & x , y , x is_collinear ;
a |^ ( n1 + 1 ) = a |^ n1 * a |^ n1 ;
<* \underbrace ( 0 , \dots , 0 } , x ) in Line ( x , a * x ) ;
set yp1 = <* y , c *> ;
FF2 /. 1 in rng Line ( D , 1 ) & FF2 /. len FF2 = Line ( D , 1 ) ;
p . m Joins r /. m , r /. ( m + 1 ) , G ;
p `2 = ( f /. i1 ) `2 .= ( f /. i1 ) `2 .= ( f /. i1 ) `2 ;
W-bound ( X \/ Y ) = W-bound X & W-bound ( X \/ Y ) = W-bound Y ;
0 + ( p `2 ) <= 2 * r + ( p `2 ) ;
x in dom g & not x in g " { 0 } ;
f1 /* ( seq ^\ k ) is divergent_to-infty & lim ( f1 /* ( seq ^\ k ) ) = f1 . x0 ;
reconsider u2 = u , v2 = v as VECTOR of ( P`1 ) | X ;
p |-count ( Product Sgm X11 ) = 0 & p |-count X11 = 1 ;
len <* x *> < i + 1 & i + 1 <= len c + 1 ;
assume that I is non empty and { x } /\ { y } = { 0. I } ;
set ii2 = ( card I + 4 ) .--> goto 0 , ii2 = goto 0 , ii2 = goto 0 ;
x in { x , y } & h . x = {} ( Tx , y ) ;
consider y being Element of F such that y in B and y <= x ` ;
len S = len ( the charact of ( ( the charact of ( A ) ) * ( the charact of B ) ) ) ;
reconsider m = M , i = I , n = N as Element of X ;
A . ( j + 1 ) = B . ( j + 1 ) \/ A . j ;
set N8 = ( G -`1 ) \/ ( G -`1 ) ;
rng F c= the carrier of gr { a } & rng F c= the carrier of gr { a } ;
Comput ( P , Q , n ) is a |. : ex r being FinSequence st r is ) ;
f . k , f . ( Let n ) in rng f & n in dom f ;
h " P /\ [#] T1 = f " P /\ [#] T2 .= [#] T2 ;
g in dom f2 \ f2 " { 0 } & f2 " { 0 } = dom f2 ;
g` /\ dom f1 = g1 " X & gX ` /\ dom f2 = g2 " X ;
consider n being element such that n in NAT and Z = G . n ;
set d1 = let f1 , d2 = dist ( x1 , y1 ) , d2 = dist ( x2 , y2 ) , d2 = dist ( x2 , y2 ) ;
b `2 + 1 / 2 < ( 1 - 1 ) / 2 + ( 1 - 1 ) / 2 ;
reconsider f1 = f as VECTOR of the carrier of the carrier of X , Y ;
attr i <> 0 implies i ^2 mod ( i + 1 ) = 1 ;
j2 in Seg len ( ( g2 . i2 ) | ( Seg ( len g2 ) ) ) ;
dom i4 = dom i2 .= a .= dom ( i + 1 ) .= dom ( i + 1 ) ;
cluster sec | ]. PI / 2 , PI / 2 .[ -> one-to-one ;
Ball ( u , e ) = Ball ( f . p , e ) .= Ball ( u , e ) ;
reconsider x1 = x0 , y1 = x1 as Function of S , IV , r be Real ;
reconsider R1 = x , R2 = y , R1 = z , R2 = x as Relation of L ;
consider a , b being Subset of A such that x = [ a , b ] ;
( <* 1 *> ^ p ) ^ <* n *> in RH ;
S1 +* S2 = S2 +* S2 +* S2 .= S2 +* S2 +* S2 .= S2 +* S2 +* S2 .= S2 +* S2 ;
( ( #Z n ) * ( cos + sin ^2 ) ) is_differentiable_on Z & for x st x in Z holds ( ( #Z n ) * ( cos + sin ^2 ) ) `| Z = f ;
cluster -> ( 0 , 1 ) -valued for Function of C , REAL ;
set C7 = 1GateCircStr ( <* z , x *> , f3 ) , C8 = 1GateCircStr ( <* x , y *> , f3 ) ;
Ea1 . e2 = ( E . e2 ) -T .= ( E . e2 ) -T .= ( E . e2 ) -T ;
( ( ( ( 1 / 2 ) (#) ( ln * f ) ) `| Z ) ) = f ;
upper_bound A = ( PI * 3 / 2 ) * 2 & lower_bound A = 0 ;
F . ( dom f , - - F ) is_transformable_to F . ( cod f , - F . cod - F . cod f ) ;
reconsider pbeing = qi , pj = q as Point of Euclid 2 ;
g . W in [#] Y0 & [#] Y0 c= [#] Y0 ;
let C be compact non vertical non horizontal Subset of TOP-REAL 2 , p be Point of TOP-REAL 2 ;
LSeg ( f ^ g , j ) = LSeg ( f , j ) ;
rng s c= dom f /\ ]. x0 - r , x0 .[ & rng s c= dom f /\ ]. x0 , x0 + r .[ ;
assume x in { idseq 2 , Rev ( idseq 2 ) , Rev ( idseq 2 ) } ;
reconsider n2 = n , m2 = m , m2 = n as Element of NAT ;
for y being ExtReal st y in rng seq holds g <= y + r ;
for k st P [ k ] holds P [ k + 1 ] ;
m = m1 + m2 .= m1 + m2 .= m1 + m2 .= m1 + m2 ;
assume for n holds H1 . n = G . n -H . n ;
set B" = f .: ( the carrier of X1 ) , B" = f .: ( the carrier of X2 ) ;
ex d being Element of L st d in D & x << d ;
assume that R -Seg ( a ) c= R -Seg ( b ) and R -Seg ( a ) c= R -Seg ( b ) ;
t in ]. r , s .] or t = r or t = s ;
z + v2 in W & x = u + ( z + v2 ) ;
x2 |-- y2 iff P [ x2 , y2 ] & P [ x2 , y2 ] ;
pred x1 <> x2 means : Def1 : |. x1 - x2 .| > 0 & |. x2 - x1 .| > 0 ;
assume that p2 - p1 , p3 - p1 - p1 , p3 - p1 - p1 , p3 - p1 - p1 is_collinear and p3 - p1 , p3 - p1 - p1 , p3 - p1 - p1 is_collinear ;
set q = ( U ^ <* 'not' A *> ) ^ <* 'not' A *> ;
let f be PartFunc of REAL-NS 1 , REAL-NS n , g be PartFunc of REAL-NS 1 , REAL-NS n ;
( n mod ( 2 * k ) ) + 1 = n mod k ;
dom ( T * ( succ t ) ) = dom ( ( succ t ) | ( dom ( T . t ) ) ) ;
consider x being element such that x in wc iff x in c ;
assume ( F * G ) . ( v . x3 ) = v . x4 ;
assume that the carrier of D1 c= the carrier of D2 and the carrier of D1 c= the carrier of D2 and the carrier of D1 c= the carrier of D2 ;
reconsider A1 = [. a , b .[ as Subset of R^1 | A , a , b .] ;
consider y being element such that y in dom F and F . y = x ;
consider s being element such that s in dom o and a = o . s ;
set p = W-min L~ Cage ( C , n ) , q = E-max L~ Cage ( C , n ) , r = W-bound L~ Cage ( C , n ) ;
n1 -' len f + 1 - len f <= len f + 1 - len f + 1 - len f ;
Seg \mathbb \mathbb \mathbb . ( q , O1 ) = [ u , v , a `2 , b `2 ] ;
set C-2 = ( ( `1 ) `1 ) . ( k + 1 ) ;
Sum ( L (#) p ) = 0. R * Sum p .= 0. V .= 0. V ;
consider i be element such that i in dom p and t = p . i ;
defpred Q [ Nat ] means 0 = Q ( $1 ) & for k st k in $1 holds P [ k , $1 , k ] ;
set s3 = Comput ( P1 , s1 , k ) , P3 = P1 +* I , s4 = P1 +* I , P3 = P3 ;
let l be variable of k , Al , A-30 be Subset of k ;
reconsider UA = union G-24 , GN = union GN as Subset-Family of [: T , T :] ;
consider r such that r > 0 and Ball ( p `2 , r ) c= Q `2 ;
( h | ( n + 2 ) ) /. ( i + 1 ) = p29 ;
reconsider B = the carrier of X1 , C = the carrier of X2 as Subset of X2 ;
pholds pca = <* - c , 1 , 1 *> & pa = <* - c , 1 *> ;
synonym f is real-valued means : Def2 : rng f c= NAT & rng f c= NAT & for n being Nat holds f . n = n ;
consider b being element such that b in dom F and a = F . b ;
x9 < card X0 + card Y0 & x9 in card X0 & y9 in card X0 + card X0 ;
attr X c= B1 means : Def1 : for B1 st X c= B1 holds \mathop { \rm _ oop) X c= B1 ;
then w in Ball ( x , r ) & dist ( x , w ) <= r ;
angle ( x , y , z ) = angle ( x-y , 0 , z ) ;
pred 1 <= len s means : : : for i being Element of NAT holds ( for s being Element of NAT st s = s holds s . i = 1 ) ;
fthat fthat c= f . ( k + ( n + 1 ) ) ;
the carrier of { 1_ G } = { 1_ G } & the carrier of G = { 1_ G } ;
pred p '&' q in \cdot ( p '&' q ) means : : : q in \cdot ( p '&' q ) ;
- ( t `1 ) < ( t `2 ) / ( 1 + ( t `2 / t `1 ) ^2 ) ;
UA . 1 = U2 /. 1 .= ( U2 /. 1 ) .= ( U2 /. 1 ) . 1 .= ( U2 /. 1 ) . 1 ;
f .: ( the carrier of x ) = the carrier of x & f .: ( the carrier of x ) = { x } ;
Indices O = [: Seg n , Seg n :] & dom O = [: Seg n , Seg n :] ;
for n being Element of NAT holds G . n c= G . ( n + 1 ) ;
then V in M @ ex x being Element of M st V = { x } ;
ex f being Element of F-9 st f is H & f is H & f is H & f is H ;
[ h . 0 , h . 3 ] in the InternalRel of G & [ h . 0 , h . 2 ] in the InternalRel of G ;
s +* Initialize ( ( intloc 0 ) .--> 1 ) = s3 +* Initialize ( ( intloc 0 ) .--> 1 ) ;
|[ w1 , v1 ]| the H of ( ( TOP-REAL 2 ) | ( ( TOP-REAL 2 ) | ( ( TOP-REAL 2 ) | ( ( TOP-REAL 2 ) | ( ( TOP-REAL 2 ) | ( ( TOP-REAL 2 ) | ( ( TOP-REAL 2 ) | ( ( TOP-REAL 2 ) | ( K ) ) ) ) ) ) )
reconsider t = t as Element of INT * , s be Element of INT * ;
C \/ P c= [#] ( ( GX | A ) \ A ) ;
f " V in ( the topology of X ) /\ D . ( the carrier of S , the topology of T ) ;
x in [#] ( ( the carrier of A ) /\ delta ( F ) ) ;
g . x <= h1 . x & h . x <= h1 . x & h . y <= h . y ;
InputVertices S = { xy , y , z } \/ { xy , y , z } .= { xy , y , z } ;
for n being Nat st P [ n ] holds P [ n + 1 ] ;
set R = Line ( M , i , a * Line ( M , i ) ) ;
assume that M1 is being_line and M2 is being_line and M3 is being_line and M3 is being_line and M3 is being_line ;
reconsider a = f4 . ( i0 -' 1 ) , b = f4 . ( i0 -' 1 ) as Element of K ;
len B2 = Sum ( Len ( F1 ^ F2 ) ) .= len ( Len F1 ) + len ( Len F2 ) ;
len ( ( the H of n ) * ( i , j ) ) = n & len ( ( the H of n ) * ( i , j ) ) = n ;
dom ( max ( f , g ) + g ) = dom ( f + g ) .= dom f /\ dom g ;
( the Sorts of seq ) . n = upper_bound Y1 & ( the Sorts of seq ) . n = upper_bound Y2 ;
dom ( p1 ^ p2 ) = dom ( f12 ^ <* p *> ) .= dom f12 ;
M . [ 1 , y ] = 1 * v1 .= ( 1 - 1 ) * v1 .= y ;
assume that W is non trivial and W .vertices() c= the carrier' of G2 and not e in the carrier' of G2 ;
C6 * ( i1 , i2 ) = G1 * ( i1 , i2 ) .= G1 * ( i1 , i2 ) ;
C8 |- 'not' Ex ( x , p ) 'or' p . ( x , y ) ;
for b st b in rng g holds lower_bound rng f\rbrace <= b - lower_bound rng f\lbrace b - a , b + a }
- ( ( q1 `1 / |. q1 .| - sn ) / ( 1 + sn ) ) = 1 ;
( LSeg ( c , m ) \/ [: NAT , { k } :] ) c= R ;
consider p be element such that p in { x } and p in L~ f and x in L~ f ;
Indices ( X @ ) = [: Seg n , Seg 1 :] & dom ( X @ ) = Seg n ;
cluster s => ( q => p ) => ( q => ( s => p ) ) -> valid ;
Im ( ( Partial_Sums F ) . m ) is_measurable_on E & ( Partial_Sums F ) . m is_measurable_on E ;
cluster f . ( x1 , x2 ) . x -> Element of D . ( x1 , x2 ) . x ;
consider g being Function such that g = F . t and Q [ t , g . t ] ;
p in LSeg ( NW-corner Z , NW-corner Z ) /\ LSeg ( NW-corner Z , NW-corner Z ) ;
set R8 = R |^ 1 ]. b , +infty .[ , R8 = R |^ 1 ;
IncAddr ( I , k ) = SubFrom ( da , db ) .= SubFrom ( da , db ) ;
seq . m <= ( the Sorts of ( X + Y ) ) . k & ( the Sorts of ( X + Y ) ) . k <= ( the Sorts of ( X + Y ) ) . k ;
a + b = ( a ` *' b ` ) ` .= a ` *' b ` .= a ` *' b ` ;
id ( X /\ Y ) = id X /\ id Y .= id ( X /\ Y ) ;
for x be element st x in dom h holds h . x = f . x ;
reconsider H = ( U1 \/ U2 ) as non empty Subset of ( the carrier of U0 ) * ;
u in ( ( c /\ ( ( d /\ e ) /\ b ) ) /\ m ) /\ j ;
consider y being element such that y in Y and P [ y , inf B ] ;
consider A being finite stable set of R such that card A = ( the carrier of R ) \ A ;
p2 in rng ( f |-- p1 ) \ rng <* p1 *> & p2 in rng <* p1 *> ;
len s1 - 1 > 1-1 & len s2 - 1 > 1 - 1 & len s2 - 1 > 0 ;
( N-min P ) `2 = N-bound P & ( N-min P ) `2 = N-bound P implies ( P ) `2 = N-bound P
Ball ( e , r ) c= LeftComp Cage ( C , k + 1 ) \/ LeftComp Cage ( C , k + 1 ) ;
f . a1 ` = f . a1 ` .= f . a1 ` .= f . a1 ` .= f . a1 ;
( seq ^\ k ) . n in ]. -infty , x0 .[ & ( seq ^\ k ) . n in dom ( f | ]. x0 , x0 + r .[ ) ;
gg . s0 = g . s0 | G . s0 .= g . s0 .= g . s0 ;
the InternalRel of S is \lbrace x , y } & the InternalRel of S is non empty ;
deffunc F ( Ordinal , Ordinal ) = phi . ( $1 , $2 ) ;
F . ( s1 . a1 ) = F . ( s2 . a1 ) .= ( F . a1 ) . a1 ;
x `2 = A . a .= Den ( o , A . a ) .= Den ( o , A . a ) ;
Cl ( f " P1 ) c= f " ( Cl P1 ) & Cl ( f " P1 ) c= f " ( Cl P1 ) ;
FinMeetCl ( ( the topology of S ) \ { x } ) c= the topology of T ;
synonym o is OperSymbol means : Def2 : o <> *' & o <> * & o <> * & o <> * ;
assume that X = Y + 1 and card X <> card Y and card Y <> card X and card X = card Y ;
the *> of s <= 1 + ( ( the +* s ) +* ( ( the +* s ) +* ( ( the +* s ) +* ( s +* ( s +* ( s +* ( s +* ( s +* ( s +* ( s +* ( s +* ( s +* ( s +* ( s +* ( s +* ( s +* ( s +* ( s +* ( s
LIN a , a1 , d or b , c // b1 , c1 or a , c // a1 , c1 ;
e / 2 . 1 = 0 & e / 2 . 2 = 1 & e / 2 . 3 = 0 ;
EE in SE & not EE in { NE } ;
set J = ( l , u ) If ;
set A1 = thesis , A2 = } , A1 = } , A2 = { A1 , A2 , p3 = { cin , d , c , d } ;
set vs = [ <* c , d *> , '&' ] , xy = [ <* d , c *> , '&' ] , } = [ <* c , d *> , '&' ] ;
x * z `2 * x " in x * ( z * N ) * x " ;
for x be element st x in dom f holds f . x = g3 . x ;
Int cell ( f , 1 , G ) c= RightComp f \/ L~ f \/ L~ f \/ L~ f ;
UA is_an_arc_of W-min C , E-max C & \subseteq L~ Cage ( C , n ) implies L~ Cage ( C , n ) c= L~ Cage ( C , n )
set f-17 = f @ "/\" g @ ;
attr S1 is convergent means : Def1 : S2 is convergent & lim ( S1 - S2 ) = 0 ;
f . ( 0 + 1 ) = ( 0 qua Ordinal ) + a .= a ;
cluster -> \lbrace be be in be be be be be be reflexive transitive non empty RelStr , F be reflexive non empty reflexive RelStr ;
consider d being element such that R reduces b , d and R reduces c , d and R reduces d , c ;
not b in dom Start-At ( ( card I + 2 ) , SCMPDS ) \/ dom Start-At ( ( card I + 2 ) , SCMPDS ) ;
( z + a ) + x = z + ( a + y ) .= z + a + y ;
len ( l \lbrack a |^ 0 , x \rbrack ) = len l & len ( l |^ 0 ) = len l ;
t4 ^ {} is ( {} \/ rng t4 ) -valued FinSequence of ( {} \/ rng t4 ) * ;
t = <* F . t *> ^ ( C . p ) ^ ( C . q ) .= <* F . t *> ^ q ;
set pp = W-min L~ Cage ( C , n ) , p = W-min L~ Cage ( C , n ) , G = Gauge ( C , n ) * ( i , 1 ) , G = Gauge ( C , n ) * ( i , 1 ) , p = G * ( i , 1 ) , q = G * ( i , 1 )
kk -' ( i + 1 ) = kk - ( i + 1 ) .= kk - ( i + 1 ) ;
consider u being Element of L such that u = u ` and u in D ` ;
len ( ( width ( G |-> a ) ) |-> a ) = width ( ( G |-> a ) * ( G * ( i , j ) ) ) ;
FM . x in dom ( ( G * the_arity_of o ) . x ) & FM . x in dom ( G * the_arity_of o ) ;
set cH2 = the carrier of H2 , cH1 = the carrier of H1 , cH2 = the carrier of H2 ;
set cH1 = the carrier of H1 , cH2 = the carrier of H2 ;
( Comput ( P , s , 6 ) ) . intpos m = s . intpos m .= s . intpos m ;
IC Comput ( Q2 , t , k ) = ( l + 1 ) .= ( l + 1 ) + 1 ;
dom ( ( cos * sin ) `| REAL ) = REAL & dom ( ( cos * sin ) `| REAL ) = REAL ;
cluster <* l *> ^ phi -> ( 1 + 1 , ( not ( n + 1 ) ) ) string for string of S ;
set b5 = [ <* that p , c6 *> , <* p *> ] , b6 = [ <* p , c6 *> , <* p *> ] ;
Line ( Segm ( M @ , P , Q ) , x ) = L * Sgm Q .= Line ( M , x ) ;
n in dom ( ( the Sorts of A ) * ( the_arity_of o ) ) & dom ( ( the Sorts of A ) * ( the_arity_of o ) ) = dom ( the Sorts of A ) ;
cluster f1 + f2 -> continuous for PartFunc of REAL , the carrier of S , the carrier of T ;
consider y be Point of X such that a = y and ||. x-y - x .|| <= r ;
set x3 = t3 . DataLoc ( ( 8 + 2 ) , 2 ) , x4 = s . SBP , 6 = s . SBP , 7 = s . SBP , 8 = s . SBP , 6 = s . SBP , 8 = s . SBP , 7 = s . SBP , 8 = s . SBP , 8 = s . SBP
set p-3 = stop I ( ) , pE = stop I ( ) ;
consider a being Point of D2 such that a in W1 and b = g . a and a in W2 ;
{ A , B , C , D , E } = { A , B , C } \/ { D , E , F , J , M } ;
let A , B , C , D , E , F , J , M , N , N , M , N , M , N , N , M , N , N , M be set ;
|. p2 .| ^2 - ( p2 `2 ) ^2 - ( p2 `2 ) ^2 >= 0 ;
l - 1 + 1 = n-1 * ( l + ( 1 - 1 ) ) + 1 ;
x = v + ( a * w1 + ( b * w2 ) ) + ( c * w2 ) ;
the TopStruct of L = , , C = reconsider D = , C = , D = L , E = the Scott Scott of L , F = the Scott Scott of L ;
consider y being element such that y in dom H1 and x = H1 . y and y in { x } ;
ff \ { n } = ( Free All ( v1 , H ) ) \ { n } .= Free All ( v1 , H ) ;
for Y being Subset of X st Y is summable & Y is summable holds Y is \overline summable & Y is not summable
2 * n in { N : 2 * Sum ( p | N ) = N & N > 0 } ;
for s being FinSequence holds len ( ( the ` of V ) * s ) = len s & len ( ( the multF of V ) * s ) = len s ;
for x st x in Z holds exp_R * f is_differentiable_in x & ( exp_R * f ) . x > 0 ;
rng ( h2 * f2 ) c= the carrier of ( ( TOP-REAL 2 ) | ( the carrier of TOP-REAL 2 ) ) | ( the carrier of ( TOP-REAL 2 ) | ( the carrier of TOP-REAL 2 ) ) ) ;
j + ( len f ) <= len f + ( len g - len f ) - len f ;
reconsider R1 = R * I as PartFunc of REAL , REAL-NS n , REAL-NS n , REAL-NS n be PartFunc of REAL n , REAL-NS n ;
C8 . x = s1 . x0 .= C8 . x .= C8 . x .= C8 . x .= ( C * ( x - x0 ) ) . x ;
power F_Complex . ( z , n ) = 1 .= x |^ n .= x |^ n .= x |^ n ;
t at ( C , s ) = f . ( ( the connectives of S ) . t ) .= f . ( s , I ) ;
support ( f + g ) c= support f \/ support g & support ( f + g ) c= support f \/ support g ;
ex N st N = j1 & 2 * Sum ( seq1 | N ) > N & N > 0 ;
for y , p st P [ p ] holds P [ All ( y , p ) ] ;
{ [ x1 , x2 ] where x1 is Subset of [: X1 , X2 :] , x2 is Subset of X2 , y2 is Element of X2 : y2 = x2 } ;
h = ( i = j |-- h , id B . i ) .= H . i .= H . i ;
ex x1 being Element of G st x1 = x & x1 * N c= A & x1 in N ;
set X = ( ( |. ( q , O1 ) . O ) `1 ) , Y = ( |. q .| ) . O ) , Z = { ( q , O1 ) . O } ;
b . n in { g1 : x0 < g1 & g1 < x0 & g1 < x0 } ;
f /* s1 is convergent & f /. x0 = lim ( f /* s1 ) & lim s1 = lim ( f /* s1 ) ;
the lattice of Y = the lattice of the lattice of Y & the topology of X = the topology of Y & the topology of Y = the topology of X ;
'not' ( a . x ) '&' b . x 'or' a . x '&' 'not' ( b . x ) = FALSE ;
2 = len ( q0 ^ r1 ) + len ( q1 ^ q2 ) .= len ( q1 ^ q2 ) + len ( q2 ^ q3 ) ;
( 1 / a ) (#) ( sec * f1 ) - id Z ) is_differentiable_on Z ;
set K1 = upper_volume ( ( lim ( lim ( H , A ) || , ( lim ( H , A ) || , ( lim ( H , A ) || A ) ) ) , ( lim ( H , A ) || A ) , ( lim ( H , A ) || A ) ) ) ;
assume e in { ( w1 - w2 ) / ( w1 - w2 ) : w1 in F & w2 in G } ;
reconsider d7 = dom a `1 , d8 = dom F `1 , d8 = dom G as finite set ;
LSeg ( f /^ q , j ) = LSeg ( f , j + q .. f ) .= LSeg ( f , j + q .. f ) ;
assume that X in { T . ( N2 , K1 ) : h . ( N2 , K1 ) = N2 } ;
assume that Hom ( d , c ) <> {} and <* f , g *> * f1 = <* f , g *> * f2 ;
dom Sb = dom S /\ Seg n .= dom Lb .= Seg n /\ Seg n .= dom Lb .= Seg n /\ Seg n .= dom ( S | Seg n ) ;
x in H |^ a implies ex g st x = g |^ a & g in H |^ a ;
* ( a , 1 ) = a `2 - ( 0 * n ) .= a `2 - ( 0 * n ) .= a `2 ;
D2 . ( j - 1 ) in { r : lower_bound A <= r & r <= D1 . i } ;
ex p being Point of TOP-REAL 2 st p = x & P [ p ] & p `2 >= 0 ;
for c holds f . c <= g . c implies f @ c= g @ c
dom ( f1 (#) f2 ) /\ X c= dom ( f1 (#) f2 ) /\ X .= dom ( f1 (#) f2 ) /\ X .= dom ( f1 (#) f2 ) ;
1 = ( p * p ) * p .= p * ( p * p ) .= p * 1 .= p * 1 ;
len g = len f + len <* x + y *> .= len f + 1 .= len f + 1 .= len f + 1 ;
dom F-11 = dom ( F | [: N1 , { x } :] ) .= [: the carrier of S , the carrier of S :] ;
dom ( f . t * I . t ) = dom ( f . t * g . t ) .= dom ( f . t ) ;
assume a in ( "\/" ( ( T |^ the carrier of S ) , F ) ) .: D ;
assume that g is one-to-one and ( the carrier' of S ) /\ rng g c= dom g and g is one-to-one and g is one-to-one ;
( ( x \ y ) \ z ) \ ( ( x \ z ) \ ( y \ z ) ) = 0. X ;
consider f such that f * f `1 = id b and f * f `2 = id a and f is one-to-one and f is one-to-one ;
( cos | [. 2 * PI * 0 , PI + ( 2 * PI * 0 ) ) .] ) is increasing ;
Index ( p , co ) <= len LS - Gij .. LS -' 1 & Index ( Gij , LS ) + 1 - Index ( Gij , LS ) ;
let t1 , t2 , t3 be Element of ( T . NAT ) * , s be Element of ( T . NAT ) * ;
"/\" ( ( Frege ( curry H ) ) . h , L ) <= "/\" ( ( Frege ( curry G ) ) . h , L ) ;
then P [ f . i0 , f . ( i0 + 1 ) , j ] & F ( i0 + 1 ) . i0 = j ;
Q [ [ D . x , 1 ] , F . [ D . x , 1 ] , F . [ x , 1 ] ] ;
consider x being element such that x in dom ( F . s ) and y = F . s . x ;
l . i < r . i & [ l . i , r . i ] is for of G . i ;
the Sorts of A2 = ( the carrier of S2 ) --> ( the carrier of S2 ) .= ( the carrier of S2 ) --> ( the carrier of S2 ) ;
consider s being Function such that s is one-to-one and dom s = NAT and rng s = F and for n being Nat st n in NAT holds s . n = F ( n ) ;
dist ( b1 , b2 ) <= dist ( b1 , a ) + dist ( a , b2 ) + dist ( a , b2 ) ;
( Lower_Seq ( C , n ) /. len Lower_Seq ( C , n ) ) /. len Lower_Seq ( C , n ) = Wq ;
q `2 <= ( UMP Upper_Arc L~ Cage ( C , 1 ) ) `2 & ( UMP L~ Cage ( C , 1 ) ) `2 <= ( UMP L~ Cage ( C , 1 ) ) `2 ;
LSeg ( f | i2 , i ) /\ LSeg ( f | i2 , j ) = {} ;
given a being ExtReal such that a <= Ia and A = ]. a , Ia .[ and a < Ia ;
consider a , b be complex number such that z = a & y = b and z + y = a + b ;
set X = { b |^ n where n is Element of NAT : n <= m & b |^ n in B } ;
( ( x * y * z \ x ) \ z ) \ ( x * y \ x ) = 0. X ;
set xy = [ <* xy , y *> , f1 ] , yz = [ <* y , z *> , f2 ] , zx = [ <* z , x *> , f3 ] , zx = [ <* x , y *> , f3 ] ;
Up /. len lp = Up . ( len lp ) .= lp . ( len lp ) .= lp . 1 ;
( ( q `2 / |. q .| - sn ) ) / ( 1 + sn ) = 1 ;
( ( p `2 / |. p .| - sn ) / ( 1 - sn ) ) < 1 ;
( ( ( S \/ Y ) /\ X ) /\ Y ) `2 = N-bound ( X \/ Y ) .= ( ( S \/ Y ) /\ X ) `2 ;
( ( seq - seq ) . k ) . k = ( seq . k - seq . k ) . k .= ( seq . k - seq . k ) . k ;
rng ( ( h + c ) ^\ n ) c= dom SVF1 ( 1 , f , u0 ) /\ dom SVF1 ( 1 , f , u0 ) ;
the carrier of X = the carrier of X0 & the carrier of X0 = the carrier of X0 & the carrier of X0 = the carrier of X0 ;
ex p4 st p3 = p4 & |. p4 - |[ a , b ]| .| = r & |. p4 - |[ a , b ]| .| = r ;
set ch = chi ( X , A ) , ch = chi ( X , A ) , ch = chi ( X , A ) ;
R |^ ( 0 * n ) = I\HM ( X , X ) .= R |^ n |^ 0 .= R |^ 0 ;
( ( ( curry ( F , n ) ) . n ) . x ) . x is nonnegative & ( ( curry ( F , n ) . m ) . x ) . x = +infty ;
f2 = C7 . ( E7 , len ( E7 , len ( K , len ( K , n , len ( K , n , len ( K , n , len ( K , n , len ( K , n , len ( K , n , len ( K , n , len ( K , n , len ( K , n ) ) ) ) ) ) ) ) ) ;
S1 . b = s1 . b .= S2 . b .= S2 . b .= S2 . b .= S2 . b .= S2 . b ;
p2 in LSeg ( p2 , p1 ) /\ LSeg ( p1 , p10 ) /\ LSeg ( p1 , p10 ) .= { p2 , p1 } ;
dom ( f . t ) = Seg n & dom ( I . t ) = Seg n & rng ( I . t ) = Seg n ;
assume o = ( the connectives of S ) . 11 & the connectives of S = ( the connectives of S ) . 11 ;
set phi = ( l1 , l2 ) support phi , phi = ( l1 , l2 ) . ( l2 , l2 ) ;
synonym p is is is is is invertible for ( p , T ) *' = 1 implies p = 0. L ;
Y1 `2 = - 1 & 0. TOP-REAL 2 <> 0. TOP-REAL 2 & ( for p being Point of TOP-REAL 2 st p in Y1 holds p `2 >= 0 ) implies Y1 is closed & ( p <> 0. TOP-REAL 2 implies Y1 is closed )
defpred X [ Nat , set , set , set ] means P [ $1 , $2 , , , , , , , , , ] ;
consider k being Nat such that for n being Nat st k <= n holds s . n < x0 + g and x0 < x0 + g ;
Det ( I |^ ( m -' n ) ) ~ = 1. K & Det ( I |^ ( m -' n ) ) = 1. K ;
( - b - sqrt ( b * a * c ) ) / ( 2 * a * c ) < 0 ;
CC . d = CC . d mod CC . d .= CC . d mod CC . d .= CC . d mod C . d ;
attr X1 is dense means : : : X1 is dense & X2 is dense & X1 is dense implies X1 meet X2 is dense SubSpace of X1 ;
deffunc F6 ( Element of E , Element of I ) = $1 * $2 + ( $1 * $2 ) * ( $2 ) ;
t ^ <* n *> in { t ^ <* i *> : Q [ i , T . t ] } ;
( x \ y ) \ x = ( x \ x ) \ y .= y ` \ 0. X .= 0. X ;
for X being non empty set for Y being Subset-Family of X holds X is Basis of product <* X , UniCl Y *>
synonym A , B are_separated means : for A , B being Subset of X st A misses B & A misses B & B misses A & B misses B ;
len ( ( - p ) * ( - p ) ) = len p & width ( - p ) * ( - p ) = width ( - p ) ;
J . v = { x where x is Element of K : 0 < v . x & x < 1 } ;
( Sgm ( support m ) ) . d - ( Sgm ( support m ) ) . e <> 0 ;
lower_bound divset ( D2 , k + k2 ) = D2 . ( k + k2 - 1 ) .= D2 . ( k + k2 - 1 ) ;
g . r1 = - 2 * r1 + 1 & dom h = [. 0 , 1 .] & rng h c= dom ( g | [. 0 , 1 .] ) ;
|. a .| * ||. f .|| = 0 * ||. f .|| .= ||. a * f .|| .= ||. a * f .|| .= ||. a * f .|| ;
f . x = ( h . x ) `1 & g . x = ( h . x ) `2 & h . y = ( h . y ) `2 ;
ex w st w in dom B1 & <* 1 *> ^ s = <* 1 *> ^ w & <* 1 *> ^ s = <* 1 *> ^ w ;
[ 1 , {} , <* d1 *> ] in ( { [ 0 , {} , {} ] } \/ S1 ) \/ S2 ;
IC Exec ( i , s1 ) + n = IC Exec ( i , s2 ) .= IC Exec ( i , s2 ) .= ( 0 + n ) ;
IC Comput ( P , s , 1 ) = IC ( s , 9 ) .= 5 .= 5 + 9 .= 5 ;
( IExec ( W6 , Q , t ) ) . intpos ( e + 1 ) = t . intpos ( e + 1 ) .= t . intpos ( e + 1 ) ;
LSeg ( f /^ q , i ) misses LSeg ( f /^ q , j ) \/ LSeg ( f /^ q , j ) ;
assume for x , y being Element of L st x in C holds x <= y or y <= x or y <= x ;
integral ( f , C , f ) = f . ( upper_bound C ) - f . ( lower_bound C ) .= f . ( lower_bound C ) - f . ( lower_bound C ) ;
for F , G being one-to-one FinSequence st rng F misses rng G holds F ^ G is one-to-one & F ^ G is one-to-one & F ^ G is one-to-one
||. R /. ( L . h ) - R /. ( L . h ) .|| < e1 * ( K + 1 * ||. h .|| ) ;
assume a in { q where q is Element of M : dist ( z , q ) <= r } ;
set p4 = [ 2 , 1 ] .--> [ 2 , 0 , 1 , 0 ] ;
consider x , y being Subset of X such that [ x , y ] in F and x c= d and y \not c= d ;
for y , x being Element of REAL st y ` in Y & x in X ` holds y <= x ` & y <= x ` ;
func |. p \bullet -> variable of A , A equals min ( NBI , p ) .= min ( NBI , p ) ;
consider t being Element of S such that x `1 , y `2 '||' z `1 , t `2 and x `2 , z `2 '||' y `2 , t `2 ;
dom x1 = Seg ( len x1 ) & len x1 = len l1 & for i st i in Seg ( len x1 ) holds x1 . i = ( x1 /. i ) . ( len x1 ) ;
consider y2 being Real such that x2 = y2 and 0 <= y2 and y2 <= 1 / 2 and y2 <= 1 / 2 ;
||. f | X /* s1 .|| = ||. f | X .|| | X .= ( f | X ) /* s1 .= ( f | X ) /* s1 ;
( the InternalRel of A ) ` /\ Y = {} \/ {} .= {} \/ {} .= {} .= {} ;
assume that i in dom p and for j being Nat st j in dom q holds P [ i , j ] and i + 1 in dom p and i + 1 in dom q and q . i = q . j ;
reconsider h = f | X ( ) as Function of X ( ) , rng f ( ) , rng f ( ) ;
u1 in the carrier of W1 & u2 in the carrier of W2 implies ( for v being Element of V st v in the carrier of W1 holds v1 = v ) & ( v = w implies u1 = u2 )
defpred P [ Element of L ] means M <= f . $1 & f . $1 <= f . $1 & f . $1 <= f . $1 ;
l . ( u , a , v ) = s * x + ( - ( s * x ) + y ) .= b ;
- ( x-y ) = - x + - ( - y ) .= - x + - y .= - x + y .= y + y ;
given a being Point of GX such that for x being Point of GX holds a , x , x , a is_collinear and a , x , x is_collinear ;
fSet = [ [ dom @ f2 , cod f2 ] , h2 = [ cod @ f2 , cod f2 ] , h2 = [ cod f2 , cod f2 ] ;
for k , n being Nat st k <> 0 & k < n & k is prime holds k , n are_relative_prime & k , n are_relative_prime implies k |^ n divides k |^ n
for x being element holds x in A |^ d iff x in ( ( A ` ) |^ d ) ` & x in A ` ;
consider u , v being Element of R , a being Element of A such that l /. i = u * a * v ;
( ( - ( p `1 / |. p .| - cn ) ) / ( 1 + cn ) ) ^2 > 0 ;
L-13 . k = Lw . k & F . k in dom ( L . k ) & F . k = L . k ;
set i2 = AddTo ( a , i , - n ) , i1 = goto ( n + 1 ) , i2 = goto ( n + 1 ) , i2 = goto ( n + 1 ) ;
attr B is thesis means : : : for S being SubSubnot set holds ( for B being Element of S holds S is B ) & ( B is finite implies S is finite ) ;
a9 "/\" D = { a "/\" d where d is Element of N : d in D } .= { a "/\" d where d is Element of N : d in D } ;
|( \square , ( q - q9 ) * |( \square , q - q )| )| >= |( \square , ( q - q ) * ( b - q ) )| ;
( - f ) . sup A = ( ( - f ) | A ) . sup A .= ( ( - f ) | A ) . sup A .= ( ( - f ) | A ) . sup A ;
Gij `1 = G * ( len G , k ) `1 .= G * ( len G , k ) `1 .= G * ( len G , k ) `1 .= G * ( len G , k ) `1 ;
( Proj ( i , n ) ) . LM = <* ( proj ( i , n ) ) . LM *> .= <* ( proj ( i , n ) ) . LM *> ;
f1 + f2 * reproj ( i , x ) is_differentiable_in ( ( the reproj of i , x ) . i ) . x ;
pred ( for x st x in Z holds tan . x <> 0 ) & ( for x st x in Z holds tan . x = tan . x ) & ( for x st x in Z holds tan . x = 1 ) implies tan is_differentiable_on Z & for x st x in Z holds tan . x = 1 & tan . x = 1 ;
ex t being SortSymbol of S st t = s & h1 . t . x = h2 . t . x & x in ( the Sorts of A ) . s ;
defpred C [ Nat ] means P8 . $1 is non empty & [: A , B :] is n -[: A , B :] & [: A , B :] is n -[: A , B :] ;
consider y being element such that y in dom ( p . i ) and ( q . i ) . y = ( p . i ) . y ;
reconsider L = product ( { x1 } +* ( index B , l ) ) as Subset of ( product A ) . ( index B ) ;
for c being Element of C ex d being Element of D st T . ( id c ) = id d & for c being Element of C st c in dom T holds T . c = id d
not ( f , n , p ) = ( f | n ) ^ <* p *> .= f ^ <* p *> .= f ^ <* p *> ;
( f (#) g ) . x = f . ( g . x ) & ( f (#) h ) . x = f . ( h . x ) ;
p in { ( 1 - 2 ) * ( G * ( i + 1 , j ) + G * ( i + 1 , j + 1 ) ) } ;
f `2 - p = ( f | ( n , L ) ) *' - ( f | ( n , L ) ) .= ( f - c ) . p ;
consider r being Real such that r in rng ( f | divset ( D , j ) ) and r < m + s ;
f1 . ( |[ r2 , r3 ]| ) in f1 .: W2 & f2 . ( |[ r2 , r3 ]| ) in f1 .: W3 ;
eval ( a | ( n , L ) , x ) = ( a | ( n , L ) ) . x .= a . x ;
z = DigA ( ty , xx ) .= DigA ( ty , xx ) .= DigA ( ty , xx ) .= DigA ( ty , xx ) .= DigA ( ty , xx ) ;
set H = { Intersect S where S is Subset-Family of X : S c= G & S is open & S is open } ;
consider S19 being Element of D * , d being Element of D * such that S ` = S19 ^ <* d *> and S = S19 ^ <* d *> ;
assume that x1 in dom f and x2 in dom f and f . x1 = f . x2 and f . x2 = f . x2 ;
- 1 <= ( ( q `2 / |. q .| - sn ) ) / ( 1 + sn ) & - 1 <= ( q `2 / |. q .| - sn ) / ( 1 + sn ) ;
0. ( V ) is Linear_Combination of A & Sum ( 0. ( V ) ) = 0. V implies Sum ( L ) = 0. ( V ) & Sum ( L ) = 0. ( V ) ;
let k1 , k2 , k2 , k2 , x4 , k2 be Instruction of SCM+FSA , a be Int-Location , k1 be Int-Location , k2 be Int-Location , k2 be Element of NAT ;
consider j being element such that j in dom a and j in g " { k ' ( i ) } and x = a . j ;
H1 . x1 c= H1 . x2 or H1 . x2 c= H1 . x1 or H1 . x2 c= H1 . x2 or H1 . x2 c= H1 . x2 ;
consider a being Real such that p = \rbrace * p1 + ( a * p2 ) and 0 <= a and a <= 1 ;
assume that a <= c & d <= b and [' a , b '] c= dom f and [' a , b '] c= dom g ;
cell ( Gauge ( C , m ) , ( X -' 1 , 0 ) ) is non empty & cell ( Gauge ( C , m ) , ( X -' 1 , 0 ) ) is non empty ;
A9 in { ( S . i ) `1 where i is Element of NAT : i in dom ( S . i ) `1 } ;
( T * b1 ) . y = L * b2 /. y .= ( F /. y ) . y .= ( F /. y ) . y .= ( F /. y ) . y ;
g . ( s , I ) . x = s . y & g . ( s , I ) . y = |. s . x - s . y .| ;
( log ( 2 , k + k ) ) ^2 >= ( log ( 2 , k + 1 ) ) ^2 / ( ( log ( 2 , k + 1 ) ) ^2 ) ) ^2 ;
then p => q in S & not x in the still of p & not p => All ( x , q ) in S ;
dom ( the InitS of r-10 ) misses dom ( the InitS of r-11 ) & dom ( the InitS of r-11 ) = dom ( the InitS of r-11 ) ;
synonym f is integer means : Def2 : for x being set st x in rng f holds x is integer ;
assume for a being Element of D holds f . { a } = a & for X being Subset-Family of D holds f . ( f .: X ) = f . union X ;
i = len p1 .= len p3 + len <* x *> .= len p3 + len <* x *> .= len p3 + 1 .= len p3 + 1 .= len p3 + 1 ;
l * ( l , 3 ) = ( g /. 1 , 3 ) + ( k * ( l , 3 ) ) - ( k * ( l , 3 ) ) .= ( k * l ) - ( k * l ) ;
CurInstr ( P2 , Comput ( P2 , s2 , l2 ) ) = halt SCM+FSA .= halt SCM+FSA .= halt SCM+FSA .= halt SCM+FSA ;
assume for n be Nat holds ||. seq .|| . n <= ( R . n ) & ( R . n ) is summable & ( R . n ) is summable ) ;
sin . \vert = sin r * cos ( ( - cos r ) * sin s ) .= 0 * sin ( ( - sin r ) * sin s ) .= 0 ;
set q = |[ g1 . t0 , g2 . t0 , g3 . t0 ]| , r = |[ g2 . t0 , g2 . t0 ]| , s = |[ g2 . t0 , g2 . t0 ]| ;
consider G be sequence of S such that for n being Element of NAT holds G . n in implies G is implies for n holds G . n in implies G is \overline { F . n } ;
consider G such that F = G and ex G1 st G1 in SM & G = ( X \/ G1 ) /\ ( X \/ G1 ) ;
the root of [ x , s ] in ( ( the Sorts of Free ( C , X ) ) * ( the Arity of S ) ) . s ;
Z c= dom ( exp_R * ( f + ( #Z 3 ) * f1 ) ) & Z c= dom ( ( #Z 3 ) * f1 ) ;
for k be Element of NAT holds seq1 . k = ( ( sum ( f , S ) ) . k ) * ( ( T . k ) . n ) ;
assume that - 1 < n and q `2 > 0 and ( q `1 / |. q .| - sn ) < 0 and ( q `2 / |. q .| - sn ) < 0 ;
assume that f is continuous and a < b and c < d and f = g and f . a = c and f . b = d and f . c = d ;
consider r being Element of NAT such that sy, r , s , r , s , t being Element of NAT such that sy, s , t , r , s and r <= q ;
LE f /. ( i + 1 ) , f /. j , L~ f , f /. ( len f ) , f /. ( len f ) ;
assume that x in the carrier of K and y in the carrier of K and ex_inf_of { x , y } , L and inf { x , y } in L ;
assume f +* ( i1 , \xi ) . 1 in ( proj ( F , i2 ) " ( A . ( i1 + 1 ) ) ) " ( A . ( i1 + 1 ) ) ) ;
rng ( ( Flow M ) ~ | ( the carrier of M ) ) c= the carrier' of M & rng ( ( Flow M ) ~ | ( the carrier of M ) ) c= the carrier' of M ;
assume z in { ( the carrier of G ) \ { t } where t is Element of T : t in F } ;
consider l be Nat such that for m be Nat st l <= m holds ||. ( s1 . m - x0 ) - ( lim s1 ) .|| < g ;
consider t be VECTOR of product G such that mt = ||. D5 . t .|| and ||. t .|| <= 1 ;
assume that the degree degree of v = 2 and v ^ <* 0 *> , v ^ <* 1 *> ^ <* 1 *> in dom p and v ^ <* 1 *> in dom p ;
consider a being Element of the Points of Ximplies a on A & not a on B & not a on B ;
( - x ) |^ ( k + 1 ) * ( ( - x ) |^ ( k + 1 ) ) " = 1 ;
for D being set for i st i in dom p holds p . i in D & p . i is FinSequence of D implies p is FinSequence of D
defpred R [ element ] means ex x , y st [ x , y ] = $1 & P [ x , y ] & P [ x , y ] ;
L~ f2 = union { LSeg ( p0 , p10 ) , LSeg ( p10 , p1 ) , LSeg ( p1 , p10 ) } .= { p1 , p10 } \/ { p1 , p10 } ;
i -' len h11 + 2 - 1 < i -' len h11 + 2 - 1 + 1 + 1 - 1 + 1 + 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1 .= i - len h11 + 1 ;
for n being Element of NAT st n in dom F holds F . n = |. ( nthesis . ( n -' 1 ) ) . x .| ;
for r , s1 , s2 , s3 holds r in [. s1 , s2 .] iff s1 <= s2 & s2 <= s3 & s1 <= s2 & s2 <= s3 & s3 <= s2
assume v in { G where G is Subset of T2 : G in B2 & G c= z1 & G c= z2 & G c= z1 } ;
let g be \vert \vert Element of INT , X be Element of INT , b be Element of INT , b be Element of INT , c be Element of INT ;
min ( g . [ x , y ] , k ) . [ y , z ] = ( min ( g , k , x , z ) ) . y ;
consider q1 be sequence of CH such that for n holds P [ n , q1 . n ] and for n holds P [ n , q1 . n ] ;
consider f being Function such that dom f = NAT & for n being Element of NAT holds f . n = F ( n ) and for n being Element of NAT holds f . n = F ( n ) ;
reconsider B-6 = B /\ B , O= O , Od = I , Bd = I as Subset of B ;
consider j being Element of NAT such that x = ( the ` of n ) \ { j } and 1 <= j and j <= n ;
consider x such that z = x and card ( x . O2 ) in card ( x . O ) and x in L1 and x in L2 and x in L1 and x in L2 ;
( C * ( k , n2 ) ) . 0 = C . ( ( ( T . k ) , n2 ) . 0 ) .= C . ( ( T . k ) , n2 ) . 0 ) ;
dom ( X --> rng f ) = X & dom ( ( X --> f ) . x ) = dom ( X --> f . x ) ;
N-bound L~ SpStSeq C <= ( b /. ( L~ SpStSeq C ) ) `2 & N-bound L~ SpStSeq C <= ( ( L~ SpStSeq C ) * ( i , j ) ) `2 & ( L~ SpStSeq C ) * ( i , j ) `2 <= ( ( L~ SpStSeq C ) * ( i , j ) ) `2 ;
synonym x , y are_collinear means : : : ex l being Subset of S st { x , y } c= l or ex l being Subset of S st { x , y } c= l ;
consider X being element such that X in dom ( f | ( n + 1 ) ) and ( f | ( n + 1 ) ) . X = Y ;
assume that for k , x , y being Element of L for a , b being Element of Image k st a = x & b = y holds x << y iff x << y & y << a ;
( 1 / 2 * ( ( ( ( ( 1 / 2 ) * ( ( #Z 2 ) * ( AffineMap ( n , 0 ) ) ) ) ) ) ) ) ) is_differentiable_on REAL ;
defpred P [ Element of omega ] means ( for n holds ( ( for m st n <= $1 holds ( m <= $1 ) implies ( $1 <= n implies ( $1 = m ) ) ) & ( $1 <= n implies ( $1 = m implies $1 = n ) ) ;
IC Comput ( P , s , 2 ) = succ IC Comput ( P , s , 1 ) .= 6 + 1 .= 6 + 1 .= 6 ;
f . x = f . g1 * f . g2 .= f . g1 * 1_ H .= f . g1 * 1_ H .= f . g1 * ( g . g2 ) .= f . g1 * ( g . g2 ) .= f . g1 * ( g . g2 ) ;
( M * ( F . n ) ) . n = M . ( ( ( canFS Omega ) . n ) . n ) .= M . ( { ( ( canFS Omega ) . n ) . n } ) ;
the carrier of L1 + L2 c= ( the carrier of L1 ) \/ ( the carrier of L2 ) & the carrier of L1 + L2 c= the carrier of L1 & the carrier of L1 + L2 c= the carrier of L2 ;
pred a , b , c , x , y , c , x , y , c , x , y , c , x , y , c , x , y , c , x , y , c , x , y , c , x , y , c , x , y , c , x , y , c , x , y , c , x , y , c , x , y , x , c , x , y , c , x , y , x , y , c , x , y , c , x
( the partial of s ) . n <= ( the partial of s ) . n * s . ( n + 1 ) & ( the Sorts of s ) . ( n + 1 ) <= ( the Sorts of s ) . n ;
pred - 1 <= r & r <= 1 & ( arccot r ) . r = - 1 & ( arccot r ) . r = - 1 & ( arccot r ) . r = 1 ;
seq in { p ^ <* n *> where n is Nat : p ^ <* n *> in T1 } & seq in T1 implies ex n st p = <* n *> ^ <* n *> ^ <* n *> ;
|[ x1 , x2 , x3 ]| . 2 - |[ y1 , y2 , x3 ]| . 2 - |[ y2 , x3 , x4 ]| . 2 = x2 - y2 - x3 - x3 , x4 - x1 , x4 - x2 , x4 - x1 , x4 - x2 - x3 ]| . 2 ;
attr for m be Nat holds F . m is nonnegative means : : for n be Nat holds ( Partial_Sums ( F ) . n ) . m is nonnegative ;
len ( ( G . z ) . ( x , z ) ) = len ( ( ( G . ( xx , z ) ) + ( ( G . ( xx , y ) ) . ( x , y ) ) ) ) .= len ( G . ( xx , y ) ) ;
consider u , v being VECTOR of V such that x = u + v and u in W1 /\ W2 and v in W3 /\ W3 and u in W2 /\ W3 ;
given F be FinSequence of NAT such that F = x and dom F = n and rng F c= { 0 , 1 } and Sum F = k and for k be Nat st k in n holds F . k = k ;
0 = ( 1 * 0 ) * u\hbox = ( ( - 1 ) * ( - 1 ) ) * ( ( - 1 ) * ( - 1 ) ) ;
consider n be Nat such that for m be Nat st n <= m holds |. ( f # x ) . m - lim ( f # x ) .| < e ;
cluster -> being } for Boolean non empty Poset , ( ( ( ( ( ( let L ) | 1 ) ) | 1 ) , ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( L ) | 1 ) ) ) | 1 ) ) ) | 1 ) ) ) ) ) ) is Boolean ;
"/\" ( BB , {} ) = Top BB .= Top the carrier of S .= "/\" ( BB , [#] S ) .= "/\" ( I , [#] S ) .= "/\" ( I , T ) .= "/\" ( I , T ) ;
( r / 2 ) ^2 + ( r / 2 ) ^2 <= ( r / 2 ) ^2 + ( r / 2 ) ^2 + ( r / 2 ) ^2 ;
for x be element st x in A /\ dom ( f `| X ) holds ( f `| X ) . x >= r2 & ( f `| X ) . x >= r2 ;
2 * r1 - c * |[ a , c ]| - ( 2 * r1 - c * |[ b , c ]| ) = 0. TOP-REAL 2 - ( 2 * r1 - c * |[ b , c ]| ) ;
reconsider p = P * ( \square , 1 ) , q = a " * ( ( - ( - ( K , n , 1 ) ) ) * ( ( - ( K , n , 1 ) ) * ( ( - ( K , n , 1 ) ) ) ) ) as FinSequence of K ;
consider x1 , x2 being element such that x1 in uparrow s and x2 in < t and x = [ x1 , x2 ] and [ x2 , x3 ] in R and [ x1 , x2 ] in R ;
for n be Nat st 1 <= n & n <= len q1 holds q1 . n = ( ( upper_volume ( g , M7 ) ) | Seg n ) . ( n + 1 ) & ( upper_volume ( g , M7 ) ) . n = ( ( upper_volume ( g , M7 ) ) | Seg n ) . n ;
consider y , z being element such that y in the carrier of A and z in the carrier of A and i = [ y , z ] and i = [ y , z ] ;
given H1 , H2 being strict Subgroup of G such that x = H1 and y = H2 and H1 is Subgroup of H2 and H2 is Subgroup of H1 and H2 is Subgroup of H2 ;
for S , T being non empty RelStr , d being Function of T , S st T is complete holds d is directed-sups-preserving & d is monotone & d is monotone & d is monotone
[ a + 0. F_Complex , b2 ] in ( the carrier of F_Complex ) & [ a + 0. F_Complex , b2 + 0. F_Complex ] in [: the carrier of F_Complex , the carrier of F_Complex :] ;
reconsider mm = max ( len ( F1 . n ) , len ( p . n ) * ( x |^ n ) ) as Element of NAT ;
I <= width GoB ( ( GoB ( h ) ) * ( len GoB ( h ) , width GoB ( h ) , width GoB ( h ) ) ) , width GoB ( h ) ) ;
f2 /* q = ( f2 /* ( f1 /* s ) ) ^\ k .= ( f2 * f1 ) /* s .= ( ( f2 * f1 ) /* s ) ^\ k .= ( ( f2 * f1 ) /* s ) ^\ k ;
attr A1 \/ A2 is linearly-independent means : : : A1 : A1 misses A2 & ( for x st x in A1 holds Lin ( A1 , x ) /\ Lin ( A2 , x ) ) = Lin ( A1 , x ) ) & Lin ( A1 , x ) = Lin ( A2 , x ) ;
func A -carrier C -> set equals union { A . s where s is Element of R : s in C & s in C } ;
dom ( Line ( v , i + 1 ) (#) ( ( -> Matrix of m , n ) * ( i , 1 ) ) ) = dom ( F ^ <* i , 1 *> ) .= dom ( F ^ <* i , 1 *> ) ;
cluster [ x `1 , 4 , x `2 ] , [ x `1 , 4 ] , [ x `1 , 4 ] , [ x `1 , 4 ] ] , [ x `1 , 4 ] , [ x `1 , 4 ] ] , [ x `1 , 4 ] , [ x `1 , 4 ] ] , [ x `1 , 4 ] ] ;
E , All ( x1 , All ( x2 , x2 ) '&' ( x2 , x1 ) '&' ( x1 , x0 ) '&' ( x1 , x0 ) '&' ( x2 , x1 ) ) ) |= x1 ;
F .: ( id X , g ) . x = F . ( id X , g . x ) .= F . ( x , g . x ) .= F . ( x , g . x ) .= F . ( x , g . x ) ;
R . ( h . m ) = F . ( x0 + h . m ) - ( h . m ) - ( h . m ) + ( h . m ) - ( h . m ) ;
cell ( G , Xs -' 1 , ( Y + 1 ) \ ( t + 1 ) ) \ L~ f meets ( UBD L~ f ) \ ( L~ f ) ;
IC Result ( P2 , s2 ) = IC IExec ( I , P , Initialize s ) .= card I .= card I .= card I .= card I + ( card I + 2 ) .= card I + ( card I + 2 ) .= card I + 2 ;
sqrt ( ( - ( ( - ( q `1 / |. q .| - cn ) ) / ( 1 - cn ) ) ^2 ) ) > 0 ;
consider x0 being element such that x0 in dom a and x0 in g " { k ' ( i ) } and y0 = a . x0 and x0 in { k ' ( i ) } and x0 in { k ' ( i ) } ;
dom ( r1 (#) chi ( A , C ) , C ) = dom chi ( A , C ) /\ dom chi ( A , C ) .= C /\ dom chi ( A , C ) .= C /\ dom ( ( r1 (#) chi ( A , C ) ) , C ) .= C /\ dom ( ( r1 (#) chi ( A , C ) ) , C ) ;
d-7 . [ y , z ] = ( ( y - z ) `2 - ( y - z ) `2 ) * ( y - z ) .= ( ( y - z ) `2 - ( y - z ) `2 ) * ( y - z ) ;
attr for i being Nat holds C . i = A . i /\ B . i implies L~ C c= ( A /\ B ) /\ ( A /\ C ) ;
assume that x0 in dom f and f is_continuous_in x0 and ||. f .|| is_continuous_in x0 and for r st 0 < r ex g st g < r & g < x0 & g in dom f and for g st g in dom f /\ dom f holds f /. g <> 0 ;
p in Cl A implies for K being Basis of p , Q being Basis of T st Q in K holds A meets Q & A meets Q implies P meets Q
for x be Element of REAL n st x in Line ( x1 , x2 ) holds |. y1 - y2 .| <= |. y1 - y2 .| & |. y2 - x .| <= |. y1 - y2 .| ;
func Sum <*> a -> Ordinal means : : : : a in it & for b being Ordinal st a in it holds it c= b ;
[ a1 , a2 , a3 ] in [: the carrier of A , the carrier of A :] & [ a1 , a2 , a3 ] in [: the carrier of A , the carrier of A :] ;
ex a , b being element st a in the carrier of S1 & b in the carrier of S2 & x = [ a , b ] & x = [ a , b ] ;
||. ( vseq . n ) - ( vseq . m ) .|| * ||. x - x0 .|| < ( e * ||. x - x0 .|| ) * ||. x - x0 .|| ;
then for Z being set st Z in { Y where Y is Element of I7 : F c= Y & Y in Z } holds z in x & z in Z ;
sup compactbelow [ s , t ] = [ sup ( ( compactbelow s ) . [ s , t ] ) , sup ( ( compactbelow s ) . [ s , t ] ) ) , sup ( ( compactbelow s ) . [ s , t ] ) ] ;
consider i , j being Element of NAT such that i < j and [ y , f . j ] in IH and [ f . i , z ] in IH and [ f . i , f . j ] in IH ;
for D being non empty set , p , q being FinSequence of D st p c= q ex p being FinSequence of D st p ^ q = q & p ^ q = q ^ p
consider e19 being Element of the affine of X such that c9 , a9 // a9 , e and a9 <> c9 and a9 <> c9 and a9 <> c9 and a9 <> c9 and a9 <> c9 and a9 <> c9 and a9 <> c9 & a9 <> c9 & a9 <> c9 & a9 <> c9 & a9 <> c9 & a9 <> c9 & a9 <> c9 & a9 <> c9 ;
set U2 = I \! \mathop { {} } , * = I \! \mathop { {} } ;
|. q3 .| ^2 = ( |. q3 .| ) ^2 + ( ( |. q3 .| ) ^2 + ( |. q2 .| ) ^2 ) .= |. q .| ^2 + ( ( |. q .| ) ^2 + ( |. q .| ) ^2 ) .= |. q .| ^2 ;
for T being non empty TopSpace , x , y being Element of [: the topology of T , the topology of T :] holds x "\/" y = x \/ y implies x "/\" y = x /\ y & x "/\" y = x /\ y
dom signature ( U1 ) = dom ( the charact of MSAlg U1 ) & Args ( o , MSAlg U1 ) = dom ( the charact of MSAlg U1 ) & Args ( o , MSAlg U1 ) = dom ( the charact of MSAlg U1 ) ;
dom ( h | X ) = dom h /\ X .= dom ( ( ||. h .|| ) | X ) .= dom ( ( ||. h .|| ) | X ) .= dom ( ( ||. h .|| ) | X ) .= dom ( ( ||. h .|| ) | X ) .= dom ( ( |. h .| ) | X ) .= X ;
for N1 , N1 being Element of ( the carrier of G ) * , N being Element of ( the carrier of G ) * st dom ( h . K1 ) = N & rng ( h . K1 ) = N1 & rng ( h . K1 ) c= N1 holds N = N1
( mod ( u , m ) + mod ( v , m ) ) . i = ( mod ( u , m ) . i ) + ( mod ( v , m ) . i ) .= ( mod ( v , m ) . i ) + ( mod ( v , m ) . i ) ;
- ( q `1 ) < - 1 or q `2 >= - q `1 & - ( q `2 ) >= - 1 & q `2 <= 1 or q `1 >= - 1 & q `2 <= 1 or q `1 >= - 1 & q `2 <= 1 ;
attr r1 = ff & r2 = ff & r1 = ff & r2 = ff & for i st i in dom ff holds r1 * ( i , j ) = ff . i * ( i , j ) ;
vseq . m is bounded Function of X , the carrier of Y & x9 . m = ( ( ( vseq . m ) , X , Y ) --> x ) . m & x9 . m = ( ( ( vseq . m ) , X , Y ) --> x ) . m ;
pred a <> b & b <> c & angle ( a , b , c ) = PI & angle ( b , c , a ) = 0 implies angle ( c , a , b ) = 0 & angle ( c , a , b ) = 0 ;
consider i , j , r being Nat such that p1 = [ i , r ] and p2 = [ j , s ] and i < j and r < s and s < j ;
|. p .| ^2 - ( 2 * |( p , q )| ) ^2 + |. q .| ^2 = |. p .| ^2 + |. q .| ^2 - ( 2 * |( p , q )| ) ^2 ;
consider p1 , q1 being Element of [: X ( ) , Y ( ) :] such that y = p1 ^ q1 and q1 = p1 ^ q1 and p1 ^ q1 = q1 ^ q1 and p1 ^ q1 = q1 ^ q1 and q1 = q1 ^ q1 ;
( ( A , r1 , r2 , s1 , s2 , s2 ) , ( A , s2 , s2 ) ) = ( s2 , s2 , s2 ) ) . ( ( A , s1 , s2 ) , ( A , s2 , s2 ) ) . ( ( A , s2 , s1 ) , s2 ) ;
( ( LMP A ) `2 = lower_bound ( proj2 .: ( A /\ Vertical_Line w ) ) ) & proj2 .: ( A /\ Vertical_Line w ) is non empty & proj2 .: ( A /\ Vertical_Line w ) is non empty ;
s |= ( k , ( k , 1 ) \bf ( s , ( k , 1 ) ) \bf ( s , ( k , 1 ) ) \bf ( s , ( k , 1 ) ) \bf ( s , ( k , 1 ) ) \bf ( s , ( k , 1 ) ) ) ;
len ( s + 1 ) = card support b1 + 1 .= card support b2 + 1 .= card support b2 + 1 .= card support b2 + 1 .= len ( s + 1 ) + 1 .= len s + 1 .= len s + 1 ;
consider z being Element of L1 such that z >= x and z >= y and for z being Element of L1 st z >= x & z `1 >= y holds z `2 >= y and z `1 >= y and z `2 >= z `2 ;
LSeg ( UMP D , |[ ( W-bound D + E-bound D ) / 2 , ( N + ( E-bound D ) / 2 ) / 2 ]| ) /\ D = { UMP D , ( ( /\ D ) / 2 ) / 2 } ;
lim ( ( ( f `| N ) / g ) /* b ) = ( lim ( ( f `| N ) / g ) /* b ) .= lim ( ( f `| N ) / g ) /\ ( ( f `| N ) / g ) /* b ) ;
P [ i , pr1 ( f ) . i , pr1 ( f ) . i , pr1 ( f ) . ( i + 1 ) , pr1 ( f ) . ( i + 1 ) ] ;
for r be Real st 0 < r ex m be Nat st for k be Nat st m <= k holds ||. ( ( seq . k ) - ( R /* s ) ) . k - ( R /* s ) . k .|| < r
for X being set , P being a_partition of X , x , a , b being set st x in a & a in P & x in P & b in P & x <> a & x in P holds a = b
Z c= dom ( ( ( #Z n ) * f ) \ ( ( #Z n ) * f ) " { 0 } ) & Z c= dom ( ( #Z n ) * f ) \ ( ( #Z n ) * f ) " { 0 } ) ;
ex j being Nat st j in dom ( l ^ <* x *> ) & j < i & y = ( l ^ <* x *> ) . j & i = 1 + len l & z = l . j & i = j + len l & j = 1 ;
for u , v being VECTOR of V , r being Real st 0 < r & u in N holds r * u + ( 1-r v ) . v in N
A , Int Cl A , Cl Int Cl A , Cl Int Cl A , Cl Cl Int Cl A , Cl Cl Int Cl A , Cl Cl Int Cl A , Cl Cl Cl Cl Int Cl A , Cl Cl Cl Cl Int Cl A , Cl Cl Cl Cl Cl Int Cl A , Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl Cl
- Sum <* v , u , w *> = - ( v + u + w ) .= - ( v + u ) + ( u + w ) .= - ( v + u ) + ( u + w ) .= - ( v + u ) + ( u + w ) ;
( Exec ( a := b , s ) ) . IC SCM R = ( Exec ( a := b , s ) ) . NAT .= Exec ( ( a := b ) , s ) . NAT .= Exec ( ( a := b ) , s ) . NAT .= Exec ( ( a , s ) := ( b , s ) ) . NAT .= s . NAT ;
consider h being Function such that f . a = h and dom h = I and for x being element st x in I holds h . x in ( the carrier of J ) \ { x } and h . x = ( the carrier of J ) \ { x } ;
for S1 , S2 , S2 being non empty reflexive RelStr , D being non empty directed Subset of [: S1 , S2 :] , f being Function of S1 , S2 , g being Function of S2 , S2 st f is directed & g is directed holds cos ( f , g ) is directed & cos ( g , f ) is directed
card X = 2 implies ex x , y st x in X & y in X & x <> y & x <> y or x = y & y = x or x = y & y = x or x = y ;
E-max L~ Cage ( C , n ) in rng ( Cage ( C , n ) :- Cage ( C , n ) ) & E-max L~ Cage ( C , n ) in rng ( Cage ( C , n ) :- Cage ( C , n ) ) ;
for T , T being tree , p , q being Element of dom T , q being Element of dom T st p divides q holds ( T , dom T ) --> ( p , q ) = T . q & ( T , dom T ) --> ( q , q ) = T . q
[ i2 + 1 , j2 ] , [ i2 + 1 , j2 ] in Indices G & f /. k = G * ( i2 + 1 , j2 ) & f /. k = G * ( i2 + 1 , j2 ) ;
cluster ( k gcd n ) divides ( k gcd n ) & n divides ( k gcd n ) & ( k divides ( k gcd n ) implies ( k divides n ) & ( k divides ( k gcd n ) ) & ( k divides ( k gcd n ) implies ( k divides n ) ) ;
dom F " = the carrier of X2 & rng F " = the carrier of X1 & F " { x } = the carrier of X2 & F " { y } = the carrier of X2 & F " { x } = the carrier of X2 ;
consider C being finite Subset of V such that C c= A and card C = n and the carrier of V = Lin ( BM \/ C ) and Lin ( BM ) = Lin ( BM \/ B ) and Lin ( BM ) = Lin ( BM \/ B ) ;
V is prime implies for X , Y being Element of [: the topology of T , the topology of T :] st X /\ Y c= V holds X c= V or Y c= V or X c= V
set X = { F ( v1 ) where v1 is Element of B ( ) : P [ v1 ] } , Y = { F ( v1 ) where v1 is Element of B ( ) : P [ v1 ] } ;
angle ( p1 , p3 , p4 ) = 0 .= angle ( p2 , p3 , p4 ) .= angle ( p2 , p3 , p4 ) .= angle ( p2 , p3 , p4 ) .= angle ( p2 , p3 , p4 ) .= angle ( p3 , p4 , p4 ) .= angle ( p2 , p3 , p4 ) ;
- sqrt ( ( - ( q `1 / |. q .| - cn ) ) ^2 / ( 1 - cn ) ^2 ) = - sqrt ( ( - ( q `1 / |. q .| - cn ) ) ^2 / ( 1 - cn ) ^2 ) .= - ( - ( q `1 / |. q .| - cn ) ) .= - 1 ;
ex f being Function of I[01] , TOP-REAL 2 st f is continuous one-to-one & rng f = P & f . 0 = p1 & f . 1 = p2 & f . 1 = p3 & f . s1 = p4 & f . s2 = p4 & f . s2 = p4 ;
attr f is partial differentiable on 2 means : Def1 : SVF1 ( 2 , pdiff1 ( f , 1 ) , u0 ) is continuous & SVF1 ( 2 , pdiff1 ( f , 1 ) , u0 ) . u0 = ( proj ( 2 , 3 ) ) . u0 ;
ex r , s st x = |[ r , s ]| & G * ( len G , 1 ) `1 < r & r < G * ( 1 , 1 ) `1 & s < G * ( 1 , 1 ) `2 & G * ( 1 , width G ) `2 < s & s < G * ( 1 , width G ) `2 ;
assume that f is_sequence_on G and 1 <= t and t <= len G and G * ( t , width G ) `2 >= N-bound L~ f and G * ( t , width G ) `2 >= N-bound L~ f and f /. k = ( GoB f ) * ( t , width G ) `2 ;
pred i in dom G means : : : for r st r (#) ( f * reproj ( i , x ) ) = r * ( reproj ( i , x ) . x ) ;
consider c1 , c2 being bag of o1 + o2 such that ( decomp c ) /. k = <* c1 , c2 *> and c /. k = c1 + c2 and c /. k = c2 /. k and c1 /. k = c2 /. k and c2 /. k = c2 /. k ;
u0 in { |[ r1 , s1 ]| : r1 < G * ( 1 , 1 ) `1 & G * ( 1 , 1 ) `2 < s1 & s1 < G * ( 1 , 1 ) `2 } ;
Cl ( X ^ Y ) . k = the carrier of X . k2 .= C4 . ( k + 1 ) .= C4 . ( k + 1 ) .= C4 . ( k + 1 ) .= C4 . ( k + 1 ) .= C4 . ( k + 1 ) ;
attr M1 = len M2 & width M1 = width M2 & M1 = M2 - M1 implies M1 = M2 - M2 & M1 = M2 - M1 & M2 = - M2 & M1 = - M2 & M1 = - M2 & M2 = - M2 ;
consider g2 be Real such that 0 < g2 and { y where y is Point of S : ||. ( - x0 ) * ( y - x0 ) - ( x0 - x0 ) * ( y - x0 ) .|| < g2 & y in N2 } c= N2 ;
assume x < ( - b + sqrt ( delta ( a , b , c ) ) ) / ( 2 * a ) or x > ( - b - sqrt ( delta ( a , b , c ) ) / ( 2 * a ) ) / ( 2 * a ) ;
( G1 '&' G2 ) . i = ( <* 3 *> ^ G1 ) . i & ( H1 '&' H2 ) . i = ( <* 3 *> ^ G1 ) . i & ( H1 '&' H2 ) . i = ( <* 3 *> ^ G1 ) . i ;
for i , j st [ i , j ] in Indices M3 holds ( M3 + M1 ) * ( i , j ) < M2 * ( i , j ) & ( M3 + M1 ) * ( i , j ) < M2 * ( i , j ) implies M1 = M2 + M1
for f being FinSequence of NAT , i being Element of NAT st i in dom f & for j being Element of NAT st j in dom f holds i divides f /. j holds i divides Sum f & for j being Element of NAT st j in dom f holds i divides j implies i divides Sum f
assume F = { [ a , b ] where a , b is Subset of X : for c being set st c in Bl & a c= c & b c= c } & a c= c & b c= c & c c= a & c c= b & a c= b & b c= c ;
b2 * q2 + ( b3 * q3 ) + - ( b3 * q2 ) + ( - ( a * q2 ) + ( - ( a * q3 ) ) ) = 0. TOP-REAL n + ( - ( a * q2 ) + ( - ( a * q3 ) ) ) .= 0. TOP-REAL n + ( - ( a * q2 ) ) .= 0. TOP-REAL n ;
Cl Cl ( Cl F ) = { D where D is Subset of T : ex B being Subset of T st D = Cl B & B in F & Cl B c= Cl F } ;
attr seq is summable means : : : for m be Nat st seq is summable holds Sum ( seq + seq ) = Sum ( seq ) + Sum ( seq ) & Sum ( seq ) = Sum ( seq ) + Sum ( seq ) ;
dom ( ( ( ( TOP-REAL 2 ) | D ) | D ) ) = ( the carrier of ( ( TOP-REAL 2 ) | D ) ) /\ D .= ( ( TOP-REAL 2 ) | D ) /\ D .= ( ( TOP-REAL 2 ) | D ) /\ D .= D ;
X [ X \to Z ] is full full non empty SubRelStr of ( ( [#] Z ) |^ the carrier of Z ) |^ the carrier of Z , the carrier of Z |^ the carrier of Z , the carrier of Z |^ the carrier of Z , the carrier of Z |^ the carrier of Z , the carrier of Z |^ the carrier of Z ;
G * ( 1 , j ) `2 = G * ( i , j ) `2 & G * ( 1 , j ) `2 <= G * ( 1 , j ) `2 & G * ( 1 , j ) `2 <= s ;
synonym m1 c= m2 means : Def2 : for p being set st p in P holds the set of m1 <= p & p is_\HM { p : p in P & p in the carrier' of m2 } & m1 <= p implies m1 = m2 & m2 = p ;
consider a being Element of B ( ) such that x = F ( a ) and a in { G ( b ) where b is Element of A ( ) : P [ b ] } and P [ a ] ;
synonym the multMagma of R is \vert means : : : : the multMagma of it = [ a , the carrier of R , a ] , the multF of R , the multF of R , the multF of R #) , the multF of it = [: the carrier of R , the carrier of R :] ;
sequence ( a , b ) + ( c , d ) + ( c , 1 ) = b + ( c , d ) .= b + ( c , d ) .= b + ( c , d ) .= ( a + c ) + ( d , d ) .= ( a + c ) + ( d , d ) ;
cluster + ( i1 , i2 ) -> in INT & for Element of INT holds it . ( i1 , i2 ) = + ( i1 , i2 ) & ( i1 = i2 implies i1 = i2 ) & ( i1 = i2 implies i1 = i2 ) & ( i1 = i2 implies i1 = i2 ) ;
( - s2 ) * p1 + ( s2 * p2 - ( s2 * p2 ) ) = ( ( - r2 ) * p1 + ( s2 * p2 - ( s2 * p2 ) ) ) + ( ( - s2 ) * p1 - ( s2 * p2 ) ) .= ( ( - s2 ) * p1 ) + ( ( s2 * p2 ) - ( s2 * p2 ) ) ;
eval ( ( a | ( n , L ) ) *' , p ) = eval ( a | ( n , L ) , x ) * eval ( p , x ) .= a * eval ( p , x ) .= a * eval ( p , x ) ;
assume that the TopStruct of S = the TopStruct of T and for D being non empty directed Subset of Omega S , V being open Subset of Omega S st V in V & V is open & for V being open Subset of Omega S holds V is open & V is open & V is open & V is open & V is open & V is open & V is open ;
assume that 1 <= k & k <= len w + 1 and TU . ( ( len ( q , w ) -succ k ) ) = ( TU . ( k + 1 ) , w -succ k ) ) . k and TU . ( k + 1 ) = ( TU . ( k + 1 ) , w -succ k ) ;
2 * a |^ ( n + 1 ) + ( 2 * b |^ ( n + 1 ) ) >= a |^ ( n + 1 ) + ( b |^ n ) + ( b |^ n ) + ( a |^ n ) + ( b |^ n ) + ( b |^ n ) ;
M , v / ( x. 3 , m ) / ( x. 0 , m ) / ( x. 4 , m ) / ( x. 0 , m ) / ( x. 4 , m ) / ( x. 0 , m ) / ( x. 4 , m ) / ( x. 0 , m ) / ( x. 4 , m ) ) / ( x. 0 , m ) / ( x. 4 , m ) / ( x. 0 , m ) ;
assume that f is_differentiable_on l and for x0 st x0 in l holds 0 < f ' ( x0 ) or for x0 st x0 in l holds f ' ( x0 ) - f ' ( x0 ) and for x0 st x0 in l holds f ' ( x0 ) - f ' ( x0 ) ;
for G1 being _Graph , W being Walk of G1 , e being set , G2 being Walk of G2 , e being set st e in W .vertices() & not e in W holds not ( e in ( the carrier' of G1 ) \ { v } ) & not ( e in ( the carrier' of G2 ) \ { v } )
not c9 is empty iff ( ( not ( ( ex y1 , y2 , y1 , y2 , y2 , y1 , y2 , y2 , y1 ) is not empty & not ( y1 is not empty & not y2 is not empty & not y2 is not empty ) & not ( y1 is not empty & not y2 is not empty ) ) & not ( y2 is not empty ) & not ( y1 is not empty & not y2 is not empty ) ;
Indices GoB f = [: dom GoB f , Seg width GoB f :] & i1 + 1 in dom GoB f & i2 + 1 in Seg width GoB f & 1 <= i2 & i2 + 1 in Seg width GoB f & 1 <= i2 & i2 + 1 <= len GoB f & 1 <= i2 & i2 + 1 <= len GoB f ;
for G1 , G2 , G3 , G3 being Group , O being Subgroup of O , G2 being stable Subgroup of O st G1 is stable & G2 is stable & G1 is stable & G2 is stable holds ( G1 * G2 ) * ( G1 * G2 ) is stable Subgroup of G1 * ( G2 * G3 ) & ( G1 * G2 ) * ( G1 * G3 ) is stable Subgroup of G2 * ( G1 * G2 )
UsedIntLoc ( int \hbox { intloc 0 , intloc 1 , intloc 2 , intloc 3 , intloc 4 , intloc 4 , intloc 0 , intloc 0 , intloc 0 ) ) = { intloc 0 , intloc 2 , intloc 3 , intloc 4 , intloc 5 , intloc 5 , intloc 6 } ;
for f1 , f2 be FinSequence of F st f1 ^ f2 is p -element & Q [ f1 ^ f2 ] & Q [ f2 ^ f1 ^ f2 ] & Q [ f1 ^ f2 ] & Q [ f1 ^ f2 ] & Q [ f1 ^ f2 ] holds f1 ^ f2 ^ f2 ] ;
( p `1 / sqrt ( 1 + ( p `2 / p `1 ) ^2 ) ) = ( q `1 / sqrt ( 1 + ( p `2 / p `1 ) ^2 ) ) / sqrt ( 1 + ( q `2 / p `1 ) ^2 ) .= q `1 / sqrt ( 1 + ( q `2 / q `1 ) ^2 ) ;
for x1 , x2 , x3 , x4 being Element of REAL n holds |( x1 - x2 , x3 - x3 , x4 - x4 )| = |( x1 , x3 - x3 , x4 - x4 )| & |( x1 - x2 , x3 - x3 - x4 )| = |. x1 - x2 - x3 .| & |. x3 - x4 .| = |. x3 - x3 .| + |. x2 - x3 .|
for x st x in dom ( ( F - G ) | A ) holds ( ( F - G ) | A ) . ( - x ) = - ( ( F - G ) | A ) . x - ( F - G ) . x
for T being non empty TopSpace , P being Subset-Family of T st P c= the topology of T & for x being Point of T ex B being Basis of x st B c= P & x in B & P is Basis of x & P is Basis of x
( a 'or' b 'imp' c ) . x = ( 'not' ( a 'or' b ) . x ) 'or' c . x .= ( 'not' ( a . x ) 'or' b . x ) 'or' c . x .= TRUE 'or' ( b . x ) 'or' c . x .= TRUE ;
for e being set st e in [: A , X1 :] ex X1 being Subset of [: Y , X :] , Y1 being Subset of Y st e = [: X1 , Y1 :] & X1 is open & Y1 is open & Y1 is open & Y1 is open & Y1 is open & Y1 is open & Y1 is open & Y1 is open & Y1 is open & Y1 is open ;
for i be set st i in the carrier of S for f be Function of [: S . i , S1 . i :] , S1 . i st f = H . i & F . i = f | ( i + 1 ) holds F . i = f | ( F . i ) & for i be set st i in dom F holds F . i = f | ( F . i ) ;
for v , w st for y st x <> y holds w . y = v . y holds Valid ( VERUM ( Al , J ) , J ) . v = Valid ( VERUM ( Al , J ) , J ) . w
card D = card D1 + card D2 - card { i , j } .= c1 + 1 - card { i , j } .= c1 + 1 - 1 .= c1 + 1 - 1 .= c1 + 1 - 1 .= c1 + 1 - 1 .= c1 + 1 - 1 .= c1 + 1 - 1 .= c1 + 1 - 1 .= c1 + 1 - 1 ;
IC Exec ( i , s ) = ( s +* ( 0 .--> succ ( s . 0 ) ) ) . 0 .= ( 0 .--> succ ( s . 0 ) ) . 0 .= ( s +* ( 0 .--> succ ( s . 0 ) ) ) . 0 .= s . 0 .= s . 0 .= s . 0 ;
len f /. ( len f -' 1 ) -' 1 + 1 = len f /. ( len f -' 1 ) - 1 + 1 .= len f -' 1 + 1 .= len f -' 1 + 1 .= len f -' 1 + 1 .= len f -' 1 + 1 .= len f -' 1 + 1 ;
for a , b , c being Element of NAT st 1 <= a & 2 <= b holds k < a + b-2 or k = a + b-2 or k = a + b-2 or k = a + b-2 or k = a + b-2 or k = a + b-2 or k = a + b-2 or k = a + b-2 ;
for f being FinSequence of TOP-REAL 2 , p being Point of TOP-REAL 2 , i being Element of NAT st p in LSeg ( f , i ) & i <= len f holds Index ( p , f ) <= i & Index ( p , f ) <= i & Index ( p , f ) <= len f
( ( curry ( P7 , k + 1 ) # x ) ) . x = lim ( ( curry ( P7 , k + 1 ) # x ) ) + ( ( curry ( P7 , k + 1 ) # x ) # x ) .= ( ( curry ( F7 , k + 1 ) # x ) # x ) . x ;
z2 = g /. ( i -' n1 + 1 ) .= g . ( i -' n2 + 1 ) .= g . ( i -' n2 + 1 + 1 ) .= g . ( i -' n2 + 1 ) .= g . ( i -' n2 + 1 ) .= g . ( i -' n2 + 1 ) .= g . ( i -' n2 + 1 ) ;
[ f . 0 , f . 3 ] in id ( the carrier of G ) \/ ( the InternalRel of G ) or [ f . 0 , f . 3 ] in the InternalRel of C6 & [ f . 0 , f . 2 ] in the InternalRel of C6 ;
for G being Subset-Family of B st G = { R [ X ] where R is Subset of [: A , B :] : R in F6 & R in F6 } holds ( for X being Subset of [: A , B :] st X in F6 holds ( for X being Subset of A st X in F6 holds X in F ) ) & ( X is open implies X is open )
CurInstr ( P1 , Comput ( P1 , s1 , m1 + m2 ) ) = CurInstr ( P1 , Comput ( P1 , s1 , m2 ) ) .= CurInstr ( P1 , Comput ( P1 , s1 , m2 ) ) .= CurInstr ( P1 , Comput ( P1 , s1 , m2 ) ) .= CurInstr ( P1 , s1 ) .= P1 . IC s1 .= P1 . IC s1 .= P1 . IC s1 .= P1 . IC s1 ;
assume that a on M and b on M and c on N and d on M and p on N and a on M and p on N and c on M and a on M and c on N and p on M and a on M and p on N and a on M and p on N and a on M and c on N and p on M and a on N and c on N and a on M and a on N and b on N and a on M and a on N and b on N and a on M and a on N and b on N and a on N and a on M and b on N and b on N and b on N and b on N and b on N and b on N and a on M and a on M and b on N and b on N and c on N and a on M and c on N and c on N and c on N and a on M
assume that T is \hbox 4 -\cal of T and F is closed and ex F being Subset-Family of T st F is closed & for n being Nat st n <= 0 holds ind F <= 0 and ind T <= n and ind F <= 0 ;
for g1 , g2 st g1 in ]. r1 - r , r2 .[ & g2 in ]. r1 - r , r2 .[ holds |. f . g1 - f . g2 .| <= ( g1 - f . g2 ) / ( |. g2 - r .| ) & |. f . g2 - f . g2 .| <= ( g1 - f . g2 ) / ( |. g2 - r .| )
cosh /. ( z1 + z2 ) = ( cosh /. z1 ) * ( sinh /. z2 ) + ( ( ( ( ( ( ( z1 + z2 ) * ( z1 + z2 ) ) * ( z2 + z1 ) ) * ( z1 + z2 ) ) ) * ( z2 + z1 ) ) .= ( ( ( ( ( ( z1 + z2 ) * ( z1 + z2 ) ) * ( z2 + z1 ) ) * ( z1 + z2 ) ) ) * ( z1 + z2 ) ;
F . i = F /. i .= 0. R + r2 .= b |^ ( n + 1 ) .= b |^ ( n + 1 ) .= <* ( n + 1 ) |^ ( n + 1 ) , a |^ ( n + 1 ) , b |^ ( n + 1 ) , b |^ ( n + 1 ) , a |^ ( n + 1 ) , b |^ ( n + 1 ) , b |^ ( n + 1 ) *> ;
ex y being set , f being Function st y = f . n & dom f = NAT & f . 0 = A ( ) & for n holds f . ( n + 1 ) = R ( n , f . n , f . n ) & for n holds f . ( n + 1 ) = R ( n , f . n ) ;
func f (#) F -> FinSequence of V means : : : for i be Nat st i in dom it holds it . i = F /. i * F /. i & for i be Nat st i in dom it holds it . i = F /. i * F /. i ;
{ x1 , x2 , x3 , x4 , x4 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , 7 , 8 , 8 , 8 , 7 , 8 , 8 , 8 , 8 , 7 , 8 , 8 , 8 , 8 , 7 , 8 , 8 , 7 , 8 , 8 , 8 , 8 , 7 , 8 , 8 , 8 , 7 , 8 } = { x1 , x2 , x3 , x4 , 7 , 8 } ;
for n being Nat for x being set st x = h . n holds h . ( n + 1 ) = o ( x , n ) & x in InputVertices S ( x , n ) & o . ( x , n ) in InnerVertices S ( x , n ) & o . ( x , n ) in InnerVertices S ( x , n ) ;
ex S1 being Element of CQC-WFF ( Al ) st SubP ( P , l , e ) = S1 & ( S , l ) `1 = ( S , l ) `1 & ( S , l ) `2 = ( S , l ) `1 & ( S , l ) `2 = ( S , l ) `2 & ( S , l ) `2 = ( S , l ) `2 ;
consider P being FinSequence of GS2 such that pp = Product P and for i st i in dom P ex t being Element of the carrier of G st P . i = t & t is i & P . i = k and P . i = ( t . i ) * ( t . i ) ;
for T1 , T2 being strict non empty TopSpace , P being Basis of T1 , Q being Basis of T2 st the carrier of T1 = the carrier of T2 & P = the topology of T2 & P = the topology of T2 & P = the topology of T1 & Q = the topology of T2 holds P = Q ;
assume that f is_\cal 2 2 , u0 and r (#) pdiff1 ( f , 3 ) is_partial_differentiable_in u0 , 2 and partdiff ( r (#) pdiff1 ( f , 3 ) , u0 , 2 ) = r * pdiff1 ( f , u0 , 3 ) and partdiff ( r (#) pdiff1 ( f , u0 ) , u0 , 2 ) = r * pdiff1 ( f , u0 ) ;
defpred P [ Nat ] means for F , G being FinSequence of ExtREAL for s being Permutation of REAL , G st len F = $1 & G = F * s & not G = F * s & not F = G & G = F * s holds Sum ( F ) = Sum ( G ) ;
ex j st 1 <= j & j < width GoB f & ( GoB f ) * ( 1 , j ) `2 <= s & s < ( GoB f ) * ( 1 , j + 1 ) `2 or s < ( GoB f ) * ( 1 , j + 1 ) `2 & s < ( GoB f ) * ( 1 , j + 1 ) `2 ;
defpred U [ set , set ] means ex F-23 be Subset-Family of T st $1 = F-23 & $2 is open & union F-23 is open & union Fp1 is Subset-Family of T & union Fp1 is Subset-Family of T & union Fp1 is Subset-Family of T & union Fp1 is Subset-Family of T & union Fp1 is NAT & union Fp1 is Subset-Family of T ;
for p4 being Point of TOP-REAL 2 st LE p4 , p4 , P , p1 , p2 & LE p4 , p , P , p1 , p2 & LE p4 , p , P , p1 , p2 & LE p4 , p , P , p1 , p2 holds LE p4 , p , P , p1 , p2 & LE p4 , p , P , p1 , p2 & LE p4 , p , P , p1 , p2 & LE p4 , p , P , p1 , p2 & LE p4 , p , P , p1 , p2 & LE p4 , p , P , p1 , p2 & LE p4 , p1 , p2 , P , p1 , p2 , p2 & LE p4 , p1 , P , p1 , p2 & LE p , p1 , P , p1 , p2 & LE p , p1 , P , p1 , p2 , p1 , p2 , p1 , p2 & LE p1 , p1 , P , p1 , p2 & LE p1 , p1 , p2 ,
f in D ( ) & for g st g <> f . y holds x = f . y implies x = y & g in D & f in D implies f in All ( x , H ) & for f being Function of E , E st f = All ( x , H ) & f . x = f . y & f . y = f . y ;
ex 8 being Point of TOP-REAL 2 st x = 8 & ( ( ( ( ( ( ( ( ( ( ( p `2 / |. p .| - sn ) ) ) ) / |. p .| ) ) ) * ( ( ( p `2 / |. p .| - sn ) ) / ( 1 + sn ) ) ) ) & ( ( ( p `2 / |. p .| - sn ) ) / ( 1 + sn ) ) * ( 1 + sn ) ) = ( ( ( p `2 / |. p .| - sn ) ) * ( 1 + sn ) ) / ( 1 + sn ) ) & ( ( p `2 / |. p .| ) ) * ( 1 + sn ) ) ;
assume for d7 being Element of NAT st d7 <= max ( n7 , n7 ) holds ( ( d7 ) . ( d7 ) = ( ( d7 ) . ( d7 ) ) . ( d7 ) ) & ( ( d7 ) . ( d7 ) = ( ( d7 ) . ( d7 ) ) . ( d7 ) ;
assume that s <> t and s is Point of Sphere ( x , r ) and s is not Point of Sphere ( x , r ) and ex e being Point of Sphere ( x , r ) st { e } = Sphere ( s , r ) /\ Sphere ( x , r ) and e = Ball ( s , r ) and e = Ball ( x , r ) ;
given r such that 0 < r and for s st 0 < s ex x1 be Point of CNS st x1 in dom f & ||. x1 - x0 .|| < s & |. x1 - x0 .| < s & |. x1 - x0 .| < s & |. x1 - x0 .| < s ;
( p | x ) | ( ( x | x ) | ( x | x ) ) = ( ( x | x ) | ( x | x ) ) | ( ( x | x ) | p ) .= ( ( x | x ) | p ) | ( ( x | x ) | p ) ;
assume that x , x + h in dom sec and ( for x st x in dom sec holds ( h . x = 4 * sin ( x + h . x ) * cos ( x + h . x ) ) & ( for x st x in dom sec holds ( ( 2 * x + h . x ) * sin ( x + h . x ) ) / ( 2 * sin ( x + h . x ) ) ^2 = ( 2 * sin x ) / ( 2 * sin ( x + h . x ) ^2 ) and ( 2 * sin ( x + h . x ) ^2 + ( 2 * sin ( x + h . x ) ^2 ) ;
assume that i in dom A and len A > 1 and B c= the carrier of ( len A ) and B c= the carrier of ( ( len A ) -tuples_on the carrier of K ) and A = ( A + B ) * ( i , j ) and len A = len B and width A = width B and len B = width B ;
for i be non zero Element of NAT st i in Seg n holds i divides n or i = <* 1. F_Complex , n , m , m , n *> & i <> 0. F_Complex & i <> 0. F_Complex & i <> 0. F_Complex & i <> 0. F_Complex & i <> 0. F_Complex & i <> 0. F_Complex & i <> 0. F_Complex & i <> 0. F_Complex implies h . i = <* 1. F_Complex , m , n , m *>
( ( ( b1 'imp' b2 ) '&' ( c1 'imp' c2 ) ) '&' ( ( b1 'or' c1 ) '&' ( c1 '&' c2 ) ) '&' ( ( b1 'or' c1 ) '&' ( c1 '&' c2 ) '&' 'not' ( c1 '&' c2 ) ) ) '&' ( ( b1 'or' c1 ) '&' 'not' ( c1 '&' c2 ) '&' 'not' ( c1 '&' c2 ) ) '&' 'not' ( c1 '&' c2 ) '&' 'not' ( c1 '&' c2 )
assume that for x holds f . x = ( ( cot * sin ) `| Z ) . x and x in dom ( cot * sin ) and x in dom ( ( cot * sin ) `| Z ) and for x st x in Z holds ( ( ( ( cot * sin ) `| Z ) `| Z ) . x = ( ( cot * sin ) `| Z ) . x ) ;
consider Rd , I-8 be Real such that Rd = Integral ( M , Re ( F . n ) ) and I-8 = Integral ( M , Im ( F . n ) ) and Integral ( M , I-8 ) = Integral ( M , Im ( F . n ) ) and Integral ( M , Im ( F . n ) ) = Integral ( M , Im ( F . n ) ) ;
ex k be Element of NAT st k = k & 0 < d & for q be Element of product G st q in X & ||. q- partdiff ( f , x , k ) .|| < r holds ||. partdiff ( f , x , k ) - partdiff ( f , x , k ) .|| < r ;
x in { x1 , x2 , x3 , x4 , x4 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 } ;
G * ( j , ii ) `2 = G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii ) `2 .= G * ( 1 , ii
f1 * p = p .= ( ( the Arity of S1 ) +* ( the Arity of S2 ) ) . o .= ( the Arity of S1 ) . o .= ( the Arity of S1 ) . o .= ( the Arity of S1 ) . o .= ( the Arity of S1 ) . o .= ( the Arity of S1 ) . o .= ( the Arity of S1 ) . o .= ( the Arity of S1 ) . o ;
func tree ( T , P , T1 , T2 ) -> DecoratedTree means : : : : q in it iff q in T & for p st p in P holds p ^ q in T1 or ex r , s st r in T & s in T1 & p = r ^ s ;
F /. ( k + 1 ) = F . ( k + 1 -' 1 ) .= F{} ( p . ( k + 1 -' 1 ) , k + 1 -' 1 ) .= F{} ( p . k , k + 1 -' 1 ) .= F{} ( p . k , k + 1 -' 1 ) .= F{} ( p . k , k + 1 -' 1 ) .= F{} ( p . k , k + 1 -' 1 ) ;
for A , B , C being Matrix of n , K st len B = len C & width B = width C & len B = width C & len A = width A & len B > 0 & len A = width B & len B > 0 & width A = width C & len B = width C & width B = 0 & len A = 0 & width B = 0 & width C = 0 holds A = B - C
seq . ( k + 1 ) = 0. F_Complex + seq . ( k + 1 ) .= ( Partial_Sums ( seq ) . ( k + 1 ) ) + ( Partial_Sums ( seq ) . ( k + 1 ) ) .= ( Partial_Sums ( seq ) . ( k + 1 ) ) + ( Partial_Sums ( seq ) . ( k + 1 ) ) .= ( Partial_Sums ( seq ) . ( k + 1 ) ) + ( Partial_Sums ( seq ) . ( k + 1 ) ) ;
assume that x in ( the carrier of Cy ) & y in ( the carrier of Cy ) and [ x , y ] in the carrier of Cy and [ y , x ] in the InternalRel of Cy and [ x , y ] in the InternalRel of Cy and [ y , x ] in the InternalRel of Cy ;
defpred P [ Element of NAT ] means for f st len f = $1 holds ( for k st k = $1 holds ( for f st f . ( k + 1 ) = ( VAL g ) . ( k + 1 ) ) holds ( VAL g ) . ( k + 1 ) = ( VAL g ) . ( k + 1 ) '&' ( VAL g ) . ( k + 1 ) ;
assume that 1 <= k and k + 1 <= len f and f is_sequence_on G and [ i , j ] in Indices G and [ i + 1 , j ] in Indices G and f /. k = G * ( i , j ) and f /. ( k + 1 ) = G * ( i , j ) and f /. ( k + 1 ) = G * ( i , j ) ;
assume that sn < 1 and q `1 > 0 and ( q `2 / |. q .| - sn ) >= sn and q `2 / |. q .| - sn ) and ( q `2 / |. q .| - sn ) >= 0 and ( q `2 / |. q .| - sn ) >= 0 and ( q `2 / |. q .| - sn ) >= 0 and q `2 / |. q .| - sn ) ;
for M being non empty TopSpace , x being Point of M , f being Point of M st x = x `1 holds ex f being sequence of ( M ) st for n being Element of NAT holds f . n = Ball ( x `1 , ( M . n ) / ( n + 1 ) ) & for n being Element of NAT holds f . n = Ball ( x `1 , ( M . n ) / ( n + 1 ) )
defpred P [ Element of omega ] means f1 is_differentiable_on Z & f2 is_differentiable_on Z & for x st x in Z holds ( f1 - f2 ) `| Z holds ( f1 - f2 ) `| Z ) . x = ( f1 . x - f2 . x ) / ( f1 . x ) ^2 / ( f2 . x - f2 . x ) ^2 / ( f2 . x ) ^2 ;
defpred P1 [ Nat , Point of CNS ] means $1 in Y & ||. ( f . $1 ) - ( f . $1 ) .|| < r & ||. ( f . $1 ) - ( f . $1 ) .|| < r & ||. ( f . $1 ) - ( f . ( $1 + 1 ) ) .|| < r ;
( f ^ mid ( g , 2 , len g ) ) . i = ( mid ( g , 2 , len g ) ) . i .= ( mid ( g , 2 , len g ) ) . ( i -' len f + 1 ) .= g . ( i -' len f + 1 ) .= g . i .= g . i .= ( f /^ ( len f -' 1 ) ) . i ;
( 1 / 2 * n0 + 2 * ( 2 * n0 + 2 * ( n0 + 2 * n0 ) ) ) = ( ( 1 / 2 * n0 + 2 * ( n0 + 2 * n0 ) ) * Cl ( ( 2 * n0 + 2 * n0 ) ) * Cl ( ( 2 * n0 + 2 * n0 ) ) * Cl ( ( 2 * n0 + 2 * n0 ) ) ) .= ( 1 / 2 * ( n0 + 2 * n0 ) ) * Cl ( ( 2 * n0 + 2 * n0 ) ;
defpred P [ Nat ] means for G being non empty strict finite RelStr , H being strict symmetric RelStr st G is space & card the carrier of G = $1 & the carrier of G = { 0. G , the carrier of H } & the carrier of G = { 0. G , the carrier of H , the carrier of H } ;
assume that not f /. 1 in Ball ( u , r ) and 1 <= m and m <= len ( f | ( i + 1 ) ) and for i st 1 <= i & i <= len ( f | ( i + 1 ) ) /\ Ball ( u , r ) <> {} and not i <= m and m <= len ( f | ( i + 1 ) ) ;
defpred P [ Element of NAT ] means ( Partial_Sums ( cos , $1 , r , x , y ) ) . ( 2 * $1 + 1 ) = ( Partial_Sums ( cos , $1 , r , x , y ) . ( 2 * $1 + 1 ) ) . ( 2 * $1 + 1 ) * ( ( cos , $1 , x , y , x ) . ( 2 * $1 + 1 ) ) ;
for x being Element of product F holds x is FinSequence of G & dom x = I & x in dom ( the support of F ) & for i being set st i in I holds x . i = ( the Sorts of A ) . i & for i being set st i in I holds x . i = ( the Sorts of A ) . i ;
( x " ) |^ ( n + 1 ) = ( x " ) |^ n * x " .= ( x |^ n ) |^ n * x " .= ( x |^ n ) |^ n * x " .= ( x |^ n ) |^ n * x " .= ( x |^ n ) |^ n * x " .= ( x |^ n ) |^ n * x " .= ( x |^ n ) |^ n ;
DataPart Comput ( P +* ( I , P , \mathop { intloc 0 } ) , Initialized s ) = DataPart Comput ( P +* I , s , LifeSpan ( P +* I , s ) + 3 ) .= DataPart Comput ( P +* I , s , LifeSpan ( P +* I , s ) + 3 ) .= DataPart Comput ( P +* I , s , LifeSpan ( P +* I , s ) + 3 ) ;
given r such that 0 < r and ]. x0 , x0 + r .[ c= dom f1 /\ dom f2 and for g st g in ]. x0 , x0 + r .[ /\ dom f2 holds f1 . g <= f1 . g and for g st g in ]. x0 , x0 + r .[ /\ dom f2 holds f1 . g <= f2 . g ;
assume that X c= dom f1 /\ dom f2 and f1 | X is continuous and f2 | X is continuous and for r st r in X /\ dom f2 & r < x0 ex g st g < r & g in dom ( f1 + f2 ) and for g st g in X /\ dom ( f2 + g2 ) holds ( f1 + f2 ) | X is continuous and ( f1 + f2 ) | X is continuous ;
for L being continuous complete LATTICE for l being Element of L ex X being Subset of L st l = sup X & for x being Element of L st x in X holds x is prime & for x being Element of L st x in X holds x is prime & x is prime & x is prime & x is prime & x is prime & x is prime
Support ( e *' A ) in { Support ( m *' p ) where m is Polynomial of n , L : ex i being Element of NAT st i in dom p & ex p being Polynomial of n , L st p /. i = p /. i & p /. i = ( m *' p ) /. i & p /. i = ( m *' p ) /. i } ;
( f1 - f2 ) /* s1 = lim ( f1 /* s1 ) - lim ( f2 /* s1 ) .= lim ( ( f1 /* s1 ) - ( f2 /* s1 ) ) .= lim ( ( f1 /* s1 ) - ( f2 /* s1 ) ) .= lim ( ( f1 /* s1 ) - ( f2 /* s1 ) ) .= lim ( ( f1 /* s1 ) - ( f2 /* s1 ) ) ;
ex p1 being Element of CQC-WFF ( Al ) st F . p = g `1 & for g being Function of [: CQC-WFF ( Al ) , D ( ) :] , D ( ) st P [ g , ( len p ) qua Nat ] & for i being Nat st i in dom p holds P [ i , g . i , f . ( len p ) , g . ( len p ) ] ;
( mid ( f , i , len f -' 1 ) ^ <* f /. j *> ) /. j = ( mid ( f , i , len f -' 1 ) ) /. j .= ( mid ( f , i , len f -' 1 ) ) /. j .= ( mid ( f , i , len f -' 1 ) ) /. j .= f /. ( j + 1 ) .= f /. j ;
( ( p ^ q ) ^ r ) . ( len p + k ) = ( ( p ^ q ) . ( len p + k ) ) . ( len p + k ) .= ( ( p ^ q ) . ( len p + k ) ) . ( len p + k ) .= ( ( p ^ q ) . ( len p + k ) ) . ( len p + k ) .= ( p ^ q ) . k ;
len mid ( upper_volume ( f , D2 ) , indx ( D2 , D1 , j1 ) + 1 ) = indx ( D2 , D1 , j1 ) -' indx ( D2 , D1 , j ) + 1 .= indx ( D2 , D1 , j1 ) - 1 .= indx ( D2 , D1 , j1 ) - 1 .= indx ( D2 , D1 , j1 ) + 1 ;
x * y * z = Mz * ( y * z ) .= ( x * ( y * z ) ) * ( y * z ) .= ( x * ( y * z ) ) * ( y * z ) .= ( x * ( y * z ) ) * ( y * z ) .= ( x * ( y * z ) ) * ( y * z ) .= x * ( y * z ) ;
v . <* x , y *> + ( <* x0 , y0 *> ) * i = partdiff ( v , ( x - x0 ) * i + ( y - x0 ) * ( i - x0 ) + ( ( x - x0 ) * ( i - x0 ) + ( y - x0 ) * ( i - x0 ) ) ) + ( ( proj ( 1 , 1 ) * ( i - x0 ) + ( proj ( 1 , 1 ) * ( i - x0 ) ) ) ;
i * i = <* 0 * ( - 1 ) - ( 0 * 1 ) - ( 0 * 0 ) , 0 * 0 + ( 0 * 0 ) + ( 0 * 0 ) + ( 0 * 0 ) , 0 * 0 + ( 0 * 0 ) + ( 0 * 0 ) + ( 0 * 0 ) + ( 0 * 0 ) , 0 * 0 + ( 0 * 0 ) + ( 0 * 0 ) * 0 .= 0 ;
Sum ( L (#) F ) = Sum ( L (#) ( F1 ^ F2 ) ) .= Sum ( ( L (#) F1 ) ^ ( L (#) F2 ) ) .= Sum ( ( L (#) F1 ) ^ ( L (#) F2 ) ) .= Sum ( L (#) F1 ) + Sum ( L (#) F2 ) .= Sum ( L (#) F1 ) + Sum ( L (#) F2 ) .= Sum ( L (#) F1 ) + Sum ( L (#) F2 ) .= Sum ( L (#) F1 ) ;
ex r be Real st for e be Real st 0 < e ex Y1 be finite Subset of X st Y1 is non empty & for Y1 be finite Subset of X st Y1 c= Y & Y1 c= Y & for Y1 be finite Subset of X st Y1 c= Y & Y1 is finite & Y1 is finite holds |. ( - r ) . Y1 - ( r * s ) . Y1 .| < r ;
( GoB f ) * ( i , j + 1 ) = f /. ( k + 2 ) & ( GoB f ) * ( i , j + 1 ) = f /. ( k + 2 ) or ( GoB f ) * ( i , j + 1 ) = f /. ( k + 2 ) & ( GoB f ) * ( i , j ) = f /. ( k + 2 ) ;
( ( cos ^2 ) (#) ( sin ^2 ) ) . x = ( ( r ^2 ) * ( sin ^2 ) ) . x .= ( ( 1 / ( r ^2 ) ) * ( sin ^2 ) ) . x .= ( ( 1 / ( r ^2 ) ) * ( cos ^2 ) ) . x .= ( ( 1 / r ) * ( cos ^2 ) ) . x .= ( ( 1 / r ) * ( 1 / r ) ) . x ;
x0 - b + sqrt ( delta ( a , b , c ) - sqrt ( delta ( a , b , c ) ) ) < 0 & x0 - b + sqrt ( delta ( a , b , c ) - sqrt ( delta ( a , b , c ) ) ) < 0 implies x0 - b + sqrt ( delta ( a , b , c ) - sqrt ( delta ( a , b , c ) ) ) > 0
assume that ex_inf_of uparrow "\/" ( X , L ) , L and ex_sup_of X , L and ex_sup_of X , L and "\/" ( X , L ) = "/\" ( uparrow "\/" ( X , L ) , L ) and for X st X in X holds "\/" ( X , L ) = "/\" ( uparrow "\/" ( X , L ) , L ) and for X st X in X holds "\/" ( X , L ) = "/\" ( X , L ) ;
( for j holds ( j = i = j implies ( j = i = j implies i = j implies j = i ) ) & ( j = i implies i = j implies j = i implies j = i ) & ( i = j implies j = i implies j = i ) implies i = j & j = i implies j = i & j = i implies j = i & j = j )