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 ;
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 finite ;
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 \bf 1 ;
assume x in I ;
q is decorated by 0 ;
assume c in x ;
1-p > 0 ;
assume x in Z ;
assume x in Z ;
1 <= k12 ;
assume m <= i ;
assume G is prime ;
assume a divides b ;
assume P is closed ;
O > 0 ;
assume q in A ;
W is not bounded ;
f is IC 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 negative ;
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 ;
let X be set ;
let X be set ;
let y be element ;
let x be element ;
P [ 0 ]
let E be set , A be Subset 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 terminal ;
Q halts_on s ;
x in \circ P ;
M < m + 1 ;
T2 is open ;
z in b +^ a ;
R2 is well-ordering ;
1 <= k + 1 ;
i > n + 1 ;
q1 is one-to-one ;
let x be trivial set ;
PP 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 Real , r be Real ;
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 ;
let E be Ordinal ;
o on 4 ;
O <> O ;
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 RealUnitarySpace , W be Subspace of V ;
not s in Y |^ 0 ;
rng f <= w ;
b "/\" e = b ;
m = m2 ;
t in h . D ;
P [ 0 ] ;
assume z = x * y ;
S . n is bounded ;
let V be RealUnitarySpace , A , B be Subset of V ;
P [ 1 ] ;
P [ {} ] ;
C1 is component ;
H = G . i ;
1 <= i + 1 ;
F . m in A ;
f . o = o ;
P [ 0 ] ;
ab <= b-a ;
R [ 0 ] ;
b in f .: X ;
assume q = q2 ;
x in [#] V ;
f . u = 0 ;
assume e1 > 0 ;
let V be RealUnitarySpace , W be Subspace of V , A be Subset of V ;
s is trivial & s is trivial ;
dom c = Q ;
P [ 0 ] ;
f . n in T ;
N . j in S ;
let T be complete LATTICE , A , B be Subset of T ;
the object of F is one-to-one ;
sgn x = 1 ;
k in support a ;
1 in Seg 1 ;
rng f = X ;
len T in X ;
vA2 < n ;
S\rbrack is bounded ;
assume p = p2 ;
len f = n ;
assume x in P1 ;
i in dom q ;
let U ;
p-25 = c ;
j in dom h ;
let k ;
f | Z is continuous ;
k in dom G ;
UBD C = B ;
1 <= len M ;
p in \lbrace x } ;
1 <= j1 ;
set A = <* \rangle ;
card a [= c ;
e in rng f ;
cluster B \oplus A -> empty ;
H has no has H ;
assume x0 <= m ;
T is increasing ;
e1 <> e1 ;
Z c= dom g ;
dom p = X ;
H is proper implies H is proper
i + 1 <= n ;
v <> 0. V ;
A c= conv A ;
S c= dom F ;
m in dom f ;
let X0 be set ;
c = sup N ;
R is connected & R is connected ;
assume not x in REAL ;
Im f is complete ;
x in Int y ;
dom F = M ;
a in On W ;
assume e in [: A , A :] ;
C c= C|[ - 1 , - 1 ]| ;
m2 <> {} ;
let x be Element of Y ;
let f be decorated IC v , t be Element of NAT ;
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 .vertices() ;
- y in I ;
let A be non empty set , B be set ;
P = 1 ;
assume r in F . k ;
assume f is simple function of S ;
let A be countable set ;
rng f c= NAT ;
assume P [ k ] ;
f <> {} ;
let o be Ordinal ;
assume x is sum of g ;
assume not v in { 1 } ;
let I1 ;
assume that 1 <= j and j < l ;
v = - u ;
assume s . b > 0 ;
d1 in C ;
assume t . 1 in A ;
let Y be non empty TopSpace , X be non empty TopSpace , Y be non empty TopSpace ;
assume a in \mathopen { \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 [#] ( f | A ) ;
[ a , c ] in X ;
m1 <> {} ;
M + N c= M + N ;
assume M is /. hhhhmeet M ;
assume f is with_inbA1 ;
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 & j1 <= j2 ;
f | A is unfolded ;
f . x < b ;
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 rng phi ;
CQ is open ;
q2 c= C1 & q2 c= C2 ;
a2 < c2 & not a2 < c2 ;
s2 is 0 -started ;
IC s = 0 ;
6 = 5 ;
let V ;
let x , y be element ;
let x be Element of T ;
assume a in rng F ;
x in dom T ` ;
let S be Subset-Family of L ;
y " <> 0 ;
y " <> 0 ;
0. V = uw -xw ;
y2 , y are_not zero ;
R ;
let a , b be Real , x be 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 , p be FinSequence of NAT ;
4 . n = N ;
set y = ( x `1 ) / 2 ;
NAT in dom g ;
l . 2 = y1 ;
|. g . y .| <= r ;
f . x in Cx0 ;
V is non empty Subset of V ;
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 f c= INT ;
G = 0 .--> goto 0 ;
let A be Subset of X ;
assume that Ax0 is dense and not 0 in A ;
|. f . x .| <= r ;
let x be Element of R ;
let b be Element of L ;
assume x in WO ;
P [ k , a ] ;
let X be Subset of L ;
let b be object of B ;
let A , B be category ;
set X = Vars ( C ) ;
let o be OperSymbol of S ;
let R be connected non empty Poset ;
n + 1 = succ n ;
x-21 c= Y1 & xY c= Y2 ;
dom f = C1 ;
assume [ a , y ] in X ;
Re ( seq ) is convergent ;
assume a1 = b1 & a2 = b2 ;
A = sInt ( A ) ;
a <= b or b <= a ;
n + 1 in dom f ;
let F be Program of S , s be State of S ;
assume r2 > x0 ;
let Y be non empty set , f , g be Function of Y , BOOLEAN ;
2 * x in dom W ;
m in dom g2 ;
n in dom g1 ;
k + 1 in dom f ;
the still not bound in { s } ;
assume x1 <> x2 ;
v2 in ( V \ { 0. V } ) \/ { 0. V } ;
not [ b `1 , b `2 ] in T ;
i-35 + 1 = i ;
T c= a11 ( T ) ;
( l `1 ) ^2 = 0 ;
let n be Nat ;
( t `2 ) ^2 = r ;
AK is_integrable_on M & f is_integrable_on M ;
set t = Bottom t ;
let A , B be real-membered set ;
k <= len G + 1 ;
[: C , D :] misses [: D , D :] ;
Product ( seq ) is non empty ;
e <= f or f <= e ;
cluster -> non empty for NAT -defined Function ;
assume c2 = b2 ;
assume h in [. q , p .] ;
1 + 1 <= len C ;
not c in B . m1 ;
cluster R .: X -> empty ;
p . n = H . n ;
assume that v-4 is convergent and lim vK = 0 ;
IC s3 = 0 ;
k in N or k in K ;
F1 \/ F2 c= F ;
Int G1 <> {} & Int G1 <> {} ;
( z `2 ) ^2 = 0 ;
p01 <> p1 & p1 <> p2 ;
assume z in { y , w } ;
MaxADSet ( a ) c= F ;
sup \mathopen { \downarrow s } in S ;
f . x <= f . y ;
let T be up-complete non empty reflexive antisymmetric RelStr ;
q |^ m >= 1 ;
a >= X & b >= Y ;
assume <* a , c *> <> {} ;
F . c = g . c ;
G is one-to-one one-to-one ;
A \/ { a } c= B ;
0. V = 0. Y ;
let I be Instruction of S , J be Program of S ;
f-24 . x = 1 ;
assume z \ x = 0. X ;
C4 = 2 |^ n ;
let B be sequence of Sigma ;
assume X1 = p .: D ;
n + l in NAT ;
f " P is compact ;
assume x1 in REAL + ( - 1 ) ;
p1 = K & p2 = K or p1 = K ;
M . k = <*> REAL ;
phi . 0 in rng phi ;
MMMit is closed ;
assume x0 <> 0. L ;
n < N7 . k ;
0 <= ( seq . 0 ) / ( 0 + 1 ) ;
- q + p = v ;
{ v } is Subset of B ;
set g = f /. j ;
R is stable Relation of R ;
set \cal R = Vertices R , S = Vertices R ;
p0 c= P4 & C0 c= rng p3 ;
x in [. 0 , 1 .] ;
f . y in dom F ;
let T be Scott Scott Scott TopAugmentation of S ;
inf the carrier of S in S ;
downarrow a = downarrow b ;
P , C , K is_collinear ;
assume x in F ( s , r ) ;
2 to_power i < 2 to_power m ;
x + z = x + z ;
x \ ( a \ x ) = x ;
||. \mathopen { \Vert } x-y .|| <= r ;
assume that Y c= field Q and Y <> {} ;
a \times b , a are_equipotent ;
assume a in A ( ) ;
k in dom ( q | i ) ;
p is non empty finite for FinSequence of S ;
i - 1 = i - 1 ;
f | A is one-to-one ;
assume x in f .: [: X , Y :] ;
i2 - i1 = 0 ;
j2 + 1 <= i2 ;
g " * a in N ;
K <> { [ {} , {} ] } ;
cluster -> with_|. -> strict for \Im yielding Function ;
|. q .| ^2 > 0 ;
|. p3 .| = |. p .| ;
s2 - s1 > 0 ;
assume x in { Gik } ;
W-min C in C & W-min C in C ;
assume x in { Gik } ;
assume i + 1 = len G ;
assume i + 1 = len G ;
dom I = Seg n & dom I = Seg n ;
assume that k in dom C and k <> i ;
1 + 1-1 <= i + 1-1 ;
dom S = dom F ;
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 partial with_|. E .| ;
let f be ManySortedSet of I ;
let z be Element of COMPLEX , x be set ;
u in { \hbox { \boldmath $ g $ } } ;
2 * n < ( 2 * n ) / 2 ;
x , y are_equipotent ;
B-11 c= V & V c= V ;
assume I is_closed_on s , P ;
U = U ( ) , U = U ( ) , T = U ( ) ;
M /. 1 = z /. 1 ;
x11 = x22 & x22 = x22 ;
i + 1 < n + 1 ;
x in { {} , <* 0 *> } ;
f . ( f . x ) <= ( f . x ) `1 ;
let l be Element of L ;
x in dom ( F . j ) ;
let i be Element of NAT ;
r is ( COMPLEX ) -valued ;
assume <* o2 , o *> <> {} ;
s . x |^ 0 = 1 ;
card ( K . n ) in M & card ( K . n ) in M ;
assume that X in U and Y in U ;
let D be Subset-Family of Omega ;
set r = q + { k + 1 } ;
y = W . ( 2 * x ) ;
assume dom g = cod f & cod g = cod f ;
let X , Y be non empty TopSpace , f , g be Function of X , Y ;
x \oplus A is interval ;
|. <*> A .| . a = 0 ;
cluster sublattice -> strict for complete lattice ;
a1 in B . s1 & a2 in B . s1 ;
let V be finite VectSp of F , A , B be Subset of V ;
A * B on B , A ;
f-3 = NAT --> 0 ;
A , B be Subset of V ;
z1 = P1 . j & z2 . j = P1 . j ;
assume f " P is closed ;
reconsider j = i as Element of M ;
a , b be Element of L ;
assume q in A \/ ( B "\/" C ) ;
dom ( F * C ) = o ;
set S = ( REAL X ) |^ n ;
z in dom ( A --> y ) ;
P [ y , h . y ] ;
{ x0 } c= dom f ;
let B be non-empty ManySortedSet of I , A be non-empty ManySortedSet of I ;
sqrt ( PI / 2 ) < Arg z ;
reconsider z9 = 0 as Nat ;
LIN a , d , c ;
[ y , x ] in [: I , I :] ;
( Q ) `1 = 0 & ( Q ) `1 = 0 ;
set j = x0 div m , n = x0 mod m ;
assume a in { x , y , c } ;
j2 - ( j - ( j - i ) ) > 0 ;
I \! \mathop { \rm \hbox { - } \varphi } = 1 ;
[ y , d ] in ( F . y ) `1 ;
let f be Function of X , Y ;
set A2 = sqrt ( B + C ) ;
s1 , s2 are_Element of R ;
j1 - 1 + 1 = 0 ;
set m2 = 2 * n + j ;
reconsider t = t as bag of n ;
I2 . j = m . j ;
i |^ s , n are_relative_prime ;
set g = f | ( D , j ) ;
assume that X is lower and 0 <= r ;
( p1 `1 ) ^2 = 1 ^2 ;
a < ( p3 `1 ) ^2 + ( p3 `2 ) ^2 ;
L \ { m } c= UBD C ;
x in Ball ( x , 10 ) ;
not a in LSeg ( c , m ) ;
1 <= i1 -' 1 + 1 - 1 ;
1 <= i1 -' 1 + 1 - 1 ;
i + i2 <= len h ;
x = W-min ( P ) ;
[ x , z ] in X \times Z ;
assume y in [. x0 , x .] ;
assume p = <* 1 , 2 , 3 *> ;
len <* A1 *> = 1 ;
set H = h . ( g2 . i ) ;
card b * a = |. a .| * |. a .| ;
Shift ( w , 0 ) |= v ;
set h = h2 ** h1 , h1 = h2 ** h1 ;
assume x in X0 /\ 4 ;
||. h .|| < d1 * ||. h .|| ;
not x in the carrier of f & not x in the carrier of f ;
f . y = F ( y ) ;
for n holds X [ n ] ;
k - l = kA ;
<* p , q *> /. 2 = q ;
let S be Subset of the lattice of T ;
P , Q are_congruent_mod s ;
Q /\ M c= union ( F | M )
f = b * ( card S ) ;
let a , b be Element of G ;
f .: X <= f . sup X ;
let L be non empty reflexive transitive RelStr , X be Subset of L , Y be Subset of L ;
Sbe is x -to_power i -to_power n ;
let r be non positive Real ;
M , v |= All ( x , y ) ;
v + w = 0. V ;
P [ len F ] & P [ F ( ) ] ;
assume InsCode ( i ) = 8 ;
the carrier of M = 0 & the carrier of M = {} ;
cluster z * ( seq . n ) -> summable for Real_Sequence ;
let O be Subset of the carrier of C ;
]. f , g .[ | X is continuous ;
x2 = g . ( j + 1 ) ;
cluster -> Element for Element of AllTermsOf S ;
reconsider l1 = lm1 as Nat ;
v2 is Vertex of r2 & v2 is Vertex of G ;
T3 is SubSpace of T2 ;
Q /\ Q <> {} ( ( TOP-REAL 2 ) | Q ) ;
let k be Nat ;
q " is Element of X ;
F ( t ) is set of M ;
assume that n <> 0 and n <> 1 ;
set e1 = EmptyBag n , e2 = EmptyBag n ;
let b be Element of Bags n ;
assume for i holds b . i is commutative ;
x is Element of ( the Sorts of A ) . s ;
not r in ]. p , q .[ ;
let R be FinSequence of REAL ;
S7 does not empty destroy b1 & b1 is not empty ;
IC SCM R <> a & IC R <> a ;
|. |[ x , y ]| .| >= r ;
1 * ( seq . n ) = seq . ( n + 1 ) ;
let x be FinSequence of NAT ;
let f be Function of C , D , g be Function of D , D ;
for a holds 0. L + a = a
IC s = s . NAT .= ( the Sorts of A ) . NAT ;
H + G = FFF ( GG ) ;
C1 . x = x2 & C2 . x = y2 ;
f1 = f . x .= f2 . x .= f2 . x ;
Sum <* p . 0 *> = p . 0 ;
assume v + W = v + u + W ;
{ a1 } = { a2 } ;
a1 , b1 _|_ b , a ;
a3 , o _|_ o , a3 ;
I1 is reflexive transitive & I2 is reflexive implies I1 is reflexive
I1 is antisymmetric antisymmetric & ( the InternalRel of C ) /\ the InternalRel of D ;
sup rng ( H1 . n ) = e & sup rng H1 = e ;
x = ( a9 * b9 ) * ( a * a9 ) ;
|. p1 .| ^2 >= 1 ^2 ;
assume j2 -' 1 < j2 -' 1 ;
rng s c= dom ( f1 + f2 ) /\ dom f1 ;
assume support a misses support b & not a in support b ;
let L be associative non empty doubleLoopStr , A , B be non empty Subset of L ;
s " + 0 < n + 1 ;
p . c = ( f . 1 ) `1 ;
R . n <= R . ( n + 1 ) ;
Directed ( I1 ) = I1 +* I2 ;
set f = x + ( y , r ) ;
cluster Ball ( x , r ) -> bounded ;
consider r being Real such that r in A ;
cluster -> non empty for Function ;
let X be non empty directed Subset of S ;
let S be non empty full full SubRelStr of L ;
cluster <* L1 . N , L2 . N *> -> complete for non trivial strict trivial non trivial strict non trivial ;
sqrt ( 1 + a ) " = a ;
( q . {} ) `1 = o ;
n + ( i - 1 ) > 0 ;
assume sqrt ( 1 + t ^2 ) <= 1 ^2 ;
card B = k + 1 + 1 ;
x in union rng ( f | ( rng f ) ) ;
assume x in the carrier of R & y in the carrier of S ;
d in C ;
f . 1 = L . F ;
the vertices of G = { v } \/ { v } ;
let G be real-weighted connected _Graph ;
e , v2 , G , v , w , y is_collinear ;
c . ( i1 + 1 ) in rng c ;
f2 /* q is divergent to \hbox { - \infty $ } ;
set z1 = - ( z2 - z1 ) , z2 = - ( z2 - z2 ) ;
assume w is llllof S , G ;
set f = p \! \mathop { t } , g = p \! \mathop { t } ;
let c be object of C ;
assume ex a st P [ a ] ;
let x be Element of REAL m m m -tuples_on the carrier of K ;
let I1 be Subset-Family of X ;
reconsider p = p as Element of NAT ;
v , w as Point of X ;
let s be State of SCM+FSA , p be Polynomial of SCM+FSA ;
p is finite & q is halting implies p is halting
stop I c= P +* ( l , n ) ;
set ci = f /. i , ci = f /. ( i + 1 ) ;
w ^ t ^ w ^ t ^ w ^ t ^ w ^ t ^ w ^ t ^ w ^ t ^ w ^ t ^ w ^ t ^ w ^ t ^ w ^ t ^ w ^
W1 /\ W = W1 /\ W2 /\ W2 ;
f . j is Element of J . j ;
let x , y be Element of T2 ;
ex d st a , b // b , d ;
a <> 0 & b <> 0 implies c <> 0
ord x = 1 & x is \sum & x is \sum & x is \sum ;
set g2 = lim ( ( lim ( s ) ) (#) ( f1 /* s ) ) ;
2 * x >= 2 * sqrt ( 1 + ( 2 * x ) ^2 ) ;
assume ( a 'or' c ) . z <> TRUE ;
f (*) g in Hom ( c , c ) ;
Hom ( c , d + c ) <> {} ;
assume 2 * Sum ( q | m ) > m ;
L1 . ( F . ( F . k ) ) = 0 ;
R1 \/ R1 = ( R1 + R2 ) \/ ( R2 + R1 ) ;
( ( - sin ) `| Z ) . x <> 0 ;
( ( ( ( exp_R * exp_R ) ) `| Z ) . x ) > 0 ;
o1 in [: X , O :] /\ [: O , O :] ;
e , v2 , G , v , w , y is_collinear ;
s3 > sqrt ( 1 - 0 ) * 0 ;
x in P .: ( F " ( F " ( f " ) ) ) ;
let J be closed closed closed Subset of R , K be Subset of R ;
h . p1 = f2 . O & f2 . O = f2 . O ;
Index ( p , f ) + 1 <= j ;
len q = width M & width q = width M ;
the carrier of Lin K c= A ;
dom f c= union rng ( F | X ) ;
k + 1 in support ( ( support n ) \ ( support m ) ) ;
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 Point of REAL ;
sqrt ( 1 / m ) + r < p ;
dom f = dom ( I * ( J * F ) ) ;
[#] ( ( TOP-REAL 2 ) | P ) = [#] ( ( TOP-REAL 2 ) | P ) ;
cluster - x -> real for ExtReal ;
then { d } c= A ;
cluster [: TOP-REAL n , TOP-REAL n :] -> finite-ind for finite-ind ;
let w1 be Element of M ;
let x be Element of dyadic ( n ) ;
u in W1 & v in W2 & u in W2 implies v + u in W1 + W2
reconsider y = y as Element of L2 ;
N is full full full full SubRelStr of T |^ N ;
sup { x , y } = c "\/" c ;
g . n = n |^ 1 .= n ;
h . J = EqClass ( u , J ) ;
let seq be summable sequence of X ;
dist ( x `1 , y ) < r / 2 ;
reconsider mm = m as Element of NAT ;
x- x0 < r1 - x0 & r1 - x0 < r1 - x0 ;
reconsider P ` = P as strict Subgroup of N ;
set g1 = p * idseq ( q `1 ) ;
let n , m , k be non zero Nat ;
assume that 0 < e and f | A is lower ;
D2 . ( I1 . I2 ) in { x } ;
cluster -> subcondensed for Subset of T ;
let P be compact non empty compact Subset of TOP-REAL 2 , p , q be Point of TOP-REAL 2 ;
Gik in LSeg ( \pi , 1 ) /\ LSeg ( \pi , 1 ) ;
let n be Element of NAT , x be Element of NAT ;
reconsider S8 = S 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 ( { {} } ) c= { [ {} , {} ] } ;
reconsider m = m2 as Element of NAT ;
reconsider d = x as Element of COMPLEX ;
let s be 0 -started State of SCMPDS , p be Point of SCMPDS ;
let t be 0 -started State of SCMPDS ;
b , b , x is_collinear & x , y , x is_collinear ;
assume that i = n \/ { n } and j = k \/ { n } ;
let f be PartFunc of X , Y ;
N2 >= sqrt ( c ^2 - sqrt ( c ^2 - 4 ) ) ;
reconsider t7 = T " as TopSpace ;
set q = h * p ^ <* d *> ;
z2 in U . ( y2 /\ Q ) /\ Q . ( y2 /\ Q ) ;
A |^ 0 = { <* \rangle *> } ;
len W2 = len W + len W2 + len W1 ;
len h2 in dom h2 & h2 . 1 = h2 . ( len h2 ) ;
i + 1 in Seg ( len s2 ) & i + 1 <= len s2 ;
z in dom g1 /\ dom f ;
assume p2 = W-min ( K ) & p2 = W-min ( K ) ;
len G + 1 <= i1 + 1 ;
f1 * f2 /* ( f1 /* ( h + c ) ) is convergent ;
cluster ( seq + seq1 ) + ( seq + seq1 ) -> summable ;
assume j in dom ( M1 /. i ) ;
let A , B , C be Subset of X ;
x , y , z is_collinear & x , y , z is_collinear ;
b ^2 - ( 4 * a ) * ( 4 * a ) >= 0 ;
<* xx *> ^ <* y *> ^ <* y *> ^ x <=' x ;
a , b ] in { a , b } ;
len p2 is Element of NAT & len p2 = len p1 & len p1 = len p2 ;
ex x being element st x in dom R & x in X ;
len q = len ( K (#) G ) ;
s1 = Initialize ( ( Initialized s ) +* ( k + 1 ) ) ;
consider w be Nat such that q = z + w ;
x ` ` is ` & x ` ` is ` ;
k = 0 & n <> k or k > n ;
then X is discrete for X being Subset of X ;
for x st x in L holds x is finite
||. f /. c .|| <= r1 & ||. f /. c .|| <= r1 ;
c in ]. p , q .[ & not c in { p } ;
reconsider V = V as Subset of the carrier of n , the carrier of n ;
N , M are_upper \ L ;
then z >= waybelow x & z >= f . x ;
M [. f , g .] = f & M [. g , h .] = g ;
( ( to_power 1 ) ) /. 1 = TRUE ;
dom g = dom f /\ X ;
mode \upupharpoons of G , V -> \upupharpoons of G ;
[ i , j ] in Indices M & [ i , j ] in Indices M implies M * ( i , j ) = M * ( i , j )
reconsider s = x " as Element of H ;
let f be Element of dom ( the Sorts of A ) ;
F1 . a1 , F1 . a1 - F2 . a1 - F2 . a1 = G1 . a1 - G1 . a1 ;
cluster circle ( a , b , r ) -> compact ;
let a , b , c , d be Real ;
rng s c= dom ( 1 / 2 ) \ ( dom ( f ^ ) " { 0 } ) ;
( curry ( F , w ) ) . k is additive ;
set k2 = card ( dom B ) , k1 = card ( dom B ) , k2 = card ( dom B ) ;
set G = Sym ( X , Y ) ;
reconsider a = [ x , s ] as terminal of G ;
let a , b be Element of M , M be Matrix of n , REAL ;
reconsider s1 = s as Element of S0 ( S ) ;
rng p c= the carrier of L & the carrier of L c= the carrier of L ;
let d be Subset of the Sorts of A ;
( x | x ) = 0 iff x = 0. W ;
I1 in dom ( stop I ) ;
let g be continuous Function of X | B , Y ;
reconsider D = Y as Subset of TOP-REAL n ;
reconsider i0 = len p1 - 1 as Integer ;
dom f = the carrier of S & rng f = the carrier of T ;
rng h c= union ( ( the carrier of J ) * ( the carrier of J ) ) ;
cluster All ( x , H ) -> \bf yielding ;
d * N1 / ( N1 * N2 ) > N1 * 1 / ( N1 * N2 ) ;
]. a , b .[ c= [. a , b .] ;
set g = f " | ( D1 | j1 ) ;
dom ( p | [: NAT , NAT :] ) = [: NAT , NAT :] ;
3 + - 2 <= k + - 2 + - 2 ;
tan is_differentiable_in ( ( tan * tan ) `| Z ) . x ;
x in rng ( f /^ p ) ;
let f , g be FinSequence of D ;
p in the carrier of S1 & q in the carrier of S1 & p in the carrier of S1 ;
rng f " { f " { f . x } = dom f /\ dom f ;
( the Target of G ) . e = v ;
width G - 1 < width G - 1 & width G - 1 <= width G ;
assume v in rng ( S | E ) ;
assume x is root or x is root ;
assume 0 in rng ( g2 | A ) ;
let q be Point of TOP-REAL 2 , p , q be Point of TOP-REAL 2 ;
let p be Point of TOP-REAL 2 , q be Point of TOP-REAL 2 ;
dist ( O , u ) <= |. p2 .| + 1 ;
assume dist ( x , b ) < dist ( a , b ) ;
<* S7 *> is Element of the carrier of C-20 ;
i <= len ( ( G _ { i2 -' 1 , j2 -' 1 } ) ) + 1 ;
let p be Point of TOP-REAL 2 , q be Point of TOP-REAL 2 ;
x1 in the carrier of I[01] & x2 in the carrier of I[01] ;
set p1 = f /. i , p2 = f /. ( i + 1 ) ;
g in { g2 : r < g2 & g2 < x0 } ;
Q = Snnn8 ( Q ) " ;
( ( 1 / 2 ) to_power ( n + 1 ) ) is summable ;
- p + I c= - p + - A ;
n < LifeSpan ( P1 , s1 ) + 1 ;
CurInstr ( p1 , Comput ( p1 , s1 , i ) ) = i ;
A /\ Cl { x } \ { x } <> {} ;
rng f c= ]. r , s + 1 .[ ;
let g be Function of S , V ;
let f be Function of L1 , L2 , L2 be Function of L1 , L2 ;
reconsider z = z as Element of [: L , 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 subcategory ;
reconsider V1 = V as Subset of X | B ;
attr p is valid means : Def6 : All ( x , p ) is valid ;
assume that X c= dom f and f .: X c= dom g ;
H |^ a " is Subgroup of H ;
let A1 be Element of O , A2 be Element of E ;
p2 , r2 , p3 is_collinear & q2 , q2 , p3 is_collinear ;
consider x being element such that x in v ^ K ;
not x in { 0. TOP-REAL 2 } ;
p in [#] ( I[01] | ( ( TOP-REAL 2 ) | B ) | D ) ;
0 . ( M . E ) < M . ( E . F ) ;
op ( c , c ) / ( id the carrier of C ) = c ;
consider c being element such that [ a , c ] in G ;
a1 in dom ( F . ( s2 . n ) ) ;
cluster -> consistent -> consistent for distributive LATTICE of L ;
set i1 = the Element of NAT , i2 = the Element of NAT , j2 = the Element of NAT ;
let s be 0 -started State of SCM+FSA ;
assume y in ( f1 \/ f2 ) .: A ;
f . len f = f /. len f .= f /. len f ;
x , f . x '||' f . x , f . y ;
attr X c= Y means : Def6 : cos ( X ) c= cos ( Y ) ;
let y be upper bound of Y , x , y ;
cluster ( x `1 ) / 2 -> non trivial for \mathfrak of S ;
set S = <* Bags n , i9 *> ;
set T = [. 0 , PI / 2 .] ;
1 in dom mid ( f , 1 , 1 ) ;
sqrt ( 4 * PI ) < sqrt ( 2 * PI ) ;
x2 in dom ( f1 + f2 ) /\ dom ( f1 + f2 ) ;
O c= dom I & { {} } c= dom I ;
( the Target 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 be Element of G opp ;
h19 . i = f . ( h . i ) ;
( p `1 ) ^2 = ( p `1 ) ^2 .= ( p `2 ) ^2 ;
i + 1 <= len Cage ( C , n ) ;
len <* P *> ^ <* P *> = len P & len P = len P ;
set NNN = the consider of the connectives of N , the Sorts of A ;
len g-2 + ( x + 1 ) <= x ;
a on B & b on C ;
reconsider r-12 = r * I . v as FinSequence of NAT ;
consider d such that x = d and a _|_ d ;
given u such that u in W and x = v + u ;
len f /. n = len ( f /^ n ) ;
set q2 = ( N-min C ) .. Cage ( C , n ) ;
set S = LSeg ( S1 , S2 ) , T = LSeg ( S1 , S2 ) ;
MaxADSet ( b ) c= MaxADSet ( P /\ Q ) ;
Cl ( G . q1 ) c= F . r2 ;
f " ( D ) meets h " ( h " ( V ) ) ;
reconsider D = E as non empty directed Subset of L1 ;
H = ( H '&' H ) '&' ( H '&' H ) ;
assume t is Element of ( \mathfrak F ) . X ;
rng f c= the carrier of S2 & rng f c= the carrier of S2 ;
consider y being Element of X such that x = { y } ;
f1 . a1 , b1 // b1 , c1 ;
the carrier of G = E \/ { E } ;
reconsider m = len - k as Element of NAT ;
set S1 = LSeg ( n , UMP ) , S2 = LSeg ( n , q ) ;
[ i , j ] in Indices ( - M1 ) & [ i , j ] in Indices ( - M ) ;
assume that P c= Seg m and M is linearly-independent ;
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 .= p * L /. 1 ;
pU . i = pU . i .= pU . i ;
let P , Q be Subset of Y ;
attr 0 < r & 1 < 1 & r < 1 ;
rng \lbrace proj ( a , X ) . i , proj ( X , Y ) . i } = [#] ( ( the Sorts of Y ) . i ) ;
reconsider x = x , y = y 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 ( ( ( s ) | ( len s ) ) ) = card ( s ) ;
reconsider x2 = x1 as Element of L2 ( ) ;
Q in FinMeetCl ( ( the topology of X ) | ( the topology of Y ) ) ;
dom ( f | X ) c= dom ( u | X ) & dom ( f | X ) c= dom u /\ X ;
pred n divides m & m divides n ;
reconsider x = x as Point of I[01] , y = x as Point of I[01] ;
a in D2 & D2 in D2 implies a in D2 & b in D2 & a in D2 & b in D2
not x0 in the still of f & not f in the still of f , the carrier' of f ;
Hom ( a , b ) <> {} & Hom ( b , c ) <> {} ;
consider k1 such that p " < k1 and p " < k1 and p " < k1 ;
consider c , d such that dom f = c \ d ;
[ x , y ] in [: dom g , dom k :] & [ x , y ] in [: dom g , dom k :] ;
set S1 = \vert \vert \mathopen { \vert } ( x , y , z ) .| ;
l = m2 & l = m2 & l = m2 & l = m1 & l = m2 & l = m2 implies l = k
x0 in dom ( u | A ) /\ ( dom ( u | A ) \ ( v | A ) ) ;
reconsider p = x as Point of TOP-REAL 2 ;
I[01] = ( ( 1 - B ) * ( 1 - B ) ) | ( ( 1 - B ) * ( 1 - B ) ) ;
f . p3 <= f . ( f . p1 ) ;
( F . x ) `1 <= ( F . x ) `1 & ( F . x ) `1 <= ( F . x ) `1 ;
( x `2 ) ^2 = ( W . ( x `1 ) ) ^2 .= ( W . ( x `2 ) ) ^2 ;
for n being Element of NAT holds P [ n ] ;
J , K be non empty Subset of I ;
assume 1 <= i & i <= len <* a " *> ;
0 |-> a = <*> the carrier of K ;
X . i in 2 -tuples_on B . i \ B . i ;
<* 0 *> in dom ( e --> [ 1 , 0 ] ) ;
then P [ a ] implies P [ succ a ] ;
reconsider s\mathclose { -1 } = ( smax ( D , E ) ) . s as terminal of D ;
- ( i - 1 ) <= len - j ;
[#] S c= [#] ( T | S ) & the TopStruct of T c= the TopStruct of T ;
for V being strict RealUnitarySpace holds V in strict Subspace of V implies V in strict Subspace of V
assume k in dom mid ( f , i , j ) ;
let P be non empty Subset of TOP-REAL 2 , p , q be Point of TOP-REAL 2 ;
let A , B be Matrix of K ;
- a * ( - b ) = a * b ;
for A being Subset of Subset of Subset of Subset ( A ) holds A // A ;
id ( o o ) in <* o2 , o1 , o2 *> ;
then ||. x .|| = 0 & x = 0. X ;
let N1 , N2 be strict normal Subgroup of G ;
j >= len ( upper_volume ( g , D1 ) ) + len ( upper_volume ( g , D1 ) ) ;
b = Q . ( len Q + 1 ) + 1 ;
f2 * ( f1 /* s ) /* ( seq ^\ k ) is divergent_to+infty ;
reconsider h = f * g as Function of [: I[01] , I[01] :] , G ;
assume that a <> 0 and Polynom ( a , b , c , d ) >= 0 ;
[ t , t ] in the InternalRel of A & [ t , t ] in the InternalRel of A ;
( v |-- E ) | n is Element of ( T . n ) -tuples_on the carrier of T ;
{} = the carrier of L1 + ( L2 + L2 ) .= the carrier of L1 + ( L2 + L2 ) ;
Directed I is_halting_on Initialized s , P & Directed I is_halting_on Initialized s , P ;
Initialized ( p +* q ) = Initialize ( ( p +* q ) +* ( q +* ( q +* p ) ) ) ;
reconsider N2 = N1 as strict net of N , N2 ;
reconsider Y = Y as Element of <* <* \subseteq \rangle , \subseteq \rangle ;
\bigsqcap ( p , p \ { p } ) <> p ;
consider j being Nat such that i2 = i1 + j and j in dom f ;
[ s , 0 ] in the carrier of S2 & [ s , 0 ] in the carrier of S2 ;
m in ( B '&' C ) \ D ;
n <= len ( ( P . n ) + len ( P . n ) ) + len ( P . n ) ;
( x1 - x2 ) `1 = ( x2 - y2 ) `1 .= ( x2 - y2 ) `1 ;
InputVertices S = { x1 , x2 , x3 , x4 , x5 , x5 , x5 , x5 , x5 } ;
let x , y be Element of FFFA1 : x in F . n ;
p = |[ p `1 , p `2 ]| .= |[ p `1 , p `2 ]| ;
g * 1_ G = h " * g " * g " * h " * h " * h " * h " ;
let p , q be Element of PFuncs ( V , C ) ;
x0 in dom ( f1 + f2 ) /\ dom ( f1 + f2 ) ;
( R qua Function ) " = R " * ( R * ( R * ( R * S ) ) ) ;
n in Seg len ( f /^ n ) .= dom ( f /^ n ) ;
for s be Real st s in R holds s <= s2 & s <= s2 ;
rng s c= dom ( f2 * f1 ) /\ dom ( f2 * f1 ) ;
synonym ( ex r being Element of Fin X st r in ( Seg n ) & r in ( Seg n ) ;
1_ K * 1_ K = 1_ K * 1_ K .= 1_ K * 1_ K ;
set S = Segm ( A , A1 , B1 , B2 , B1 , B2 ) ;
ex w st e = sqrt ( w ) & w in F & w in G ;
curry ( P\rbrack , k ) # x is convergent ;
cluster -> open for Subset of [: T , T :] ;
len f1 = 1 .= len ( f1 ^ f2 ) .= len f1 + len f2 .= len f1 + len f2 ;
sqrt ( i * p ) < sqrt ( 2 * p ) ;
let x , y be Element of ( the carrier of U1 ) \/ ( the carrier of U2 ) ;
b1 , c1 // b9 , c9 & not o , c1 // b9 , c9 ;
consider p being element such that c1 . j = { p } ;
assume that f " { 0 } = {} and f " { 0 } = {} ;
assume IC Comput ( F , s , k ) = n ;
Reloc ( J , card I ) does not destroy a ;
Macro ( card I + 1 ) does not destroy c ;
set m2 = LifeSpan ( p3 , Comput ( p3 , s3 , m1 ) ) , E = P +* I , F = P +* I , M = LifeSpan ( p3 , s3 ) ;
IC Comput ( P , s , i ) in dom Initialize ( ( Initialize ( s ) ) . f ) ;
dom t = the carrier of ( SCM R ) ;
( ( E-max L~ f ) .. f ) .. f = 1 ;
let a , b be Element of PFuncs ( V , C ) ;
Cl ( union F ) c= Cl ( union F ) ;
the carrier of X1 union X2 misses A1 \/ A2 ;
assume not LIN a , f . ( a , f . a ) , g . ( a , g . a ) ;
consider i be Element of M such that i = d and i in d ;
then Y c= { x } or Y = {} ;
M , v / ( y , x ) / ( y , x ) / ( y , x ) / ( y , x ) / ( y , x ) / ( y , x ) / ( y , x ) / ( y , x ) / (
consider m being element such that m in Intersect ( F . m ) ;
reconsider A1 = ( support u1 ) \/ ( support v1 ) as Subset of X ;
card ( A \/ B ) = k-1 + ( 2 * 1 ) ;
assume that a1 <> a3 and a2 <> a4 and a3 <> a4 and a4 <> a4 and a4 <> a4 and a4 <> a4 and a4 <> a4 and a4 <> a4 and a4 <> a4 and a4 <> a4 and a4 <> a4 and a4 <> a4 and a4 <> a4 and a4 <> a4
cluster s \! \mathop { \rm \hbox { - } \vert V } -> |. S .| -\mathop { \rm \hbox { - } \vert } ;
Ln2 /. ( n2 + 1 ) = Lh2 . ( n2 + 1 ) ;
let P be compact non empty Subset of TOP-REAL 2 ;
assume that r in LSeg ( p1 , p2 ) and r in LSeg ( p1 , p2 ) and p in LSeg ( p2 , p3 ) ;
let A be non empty compact Subset of TOP-REAL n , p , q be Point of TOP-REAL n ;
assume [ k , m ] in Indices ( ( - D ) * ( i , j ) ) ;
0 <= ( ( 1 / 2 ) |^ p ) * ( ( 1 / 2 ) |^ p ) ;
( F . N ) . x = +infty ;
attr X c= Y means : Def6 : Z c= V \ V & X \ V c= Y \ V ;
( y * z ) * ( z * w ) <> 0. I & ( y * z ) * ( z * w ) <> 0. I ;
1 + card ( X \ { w } ) <= card ( u \ { w } ) + card ( X \ { w } ) ;
set g = z \circlearrowleft ( L~ z ) , h = z .. z ;
then k = 1 implies p . k = <* x , y *> . k ;
cluster -> ( C , X ) for Element of C ( ) ;
reconsider B = A as non empty Subset of TOP-REAL n ;
let a , b , c be Function of Y , BOOLEAN ;
L1 . i = ( i .--> g ) . i .= g . i ;
Plane ( x1 , x2 , x3 , x4 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 ,
n <= indx ( D2 , D1 , j1 ) + 1 ;
( g2 . O ) `1 = ( - 1 ) * ( ( - 1 ) * ( - 1 ) ) `1 ;
j + p .. f - len f <= len f - len f ;
set W = W-min ( C ) , E = E-bound ( C ) ;
S1 . ( a , e ) = a + e .= a + e + e .= a + e ;
1 in Seg width ( M * ( ( p * ( q ) ) ) ) ;
dom ( i (#) Im ( f ) ) = dom ( Im ( f ) ) ;
CurInstr ( x `1 , x `2 ) = W . ( a , p . ( a , p ) ) ;
set Q = |= |= ( g , f ) , h = |= ( g , f ) ;
cluster -> stable for ManySortedSet of U1 ;
attr F = { A } means : Def1 : F is discrete ;
reconsider z9 = One as Element of product G ;
rng f c= rng ( f1 ^ f2 ) \/ rng ( f2 ^ ) ;
consider x such that x in f .: A and x in f .: C ;
f = <*> ( the carrier of F_Complex ) & f is one-to-one ;
E , v / ( x , y ) |= H / ( x , y ) ;
reconsider n1 = n as Morphism of o1 , o2 ;
assume that P is associative and R is associative and P * R = R * P ;
card ( B2 \/ { x } ) = card ( B2 \/ { x } ) ;
card ( x \ B1 ) /\ ( x \ B2 ) = 0 ;
g + R in { s : g-r < s & s < g } ;
set q9 = ( q , <* s *> ) -\hbox { - } , n = ( q , <* s *> ) \hbox { - } ;
for x being element st x in X holds x in rng f1 & x in rng f1 ;
h2 /. ( i + 1 ) = h2 . ( i + 1 ) ;
set \mathbb w = max ( B , min ( B , min ( C , max ( C , max ( C , max ( C , max ( C , l ) ) ) ) ) ) ) ;
t in Seg width ( I ^ ( n , n ) ) ;
reconsider X = dom f as Element of Fin C ( ) ;
IncAddr ( i , k ) = halt SCM+FSA + k .= ( l + k ) + k ;
( ( GoB f ) * ( i , j ) ) `2 <= ( GoB f ) * ( i , j ) `2 ;
attr R is condensed means : Def6 : for x being Element of R holds Cl R is condensed & Cl R is condensed ;
attr 0 <= a & a <= 1 & b <= 1 implies a * b <= 1 * a ;
u in ( ( c /\ ( ( d /\ b ) /\ e ) /\ f ) ) /\ j ;
u in ( ( c /\ ( ( d /\ e ) /\ f ) /\ j ) /\ f ) /\ j ) /\ f ;
len C + ( - 2 ) >= 9 + ( - 3 ) + ( - 3 ) ;
x , y , z is_collinear & x , y , z is_collinear ;
a |^ ( n1 + 1 ) = a |^ n1 * a |^ ( n1 + 1 ) ;
<* \underbrace ( 0 , \dots , 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 ,
set y1 = <* y , c *> ;
F /. 1 in rng Line ( D , 1 ) & F /. 1 in rng Line ( D , 1 ) ;
p . m joins r /. m , r /. ( m + 1 ) ;
( p `2 ) ^2 = ( f /. i1 ) `2 .= ( f /. i1 ) `2 ;
( W-min X ) \/ ( W-min X ) = ( W-min X ) \/ ( W-min X ) ;
0 + ( p `2 ) ^2 <= 2 * r + ( p `2 ) ^2 ;
x in dom g & not x in g " { 0 } ;
f1 /* ( seq ^\ k ) ^\ k is divergent to \hbox { x0 } ;
reconsider u2 = u as VECTOR of \bf Pmin ( X , Y ) ;
p \! \mathop { \rm \hbox { - } Sgm ( X ) } = 0 ;
len <* x *> < i + 1 + 1 ;
assume that I is non empty and { x } /\ { y } = {} ;
set i2 = card I + card J + card J + card I + card J + card J + card J + card J + card J + card J + card J + card J + card J + card J + card J + card J + card J + card J + card
x in { x , y } & h . x = {} implies h . x = {} ;
consider y being Element of F such that y in B and y <= x `1 ;
len S = len ( the charact of A ) & len ( the charact of A ) = len ( the charact of A ) ;
reconsider m = M , i = N as Element of X ;
A . ( j + 1 ) = B . ( j + 1 ) \/ A . j ;
set Nmin = : : : : : : : : : \leq ( G . n ) `1 <= ( G . n ) `1 ;
rng F c= the carrier of gr ( { a } ) & rng F c= the carrier of gr ( { a } ) ;
4 -1 ( F ( K ) , n , n ) is complex-valued FinSequence ;
f . k , f . ( n + 1 ) ] in rng f ;
h " ( P /\ [#] ( T | P ) ) /\ [#] ( T | P ) = f " ( f " P ) ;
g in dom ( f2 \ ( f2 " { 0 } ) ) \ ( f2 " { 0 } ) " { 0 } ;
gX /\ dom ( f1 | X ) = ( g1 | X ) " ( dom ( f1 | X ) ) ;
consider n being element such that n in NAT and Z = G . n ;
set d1 = \bf \bf L ( x1 , y1 , y2 ) , d2 = dist ( y1 , y2 ) ;
b `2 + sqrt ( 1 + ( 1 + ( 1 + 2 ) ) ^2 ) < 1 + ( 1 + ( 1 + 2 ) ) ^2 ;
reconsider f1 = f as VECTOR of the carrier of X ;
attr i <> 0 implies i |^ ( i + 1 ) mod ( i + 1 ) = 1 ;
j2 in Seg len ( g2 . i2 ) & j in Seg len ( g2 . i2 ) ;
dom ( i .--> ( 4 * a ) ) = dom ( i .--> ( 4 * a ) ) .= dom ( i .--> ( 4 * a ) ) .= dom ( i .--> a ) .= dom ( i .--> a ) .= dom ( i .--> a ) ;
cluster sec | ]. PI / 2 , PI / 2 .[ -> one-to-one for Function of REAL , REAL ;
Ball ( u , e ) = Ball ( f . p , e ) ;
reconsider x1 = x0 as Function of S , T ;
reconsider R1 = x , R2 = y as Relation of L ;
consider a , b being Subset of A such that x = [ a , b ] ;
( <* 1 *> ^ p ) ^ <* n *> ^ <* n *> in R ;
S1 +* S2 +* ( S1 +* S2 ) = S2 +* ( S2 +* S2 ) ;
( ( ( ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) ) (#) ( ( - 1 ) ) ) ) ) ) ) ) ) ) ) is_differentiable_on
cluster -> continuous for Function of C , REAL ;
set C7 = 1GateCircStr ( <* z , x *> , f3 ) ;
E . ( e1 + ( e2 + T ) ) = E . ( ( e1 + T ) ) -T . ( e1 + T ) ;
( ( ( arctan * ( f + g ) ) `| Z ) ) . x = ( ( arctan * ( f + g ) ) `| Z ) . x ;
sup A = \frac 3 * PI / 2 & lower_bound A = 0 ;
F ( dom f , - F ( - f ) ) is Functor of F ( - f , - F ( - f ) ) ;
reconsider p8 = q as Point of TOP-REAL 2 , q1 , q2 be Point of TOP-REAL 2 ;
g . W in [#] ( Y | 0 ) & [#] ( Y | 0 ) c= [#] ( Y | 0 ) ;
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2 ;
LSeg ( f ^ g , j ) = LSeg ( f , j ) /\ LSeg ( f , j ) ;
rng s c= dom f /\ ]. - r , x0 .[ & f | ]. - r , x0 .[ is continuous ;
assume x in { ( idseq 2 ) . ( ( TOP-REAL 2 ) . x ) } ;
reconsider n2 = n , m2 = m as Element of NAT ;
for y being ExtReal st y in rng seq holds g <= y & g <= y ;
for k st P [ k ] holds P [ k + 1 ]
m = m1 + m2 + m2 .= m1 + m2 + m2 + m2 + m2 ;
assume for n holds H1 . n = G . n -H . n ;
set BX = f .: ( the carrier of X1 ) , BX = f .: ( the carrier of X2 ) ;
ex d being Element of L st d in D & x << d ;
assume R " ( a " ) c= R " ( a " ) ;
t in ]. r , s .[ or t = r or t = s ;
z + v2 in W & x = u + ( z + v1 ) ;
x2 |-- ( y2 , y2 ) iff P [ x2 , y2 ] ;
pred x1 <> x2 & |. x1 - x2 .| > 0 & |. x1 - x2 .| < 0 ;
assume p2 - p1 , p3 - p1 - p3 - p3 , p1 - p3 - p1 - p3 - p3 - p1 - p3 - p3 - p1 , p2 - p3 - p3 - p3 - p3 , p1 - p3 - p3 - p3 - p1 , p2 - p3 - p3 - p3 - p1 , p2 - p3 - p3 - p1 - p3 - p3 - p3
set q = ( ex f st f ^ <* 'not' A *> ) ^ <* 'not' A *> ;
let f be PartFunc of REAL , REAL-NS 1 , REAL-NS n , r be Real ;
( n mod ( 2 * k ) ) ! = n mod k ;
dom ( T * ( succ t ) ) = dom dom ( T * ( succ t ) ) ;
consider x being element such that x in w and x in c and x in c ;
assume ( F * G ) . x3 = v . x3 & ( F * G ) . x3 = v . x3 ;
assume the Sorts of ( D1 ) c= the Sorts of ( D2 ) & the Sorts of ( D2 ) c= the Sorts of ( D1 ) ;
reconsider A1 = [. a , b .] as Subset of R^1 ;
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 ( C , n ) , q = Gauge ( C , n ) * ( i , j ) ;
n1 - len f + 1 - len g <= len g + len g - 1 ;
ConsecutiveDelta ( q , O ) = [ u , v , a ] & Q [ u , v ] ;
set C-2 = ( \mathclose { |[ a ]| } ) . ( k + 1 ) ;
Sum ( L (#) p ) = 0. R * Sum p .= 0. V * p . x .= 0. V ;
consider i being element such that i in dom p and t = p . i ;
defpred Q [ Nat ] means $1 = ( Q . $1 ) & ( Q . $1 ) = ( Q . $1 ) ;
set s3 = Comput ( P1 , s1 , k ) , P1 = Comput ( P1 , s1 , k ) ;
let l be k -Al of k , A , B be Element of l ;
reconsider U = union ( G . n ) as Subset-Family of ( T . n ) ;
consider r such that r > 0 and Ball ( p `1 , r ) c= Q ` ;
( h | ( n + 2 ) ) /. i = p29 . ( p /. i ) ;
reconsider B = the carrier of X1 union X2 as Subset of X ;
p9 = <* - ( c-16 . 1 ) , - ( c-16 . 1 ) *> ;
cluster f -> real-valued for Function of NAT , NAT ;
consider b being element such that b in dom F and a = F . b ;
x0 < card ( [: X , Y :] | [: X , Y :] ) + card ( [: Y , X :] | [: Y , X :] ) ;
attr X c= B1 , B2 , T means : Def6 : for B holds \mathop { \rm BU , B holds B is succ of X ;
then w in Ball ( x , r ) & dist ( x , w ) <= r ;
angle ( x , y , z ) = angle ( x , y , z ) ;
attr 1 <= len s means : Def6 : len s = len s & len s = 0 ;
f c= f . ( k + ( n + 1 ) ) ;
the carrier of { 1_ G } = { 1_ G } & the carrier of G = { 1_ G } ;
pred p '&' q in TAUT ( Al ) & q '&' p in TAUT ( Al ) ;
- ( t `2 / t `1 ) < ( - t `1 ) / t `1 ;
U . 1 = U /. 1 .= U . ( 1 ) .= U . ( 1 ) .= U . ( 1 ) ;
f .: ( the carrier of x ) = the carrier of x & f .: ( the carrier of x ) = the carrier of x ;
Indices ( O * ( O , j ) ) = [: Seg n , Seg n :] & [: O , Seg n :] = [: Seg n , Seg n :] ;
for n being Element of NAT holds G . n c= G . ( n + 1 ) ;
then V in M .: \square ex x being Element of M st V = { x } ;
ex f be Element of F st f is invertible & ( A * ) is Matrix of n , K ;
[ h . 0 , h . 3 ] in the InternalRel of G & [ h . 0 , h . 3 ] in the InternalRel of G ;
s +* ( ( intloc 0 ) .--> 1 ) = a3 +* ( ( intloc 0 ) .--> 1 ) ) ;
|[ w1 , v1 ]| + |[ v1 , v2 ]| <> 0. TOP-REAL 2 & |[ v1 , v2 ]| + |[ v2 , v1 ]| = |[ v2 , v2 ]| ;
reconsider t = t as Element of ( INT ( X ) ) -tuples_on the carrier of K ;
C \/ P c= [#] ( ( [#] ( ( ( ( G \ A ) \ A ) ) \ A ) ) ) ;
f " ( V ) in ( ( ( X ) /\ ( ( X , the carrier of V ) ) /\ ( the carrier of V ) ) ) /\ ( X , the carrier of V ) ;
x in [#] ( ( the carrier of F ) /\ A ) ;
g . x <= h1 . x & h . x <= h1 . x ;
InputVertices S = { xy , yz , yz , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , 8 } ;
for n being Nat st P [ n ] holds P [ n + 1 ]
set R = Line ( M , i ) * Line ( M , i ) ;
assume that M1 is being_line and M2 is being_line and M1 is being_line and M2 is being_line ;
reconsider a = ( f2 . i0 - 1 ) / ( i - 1 ) as Element of K ;
len ( ( ( Len F1 ) ^ ( F ^ F2 ) ) ) = Sum ( ( ( F ^ ( len F1 ) ) ^ ( F ^ F2 ) ) ) ;
len ( ( the an of n ) * ( i , j ) ) = n & ( i , j ) * ( i , j ) = n ;
dom max ( f + g ) = dom ( f + g ) /\ dom ( h + c ) ;
( the superior of ( Y ) ) . n = ( ( the Sorts of ( Y ) ) . n ) . n .= ( the Sorts of ( Y ) ) . n ;
dom ( p1 ^ p2 ) = dom ( f ^ p2 ) /\ dom ( f ^ ) ;
M . [ 1 , y ] = 1 * v1 .= ( 1 - 1 ) * v1 .= ( 1 - 1 ) * v2 .= ( 1 - 1 ) * v1 ;
assume that W is non trivial and W .last() c= the carrier of G2 and W is closed ;
C6 * ( i1 , j1 ) = G * ( i1 , j1 ) .= G * ( i1 , j1 ) ;
C8 |- 'not' All ( x , p ) 'or' p ( x , y ) ;
for b st b in rng g holds lower_bound rng fb <= b holds lower_bound fb <= b
- sqrt ( ( q `1 / |. q .| - sn ) / ( 1 + sn ) ) ^2 ) = 1 ^2 + ( q `2 / |. q .| - sn ) ^2 ;
( LSeg ( c , m ) \/ LSeg ( l , k ) ) \/ LSeg ( l , k ) c= R ;
consider p being element such that p in LSeg x and p in L~ f and x in L~ f ;
Indices ( X @ ) = [: Seg n , Seg n :] & [: Seg n , Seg n :] = [: Seg n , Seg n :] ;
cluster s => ( q => p ) -> valid for valid ;
Im ( ( Partial_Sums F ) . m ) is_measurable_on E ;
cluster f . ( x1 , x2 ) -> Element of D ( ) equals f . ( x1 , x2 ) ;
consider g being Function such that g = F . t and Q [ t , g . t ] ;
p in LSeg ( ( GoB f ) * ( i , j1 ) , ( GoB f ) * ( i , j1 ) ) ;
set R8 = R |^ ]. - 1 , + 1 .[ ;
IncAddr ( I , k ) = AddTo ( d , k ) .= CurInstr ( I , k ) ;
seq . m <= ( ( the Sorts of A1 ) . m ) . k & ( the Sorts of A2 ) . k <= ( the Sorts of A1 ) . k ;
a + b = ( a ` + b ` ) ` ` ` .= ( a ` + b ` ) ` ;
id ( X /\ Y ) = id ( X /\ Y ) /\ id ( X /\ Y ) ;
for x being element st x in dom h holds h . x = f . x ;
reconsider H = U1 \/ U2 as non empty Subset of U0 ;
u in ( ( c /\ ( ( d /\ e ) /\ f ) /\ j ) /\ j ) /\ m ;
consider y being element such that y in Y and P [ y , inf B ] ;
consider A being finite stable Subset of R such that card A = card ( \alpha ) and card A = card ( \alpha ) ;
p2 in rng ( f |-- p1 ) \ rng <* p1 *> & rng <* p1 *> \ rng <* p1 *> c= rng f \ rng <* p1 *> ;
len s1 > 0 & len s2 > 0 & len s1 > 0 & len s2 > 0 implies len s1 > 0 & len s2 > 0 & len s2 > 0
( ( N-min ( P ) ) ) `2 = ( E-max ( P ) ) `2 .= ( E-max ( P ) ) `2 .= ( E-max ( P ) ) `2 .= ( E-max ( P ) ) `2 ;
Ball ( e , r ) c= LeftComp ( Cage ( C , n + 1 ) ) ;
f . a1 ` ` ` = f . ( a1 ` ` ` ` ` ` ` ` ) ` .= ( f . a1 ` ) ` ` ` ;
( seq ^\ k ) . n in ]. - r , x0 .[ /\ ]. x0 , x0 + r .[ ;
gg . x0 = g . ( ( ( f . x0 ) | G ) . x0 ) .= ( g . x0 ) * ( f . x0 ) ;
the InternalRel of S is InternalRel of field ( the InternalRel of S ) & the InternalRel of S is reflexive ;
deffunc F ( Ordinal , Ordinal ) = phi ( $2 , $1 ) ;
F . ( s1 . a1 ) = F . ( s2 . a1 ) .= ( s2 . a1 ) * ( s2 . a1 ) ;
x `2 = A ( o ) .= Den ( o , A ( ) ) . a ;
Cl ( f " ( P1 /\ P1 ) ) c= f " ( f " ( P1 /\ P1 ) ) ;
FinMeetCl ( ( the topology of S ) | ( the topology of T ) ) c= the topology of T & the topology of T c= the topology of T ;
synonym o is constructor means : Def6 : o <> {} & o <> {} & o <> {} & o <> {} ;
assume that X + Y = Y + ( card X ) and card X <> card Y + card Y ;
the g1 of the InitS of s <= 1 + ( the InitS of s ) & the InitS of s = ( the InitS of s ) . ( len s ) ;
LIN a , a1 , d or b , c // b1 , c1 & b , c // c1 , c2 ;
e . 1 = 0 & e . 2 = 1 & e . 3 = 0 & e . 3 = 0 ;
E in SO & not E in { N } & E in { N } ;
set J = ( l , u ) \mathop { \rm \hbox { - } ;
set A1 = 1GateCircStr ( a9 , b9 , c9 ) , A2 = \vert a9 , c9 .| , C1 = |. b9 .| , C2 = |. b9 .| , C2 = |. b9 .| , C2 = |. a9 .| , C2 = |. b9 .| , C2 = |. b9 .| , C1 = |. b9 .| , C2 = |. b9 .| , C2 = |. b9 .| ;
set c9 = [ <* c9 , yz *> , <* cin , dp *> ] , xy = [ <* xy , yz *> , [ bm , cm ] ] , xy = [ <* xy , yz *> , [ xy , yz ] ] ;
x * z " * x " in x * ( z * N ) * x " ;
for x being element st x in dom f holds f . x = f3 . x & f . x = f3 . x ;
Int cell ( GoB f , 1 , G ) c= RightComp f \/ RightComp f \/ RightComp f \/ RightComp f ;
U is_an_arc_of W-min ( C ) , W-min ( C ) , W-min ( C ) ;
set f-17 = f .: @ g , @ f .: @ g ;
attr S1 is convergent means : Def6 : S1 is convergent & lim S1 = x0 & for n holds S1 . n = ( lim S1 ) * ( lim S2 ) ;
f . ( 0 + 1 ) = ( 0 qua Ordinal ) + a .= a ;
cluster reflexive transitive transitive for RelStr , P , Q be reflexive transitive transitive transitive reflexive reflexive transitive transitive transitive transitive reflexive reflexive transitive transitive transitive ;
consider d being element such that R reduces b , d and R reduces c , d ;
not b in dom Start-At ( ( card I + card J + 2 ) , SCMPDS ) ;
( z + a ) + x = z + ( a + y ) .= z + ( a + y ) ;
len ( l (#) ( a |^ 0 ) ) = len l & len ( l |^ 0 ) = len l ;
( t4 ) \setminus {} is ( {} , rng t ) -valued Function of ( rng t ) \ rng t ;
t = <* F . t *> ^ ( C . p ^ q ) ;
set p-2 = W-min ( C , n ) , pmin = Gauge ( C , n ) * ( i , j ) ;
k - ( i + 1 ) = ( k - 1 ) - ( i + 1 ) ;
consider u being Element of L such that u = u ` and u in D and u in D ;
len ( ( ( width G ) |-> a ) ) |-> ( len G ) ) = width ( ( width G ) --> a ) .= width ( ( width G ) --> a ) ;
F . x in dom ( G * ( the_arity_of o ) ) ;
set H2 = the carrier of H2 , H = the carrier of H2 , I = the carrier of H2 ;
set H1 = the carrier of H1 , H2 = the carrier of H2 , H2 = the carrier of H2 ;
( Comput ( P , s , 6 ) ) . intpos ( m + 6 ) = s . intpos ( m + 6 ) ;
IC Comput ( Q , t , k ) + ( l + 1 ) = l + ( l + 1 ) ;
dom ( ( ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( (
cluster <* l *> ^ phi -> ( 1 + 0 ) -element for string of S ;
set b5 = [ <* \hbox { \boldmath $ p $ } , 9 *> , and2 ] ;
Line ( Segm ( M , P , Q ) , x ) = L * Sgm Q * Sgm Q ;
n in dom ( ( the Sorts of A ) * ( the_arity_of o ) ) ;
cluster f1 + f2 -> continuous for PartFunc of REAL , REAL ;
consider y be Point of X such that a = y and ||. \mathopen { \Vert y \mathclose { \Vert } .|| <= r ;
set x3 = ( t . SBP ) . DataLoc ( ( s . SBP ) . SBP , 2 ) . DataLoc ( s . SBP ) ) ;
set pE = stop I , pE = stop I , pE = stop I , pE = stop I , pE = \cal I ;
consider a being Point of D2 such that a in W1 and b = g . a ;
{ A , B , C , D , E , F , J , M , N , M , N , N , N , N , M , N , N , N , M , N , N , M , N , N , N , M , N , N , N , M , N , N , M , N ,
let A , B , C , D , E , F , J , M , N , N , M , N , N , N , N , M , N , N , M , N , N , M , N , N , M , N , N , M , N , N , M , N , N , M ,
|. p2 .| ^2 - ( p2 `2 / |. p2 .| - sn ) ^2 >= 0 ;
l - 1 + 1 = l * ( l + 1 ) + ( l - 1 ) ;
x = v + ( a * w1 + ( b * w2 ) ) + ( c * w2 ) + ( c * w2 ) ;
the TopStruct of L = ( ( the topology of L ) | the topology of L ) | ( the topology of L ) ;
consider y being element such that y in dom H1 and x = H1 . y and y in H1 . y ;
( f \ { n } ) \ { n } = ( f \ { n } ) \ ( f \ { n } ) ;
for Y being Subset of X st Y is summable & Y is summable holds Y is not empty iff Y is not empty
2 * n in { N : 2 * Sum ( p | N ) > N } & N > 0 ;
for s being FinSequence holds len ( ( the { F } ) * ( the Arity of S ) ) = len s & ( the ResultSort of S ) * ( the ResultSort of 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 * f1 ) ) c= the carrier of ( TOP-REAL 2 ) | K1 ;
j + ( len f - len f ) <= len f + ( len f - len f ) ;
reconsider R1 = R * I as PartFunc of REAL , REAL n ;
C8 . x = s1 . ( |[ a , d ]| ) .= C8 . ( |[ a , d ]| ) .= C8 . ( |[ a , d ]| ) ;
power ( F_Complex , z ) . ( z , n ) = 1 .= x |^ n .= x |^ n ;
t -\mathop { > 0 ( C , s ) = f . ( the connectives of S ) . ( t , C ) ;
support ( f + g ) c= support f \/ support ( f + g ) /\ support ( f + g ) ;
ex N st N = j1 & 2 * Sum ( ( r * ( r * N ) ) ) > N ;
for y , p st P [ p ] holds P [ 'not' p ]
{ [ x1 , x2 ] } is Subset of [: X1 , X2 :] & { x1 , x2 } is Subset of [: X2 , Y2 :] ;
h = ( j |-- h ) . ( id B , id B ) .= H . ( id B ) .= H . ( id B ) ;
ex x1 be Element of G st x1 = x & x1 * N c= A & x1 * N c= A * N ;
set X = ( ConsecutiveDelta ( q , O ) ) . ( ( d , O ) . O ) , O = ( d , O ) . O ) ;
b . n in { g1 : x0 - r < g1 & g1 < x0 } ;
f /* ( s1 + c ) is convergent & f /. ( lim s1 ) = lim ( f /* s1 ) ;
the lattice of lattice Y = the lattice of lattice (# the carrier of Y , the carrier of X #) & the carrier of lattice = the carrier of lattice ;
'not' ( a . x ) '&' b . x 'or' 'not' ( a . x ) = TRUE ;
2 = len ( q ^ <* 0 *> ) + len ( q ^ <* 1 *> ) .= len ( q ^ <* 1 *> ) + len <* 1 *> ;
( ( 1 / a ) (#) ( ( sec * f1 ) - ( ( sec * f1 ) - ( tan * f2 ) ) ) ) `| Z ) = ( ( ( ( tan * f1 ) - ( tan * f2 ) ) ) `| Z ) ;
set K = upper upper ( f , A ) , H = integral ( f , H ) , K = integral ( f , H ) , H = integral ( f , H ) , I = integral ( f , H ) ;
assume e in { |[ w , w1 ]| : w1 in F & w2 in G & w1 in F & w2 in G } ;
reconsider d1 = dom a `2 , d2 = dom F as finite Subset of NAT ;
LSeg ( f , j ) .. f -' q = LSeg ( f , j ) + q .. f -' q .. f -' q .. f ;
assume X in { T ( N2 , K ) : h . ( N2 , K ) = N ( N2 , K ) } ;
assume Hom ( d , c ) <> {} & <* f , g *> * ( f , g ) = <* f , g *> * ( f , h ) ;
dom Sit = dom S /\ Seg n .= dom L /\ Seg n .= dom L /\ Seg n .= dom L /\ Seg n .= dom L /\ dom ( L | n ) .= dom L /\ dom ( L | n ) .= dom L /\ dom ( L | n ) .= dom L /\ dom L /\ dom L ;
x in H |^ a implies ex g st x = g |^ a & g in H |^ a & g in H |^ a ;
a * ( ( n , 1 ) * ( a , 1 ) ) = a * ( 0 , 1 ) .= a * ( 0 , 1 ) .= a * ( 0 , 1 ) ;
D2 . j in { r : lower_bound A <= r & r <= upper_bound A } ;
ex p being Point of TOP-REAL 2 st p = x & P [ p ] & p <> 0. TOP-REAL 2 ;
for c holds f . c <= g . c implies f ^ g tolerates f ^ g ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h ^ h
dom ( f1 (#) f2 ) /\ X c= dom ( f1 (#) f2 ) /\ X /\ dom ( f2 (#) f1 ) ;
1 = sqrt ( p * p ) .= p * sqrt ( 1 + ( p * q ) ^2 ) .= p * sqrt ( 1 + ( p * q ) ^2 ) ;
len g = len f + len <* x *> .= len f + len <* y *> .= len f + len <* y *> ;
dom ( F | [: N1 , N2 :] ) = [: N1 , N1 :] & dom ( F | [: N1 , N2 :] ) = [: N1 , N1 :] ;
dom ( f . t * I . t ) = dom ( ( f . t ) * ( g . t ) ) ;
assume a in ( "\/" ( ( T |^ \alpha ) ) .: D ) .: D ;
assume that g is one-to-one and ( the carrier of S ) /\ rng g c= dom g and g . ( g . x ) = g . ( g . x ) ;
( ( x \ y ) \ z ) \ ( ( x \ y ) \ z ) = 0. X ;
consider f such that f * f = id ( the carrier of b ) and f * f = id ( the carrier of b ) ;
( ( ( cos * f ) | [. 0 , PI / 2 .] ) ) | [. 0 , PI / 2 .] is increasing ;
Index ( p , co ) <= len LS - Index ( Gik , LS ) + 1 - Index ( Gik , LS ) + 1 - Index ( Gik , LS ) + 1 ;
t1 , t2 , t1 , t2 , t2 , t1 , t2 , t2 , t2 , t1 , t2 , t2 , t2 , t1 , t2 , t2 , t1 , t2 , t2 , t2 , t1 , t2 , t2 , t2 , t1 , t2 , t2 , t2 , t1 , t2 , t2 , t2 , t1 , t2 , t2 , t2 , t1 , t2 , t2 ,
( ( ( ( ( ( ( ( L ) ) ) ) . h ) ) . h ) . h ) . h <= ( ( ( ( the Sorts of ( ( the Sorts of ( L ) ) . h ) ) . h ) ) . h ;
then P [ f . i0 , f . x0 ] & F ( f . x0 + f . x0 ) < j ;
Q [ ( [ D . x , 1 ] ) `1 , F . ( [ D . x , 1 ] `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 Element of G . i ;
the Sorts of A2 = ( the Sorts of A2 ) --> ( the Sorts of A2 ) & the Sorts of ( the Sorts of A2 ) --> ( the Sorts of A1 ) ;
consider s being Function such that s is one-to-one and dom s = NAT and rng s c= { 0 } and rng s c= { 1 } ;
dist ( y1 , y2 ) <= dist ( y1 , y2 ) + dist ( a , y2 ) ;
( ( ex C , n st C /. len \mathop { \rm Cage ( C , n ) ) ) .. ( ( Cage ( C , n ) ) .. ( Cage ( C , n ) ) ) = len ( ( Cage ( C , n ) ) .. ( Cage ( C , n ) ) ) ;
q <= ( ( ( UMP C ) ) . ( len Gauge ( C , n ) ) ) `2 ;
LSeg ( f | i2 , i ) /\ LSeg ( f | i2 , j ) = {} ;
given a being Real such that a <= I and A = ]. a , b .] and A = ]. a , b .] ;
consider a , b being complex number such that z = a & y = b and z = a + b ;
set X = { b where b is Element of NAT : b in X & a < b } ;
( ( x * y ) \ z ) \ ( x \ y ) ) \ ( x \ z ) = 0. X ;
set xy = [ <* xy , yz , z *> , \vert yz , a4 ] , \vert a4 - a4 , x5 - a4 , \vert x5 - a4 , \vert x5 - a4 .| , \vert a4 - a4 .| ;
Carrier ( l ) /. len l = Carrier ( l ) . len l .= ( f /. len l ) * ( f /. len l ) ;
sqrt ( ( q `1 / |. q .| - sn ) / ( 1 + sn ) ) ^2 ) = 1 ^2 + ( q `2 / |. q .| - sn ) ^2 ;
sqrt ( ( p `1 / |. p .| - sn ) / ( 1 + sn ) ) ^2 ) < 1 / ( 1 + sn ) ^2 ;
( ( ( ( TOP-REAL 2 ) | X ) ) | X ) `2 = ( ( ( TOP-REAL 2 ) | X ) ) . p `2 .= ( ( TOP-REAL 2 ) | X ) . p ;
( ( ( s1 - ( s1 - ( lim s1 ) ) ) ) - ( ( lim s1 ) - ( lim s1 ) ) ) ) . k = ( ( s1 - ( lim s1 ) ) ) . k ;
rng ( ( h + c ) ^\ n ) c= dom SVF1 ( 1 , f , u0 ) ;
the carrier of X = the carrier of X & the carrier of X = the carrier of Y & the carrier of Y = the carrier of X ;
ex p3 st p3 = p3 & |. p3 - p3 .| = r & |. p3 - p3 .| = r ;
set h = \raise .4ex \hbox { $ \chi $ } , A , B , C , D ;
R |^ ( 0 * n ) = Ireal ( X , n ) .= R |^ n * R |^ n .= R |^ n * R |^ n ;
( Partial_Sums ( ( ( ( ( ( F ) ) . n ) ) ) . m ) ) . n ) . n is nonnegative ;
f2 = C7 . ( ( E8 ) . ( V , C ) ) .= ( C8 ) . ( ( V , C ) . ( V , C ) ) ;
S1 . b = s1 . b .= S2 . b .= S2 . b .= S2 . b ;
p2 in LSeg ( p2 , p1 ) /\ LSeg ( p1 , p2 ) \/ LSeg ( p2 , p3 ) /\ LSeg ( p3 , p2 ) ;
dom ( f . t ) = Seg n & dom ( I . t ) = Seg n & dom ( I . t ) = Seg n ;
assume o = ( the connectives of S ) . 11 & ( the connectives of S ) . 11 in ( the carrier' of S ) . 11 ;
set phi = ( l1 , l ) \mathop { \rm X , X = ( l , l ) \mathop { \rm \hbox { - } :] ;
synonym p is T means : Def6 : HT ( p , T ) = 1 ;
( Y1 `2 ) ^2 = ( - 1 ) * ( ( - 1 ) * ( ( - 1 ) * ( - 1 ) ) ) & ( - 1 ) * ( ( - 1 ) * ( - 1 ) ) <> 0. TOP-REAL 2 ;
defpred X [ Nat , set , set ] means P [ $1 , $2 , set ] means $2 = [ $1 , $2 ] ;
consider k be Nat such that for n be Nat st k <= n holds s . n < x0 + g . n ;
Det ( I ^ ( ( m -' n ) ) ) = ( 1_ K ) * ( ( m -' n ) ) .= 1_ K ;
sqrt ( ( - b ) ^2 - sqrt ( b ^2 - a ^2 ) ) < 0 ;
CQ . d = CQ . ( d , ( d . ( d . ( d . ( d . ( d . ( d . ( d . ( d . ( d . ( d . ( d . ( d . ( d . ( d . ( d . ( d . ( d . ( d . ( d . ( d . ( d . ( d . ( d . ( d . ( d . (
attr X1 is dense means : Def6 : X1 is dense & X2 is dense & X1 /\ X2 is dense implies X1 meet X2 is dense ;
deffunc F ( Element of E , Element of I , Element of I ) = ( $1 * $2 ) * ( $2 + $2 ) ;
t ^ <* n *> in { t ^ <* n *> : Q [ i , T ( ) ] } ;
( x \ y ) \ x = ( x \ x ) \ y .= y \ x ` .= y \ y ` ;
for X being non empty set holds X is Basis of [: X , Y :] iff X is Basis of [: X , Y :]
synonym A , B are_equipotent for A , B , C , D , E , F , J , M , N , N , N , N , N , M , N , N , N , M , N , N , M , N , N , M st M , N misses A & N , M misses B & M , N // N & M , N // N implies M , N // N & M ,
len ( M * p ) = len p & width ( M * p ) = width M & width ( M * p ) = width M & width ( M * p ) = width M ;
v2 = { x where x is Element of K : 0 < x & x < 1 } ;
( Sgm ( Seg m ) ) . d - ( Sgm ( Seg m ) ) . d - ( Sgm ( Seg m ) ) . e <> 0 ;
lower_bound divset ( D2 , k + indx ( D2 , D1 , k ) + 1 ) = D2 . ( k + 1 ) - indx ( D2 , D1 , k ) + 1 ) ;
g . r1 = ( - 2 * r1 + 1 ) * h + ( - 2 * r1 ) * h & dom h = [. 0 , 1 .] ;
|. a .| * ||. f .|| = 0 * ||. f .|| .= ||. a * f .|| .= ||. a * f .|| .= ||. a * f .|| .= ||. a * f .|| ;
f . x = ( h . x ) `1 & g . x = ( h . x ) `1 & g . x = ( h . x ) `1 ;
ex w st w in dom B1 & <* 1 *> ^ s = <* 1 *> ^ w ^ w ^ w ^ w ^ w ^ w ^ ( 1 + 1 ) ;
[ 1 , {} , <* d1 *> ] in ( ( { [ 0 , {} ] } \/ { {} } ) \/ { {} } ) \/ ( { {} } ) ;
IC Exec ( i , s1 ) + n = IC Exec ( i , s1 ) + n .= IC Exec ( i , s1 ) + n ;
IC Comput ( P , s , 1 ) = IC Comput ( P , s , 1 ) .= 5 + 1 .= 5 + 1 ;
( IExec ( W6 , Q , t ) ) . intpos ( i + 1 ) = t . intpos ( i + 1 ) ;
LSeg ( f , i ) misses LSeg ( f , i ) \/ LSeg ( f , j ) \/ LSeg ( f , j ) ;
assume for x , y being Element of L st x in C & y in C holds x <= y or y <= x ;
\int ( f ' _ \ast ( f ' _ \ast ( h + c ) ) ) .|| = f . ( ( f /* c ) - ( f /* c ) ) . n ;
for F , G being one-to-one FinSequence st rng F misses rng G & rng F misses rng G holds F ^ G is one-to-one
||. R /. ( L . h ) - R /. ( K . h ) .|| < e * ( K . h ) + e * ( K . h ) ;
assume a in { q where q is Element of M : dist ( z , q ) <= r & q <= r } ;
set p3 = |[ 2 , 1 ]| .--> |[ 0 , 1 ]| ;
consider x , y being Subset of X such that [ x , y ] in F and x c= d and y c= d and x in d and y in F and x in d ;
for y , x being Element of REAL st y in Y & x in Y & y in X & x in Y holds y <= x `1
func |. p ^ |. p .| -> ^ |. p .| -> ^ of A equals : Def6 : ( |. p .| ^ |. p .| ) ^ |. p .| ^ |. p .| ;
consider t being Element of S such that x , y '||' z , t and x , y '||' z , t and x , y '||' t , t ;
dom x1 = Seg len ( x1 ^ x2 ) & len ( x1 ^ x2 ) = len ( x1 ^ x2 ) & len ( x1 ^ x2 ) = len ( x1 ^ x2 ) ;
consider y2 being Real such that x2 = y2 and 0 <= y2 and y2 <= 1 and 0 <= y2 and y2 <= 1 and p `2 <= 1 and p `2 <= ( ( - 1 ) * ( - 1 ) ) `2 ;
||. f /* ( ( f /* ( s1 + s1 ) ) - f /* ( s1 + s2 ) .|| ) = ||. f /* ( s1 + s2 ) .|| ;
( the InternalRel of A ) ` ` /\ ( the InternalRel of A ) ` = {} ( {} ( A ) ) ` .= {} ( A ) ` .= {} ( A ) ` ;
assume that i in dom p and for j being Nat st j in dom q holds P [ j , i ] and for j being Nat st j in dom p holds P [ j , i ] ;
reconsider h = f | [: X , Y :] as Function of [: X , Y :] , Y ;
u1 in the carrier of W1 & u2 in the carrier of W2 & v2 in the carrier of W1 & u in the carrier of W2 & u in the carrier of W2 & v in the carrier of W1 & u in the carrier of W2 implies u1 + u2 in the carrier of W1 & u1 + u2 in the carrier of W2
defpred P [ Element of L ] means M . $1 <= f . $1 & f . $1 <= f . $1 ;
T . ( u , a , v ) = s * x + ( - ( s . x ) + ( - ( s . x ) ) ) .= b ;
- ( x - y ) = - x + ( - y ) .= - x + ( - x ) .= - x + ( - y ) .= - x + ( - y ) .= - x + ( - y ) .= - x + ( - y ) .= - x + ( - y ) .= - x + ( - y ) ;
given a being Point of Gsuch that for x being Point of Gholds a . x = x and a is not empty ;
f\sqcup f2 = [ [ dom ( ( f . O ) , cod ( f . O ) ] , [ f . O ] ] , [ f . O , [ f . O ] ] ] , [ f . O ] , [ f . O ] ] ] , [ f . O ] ] ;
for k , n being Nat st k <> 0 & k < n & k < n & k <= n holds k |^ n is prime
for x being element holds x in A |^ d iff x in ( A ` ) ` & x in ( A ` ) `
consider u , v being Element of R such that l /. i = u * v and l /. i = a * v ;
sqrt ( ( sqrt ( ( p `1 / |. p .| - sn ) / ( 1 + sn ) ) / ( 1 + sn ) ) ^2 ) > 0 ;
L-13 . k = LF . ( F . k ) & F . ( F . k ) in dom ( L * F ) ;
set i2 = AddTo ( a , i , n ) , i2 = AddTo ( a , i , n ) ;
attr B is consistent means : Def6 : for S holds S ( S , x ) = ( B ( S ) ) . S & S ( S ) . x = ( B ( S ) ) . x ;
a9 " D = { a "/\" d where d is Element of N : d in D & d in D } ;
| ( ( \square | ( q | q ) ) ) . b - ( ( q | q ) . b ) >= | ( dom ( ( q | q ) | ( q | q ) ) ) . b ;
( - f ) . ( sup A ) = ( - f ) . ( sup A ) .= ( - f ) . ( sup A ) ;
( G * ( len G , j ) ) `1 = ( G * ( len G , j ) ) `1 .= ( G * ( len G , j ) ) `1 .= ( G * ( len G , j ) ) `1 ;
( Proj ( i , n ) ) . L = <* ( proj ( i , n ) ) . L *> . ( <* proj ( i , n ) . L *> ) . ( <* proj ( i , n ) . L *> ) ;
f1 + f2 * reproj ( i , x ) is_differentiable_in ( ( f1 + f2 ) * reproj ( i , x ) ) . x ;
attr ( ( ( for x st x in Z holds ( ( exp_R * exp_R ) `| Z ) ) `| Z ) . x = ( exp_R * exp_R ) . x + ( exp_R * exp_R ) . x ;
ex t being SortSymbol of S st t = s & ( h1 . t ) . x = h2 . x & ( h2 . t ) . x = h2 . x ;
defpred C [ Nat ] means ( P . $1 ) is consistent & ( P . $1 ) is consistent ) & ( P . $1 ) is \vert ;
consider y being element such that y in dom ( p . i ) and q . i = ( p . i ) . y ;
reconsider L = product ( { x1 } ) ^ ( ( index B ) ^ ( index A ) ) as Basis of A ;
for c being Element of C holds T . ( id c ) = id ( the carrier of C ) & T . ( id c ) = id ( the carrier of C ) ;
LIN f . n , p ^ <* p *> , q ^ <* p *> .= f ^ <* p *> ^ <* q *> ;
( f * g ) . x = f . ( g . x ) & ( f * h ) . x = f . ( h . x ) ;
p in { |[ 1 / 2 * ( G * ( i + 1 , j + 1 ) `2 ]| } ;
f `2 - p `2 = ( ( c | n ) *' ) . ( - p `2 ) .= ( ( c - n ) *' ) . ( - p `2 ) .= ( ( c - n ) *' ) . ( - p `2 ) .= ( ( - n ) *' ) . ( - p `2 ) .= ( - n ) *' ;
consider r be Real such that r in rng ( f | divset ( D , j ) ) and r < m + s ;
f1 . [ ( ( ( ( r - 8 ) / 2 ) * ( ( r - 8 ) / 2 ) ) * ( ( r - 8 ) / 2 ) ) , ( ( r - 8 ) / 2 ) * ( ( r - 8 ) / 2 ) ) , ( ( r - 8 ) / 2 ) * ( ( r - 8 ) / 2 ) ) ] in f1 .: ( ( r - 8 ) / 2 ) ;
eval ( a | n , x ) = eval ( a | n , x ) .= a . ( x | n ) .= a . x ;
z = DigA ( t9 , x ) .= DigA ( t9 , x ) .= DigA ( t9 , x ) .= DigA ( t9 , x ) ;
set H = { Intersect ( S ) where S is Subset-Family of X : S is closed & S is closed } ;
consider S19 being Element of D ( ) , d being Element of D ( ) such that S = S19 ^ <* d *> and d in S ( ) and d in S ( ) and d in S ( ) ;
assume that x1 in dom f and x2 in dom f and f . x1 = f . x2 and f . x2 = f . x2 ;
- 1 <= sqrt ( ( q `1 / |. q .| - sn ) / ( 1 + sn ) ) ^2 ) ;
Carrier ( K ) is Linear_Combination of A & Sum ( K ) = 0. K & Sum ( K ) = 0. K & Sum ( L ) = 0. K ;
let k1 , k2 , k1 , k2 , k2 , x4 , x5 , J , M , M , N , N , M , N , N , M , N , N , M , N , N , M , N , N , M , N , N , M , N , N , M be Element of NAT ;
consider j being element such that j in dom a and j in g " { k } and x = a . j ;
H1 . x1 c= H1 . x2 or H1 . x2 c= H1 . x2 or H1 . x2 c= H1 . x2 ;
consider a being Real such that p = a * p1 + ( a * p2 ) and 0 <= a and a <= 1 and a <= 1 ;
assume that a <= c and d <= b and [ a , b ] c= dom f and [ a , b ] c= dom g and g . a = g . b ;
cell ( Gauge ( C , m ) , m -' 1 , width Gauge ( C , m ) -' 1 ) is non empty ;
A5 in { ( S . i ) `1 where i is Element of NAT : i in dom ( S . i ) `1 & ( S . i ) `2 <= ( S . i ) `2 } ;
( T * b1 ) . y = L * ( b2 . y ) .= ( F * b2 ) . y .= ( F * b2 ) . y ;
g . ( s , I ) . x = s . y & g . ( s , I ) . y = |. s . x .| ;
( log ( 2 , k ) ) ^2 + ( log ( 2 , k ) ) ^2 >= ( log ( 2 , k ) ) ^2 ;
then that p => q in S and not x in the still of p and not p => q in the still of p ;
dom ( the succ of ( r , the InitS of ( r , the InitS of ( r , the InitS of ( r , the InitS of ( r , the InitS of ( r , the Sorts of ( r , the Sorts of ( r , the Sorts of ( r , the Sorts of ( r , the Sorts of ( r , the Sorts of ( r , the Sorts of ( r , the Sorts of ( r , the Sorts of ( r , the Sorts of ( r ,
cluster f -> extended real for Function of rng f , REAL ;
assume for a being Element of D holds f . { a } = a & f . ( f .: { a } ) = f . ( union X ) ;
i = len p1 .= len p1 + len p3 .= len p3 + len p3 .= len p3 + len p3 + len p3 .= len p3 + len p3 + p3 .= len p3 + p3 + p3 + p3 + p3 + p3 + p3 + p3 + p3 + p3 + p3 + p3 + p1 + p3 + p3 + p3 + p3 + p3 + p3 + p3 + p3 + p3 + p3 + p3 + p3 + p3 + p3 + p3 + F + F + F + F + p3 .= F + p3
( l /. 3 ) `1 = ( g /. 3 ) `1 + ( g /. 3 ) `1 .= ( g /. 3 ) `1 + ( g /. 3 ) `1 .= ( g /. 3 ) `1 + ( g /. 3 ) `1 .= ( g /. 3 ) `1 + ( g /. 3 ) `1 ;
CurInstr ( P2 , Comput ( P2 , s2 , l ) ) = halt SCM+FSA .= halt SCM+FSA .= IC Comput ( P2 , s2 , l ) ;
assume for n be Nat holds ||. ( seq . n ) - ( seq . n ) .|| <= ( ||. seq .|| ) . n & ( ||. seq .|| ) . n <= ( ||. seq .|| ) . n ;
sin . ( r * PI ) = sin . ( r * PI ) .= sin . ( r * PI ) .= 0 .= 0 ;
set q = |[ g1 `1 * ( t `2 - g2 `2 ) , g2 `2 * ( t `2 - g2 `2 ) ]| ;
consider G being sequence of S such that for n be Element of NAT holds G . n in W5 ( F . n ) ;
consider G such that F = G and ex G1 st G1 in SF1 & G in G1 & F in G1 & G in G1 & G in G1 ;
the root of ( x , s ) . s in ( the Sorts of Free ( F , X ) ) . s & ( the Sorts of Free ( F , X ) ) . s = ( the Sorts of Free ( F , X ) ) . s ;
Z c= dom ( ( ( exp_R ^ ) (#) ( exp_R + ( exp_R + exp_R ) ) ) ) `| Z ) ;
for k be Element of NAT holds ( ( Im ( f ) ) . k ) . k = ( ( Im ( f ) ) . k ) . k
assume that - 1 < n and - 1 < n and - 1 < n and n < 1 and - 1 < n and - 1 < n and - 1 < n and n < 1 ;
assume that f is continuous and a < b and a < b and f . a = c and f . b = d and f . a = c ;
consider r being Element of NAT such that Comput ( P1 , s1 , i ) = Comput ( P1 , s1 , i ) and r <= q and r <= q ;
LE f /. ( i + 1 ) , f /. ( j + 1 ) , f /. ( j + 1 ) , f /. ( j + 1 ) , f /. ( j + 1 ) , f /. ( j + 1 ) ;
assume that x in the carrier of K and y in the carrier of K and inf { x , y } in the carrier of K and x in the carrier of K and y in the carrier of K ;
assume f +* ( i1 , \xi ) in ( ( proj ( F , i2 ) * ( i1 , i2 ) ) ) " ( ( proj ( F , i2 ) * ( i1 , i2 ) ) " ) ;
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 ) \times { t } where t is Element of T : t in X & t in X } ;
consider l be Nat such that for m be Nat st l <= m holds ||. ( s1 . m ) - ( lim s1 ) .|| < g ;
consider t be VECTOR of product G such that for t be Element of dom ( D . t ) holds ||. t .|| <= ||. ( D . t ) .|| * ||. t .|| ;
assume that the carrier of v = 2 and v ^ <* 0 *> ^ <* 1 *> ^ <* 1 *> ^ <* 1 *> ^ <* 1 *> ^ <* 1 *> ^ <* 1 *> ^ <* 1 *> ^ <* 1 *> ^ <* 1 *> ^ <* 1 *> ^ <* 1 *> ^ <* 1 *> ^ <* 1 *> ^ <* 1 *> ^ <* 1 *> ^ <* 1 *> ^ <* 1 *> ^ <* 1 *> ^ <* 1 *> ^ <* 1 *> ^ <*
consider a being Element of the Points of X , A such that a on A and not a on A and not a on A and not a on A ;
( - x ) |^ ( k + 1 ) * ( ( - x ) |^ ( k + 1 ) ) " = 1 ;
for D being set st for i st i in dom p holds p . i in D . i holds p . i in D . i
defpred R [ element ] means ex x , y st [ x , y ] = $1 & P [ x , y ] ;
L~ f2 = union { LSeg ( 0 , p2 ) , LSeg ( |[ 0 , 0 ]| , |[ 0 , 0 ]| ) , |[ 0 , 0 ]| } ;
i - len h11 + 2 - 1 < i - len h11 + 1 - 1 + 1 - 1 ;
for n be Element of NAT st n in dom F holds F . n = |. ( n -' 1 ) .|
for r , s1 , s2 holds r in [. s1 , s2 .] iff r in [. s1 , s2 .] & s1 <= s2 & s2 <= 1 & s1 <= 1 & s2 <= 1 & s1 <= 1 & s1 <= 1 & s2 <= 1 & s1 <= 1 & s2 <= 1 & s1 <= 1 & s1 <= 1 & s2 <= 1 }
assume v in { G where G is Subset of T2 : G in ( B1 \ B2 ) & G in B1 & G c= B1 } ;
let g be Element of A , X , Y be non-empty ManySortedSet of ( the carrier of A ) , f be Function of X , Y ;
min ( g . [ x , y ] , k ) . [ x , y ] = ( min ( g . k , g . x ) ) . [ y , z ] ;
consider q1 be sequence of Ca such that for n holds P [ n , q1 . n ] ;
consider f being Function such that dom f = NAT and for n being Element of NAT holds f . n = F ( n ) and f . n = F ( n ) ;
reconsider BO = B /\ O , O = O /\ O as Subset of [: O , O :] ;
consider j be Element of NAT such that x = the Element of n and 1 <= j and j <= n and 1 <= n and n <= len f and 1 <= j and j <= len f and 1 <= j and j <= len f and 1 <= j and j <= len f and f /. j = f /. j ;
consider x such that z = x and card ( x . O ) in card ( x . O ) and x in ( x . O ) . O and x in ( x . O ) . O ;
( C * ( T4 ) ) . 0 = C . ( ( T4 ) . ( n + n2 ) ) ) .= C . ( ( T4 ) . 0 ) ;
dom ( X --> rng f ) = X & dom ( X --> f ) = X & dom ( X --> f ) = X ;
( ( TOP-REAL 2 ) | ( L~ Cage ( C , n ) ) ) `2 <= ( ( GoB Cage ( C , n ) ) * ( i , j ) `2 ) `2 ;
synonym x , y are_not collinear means : Def6 : { x , y } = y or { x , y } is \mathopen of x , y ;
consider X being element such that X in dom ( f | ( n + 1 ) ) and ( f | ( n + 1 ) ) . X = Y ;
assume that Im k is continuous and for x , y being Element of L st x = y & y = x & x <= y holds x << y iff x << y & y \ x <= x & x \ y <= y \ x ;
( ( 1 / 2 ) (#) ( ( cos - ( cos - ( cos - ( sin - ( cos - ( cos - ( cos - ( sin - ( cos - ( cos - ( sin - ( cos - ( sin - ( cos - ( sin - ( cos - ( sin - ( cos - ( sin - ( sin - ( sin - ( sin - ( cos - ( sin - ( cos - ( cos - ( sin - ( cos - ( sin - ( sin - ( cos - ( sin - ( sin - ( cos - ( cos ) ) ) ) ) ) )
defpred P [ Element of omega ] means ( the partial of A1 ) . $1 = A1 . ( $1 ) & ( the partial of A2 ) . $1 = ( the partial of A2 ) . $1 ;
IC Comput ( P , s , 2 ) = succ IC Comput ( P , s , 2 ) .= 6 + 1 .= 6 + 1 .= 6 + 1 ;
f . x = f . ( g1 . ( g1 . ( g2 . ( g2 . x ) ) ) * f . ( g2 . x ) ) .= f . ( g1 . ( g2 . x ) ) * f . ( g2 . x ) .= f . ( g1 . x ) * f . ( g2 . x ) ;
( M * ( F . n ) ) . n = M . ( F . n ) .= M . ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( F ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) . n ) .= M . ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( F F ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
the carrier of L1 + L2 c= ( the carrier of L1 ) \/ ( the carrier of L2 ) \/ ( the carrier of L2 ) ;
pred a , b , c , x , y , z is_collinear means : Def6 : for x , y , z being Element of X holds x , y , z , x , y is_collinear & x , y , z , x , y is_collinear & x , y , z , x is_collinear & x , z , y , z is_collinear ;
( the PartFunc of product G ) . n <= ( the Sorts of product G ) . n * ( the Sorts of A ) . n ;
attr - 1 <= r & r <= 1 implies ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( - 1 ) ) ) ) `| ( [. - 1 , 1 .] ) = ( - 1 ) * ( ( - 1 ) * ( ( - 1 ) * ( ( - 1 ) * ( ( - 1 ) * ( ( - 1 ) * ( - 1 ) ) ) )
s in { p ^ <* n *> where n is Nat : p ^ <* n *> in T & p ^ <* n *> in T } ;
|[ x1 , x2 , x3 ]| . 2 - |[ y1 , y2 ]| . 2 - |[ y1 , y2 ]| . 2 - |[ y1 , y2 ]| . 2 - y1 + y2 . 2 , y2 ]| . 2 - y1 + y2 . 2 - y1 . 2 , y2 - y1 + y2 ]| . 2 + y1 . 2 - y2 . 2 + y1 . 2 - y1 . 2 , y2 . 2 + y1 . 2 + y2 . 2 + y1 . 2 + y1 . 2 - y1
attr for m being Nat holds F . m is non-negative means : Def6 : ( F . m ) is nonnegative ;
len ( ( ( carr G ) . z ) + ( ( carr G ) . ( y1 , y2 ) ) ) = len ( ( ( carr G ) . y1 ) + ( ( carr G ) . y2 ) ) ;
consider u , v being VECTOR of V such that x = u + v and u in W1 /\ W2 and v in W2 /\ W3 and u in W2 /\ W3 ;
given F being FinSequence of NAT such that F = x and dom F = n and dom F = { 0 , 1 } and rng F c= { 0 , 1 } and Sum F = 1 and Sum F = 1 ;
0 = ( 1 - @ ) * cos . uq iff 1 - 0 = ( 1 - @ q ) * ( 1 - 0 ) ;
consider n be Nat such that for m be Nat st n <= m holds |. ( f # x ) . m - lim ( f # x ) .| < e ;
cluster non empty strict for RelStr for RelStr of L , ( ( the carrier of L ) --> ( ( the carrier of L ) --> ( the carrier of L ) ) ) , ( the carrier of L ) --> ( ( the carrier of L ) --> ( the carrier of L ) ) ;
"/\" ( B , L ) = Bottom S .= Bottom S .= Bottom S .= Bottom S .= Bottom S .= Bottom S .= Bottom S .= Bottom S ;
sqrt ( r ^2 + ( r ^2 + ( r ^2 + ( r ^2 + r ^2 ) ) ^2 ) ) <= sqrt ( r ^2 + ( r ^2 + ( r ^2 ) ^2 ) ) ;
for x being element st x in A /\ dom ( f `| X ) holds ( f `| X ) . x >= r2
2 * r1 " * |[ a , c ]| - ( 2 * r1 ) * |[ b , c ]| + ( 2 * r1 ) * |[ a , c ]| = 0. TOP-REAL 2 ;
reconsider p = P /. ( \square , 1 ) , q = a " * ( ( - 1_ K ) * ( ( - 1_ K ) * ( 1 , 1 ) ) ) as FinSequence of K ;
consider x1 , x2 being element such that x1 in uparrow s and x2 in uparrow t and x = [ x1 , x2 ] and x in uparrow t and y = [ x1 , x2 ] ;
for n being Nat st 1 <= n & n <= len q1 holds q1 . n = ( ( lower ( g , n ) ) . n ) * ( ( lower ( g , n ) ) . x )
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 & y = H2 & H1 = H2 & H2 = H & H1 = H ;
for S , T being non empty RelStr , d being Function of T , S for d being Function of T , S holds d is directed-sups-preserving iff d is directed-sups-preserving & d is directed-sups-preserving & d is directed-sups-preserving
[ a + 0 , b ] in ( the carrier of V ) & [ b , a ] in ( the carrier of V ) & [ a , b ] in [: the carrier of V , the carrier of V :] ;
reconsider m2 = max ( len ( F . n ) * ( p . n ) ) as Element of NAT ;
I <= width GoB ( GoB ( h ) ) & GoB ( h ) * ( i , j ) `2 = ( GoB h ) * ( i , j ) `2 & GoB h = ( GoB h ) * ( i , j ) `2 & GoB h = ( GoB h ) * ( i , j ) `2 ;
f2 /* q = ( f2 /* ( f1 /* ( f1 /* s ) ) ) ^\ k .= ( f2 /* ( f1 /* s ) ) ^\ k .= ( f2 /* ( f1 /* s ) ) ^\ k ;
attr A1 : A1 \/ A2 is linearly-independent means : Def6 : for A , B being Subset of V holds ( A1 \/ A2 ) /\ ( A1 \/ A2 ) = {} & ( A1 \/ A2 ) /\ ( A1 \/ A2 ) = {} ;
func A -| C -> set equals union { A ( ) where A is Element of C ( ) : A ( ) = C ( ) & A ( ) is finite } ;
dom ( ( Line ( v , i + 1 ) ) ) = dom ( ( F ^ ) ) ^ ( ( ( ( ( p ^ ) ) ^ ) ) ) ^ ) ) .= dom ( F ^ ) ) ;
cluster [ x `1 , x `2 ] -> ( [ x `1 , x `2 ] ) `1 , [ x `2 ] `2 , [ x `2 , x `2 ] `2 ] `1 -> [: x `1 , x `2 `2 :] ;
E , All ( x2 , x1 ) |= All ( x2 , x2 ) 'or' All ( x2 , x1 ) '&' All ( x3 , x2 ) '&' All ( x3 , x2 ) '&' All ( x3 , x3 ) '&' All ( x3 , x1 ) '&' All ( x4 , x2 ) '&' All ( x4 , x3 ) '&' All ( x4 , x3 ) '&' All ( x4 , x3 ) '&' All ( x4 , x3 ) '&' All ( x4 , x1 ) '&' All ( x4 , x3 ) '&' All ( x4 , x3 ) '&' All ( x4 , x3 ) '&' All ( x4 , x3 )
F .: ( id X , g . x ) = F . ( id X , g . x ) .= F . ( id X , g . x ) .= F . ( id X , g . x ) .= F . ( x , g . x ) .= F . ( x , g . x ) ;
R . ( h . m ) = F . ( x0 + h . m ) - ( h . x0 ) + ( h . x0 ) .= ( h . m ) -f . x0 + ( h . x0 ) ;
cell ( G , ( X -' 1 ) -' 1 , Y -' 1 ) \ L~ f ) meets ( L~ f -' 1 ) \ ( L~ f -' 1 ) ;
IC Comput ( P2 , s2 , i ) = IC Comput ( P2 , s2 , i ) .= IC Comput ( P2 , s2 , i ) .= IC Comput ( P2 , s2 , i ) .= IC Comput ( P2 , s2 , i ) ;
sqrt ( ( ( - ( q `1 / |. q .| - sn ) / ( 1 + sn ) ) / ( 1 + sn ) ) ^2 ) > 0 ;
consider x0 being element such that x0 in dom a and x0 in g and x0 in g " { x0 } and x0 in dom g and g . x0 = a . x0 and g . x0 = ( f . x0 ) * ( f . x0 ) ;
dom ( r1 (#) ( ( - 1 ) (#) ( f | A ) ) ) = dom ( ( - 1 ) (#) ( f | A ) ) .= dom ( ( - 1 ) (#) ( f | A ) ) .= dom ( ( - 1 ) (#) ( f | A ) ) .= A ;
d . [ y , z ] = ( [ y , z ] `1 ) * ( [ y , z ] `1 ) - ( y `1 ) * ( y `2 ) + ( y `2 ) * ( y `2 ) - ( y `2 ) * ( y `2 ) ;
hence for i being Nat holds C . i = A . i /\ B . i implies -5 . i c= ( A . i ) /\ ( B . i )
assume that x0 in dom f and f is continuous and for x st x in dom f holds f . x - f . x0 = ( f . x ) * ( f . x - f . x0 ) ;
p in Cl A implies for K being Basis of T for Q being Basis of T st Q in K & Q is open holds A meets Q
for x be Element of REAL n st x in Line ( x1 , x2 ) holds |. y1 - y2 .| <= |. y1 - y2 .|
func <* a *> -> Ordinal of a means : Def1 : for b being Ordinal st a in it holds it . b = a & it . b = b ;
[ a1 , a2 ] in ( ( the carrier of A ) \/ ( the carrier of B ) ) \/ ( the carrier of C ) & ( the carrier of A ) \/ ( the carrier of C ) c= ( the carrier of A ) \/ ( the carrier of C ) ;
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 ) . m - ( vseq . m ) . n ) .|| < \frac { e } * ||. x .|| + ||. x .|| * ||. x .|| ;
then for Z being set st Z in { Y where Y is Element of I : F . Y = Z } holds z in Z & z in Z ;
sup ( { [ s , t ] } , [ y , t ] ] } = [ sup [: { y } , { t } :] , [ y , t ] ] ] .= [ y , t ] ;
consider i , j being Element of NAT such that i < j and [ y , f . i ] in [: I , J :] and [ f . i , f . j ] in [: I , J :] and [ f . i , f . j ] in [: I , J :] ;
for D being non empty set , p , q being FinSequence of D st p ^ q = q ^ p & p ^ q = q ^ p holds p ^ q ^ q ^ q ^ p ^ q ^ q
consider e1 be Element of the carrier of X such that not LIN c9 , e1 , e1 and not LIN e1 , e1 , e1 and not LIN e1 , e1 , e1 and not LIN e1 , e1 , e1 and not LIN e1 , e1 , e1 and not LIN e1 , e1 , e1 and not LIN e1 , e1 , e1 and not LIN e1 , e1 , e1 ;
set U = I \! \mathop { \rm \hbox { - } \rm \hbox { - } cluster } ;
|. q2 .| ^2 = ( ( |. q2 .| ) ^2 + ( |. q2 .| ) ^2 ) ^2 .= ( |. q2 .| ) ^2 + ( |. q2 .| ) ^2 .= ( |. q2 .| ) ^2 + ( |. q2 .| ) ^2 .= ( |. q2 .| ) ^2 + ( |. q2 .| ) ^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 & x "\/" y = x "\/" y
dom ( ( the charact of U1 ) * the Arity of U2 ) = dom ( the charact of U2 ) & dom ( the charact of U2 ) = dom the charact of U2 & dom ( the charact of U2 ) = dom the charact of U2 ;
dom ( h | X ) = dom h /\ X .= dom ( ( |. h .| ) | X ) .= dom ( |. h .| ) /\ X .= dom ( |. h .| ) /\ X .= dom ( |. h .| ) /\ X .= dom ( |. h .| ) /\ dom ( |. h .| ) .= dom ( |. h .| ) /\ dom ( |. h .| ) .= dom ( |. h .| ) /\ dom ( |. h .| ) ;
for N1 , N2 be Element of [: N1 , N2 :] holds ( h . N1 ) . ( N1 , N2 ) = N . ( N1 , N2 ) & ( h . N1 ) . ( N1 , N2 ) = N . ( N1 , N2 )
( mod ( u , m ) ) . i + ( mod ( v , m ) ) . i = ( mod ( u , m ) ) . i + ( mod ( v , m ) ) . i ;
- ( q `1 / |. q .| - sn ) / ( 1 + sn ) < - ( q `1 / |. q .| - sn ) / ( 1 + sn ) & - ( q `1 / |. q .| - sn ) / ( 1 + sn ) <= - ( q `2 / |. q .| - sn ) / ( 1 + sn ) ;
attr r1 = f . ( f1 . n ) & r1 = f . ( f1 . n ) & r2 = f . ( f1 . n ) ;
vseq . m is bounded Function of X , the carrier of Y & ( vseq . m ) . n = ( ( vseq . n ) . m ) * ( ( vseq . n ) . m ) ;
attr a <> b & b <> c & a <> c & b <> d & c <> d & a , b , c is_collinear & angle ( a , b , c , d ) = 0 & angle ( a , b , c , d ) = 0 ;
consider i , j being Nat such that p1 = [ i , j ] and p = [ i , j ] and p = [ i , j ] and q = [ i , j ] ;
|. p .| ^2 - ( 2 * ( p `2 - q `1 ) ^2 ) = |. p .| ^2 + ( |. q .| ) ^2 + ( |. q .| ) ^2 ;
consider p1 , q1 being Element of [: X , Y :] such that y = p1 ^ q1 and q1 ^ q2 = p1 ^ q1 and p1 ^ q1 = q1 ^ q2 and q1 ^ q2 = q2 ^ q2 and p1 ^ q1 ^ q2 = q2 ^ q2 ;
\bf 2 ( r1 , r2 , s1 , s2 , s1 , s2 , s2 , s2 , s1 , s2 , s2 ) = sqrt ( ( s2 - s1 ) * ( s2 - s2 ) ) * ( s2 - s1 ) ) .= ( s2 - s1 ) * ( s2 - s2 ) ;
( ( ( TOP-REAL 2 ) | ( A ) ) | ( ( ( TOP-REAL 2 ) | ( A ) ) | ( ( A ) | ( ( A ) ) | ( ( A ) ) | ( ( A ) ) | ( ( A ) ) ) ) ) ) ) is empty ;
s , H |= H1 '&' H2 iff s |= H1 '&' H2 iff s |= H1 '&' H2 & s |= H1 '&' H2 iff s |= H1 '&' H2 & s |= H1 '&' H2 )
len ( ( ( support b1 ) + 1 ) + 1 ) = card ( support b1 ) + ( ( support b1 ) + ( support b1 ) + ( support b2 ) ) .= card ( support b1 ) + ( support b1 ) + ( support b1 ) .= ( support b1 ) + ( support b1 ) + ( support b1 ) .= ( support b1 ) \/ ( support b1 ) \/ ( support b1 ) .= ( support b1 ) \/ ( support b1 ) .= ( support b1 ) \/ ( support b1 ) \/ ( support b1 ) .= ( support b1 ) \/ ( support b1 ) \/ ( support b1 ) \/ ( support b1 ) \/
consider z be Element of L1 such that z >= x and z >= y and for z being Element of L1 st z >= x & z >= y holds z >= y ;
LSeg ( ( ( UMP D ) + ( |[ ( ( ( TOP-REAL 2 ) + ( ( TOP-REAL 2 ) + ( ( TOP-REAL 2 ) + ( TOP-REAL 2 ) ) / 2 ) - ( ( TOP-REAL 2 ) + ( ( TOP-REAL 2 ) + ( ( TOP-REAL 2 ) + ( ( TOP-REAL 2 ) + ( ( TOP-REAL 2 ) + ( ( TOP-REAL 2 ) + ( ( TOP-REAL 2 ) + ( TOP-REAL 2 ) ) / 2 ) ) ) ) ) ) /\ LSeg ( ( ( ( TOP-REAL 2 ) - ( ( TOP-REAL 2 ) - ( ( TOP-REAL 2 ) ) / 2 ) - ( ( ( TOP-REAL 2 ) ) / 2
lim ( ( ( f `| N ) /* ( g `| N ) /* b ) - ( f `| N ) /* a ) ) = ( ( ( f `| N ) /* b ) /* a .= ( ( f `| N ) /* b ) - ( ( f `| N ) /* a ) ;
P [ i , pr1 ( f ) . i , 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 ) - ( lim seq ) .|| < r
for X being set , P being a_partition of X , x being set st x in P & x in P & y in P & x in P & P . x = a holds a = b
Z c= dom ( ( ( ( ( ( ( ( ( exp_R * f ) ) ) - ( exp_R * f ) ) - ( exp_R * ( exp_R * f ) ) ) ) ) - ( ( exp_R * ( exp_R * f ) - ( exp_R * f ) ) ) ) ) ) ) ;
ex j being Nat st j in dom ( l ^ <* x *> ) & j < i & i < len l implies z = ( l ^ <* x *> ) . j & z = ( l ^ <* x *> ) . j & z = ( l ^ <* x *> ) . j
for u , v being VECTOR of V , r being Real st 0 < r & u < 1 holds r * u + ( 1 - r ) * v in N
A , Int A are_equipotent implies Int A , Int A are_equipotent & Int A , Int A are_equipotent & Int A , Int A ` ` are_equipotent & Int A , Int A ` ` ` ` ` misses Int A ` & Int A , Int A ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` is open & Int A ` = ( Int A ) ` & Int A ` is open & Int A ` is open & A ` is open & A ` is open & A ` is open & A ` is open & A ` is open & A ` is open & A ` is open & A ` is open & A `
- Sum <* v , u , w *> = - ( v + u ) .= ( - ( v + u ) ) + ( - ( v + u ) ) .= ( - ( v + u ) ) + ( - ( v + u ) ) .= ( - ( v + u ) ) + ( - ( v + u ) ) .= ( - ( v + u ) ) + ( - ( v + u ) ) .= ( - ( v + u ) ) + ( - ( v + u ) .= ( - ( v + u ) .= ( - ( v + u ) .= ( - ( v + u ) ;
( Exec ( a := b , s ) ) . IC SCM = ( Exec ( a , s ) ) . IC SCM R .= succ IC s .= succ IC s .= succ IC s .= succ IC s .= succ IC s .= succ IC s ;
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 ;
for S1 , S2 being non empty RelStr for D being non empty Subset of S1 for D holds [: S1 , S2 :] is directed & [: S1 , S2 :] is directed & [: S1 , S2 :] is directed & [: S1 , S2 :] is directed & [: S1 , S2 :] is directed & [: S1 , S2 :] is directed & [: S1 , S2 :] is directed & [: S1 , S2 :] is directed & [: S1 , S2 :] is directed & [: S1 , S2 :] is directed & [: S1 , S2 :] is directed & [: S1 , S1 :] is directed & [: S1 , S2 :] is directed & [: S1 , S1 :] is directed &
card X = 2 implies ex x st x in X & ex y st x in X & y in X & x in Y & y in Y & x in Y & y in X & x in Y ;
W-min L~ Cage ( C , n ) in rng ( Cage ( C , n ) \circlearrowleft Cage ( C , n ) \circlearrowleft p ) ;
for T , T , p , q being Element of dom T holds ( T -tree p ) . q = T . ( q ^ p )
[ i2 + 1 , j2 ] in Indices G & [ i2 + 1 , j2 ] in Indices G & f /. k = G * ( i2 + 1 , j2 ) ;
cluster k |^ n -> natural for Nat , m , n be Element of NAT , k be Element of NAT st k divides m & k divides n & k divides m holds k divides m * n & k divides m * n implies k divides m
dom F " = the carrier of X1 & rng F = the carrier of X2 & rng F " = the carrier of X1 & rng F " = the carrier of X2 & rng F " = the carrier of X2 & rng F = the carrier of X1 & rng F = the carrier of X2 & rng F is closed ;
consider C being finite Subset of V such that C c= A and card C = m and the carrier of V c= the carrier of W and the carrier of W c= the carrier of W and the carrier of W c= the carrier of W ;
V is prime iff for X , Y being Subset of [: the topology of T , the topology of T :] st X /\ Y c= V & X c= V holds X is open & Y is open & Y is open & X is open & Y is open & Y is open & X is open & Y is open & Y is open & X is open & Y is open & Y is open ;
set X = { F ( v1 ) where v1 is Element of B ( ) : P [ v1 ] } , Y = { F ( v1 ) where v1 is Element of A ( ) : P [ v1 ] } ;
angle ( p1 , p3 , p2 , p3 , p4 , p1 , p2 , p1 , p2 , p3 ) = 0 .= angle ( p2 , p3 , p1 , p2 ) .= angle ( p2 , p3 , p2 , p1 , p2 ) ;
- sqrt ( ( ( q `1 / |. q .| - sn ) / ( 1 + sn ) ) / ( 1 + sn ) ) ^2 ) = ( - ( q `2 / |. q .| - sn ) ) / ( 1 + sn ) .= ( - ( q `2 / |. q .| ) / ( 1 + sn ) .= ( ( q `2 / |. q .| ) / ( 1 + sn ) ) / ( 1 + sn ) ;
ex f being Function of I[01] , TOP-REAL 2 st f is continuous one-to-one & f is continuous one-to-one & rng f = P & f . 0 = p1 & f . 1 = p2 & f . 1 = p3 ;
attr f is partial differentiable of RNS means : Def6 : SVF1 ( 2 , pdiff1 ( f , 1 ) , u0 ) is PartFunc of u0 , REAL ;
ex r , s st x = |[ r , s ]| & ( G * ( len G , 1 ) , 1 ) `2 < s & s < G * ( 1 , 1 ) `2 & s < G * ( 1 , 1 ) `2 ;
assume that f is elements which is elements which and 1 <= len G and 1 <= t and t <= width G and G * ( t , t ) `2 <= N * ( t , t ) `2 and t <= N * ( t , t ) `2 and t <= N * ( t , t ) `2 and t <= N * ( t , t ) `2 and t <= N * ( t , t ) `2 and t <= N * ( t , t ) `2 and t <= N * ( t , t ) `2 and t <= N * ( t , t ) `2 and t <= N * ( t , t ) `2 and t
attr i in dom G means : Def6 : r * ( f * reproj ( i , x ) ) . i = r * ( f * reproj ( i , x ) ) . x ;
consider c1 , c2 being bag of o1 such that ( O + c ) /. k = <* c1 + c2 *> and ( O + c ) /. k = <* c1 + c2 *> /. k and c = c1 + c2 /. k ;
x0 in { |[ r1 , s1 ]| : r1 < s1 & s1 < 1 } & LSeg ( G * ( 1 , 1 ) , G * ( 1 , 1 ) ) = { |[ r1 , s1 ]| : G * ( 1 , 1 ) `2 < G * ( 1 , 1 ) `2 } ;
Cl X ^ Y . ( k2 + 1 ) = the carrier of X . ( k2 + 1 ) .= ( C . ( k2 + 1 ) ) . ( k2 + 1 ) .= ( C . ( k2 + 1 ) ) . ( k2 + 1 ) .= ( C . ( k2 + 1 ) ) . ( k2 + 1 ) .= ( C . ( k2 + 1 ) ) .= ( C . ( k2 + 1 ) ) . ( k2 + 1 ) .= ( C . ( k2 + 1 ) .= ( C . ( k2 + 1 ) ) . ( k2 + 1 ) .= ( C . ( k2 + 1 ) ;
attr len M1 = len M1 & width M1 = width M1 & width M1 = width M1 & width M1 = width M1 & width M1 = width M1 & width M1 = width M1 & width M1 = width M1 implies M1 + M2 is Matrix of n , K
consider g2 be Real such that 0 < g2 and for y be Point of S st y in { y where y is Point of T : ||. y - x0 .|| < g2 & ||. y - x0 .|| < g2 & g2 /. y - x0 < g2 /. x0 } c= N2 ;
assume x < sqrt ( ( - a ) * sqrt ( ( a + b ) * sqrt ( a + b ) ) ) or x > sqrt ( ( - a ) * sqrt ( a + b ) ) ;
( G1 '&' G2 ) . i = ( <* 3 *> ^ H1 ^ H2 ) . i & ( H1 ^ H2 ) . i = ( <* 3 *> ^ H1 ) . i & ( H1 ^ H2 ) . i = ( H1 ^ H2 ) . i ;
for i , j st [ i , j ] in Indices ( M + M1 ) holds ( M + M2 ) * ( i , j ) < M * ( i , j )
for f being FinSequence of NAT , i being Element of NAT st for j being Element of NAT st j in dom f holds f /. j divides f /. ( j + 1 ) & i divides j holds f /. j divides f /. ( j + 1 )
assume F = { [ a , b ] where a , b is Element of X : for c being Element of X st c in B & c in B holds a c= b } ;
b2 * ( q + ( - ( q `2 / |. q .| - sn ) ) * ( q `2 / |. q .| - sn ) ) + ( - ( q `2 / |. q .| - sn ) ) * ( q `2 / |. q .| - sn ) ) = 0. TOP-REAL n + ( ( q `2 / |. q .| - sn ) * ( q `2 / |. q .| - sn ) ) ;
Cl ( F \ { D where D is Subset of T : D is closed & ex B being Subset of T st B = Cl ( B ) & D is closed & B is closed & A /\ D = Cl ( B \ { D } ) } ;
attr seq is summable means : Def6 : for n holds seq . n = ( Partial_Sums seq ) . n + ( Partial_Sums seq ) . n ) & Partial_Sums ( seq ) . n = ( Partial_Sums seq ) . n + ( Partial_Sums seq ) . n = ( Partial_Sums seq ) . n + ( Partial_Sums seq ) . n ;
dom ( ( ( ( TOP-REAL 2 ) | D ) | K1 ) ) = ( ( ( TOP-REAL 2 ) | K1 ) ) | K1 .= ( ( ( TOP-REAL 2 ) | K1 ) ) /\ K1 .= ( ( ( TOP-REAL 2 ) | K1 ) ) /\ K1 .= ( ( ( TOP-REAL 2 ) | K1 ) ) /\ K1 .= ( ( TOP-REAL 2 ) | K1 ) | K1 .= ( ( TOP-REAL 2 ) | K1 ) | K1 .= ( ( TOP-REAL 2 ) | K1 ) | K1 .= ( ( TOP-REAL 2 ) | K1 .= ( ( TOP-REAL 2 ) | K1 ) | K1 ) | K1 .= ( ( ( 2 ) | K1 ) | K1 ) | K1 .= ( ( TOP-REAL 2 ) | K1 ) |
[ X \to Z ] is full full full full full full full full of ( X |^ Z ) |^ the carrier of Z , the carrier of Z :] & [ X |^ Z , Y |^ ( X ) |^ ( X ) |^ ( Y ) ] is full full full full full non empty Subset of Z ;
( G * ( 1 , j ) `2 ) `2 = ( G * ( 1 , j ) `2 ) `2 & ( G * ( 1 , j ) `2 <= ( G * ( 1 , j ) `2 ) `2 ;
cluster m1 c= m2 -> m2 for set of P , p , q be Element of P , m , n be Element of NAT st p in P & q in the carrier of ( P , m ) holds the non empty set of ( P , m ) c= the carrier of ( P , n )
consider a being Element of B ( ) such that x = F ( a ) and a in { G ( ) where b is Element of B ( ) : P [ b ] } and P [ a ] ;
cluster multiplicative loop over R for multiplicative non empty multMagma , s , t , s be Element of R , a , b be Element of the carrier of R , s be Element of it : s is Element of it & a is Element of it iff s is Element of it & a is Element of it & b is Element of it iff the carrier of it = the carrier of it & a is Element of it & b is Element of it & it is Element of it iff the carrier of it = the carrier of it = the carrier of it & the carrier of it = the carrier of it & the carrier of it = the carrier of it & the carrier of it = the carrier of it = the carrier of it & the carrier of it = the carrier of it = the carrier
\HM { \HM { \HM { a } \HM { b } \HM { c } } + 1 = b + c .= b + d .= b + d .= b + d .= b + d .= b + d .= b + d + d .= b + d + d .= b + c + d + d .= b + d + d .= b + d + d .= b + d + d + d .= b + c + d + d .= b + d + d + d .= b + d + d + d .= b + d + d + d .= b + d + d + d + d + d .= b + c + d + d + d + d .= b + c + d + d + d .= b + d + d + d +
cluster -> add-associative for Element of INT , i , j , k be Element of INT holds ( ( i , j ) --> ( k , j ) ) . ( i , j ) = ( i , j ) --> ( k , j ) . ( i , j )
( ( ( 2 * p1 + 1 ) * p2 + ( 2 * p1 ) * p2 ) ) / ( 2 * p1 + ( 2 * p2 ) * p2 ) = ( ( 2 * p1 + ( 2 * p2 ) ) / ( 2 * p1 ) ) ;
eval ( ( a | n ) *' , x ) = eval ( a | n , x ) * eval ( p , x ) .= a * eval ( p , x ) * eval ( p , x ) .= a * eval ( p , x ) * eval ( p , x ) .= a * eval ( p , x ) ;
assume that the TopStruct of S = the TopStruct of T and for D being non empty TopSpace st D is open & D is open holds for V being Subset of S st V is open & V is open & V is open & V is open holds V is open & V is open & V is open & V is open & 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 + 1 <= len w + 1 + ( ( q `2 ) /. ( k + 1 ) ) and T /. ( k + 1 ) = ( T /. ( k + 1 ) ) . ( k + 1 ) ;
2 * ( n + 1 ) + ( 2 * ( n + 1 ) ) + ( 2 * ( n + 1 ) ) + ( 2 * ( n + 1 ) ) + ( 2 * ( n + 1 ) ) + ( 2 * ( n + 1 ) ) + ( 2 * ( n + 1 ) ) + ( 2 * ( n + 1 ) ) + ( 2 * ( n + 1 ) ) + ( 2 * ( n + 1 ) ) + ( 2 * ( n + 1 ) ) + ( 2 * ( n + 1 ) ) + ( 2 * ( n + 1 ) ) + ( 2 * ( n + 1 ) ) + ( 2 * ( n + 1 ) ) + ( 2 * ( n + 1 ) ) + ( 2 *
M , v / ( x. 3 , 4 ) / ( x. 0 , 4 ) / ( x. 4 , x. 0 ) / ( x. 4 , x. 0 ) / ( x. 4 , x. 0 ) / ( x. 4 , x. 0 ) / ( x. 4 , x. 0 ) / ( x. 4 , x. 0 ) / ( x. 4 , x. 0 ) / ( x. 4 , x. 0 ) / ( x. 4 , x. 0 ) ) / ( x. 4 , x. 0 ) / ( x. 4 , x. 4 , x. 0 ) / ( x. 4 , x. 0 ) / ( x. 4 , x. 0 ) / ( x. 4 , x. 0 ) / ( x. 4 , x. 0 ) / ( x. 4 , x. 0 , x. 0 ) / ( x. 4 , x. 0 ) /
assume that f is_differentiable_on l and for x0 st x0 in l holds 0 < f . x0 - r & for x0 st x0 in dom f & x0 < x0 holds f . x0 < f . x0 - r ;
for G1 being _Graph , W being Walk of G1 , e being Vertex of G2 holds not e in W iff W is walk of G & e is walk of G & W is closed & W is closed
c22 is not empty iff XOR2 is not empty & not empty iff not empty is not empty & not empty is not empty & not empty is not empty & not empty & not empty is not empty & not empty is not empty & not empty is not empty & not empty is not empty & not empty & not empty & not empty is not empty & not empty is not empty & not empty is not empty & not empty & not empty is not empty & not empty & not empty is not empty & not empty is not empty & not empty & not empty is not empty & not empty is not empty & not empty & not empty is not empty & not empty is not empty & not empty & not empty & not empty & not empty is not empty & not empty & not empty & not empty &
Indices GoB ( f ) = [: dom GoB f , Seg width GoB f :] & [: dom GoB f , Seg width GoB f :] = [: dom GoB f , Seg width GoB f :] & [: dom GoB f , Seg width GoB f :] = [: dom GoB f , Seg width GoB f :] & [: dom GoB f , Seg width GoB f :] = [: dom GoB f , Seg width GoB f :] ;
for G1 , G2 , G1 , G2 , H being strict Subgroup of O holds G1 is Subgroup of G2 & G1 is Subgroup of G1 & G2 is Subgroup of G2 iff G1 is Subgroup of G2 & G2 is Subgroup of G2 & G1 is Subgroup of G2 & G2 is Subgroup of G2 & G1 is Subgroup of G2 & G2 is Subgroup of G2 & G1 is Subgroup of G2 & G2 is Subgroup of G2
UsedIntLoc ( ( the Sorts of t ) +* ( ( the Sorts of t ) +* ( ( the Sorts of t ) +* ( ( the Sorts of t ) +* ( ( the Sorts of t ) +* ( ( the Sorts of t ) +* ( ( the Sorts of t ) ) ) ) ) ) ) ) ) ) = ( the Sorts of t ) +* ( ( the Sorts of t ) +* ( ( the Sorts of t ) ) ) ;
for f1 , f2 being FinSequence of F st f1 ^ f2 is p -element & ( for n being Element of NAT holds f1 ^ f2 is p ^ <* n *> ) & ( for n being Element of NAT holds f1 . n = ( f1 ^ f2 ) . ( n + 1 ) holds f1 . ( n + 1 ) = f2 . ( n + 1 )
sqrt ( ( p `1 / |. p .| - sn ) / ( 1 + sn ) ) ^2 ) = sqrt ( ( q `1 / |. q .| - sn ) / ( 1 + sn ) ) ^2 ;
for x1 , x2 , x3 , x4 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , v2 , x5 , x5 , x5 , x5 , x5 , x5 , v2 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , 6 , x5 , x5 , 6 , x5 , 8 , 8 , 8 , 8 , 8 , 8 , 8 , 6 , 8 , 8 , 8 , 8 , 6 , 8 , 8 , 6 , 8 , 8 , 8 , 6 , 8 , 8 , 6 , 6 , 8 , 8 , 6 , 6 , 8 , 8 , 8 , 8 , 6 , 8 , 8 , 8 , 8 , 6 , 8 , 8 , 8 , 8 , 6 , 6 , 8
for x st x in dom ( cos | A ) holds ( cos | A ) . x = ( cos | A ) . x
for T being non empty TopSpace , P being Basis of T , B being Basis of T for P being Basis of T st P c= the topology of T & P is Basis of T holds P is Basis of T
( a 'or' b ) . x = 'not' ( a 'or' b ) . x 'or' ( 'not' a 'or' b ) . x .= TRUE 'or' TRUE .= TRUE 'or' TRUE .= TRUE 'or' TRUE .= TRUE 'or' TRUE .= TRUE 'or' TRUE .= TRUE .= TRUE 'or' TRUE .= TRUE .= TRUE 'or' TRUE .= TRUE 'or' TRUE .= TRUE .= TRUE 'or' TRUE .= TRUE .= TRUE 'or' TRUE .= TRUE 'or' TRUE .= TRUE 'or' TRUE .= TRUE .= TRUE 'or' TRUE .= TRUE .= TRUE ;
for e being set st e in A8 ex X1 being Subset of X st e = X1 & ex Y1 being Subset of X st Y1 = Y1 & Y1 is open & Y1 is open & Y1 is open & Y2 is open & Y1 is open & Y1 is open & Y2 is open & Y1 is open & Y1 is open & Y1 is open & Y1 is open & Y2 is open & Y1 is open & Y1 is open & Y2 is open & Y1 is open & Y1 is open & Y1 is open & Y2 is open & Y1 is open & Y1 is open & Y1 is open & Y2 is open & Y1 is open & Y1 is open & Y1 is open & Y1 is open & Y2 is open & Y1 is open & Y1 is open & Y1 is open & Y2
for i being set st i in the carrier of S for f being Function of [: ( the carrier of S1 ) , ( the carrier of S2 ) | ( the carrier of S2 ) :] , ( the carrier of S1 ) | ( the carrier of S2 ) st F = f | ( the carrier of S1 ) holds F . i = f | ( the carrier of S2 ) ;
for v , w st for x st x <> y holds w . ( y . x ) = v . ( y . x ) & J . ( y . x ) = v . ( y . x ) ;
card ( D \ ( D1 + D2 ) ) = card ( ( D1 + D2 ) + ( D1 + D2 ) ) + ( D1 + D2 ) ) .= 2 * ( D1 + D2 ) + ( D1 + D2 ) .= 2 * ( D1 + D2 ) + ( D1 + D2 ) + ( D2 + ) .= 2 * ( D1 + D2 ) + ( D2 + ) .= 2 * ( D1 + D2 ) + ( D2 + ) .= 2 * ( D1 + D2 ) + ( D2 + D2 ) .= 2 * ( D1 + D2 ) + ( D2 + k2 ) + ( D2 + k2 ) + ( D2 + k2 ) .= 2 * ( D1 + D2 ) + ( D2 + k2 ) .= 2 * ( D1 + D2 )
IC Exec ( i , s ) = ( s +* ( 0 .--> ( s . 0 ) ) ) . ( 0 + 1 ) .= ( ( s +* ( 0 .--> ( s . 0 ) ) ) . 0 .= ( ( s +* ( 0 .--> ( s . 0 ) ) ) ) . 0 .= ( ( s +* ( 0 .--> ( s . 0 ) ) ) . 0 .= ( ( s +* ( 0 .--> ( s . 0 ) ) ) ) . 0 .= ( ( ( s . 0 ) ) . 0 .= ( ( s . 0 ) ) . 0 .= ( ( s . 0 ) ) . 0 .= ( ( s . 0 ) ) . 0 .= ( ( s . 0 ) ) . 0 .= ( ( s .
len f /. ( i1 -' 1 + 1 ) + 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1 = ( len f -' i1 + 1 ) + 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1 .= ( len f -' i1 + 1 ) + 1 - 1 + 1 - 1 - 1 + 1 - 1 - 1 + 1 - 1 + 1 + 1 - 1 + 1 + 1 - 1 + 1 - 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1 + 1 -
for a , b being Element of NAT st 1 <= a & a <= b & b <= a holds a + b < a + b or a + b < b + c
for f being FinSequence of TOP-REAL 2 , p being Point of TOP-REAL 2 holds p in LSeg ( f , p ) iff ex f being Function of TOP-REAL 2 st f . ( p , f . p ) = f . ( p , f . p ) & Index ( p , f . p ) = 1
lim ( ( ( ( curry ( F ) ) # . k ) + ( ( curry ( F ) # x ) ) # x ) ) ) = lim ( ( ( ( ( curry F ) # x ) # x ) ) ) + ( ( ( ( ( curry F ) # x ) # x ) ) . n ) ;
z2 = g /. ( i -' n1 + 1 ) .= g /. ( i -' n1 + 1 ) .= g /. ( i -' n1 + 1 + 1 ) .= g /. ( i -' n1 + 1 ) .= g /. ( i -' n1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + ( ( i -' 1 + 1 + 1 + 1 + ( i -' 1 + ( i -' n1 + ( i -' n1 + ( i -' n1 + ( i -' n1
[ f . 0 , f . 3 ] in id ( the InternalRel of G ) \/ ( the InternalRel of G ) or [ f . 0 , f . 3 ] in the InternalRel of G & [ f . 0 , f . 3 ] in the InternalRel of G ;
for G being Subset-Family of B holds G = { [ X , Y ] where X is Subset of A ( ) : ( ( union F ) | X ) . ( X , Y ) = ( Intersect F ) . ( X , Y ) & ( Intersect F ) . ( X , Y ) = ( Intersect F ) . ( X , Y ) ;
CurInstr ( P1 , Comput ( P1 , s1 , m1 ) ) = CurInstr ( P1 , Comput ( P1 , s1 , m1 ) ) .= CurInstr ( P1 , Comput ( P1 , s1 , m1 ) ) .= CurInstr ( P1 , Comput ( P1 , s1 , m1 ) ) .= CurInstr ( P1 , Comput ( P1 , s1 , m1 ) ) ;
assume that a on M and b on N and c on N and a on M and b on N and not on M on N and not on M and not on N and not on M and not on M on N and not on M and not on N and not on M on M and not on M and not on N and M on M and not on M and not on M and not on N and not on M on N and not on M and not on N and ( on N & not on M on N and ( on M on N & not on M & ( on M on N & not on N & ( on M & not on M on N & not on N on N & ( on M & ( on M & not on M on N & ( on M & not on M on N & not on M on N & not on N & not on M on N & not on N on N
assume that T is \hbox { T _ 4 } and ex F being Subset-Family of T st F is closed & for n being Nat holds F is finite-ind & F is finite-ind & F is finite-ind & F is finite-ind & F is finite-ind & F is finite-ind ;
for g1 , g2 st g1 in ]. r1 - r , r2 .[ & g2 in ]. r1 - r , r2 + r .[ holds |. ( f - g ) . g1 - ( f - g ) . g2 .| <= ( ( f - g ) / ( r1 - r ) ) . g2
( \HM { the } \HM { function } \HM { sin } ) + ( \HM { the } \HM { function } \HM { sin } ) = ( \HM { the } \HM { function } \HM { sin } ) + ( \HM { the } \HM { function } \HM { sin } ) .= ( \HM { the } \HM { function } \HM { sin } ) + ( ( \HM { the } \HM { function } \HM { sin } ) ) ) ;
F . i = F /. i .= F /. i + r . ( n + 1 ) .= <* b *> ^ <* n *> .= <* b *> ^ <* n *> .= <* n + 1 *> ^ <* n + 1 *> .= <* n + 1 *> ^ <* n + 1 *> ;
ex y being set , f being Function st y = f . n & dom f = NAT & f . 0 = A & for n being Nat holds f . ( n + 1 ) = f . ( n + 1 ) & f . ( n + 1 ) = f . ( n + 1 ) ;
func f * F -> FinSequence of V means : Def1 : len it = len F & for i be Nat st i in dom F holds it . ( F . i ) = F . ( F . i ) * F . ( F . i ) ;
{ x1 , x2 , x3 , x4 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , 8 } = { x1 , x2 , x3 , x4 , x5 , x5 , x5 , x5 , 8 } \/ { x5 , 8 , 8 , 8 , 8 } .= { x1 , x2 , x3 , x4 } \/ { x4 , x5 , 8 } ;
for n being Nat for x being set st x = h . n holds h . ( n + 1 ) = o ( x , n ) & h . ( n + 1 ) = o ( x , n ) & h . ( n + 1 ) = o ( x , n ) ;
ex S1 be Element of k ( ) st ( [ P ( ) , e ( ) ] ) & ( [ S ( ) , e ( ) ] ) `1 = [ S ( ) , e ( ) ] ;
consider P being FinSequence of ( the carrier of G ) * such that P = Product P and for t being Element of the carrier of G st t in P ex t1 being Element of the carrier of G st P . t = t1 & t . t = t2 & t1 . t = t2 ;
for T1 , T2 being non empty TopSpace , T1 , T2 being Basis of T2 for P being Basis of T2 , Q being Subset of T2 , P being Subset of T2 , Q being Subset of T2 st P = the topology of T2 & Q is Basis of T2 & P is Basis of T2 & Q is Basis of T2 & P is Basis of T2 holds P is Basis of T2
assume that f is partial differentiable of partial u0 , CNS and r (#) ( pdiff1 ( f , 3 ) ) is_partial_differentiable_in u0 , i and r (#) ( pdiff1 ( f , 3 ) ) = r (#) pdiff1 ( f , 3 ) ;
defpred P [ Nat ] means for F being FinSequence of bool ( the carrier of V ) , G being FinSequence of bool ( the carrier of V ) st len F = $1 & for s being Permutation of V holds Sum ( F ) = Sum ( G ) * ( F * s ) ;
ex j st 1 <= j & j < width GoB ( f ) & ( GoB f ) * ( 1 , j ) `2 <= s & ( GoB f ) * ( 1 , j + 1 ) `2 <= s & s `2 <= ( GoB f ) * ( 1 , j + 1 ) `2 & s `2 <= ( GoB f ) * ( 1 , j + 1 ) `2 ;
defpred U [ set , set ] means ex F being Subset-Family of T st ( F = ( F . $1 ) \ F . $1 ) & ( F . $1 ) \ F . $1 = F . $1 & ( F . $1 ) \ F . $1 = F . $1 \ F . $1 ) & ( F . $1 ) \ F . $1 = F . $1 \ F . $1 ;
for p2 being Point of TOP-REAL 2 st LE p2 , p3 , p1 , p2 & LE p2 , p3 , p1 , p2 & LE p2 , p3 , p2 & LE p3 , p1 , p2 & LE p2 , p3 , p1 , p2 & LE p3 , p1 , p2 & LE p2 , p3 , p2 , p1 , p2 & LE p3 , p1 , p2 & LE p2 , p3 , p2 & LE p3 , p1 , p2 , p2 & LE p3 , p1 , p2 , p2 & LE p2 , p1 , p2 , p2 , p1 , p2 & LE p2 , p1 , p2 , p2 , p1 , p2 & LE p2 , p1 , p2 , p2 , p2 , p1 , p2 & LE p3 , p1 , p2 , p1 , p1 , p2 , p1 , p2 & LE p2 , p1 , p2 & LE p2 , p1 , p2 , p1 , p2 , p1 , p2 , p1 , p2 , p1 , p2 , p1 , p2 , p1
f in St ( E , H ) & for y st y <> f . y holds g . y = f . y iff for y st y in dom ( f . y ) holds y in Free ( H , H ) & f . y = f . y ) implies f . y = f . y
ex p2 being Point of TOP-REAL 2 st x = p2 & ( for p st p in 8 & p <> 0. TOP-REAL 2 holds ( |. p .| ) . p = ( |. p .| ) . p & ( |. p .| ) . p = ( |. p .| ) . p & ( |. p .| ) . p = ( |. p .| ) . p ;
assume for d being Element of NAT st d <= ( n + 1 ) -NAT & ( n + 1 ) -NAT <= ( n + 1 ) -NAT & ( n + 1 ) -NAT <= ( n + 1 ) -NAT & ( n + 1 ) -NAT <= ( n + 1 ) -NAT ;
assume that s <> t and s is Point of Closed-Interval-TSpace ( x , r ) and s is Point of Closed-Interval-TSpace ( x , r ) and not ex e being Point of Ball ( x , r ) st e in Ball ( x , r ) & not ex e being Point of Ball ( x , r ) st e in Ball ( x , r ) & e in Ball ( x , r ) & e in Ball ( x , r ) ;
given r such that 0 < r and for s st 0 < s ex x1 st x1 < s & |. x1 - x0 .| < s & |. f /. x1 - f /. x0 .| < r ;
( p | x ) | ( ( x | x ) | ( ( x | x ) | ( x | x ) ) ) = ( ( ( x | x ) | ( x | x ) ) ) | ( ( x | x ) ) | ( ( x | x ) | ( x | x ) ) ;
assume that x + h in dom ( ( ( \HM { the } \HM { function } \HM { cos } ) (#) ( ( \HM { the } \HM { function } \HM { cos } ) + ( \HM { the } \HM { function } \HM { sin } ) ) ) ) ) and ( ( ( \HM { the } \HM { function } ) (#) ( ( \HM { the } \HM { function } \HM { cos } ) ) `| Z ) = ( ( ( \HM { the } \HM { function } ) * ( ( \HM { the } \HM { function } ) ) ) ) `| Z ) ) . x = ( ( ( \HM { the } ) ) . x ) . x ) . x ) . x ) / ( ( \HM { the } ) . x ) . x + ( ( ( \HM { the } \HM { ( \HM { the } ) . x ) ^2 + ( ( \HM { the } \HM { ( } ) . x
assume that i in dom A and len A > 1 and len A > 1 and width A > 1 and width A = 1 and width A = 1 and width A = 1 and width A = 1 and width A = 1 and width A = 1 and width A = 1 and width A = 1 and width A = 1 and width A = 1 and width A = 1 and A is Matrix of n , m ;
for i being non zero Element of NAT st i in Seg n holds ( i divides n ) & ( i divides n implies h . i = ( n |^ n ) * h . i ) & ( i divides n ) * h . i = ( n |^ n ) * h . i
( ( b1 => b2 ) '&' ( b2 => c ) ) '&' ( ( b1 => b2 ) '&' ( b2 => c ) ) '&' ( ( b1 => b2 ) '&' ( b2 '&' c ) ) '&' ( ( b1 => b2 ) '&' ( b2 '&' c ) ) '&' ( ( b1 '&' b2 ) '&' ( b2 '&' c ) ) '&' ( ( b1 '&' b2 ) '&' ( ( b1 '&' b2 ) '&' ( b2 '&' c ) ) '&' ( ( b1 '&' b2 ) '&' ( b2 '&' c ) ) '&' ( ( b1 '&' c ) '&' ( b2 '&' c ) ) '&' ( ( b2 '&' c ) ) '&' ( ( b2 '&' c ) '&' ( b2 '&' c ) ) '&' ( b2 '&' c ) ) '&' ( b2 '&' c ) ) '&' ( ( b2 '&' c ) '&' ( b2 '&' c ) '&' ( ( b2 '&' c ) '&' ( ( b2 '&' c ) '&' ( ( b2 '&' c ) '&' ( ( b2 ) '&'
assume that for x holds f . x = ( ( - 1 ) (#) ( ( - 1 ) (#) ( - 1 ) ) ) . x and for x st x in dom ( ( - 1 ) (#) ( - 1 ) ) holds ( ( - 1 ) (#) ( - 1 ) ) . x = ( - 1 ) * ( - 1 ) ;
consider Rd be Real such that Rd = Integral ( F , ( F . n ) ) and Integral ( M , ( F . n ) ) = Integral ( M , ( F . n ) ) and Integral ( M , ( F . n ) ) = Integral ( M , ( F . n ) ) ;
ex k be Element of NAT st x0 = k & 0 < d & for q be Element of product G st q in X & ||. q-f . q .|| < r holds ||. partdiff ( f , q , k ) - partdiff ( f , x ) .|| < r ;
x in { x1 , x2 , x3 , x4 , x5 , x5 , x5 , x5 , x5 , x5 , 8 , 8 , 8 , 6 , 8 , 8 , 6 } or x in { x1 , x2 , x3 , x4 } & x in { x1 , x2 , x4 } & x in { x1 , x2 , x3 , x4 } ;
( G * ( j , i ) ) `2 = ( G * ( j , i ) ) `2 .= ( G * ( j , i ) ) `2 .= ( G * ( j , i ) ) `2 .= ( G * ( j , i ) ) `2 .= ( G * ( j , i ) ) `2 .= ( G * ( j , i ) ) `2 .= ( G * ( j , i ) ) `2 .= ( G * ( j , i ) `2 .= ( G * ( j , i ) `2 .= ( G * ( j , i ) `2 .= ( G * ( j , i ) `2 .= ( G * ( j , i ) `2 .= ( G * ( j , i ) `2 .= ( G * ( j , i ) `2 .= ( G * ( j , i ) `2 .= G * ( j , i ) `2 .= G * ( j , i ) `2 .= G * ( j , i ) `2 .=
f1 * p = p . o .= ( the Arity of S1 ) . o .= ( the Arity of S2 ) . o .= ( the Arity of S2 ) . o .= ( the Arity of S1 ) . o .= ( the Arity of S1 ) . o .= ( the Arity of S1 ) . o .= ( the Arity of S2 ) . o .= ( the Arity of S2 ) . o ;
func [: T , P , T :] -> FinSequence of T means : Def1 : for p , q st p in P & q in P & p in T & q in T & p in T & q in T & p in T & q in T & p in T & q in T & p in T & q in T & p in T } ;
F /. ( k + 1 ) = F . ( p . k + F /. ( k + 1 ) ) .= F . ( p . ( k + 1 ) ) .= F . ( p . ( k + 1 ) ) .= F . ( p . ( k + 1 ) ) .= F . ( p . ( k + 1 ) ;
for A , B , C being Matrix of n , K st len B = len C & len A = len C & width A = width C & width B = width C & width A = width C & width B = width C & width B = width C & width B = width C holds A * ( BC ) = A * ( BC )
seq . ( k + 1 ) = ( 0. X ) + ( ( seq . k ) + ( seq . k ) ) .= ( ( seq . k ) + ( seq . k ) ) + ( seq . k ) .= ( ( seq . k ) + ( seq . k ) ) + ( seq . k ) .= ( ( seq . k ) + ( seq . k ) ) + ( seq . k ) ;
assume that x in ( the carrier of C1 ) & y in ( the carrier of C2 ) & x in the carrier of C2 & y in the carrier of C2 & x in the carrier of C2 & y in the carrier of C2 ;
defpred P [ Element of NAT ] means for f st len f = $1 & f . ( $1 + 1 ) = ( ( for k st k < $1 holds f . k = ( ( ( g . k ) ) . ( f . ( $1 + 1 ) ) ) ) ) * ( ( ( ( g . k ) . ( f . ( $1 + 1 ) ) ) ) ) ;
assume that 1 <= k and k + 1 <= len f and f /. k = G * ( i , j ) and [ k + 1 , j ] in Indices GoB f and f /. k = G * ( i , j ) and f /. k = G * ( i + 1 , j ) ;
assume that s < 1 and ( q `2 / |. q .| - sn ) / ( 1 + sn ) ^2 > 0 and ( q `2 / |. q .| - sn ) / ( 1 + sn ) ^2 >= 0 and ( q `2 / |. q .| - sn ) / ( 1 + sn ) ^2 >= 0 and ( q `2 / |. q .| - sn ) / ( 1 + sn ) ^2 ) >= 0 ;
for M being non empty dist , x being Point of M holds x = x & ex f being Function of M , TOP-REAL n st for n being Element of NAT holds f . n = Ball ( x , f . n ) & f . n = Ball ( x , f . n )
defpred P [ Element of omega ] means ( f1 - f2 ) . $1 - ( f1 . $1 ) / ( ( f1 - f2 ) . $1 ) / ( ( f1 - f2 ) . $1 ) & ( f1 - f2 ) . $1 ) / ( ( f1 - f2 ) . $1 ) = ( f1 - f2 ) / ( ( f1 - f2 ) . $1 ) ;
defpred P1 [ Nat ] means ( for r be Point of C st r in Y & r < $1 & $1 < ( f . $1 ) `2 holds ||. ( f . $1 ) `2 - ( f . $1 ) `2 .|| < r & ||. ( f . $1 ) `2 - ( f . $1 ) `2 .|| < r ;
( f ^ mid ( g , 2 , len g ) ) . i = ( g ^ mid ( g , 2 , len g ) ) . i .= g . ( i + 1 ) .= g . ( i + 1 ) .= g . ( i + 1 ) .= g . ( i + 1 ) .= g . ( i + 1 ) ;
sqrt ( 1 - ( n + 2 ) * ( n + 1 ) ) = ( sqrt ( 1 - ( n + 2 ) * ( n + 1 ) ) ) * ( sqrt ( 1 - ( n + 2 ) * ( n + 1 ) ) ) .= 1 * sqrt ( 1 - ( n + 2 ) * ( n + 1 ) ) .= 1 * sqrt ( 1 - ( n + 2 ) * ( n + 1 ) ) ;
defpred P [ Nat ] means for G being finite Group , F being ( set , set ) , f being Function of [: the carrier of G , the carrier of G :] , the carrier of G holds the carrier of G = the carrier of F & the carrier of G = the carrier of G & the carrier of G = the carrier of G ;
assume that f /. 1 in Ball ( u , r ) and not 1 <= m and m <= len f and not f /. ( m + 1 ) in LSeg ( f /. ( m + 1 ) , f /. ( m + 1 ) ) and not f /. ( m + 1 ) in LSeg ( f /. ( m + 1 ) , f /. ( m + 1 ) ) ;
defpred P [ Element of NAT ] means ( Partial_Sums ( ( ( ( ( ( ( x ) ) ) ) (#) ( ( x - r ) (#) ( ( x - r ) (#) ( ( x - r ) ) (#) ( ( x - r ) ) ) ) ) ) ) . $1 = ( ( ( x - r ) (#) ( ( x - r ) (#) ( x - r ) ) ) ) . $1 ;
for x being Element of product F holds x is FinSequence of product F & x in dom ( the Sorts of F ) iff x in dom ( the Sorts of F ) & x in dom ( the Sorts of F ) & for i being set st i in dom ( the Sorts of F ) holds x in ( the Sorts of F ) . i
( x " ) |^ ( n + 1 ) = ( x " ) |^ n * x " .= ( x " ) |^ n * x " .= ( x " ) |^ n .= x |^ n * x |^ n .= x |^ n * x |^ n .= x |^ n * x |^ n .= x |^ n * x |^ n ;
DataPart ( ( Comput ( P +* I , s , LifeSpan ( P +* I , s ) ) ) ) . ( ( Initialized s ) . ( k + 1 ) ) = DataPart Comput ( P +* I , s , k ) . ( k + 1 ) .= DataPart Comput ( P +* I , s , k ) . ( k + 1 ) ;
given r such that 0 < r and ]. x0 - r , x0 .[ c= dom ( f1 + f2 ) /\ dom ( f1 + f2 ) and for g st g in dom ( f1 + f2 ) /\ dom ( f1 + f2 ) holds ( f1 + f2 ) . g <= ( f1 + f2 ) . g ;
assume that X c= dom ( f1 + f2 ) /\ dom ( f2 + f3 ) and ( f1 + f2 ) | dom ( f1 + f2 ) is continuous and ( f1 + f2 ) | dom ( f1 + f2 ) is continuous ;
for L being continuous complete LATTICE for X being Subset of L for l being Element of L st l in X holds x in X & for X being Subset of L st l in X holds x is prime & for X being Subset of L st l in X holds x is prime & x is prime holds x is prime
Support ( A *' p ) = { m *' p where m is Element of NAT : A *' p = { m *' p : ex n being Element of NAT st n in dom p & p . n = p . ( m *' p ) } ;
( f1 - f2 ) /* ( f1 /* ( f1 /* ( h + c ) ) ) = ( f1 /* ( h + c ) ) /* ( h + c ) .= ( f1 /* ( h + c ) ) /* ( h + c ) .= ( f1 /* ( h + c ) ) - ( f2 /* ( h + c ) ) ;
ex p1 being ( Al ( ) ) ( ) = g . ( p ( ) ) & F ( p ( ) ) = f ( p ( ) ) & for g being Function of Al ( ) , D ( ) st P [ g ] holds P [ g ( ) ] ;
( mid ( f , i , len f -' 1 ) ) /. j = ( mid ( f , i , len f -' 1 ) ) /. j .= ( mid ( f , i , len f -' 1 ) ) /. j .= ( mid ( f , i , len f -' 1 ) ) /. j .= ( mid ( f , i , len f -' 1 ) ) /. j ;
( ( p ^ q ) ^ r ) . k = ( ( p ^ q ) . k ) . ( len p + k ) .= ( ( p ^ q ) . k ) . ( len p + k ) .= ( p ^ q ) . ( len p + k ) .= ( p ^ q ) . k ;
len ( ( upper_volume ( f , indx ( D2 , D1 , j1 ) ) ) + 1 ) - indx ( D2 , D1 , j1 ) + 1 ) = len ( ( indx ( D2 , D1 , j1 ) ) + 1 ) - indx ( D2 , D1 , j1 ) + 1 ) ;
x * y = ( M * ( x * y ) ) * ( ( M * y ) * z ) .= x * ( M * ( y * z ) ) .= x * ( M * ( y * z ) ) .= x * ( M * ( y * z ) ) .= x * ( M * ( y * z ) ) .= x * ( M * ( y * z ) ) .= x * ( M * ( y * z ) ) .= x * ( M * ( y * z ) .= x * ( M * ( y * z ) ) .= x * ( M * ( y * z ) ) .= x * ( M * ( y * z ) .= x * ( M * ( y * z ) .= x * ( M * ( y * z ) ) * x * ( M * ( M * ( y * z ) .= x * ( M * ( M * ( M * ( y * z ) ) .= x * ( M * ( y * z ) .= x * ( M * ( M * ( y * z ) ) .= x * ( M * ( y * ( y
v . <* x , y *> = ( <* x0 , y0 *> ) . i * ( <* x0 , y0 *> . i ) * ( ( proj ( i , y ) . x ) ) + ( ( proj ( i , y ) . y ) ) * ( ( proj ( i , y ) . x ) ) * ( ( proj ( i , y ) . y ) ) ) ;
i * i = <* 0 * ( 1 - 0 ) + ( 1 - 0 ) * ( 1 - 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 , 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 , 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 , 0 , 0 , 0 , 0 , 0 , 0 , 0 , 0 , 0 , 0 , 0 , 0 , 0 , 0 , 0
Sum ( L (#) F ) = Sum ( L (#) F ) + Sum ( F (#) G ) .= Sum ( L (#) F ) + Sum ( L (#) G ) .= Sum ( L (#) F ) + Sum ( L (#) G ) .= Sum ( L (#) F ) + Sum ( L (#) G ) .= Sum ( L (#) F ) + Sum ( L (#) G ) .= Sum ( L (#) F ) + Sum ( L (#) G ) .= Sum ( L (#) F ) + Sum ( L (#) F ) .= Sum ( L (#) F ) + Sum ( L (#) F ) + Sum ( L (#) F ) + Sum ( L (#) F ) + Sum ( L (#) F ) .= Sum ( L (#) F ) .= Sum ( L (#) F ) + Sum ( L (#) F ) .= Sum ( L (#) F ) + Sum ( L (#) F ) + Sum ( L (#) F ) + Sum ( L (#) G ) .= Sum ( L (#) F ) + Sum ( L (#) F ) + Sum ( L (#) G ) .= Sum ( L (#) F ) + Sum ( L (#) F ) + Sum ( L (#) F ) .= Sum (
ex r be Real st for Y be Subset of X , Y be Subset of REAL st Y is open & Y c= Y & for Y be Subset of X st Y is open & Y is open & Y is open & Y is open holds r <= Y
( GoB f ) * ( i , j + 1 ) = f /. ( k + 1 ) & ( GoB f ) * ( i , j + 1 ) = f /. ( k + 1 ) or ( GoB f ) * ( i , j ) = f /. ( k + 1 ) & ( GoB f ) * ( i , j + 1 ) = f /. ( k + 1 ) ;
( ( ( r / 2 ) * ( ( 1 - r ) / 2 ) ) / 2 ) * ( ( 1 - r ) / 2 ) ) = ( ( 1 - r ) / 2 ) * ( ( 1 - r ) / 2 ) .= ( 1 - r ) / 2 * ( ( 1 - r ) / 2 ) .= ( 1 - r ) / 2 * ( 1 - r ) .= ( 1 - r ) / 2 * ( 1 - r ) .= ( 1 - r ) / 2 * ( 1 - r ) .= ( 1 - r ) / 2 * ( 1 - r ) / 2 * ( 1 - r ) / 2 * ( 1 - r ) .= ( 1 - r ) .= ( 1 - r ) / 2 * ( 1 - r ) .= ( 1 - r ) / 2 * ( 1 - r ) / 2 * ( 1 - r ) / 2 * ( 1 - r ) / 2 * ( 1 - r ) / 2 * ( 1 - r ) / 2 * ( 1 - r ) .= ( 1 - r ) / 2 * ( 1 - r ) / 2 *
x- ( ( - a ) * sqrt ( ( - a ) * sqrt ( 2 * a ) + ( - a ) * sqrt ( 2 * a ) ) ) > 0 & - sqrt ( 2 * a ) < 0 or - sqrt ( 2 * a ) < 0 ;
assume that inf \mathopen { \uparrow } X /\ C and for X holds inf X in X /\ C and inf X in X /\ C and inf X in C /\ ( X /\ C ) and inf X in C /\ ( X /\ C ) and not inf X in C /\ ( X /\ C ) ;
( ( B ) . j ) . i = ( j |-> ( i , j ) ) . i & ( j --> ( i , j ) ) . i = ( j |-> ( i , j ) ) . i & ( j --> ( i , j ) ) . i = j |-> ( i , j ) . i ;