thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
contradiction ;
contradiction ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
contradiction ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
assume not thesis ;
assume not thesis ;
B ;
a <> c
T c= S
D c= B
c in X ;
b in X ;
X ;
b in D ;
x = e ;
let m ;
h is onto ;
N in K ;
let i , j ;
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 .= X ;
assume x in I ;
q is as Nat ;
assume c in x ;
as Real ;
assume x in Z ;
assume x in Z ;
1 <= kr2 ;
assume m <= i ;
assume G is finite ;
assume a divides b ;
assume P is closed ;
\bf 2 > 0 ;
assume q in A ;
W is not bounded ;
f is means : Def1 : f is .| ;
assume A is boundary ;
g is special ;
assume i > j ;
assume t in X ;
assume n <= m ;
assume x in W ;
assume r in X ;
assume x in A ;
assume b is even ;
assume i in I ;
assume 1 <= k ;
X is non empty ;
assume x in X ;
assume n in M ;
assume b in X ;
assume x in A ;
assume T c= W ;
assume s is atomic ;
b `2 <= c `2 ;
A meets W ;
i `2 <= j `2 ;
assume H is universal ;
assume x in X ;
let X be set ;
let T be Tree ;
let d be element ;
let t be element ;
let x be element ;
let x be element ;
let s be element ;
k <= 5 ;
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 , p2 ;
Q halts_on s ;
x in that x in that x in that x in that x in that x in that x in that x in that x in
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 ;
PM is one-to-one ;
n <= n + 2 ;
1 <= k + 1 ;
1 <= k + 1 ;
let e be Real ;
i < i + 1 ;
p3 in P ;
p1 in K ;
y in C1 ;
k + 1 <= n ;
let a be Real , b 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 , r ;
let E be Ordinal ;
o : o <= 4 ;
O <> O2 ;
let r be Real ;
let f be FinSeq-Location ;
let i be Nat ;
let n be Nat ;
Cl A = A ;
L c= Cl L ;
A /\ M = B ;
let V be RealUnitarySpace , W be Subspace of V ;
not s in Y |^ 0 ;
rng f <= w
b "/\" e = b ;
m = m3 ;
t in h . D ;
P [ 0 ] ;
assume z = x * y ;
S . n is bounded ;
let V be RealUnitarySpace , W be Subspace of V ;
P [ 1 ] ;
P [ {} ] ;
C1 is component ;
H = G . i ;
1 <= i `1 + 1 ;
F . m in A ;
f . o = o ;
P [ 0 ] ;
aZ <= non < \pi ;
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 ;
s is trivial & s is non empty ;
dom c = Q
P [ 0 ] ;
f . n in T ;
N . j in S ;
let T be complete LATTICE , X be Subset of T ;
the Arrows of F is one-to-one
sgn x = 1 ;
k in support a ;
1 in Seg 1 ;
rng f = X ;
len T in X ;
vbeing < n ;
S\HM { x } is bounded ;
assume p = p2 ;
len f = n ;
assume x in P1 ;
i in dom q ;
let U2 , U2 , U1 , U2 ;
pp `2 = c ;
j in dom h ;
let k ;
f | Z is continuous ;
k in dom G ;
UBD C = B ;
1 <= len M ;
p in `1 ;
1 <= jj ;
set A = Seg n ;
card a [= c ;
e in rng f ;
cluster B \oplus A -> empty ;
H is non empty and H is non empty ;
assume n0 <= m ;
T is increasing ;
e2 <> e2 & e2 <> e1 ;
Z c= dom g ;
dom p = X ;
H is proper ;
i + 1 <= n ;
v <> 0. V ;
A c= Affin A ;
S c= dom F ;
m in dom f ;
let X0 be set ;
c = sup N ;
R is_connected in union M ;
assume not x in REAL ;
Im f is complete ;
x in Int y ;
dom F = M ;
a in On W ;
assume e in A ( ) ;
C c= C-26 ;
m9 <> {} ;
Element of Y ;
let f be ) ;
not n in Seg 3 ;
assume X in f .: A ;
assume that p <= n and p <= m ;
assume not u in { v } ;
d is Element of A ;
A / b misses B ;
e in v + dom meets ( X \ Y ) ;
- y in I ;
let A be non empty set , B be set ;
P0 = 1 ;
assume r in F . k ;
assume f is simple ;
let A be l countable set ;
rng f c= NAT * ;
assume P [ k ] ;
ff <> {} ;
let o be Ordinal ;
assume x is sum of squares ;
assume not v in { 1 } ;
let IC , I ;
assume that 1 <= j and j < l ;
v = - u ;
assume s . b > 0 ;
d3 in dom f ;
assume t . 1 in A ;
let Y be non empty TopSpace , X be non empty Subset of Y ;
assume a in uparrow s ;
let S be non empty Poset ;
a , b // b , a ;
a * b = p * q ;
assume x , y are_the space of V ;
assume x in Omega ( f ) ;
[ a , c ] in X ;
mm <> {} ;
M + N c= M + M ;
assume M is connected hhfor ;
assume f is \llangle bbsnNat :] ;
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 or k2 = k2 ;
m + 1 < n + 1 ;
s in S \/ { s } ;
n + i >= n + 1 ;
assume Re y = 0 ;
k1 <= j1 & k1 <= j2 ;
f | A is non empty continuous ;
f . x - a <= 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 sup phi ;
Cj in X ;
q2 c= C1 & q2 c= C2 ;
a2 < c2 & c2 < c1 ;
s2 is 0 -started ;
IC s = 0 ;
s4 = s4 , P4 = s4 , P4 = s4 , P4 = i2 , P4 = j2 , P4 = i2 , P4 = j2 , P4 = i2 ,
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 function of L ;
y " <> 0 ;
y " <> 0 ;
0. V = uw ;
y2 , y , w be <> 0 ;
R8 in X ;
let a , b be Real , x be Element of REAL ;
let a be Object of C ;
let x be Vertex of G ;
let o be Object of C , a be Object of C ;
r '&' q = P \lbrack l \rbrack ;
let i , j be Nat ;
let s be State of A , a be Int-Location ;
s4 . n = N ;
set y = ( x `1 ) / ( x `2 ) ;
mi in dom g ;
l . 2 = y1 ;
|. g . y .| <= r ;
f . x in CX0 ;
V1 is non empty ;
let x be Element of X ;
0 <> f . g2 ;
f2 /* q is convergent ;
f . i is_measurable_on E ;
assume \xi in N-22 ;
reconsider i = i as Ordinal ;
r * v = 0. X ;
rng f c= INT & rng f c= INT ;
G = 0 .--> goto 0 ;
let A be Subset of X ;
assume that A0 is dense and A is dense ;
|. f . x .| <= r ;
let x be Element of R ;
let b be Element of L ;
assume x in W-19 ;
P [ k , a ] ;
let X be Subset of L ;
let b be Object of B ;
let A , B be category ;
set X = Vars , C = Vars , D = Vars , F = F ;
let o be OperSymbol of S ;
let R be connected non empty Poset ;
n + 1 = succ n ;
xx c= Z1 & xx c= Z1 ;
dom f = C1 & dom g = C2 ;
assume [ a , y ] in X ;
Re seq is convergent & lim ( seq ) = 0 ;
assume a1 = b1 & a2 = b2 ;
A = sInt A ;
a <= b or b <= a ;
n + 1 in dom f ;
let F be Instruction of S , i be Nat ;
assume r2 > x0 & r1 < x0 ;
let Y be non empty set , X be set ;
2 * x in dom W ;
m in dom ( g2 * g1 ) ;
n in dom g1 & n + 1 in dom g1 ;
k + 1 in dom f ;
the still of S is finite ;
assume x1 <> x2 & y1 <> y2 ;
v1 in V1 & v2 in V1 ;
not [ b `1 , b ] in T ;
( i + 1 ) = i ;
T c= and T c= and T c= T ;
( l `1 ) ^2 = 0 ;
let n be Nat ;
( t `2 ) = r ;
AA is_integrable_on M & AA is_integrable_on M ;
set t = Top t ;
let A , B be real-membered set ;
k <= len G + 1 ;
cC misses V ( ) ;
product ( seq ) is non empty ;
e <= f or f <= e ;
cluster non empty normal for Ordinal ;
assume c2 = b2 & c2 = b3 ;
assume h in [. q , p .] ;
1 + 1 <= len C ;
not c in B . m1 ;
cluster R .: X -> empty ;
p . n = H . n ;
assume that vseq is convergent and vseq is convergent ;
IC s3 = 0 & IC s3 = 0 ;
k in N or k in K ;
F1 \/ F2 c= F ;
Int G1 <> {} & Int G2 <> {} ;
( z `2 ) ^2 = 0 ;
p11 <> p1 & p1 in P ;
assume z in { y , w } ;
MaxADSet ( a ) c= F ;
ex_sup_of downarrow s , S ;
f . x <= f . y ;
let T be up-complete non empty reflexive antisymmetric RelStr ;
q |^ m >= 1 ;
a is_>=_than X & b is_>=_than Y ;
assume <* a , c *> <> {} ;
F . c = g . c ;
G is one-to-one & H is one-to-one ;
A \/ { a } \not c= B ;
0. V = 0. Y ;
let I be the ] Instruction of S , s ;
f-24 . x = 1 ;
assume z \ x = 0. X ;
C4 = 2 to_power n ;
let B be SetSequence of Sigma ;
assume X1 = p .: D ;
n + l2 in NAT ;
f " P is compact ;
assume x1 in [: the carrier of I[01] , the carrier of I[01] :] ;
p1 `1 = K & p2 `2 = K ;
M . k = <*> REAL ;
phi . 0 in rng phi ;
\frac MMMInt A } is closed
assume z0 <> 0. L & z0 <> 0. L ;
n < ( N . k ) ;
0 <= seq . 0 & seq . 0 <= seq . 0 ;
- q + p = v ;
{ v } is Subset of B ;
set g = f `| 1 ;
[: R , S :] is stable ;
set cR = Vertices R ;
p0 c= P3 & p2 c= P3 ;
x in [. 0 , 1 .[ ;
f . y in dom F ;
let T be Scott Scott Scott Scott Scott Scott of S ;
ex_inf_of the carrier of S , S ;
downarrow a = downarrow b ;
P , C , K is_collinear ;
assume x in F ( s , r , t ) ;
2 to_power i < 2 to_power m ;
x + z = x + z + q ;
x \ ( a \ x ) = x ;
||. x - y .|| <= r ;
assume that Y c= field Q and Y <> {} ;
a ~ , b ~ are_isomorphic ;
assume a in A ( i ) ;
k in dom ( q | Seg 4 ) ;
p is holds p is holds p is holds p is holds p is }
i - 1 = i-1 ;
f | A is one-to-one ;
assume x in f .: X ( ) ;
i2 - i1 = 0 & i2 = 0 ;
j2 + 1 <= i2 & j2 + 1 <= width G ;
g " * a in N ;
K <> { [ {} , {} ] } ;
cluster strict for for for for } : a is strict commutative Ring ;
|. q .| ^2 > 0 ;
|. p4 .| = |. p .| ;
s2 - s1 > 0 & s2 - s1 > 0 ;
assume x in { Gik } ;
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 + j ;
dom S = dom F & rng S c= 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 non void non empty non void holds the - of S is holds S is non empty
let f be ManySortedSet of I ;
let z be Element of COMPLEX , x be Element of COMPLEX ;
u in { ag } ;
2 * n < 2 * n ;
let x , y be set ;
B-11 c= V1 \/ V2 & B-11 c= V1 ;
assume I is_closed_on s , P ;
U2 = U2 & U2 = U2 implies U2 is open
M /. 1 = z /. 1 ;
x11 = x22 & x22 = x22 ;
i + 1 < n + 1 + 1 ;
x in { {} , <* 0 *> } ;
( f . x ) <= ( f . x ) ;
let l be Element of L ;
x in dom ( F . -17 ) ;
let i be Element of NAT ;
r8 is COMPLEX -valued ;
assume <* o2 , o *> <> {} ;
s . x |^ 0 = 1 ;
card K1 in M & card K1 in M ;
assume X in U & Y in U ;
let D be Subset-Family of Omega ;
set r = Seg ( k + 1 ) ;
y = W . ( 2 * x ) ;
assume dom g = cod f & cod g = cod f ;
let X , Y be non empty TopSpace , f be Function of X , Y ;
x \oplus A is interval ;
|. <*> A .| . a = 0 ;
cluster strict for Sublattice of L ;
a1 in B . s1 & a2 in B . s2 ;
let V be finite \rm qua VectSp of F , W be Subspace of V ;
A * B on B , A ;
f-3 = NAT --> 0 .= 0 ;
let A , B be Subset of V ;
z1 = P1 . j & z2 = P2 . j ;
assume f " P is closed ;
reconsider j = i as Element of M ;
let a , b be Element of L ;
assume q in A \/ ( B "\/" C ) ;
dom ( F * C ) = o ;
set S = INT |^ X ;
z in dom ( A --> y ) ;
P [ y , h . y ] ;
{ x0 } c= dom f & { x0 } c= dom f ;
let B be non-empty ManySortedSet of I , A be ManySortedSet of I ;
( PI / 2 ) * PI < Arg z ;
reconsider z9 = 0 , z9 = 1 as Nat ;
LIN a , d , c ;
[ y , x ] in IF ;
( Q Q ) * ( 1 , 3 ) = 0 ;
set j = x0 div m , i = x0 mod m ;
assume a in { x , y , c } ;
j2 - jj > 0 & j2 - 1 > 0 ;
I = 1 & I = 1 ;
[ y , d ] in [: F , F :] ;
let f be Function of X , Y ;
set A2 = ( B \/ C ) /\ C ;
s1 , s2 are_/ 2 implies s1 , s2 are_/ 2
j1 -' 1 = 0 & j2 -' 1 = 0 ;
set m2 = 2 * n + j ;
reconsider t = t as bag of n ;
I2 . j = m . j ;
i |^ s , n are_relative_prime & i |^ n , m are_relative_prime ;
set g = f | D-21 ;
assume that X is lower and 0 <= r ;
( p1 `1 ) ^2 = 1 ;
a < p3 `1 & p3 `1 < b ;
L \ { m } c= UBD C ;
x in Ball ( x , 10 ) ;
not a in LSeg ( c , m ) ;
1 <= i1 -' 1 & i1 -' 1 <= len f ;
1 <= i1 -' 1 & i1 -' 1 <= len f ;
i + i2 <= len h ;
x = W-min ( P ) & y = W-min ( P ) ;
[ x , z ] in X ~ ;
assume y in [. x0 , x .] ;
assume p = <* 1 , 2 , 3 *> ;
len <* A1 *> = 1 ;
set H = h . g9 , I = h . ( g . x ) ;
card b * a = |. a .| ;
Shift ( w , 0 ) |= v ;
set h = h2 ** h1 , g = h2 ** h2 ;
assume x in ( X /\ 4 ) /\ ( X /\ 4 ) ;
||. h .|| < d1 & ||. h .|| < s ;
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 = k\leq ;
<* p , q *> /. 2 = q ;
let S be Subset of the carrier of Y ;
let P , Q be + + t ;
Q /\ M c= union ( F | M )
f = b * ( CFS ( S ) ) ;
let a , b be Element of G ;
f .: X <= f . sup X
let L be non empty transitive reflexive RelStr , X be Subset of L ;
S-20 is x -8 -basis i ;
let r be non positive Real ;
M , v |= x \hbox { y } ;
v + w = 0. ( Z , W ) ;
P [ len ( F | k ) ] ;
assume InsCode ( i ) = 8 or InsCode ( i ) = 7 ;
the zero of M = 0 & the zero of M = 0 ;
cluster z * seq -> summable for Real_Sequence ;
let O be Subset of the carrier of C ;
||. f .|| | X is continuous ;
x2 = g . ( j + 1 ) ;
cluster -> [#] S -> [#] string .. ;
reconsider l1 = l-1 as Nat ;
v4 is Vertex of r2 & v4 is Vertex of G ;
T2 is SubSpace of T2 & T1 is SubSpace of T2 ;
Q1 /\ Q19 <> {} & Q1 /\ Q29 <> {} ;
let k be Nat ;
q " is Element of X & q is Element of X ;
F . t is set of empty ;
assume that n <> 0 and n <> 1 ;
set en = EmptyBag n , en = EmptyBag n ;
let b be Element of Bags n ;
assume for i holds b . i is commutative ;
x is root of ( p `2 ) / ( p `2 ) ;
not r in ]. p , q .] ;
let R be FinSequence of REAL , a be Real ;
S7 does not destroy b1 & S7 does not destroy b1 ;
IC SCM R <> a & IC SCM R <> a ;
|. - |[ x , y ]| .| >= r ;
1 * seq = seq implies seq is convergent & lim seq = 0
let x be FinSequence of NAT , k be Nat ;
let f be Function of C , D , g be Function of C , D ;
for a holds 0. L + a = a
IC s = s . NAT & IC s = n ;
H + G = F\hbox ( G-] ) ;
CS1 . x = x2 & CS2 . x = y2 ;
f1 = f .= f2 .= f2 * f1 ;
Sum <* p . 0 *> = p . 0 ;
assume v + W = v + u + W ;
{ a1 } = { a2 } & { a2 } = { a2 } ;
a1 , b1 _|_ b , a ;
d3 , o _|_ o , a3 ;
II is reflexive & II is reflexive implies I is transitive
IC is antisymmetric implies [: the carrier of C , the carrier of C :] is antisymmetric
sup rng H1 = e & sup rng H2 = e ;
x = ( a * ( - 1 ) ) * ( - 1 ) ;
|. p1 .| ^2 >= 1 ;
assume j2 - 1 < j2 & j2 < len G ;
rng s c= dom f1 & rng s c= dom f2 ;
assume support a misses support b & support b misses support a ;
let L be associative commutative non empty doubleLoopStr , p be Polynomial of L ;
s " + 0 < n + 1 ;
p . c = ( f " ) . 1 ;
R . n <= R . ( n + 1 ) ;
Directed ( I1 , I2 ) = I1 ;
set f = + ( x , y , r ) ;
cluster Ball ( x , r ) -> bounded ;
consider r being Real such that r in A ;
cluster non empty -> non empty NAT -defined for Function ;
let X be non empty directed Subset of S ;
let S be non empty full SubRelStr of L ;
cluster <* [ ] , 0 ] *> -> complete non trivial ;
( 1 - a " ) * ( 1 - a " ) = a ;
( q . {} ) `1 = o ;
n - ( i - 1 ) > 0 ;
assume ( 1 - 2 ) <= t `1 / |. t .| ;
card B = k + 1-1 ;
x in union rng ( f | X ) ;
assume x in the carrier of R & y in the carrier of S ;
d in D ;
f . 1 = L . ( F . 1 ) ;
the vertices of G = { v } & { v } c= G ;
let G be : wfinite _Graph ;
e , v6 be set ;
c . ( i - 1 ) in rng c ;
f2 /* q is divergent_to+infty & f2 /* q is divergent_to+infty ;
set z1 = - z2 , z2 = - z1 ;
assume w is_llof S , G ;
set f = p |-count t , g = p |-count t , h = p |-count t , f = p |-count t , g = p |-count t , h = p |-count t , f = p |-count t
let c be Object of C ;
assume ex a st P [ a ] ;
let x be Element of REAL m , y be Element of REAL m ;
let IB be Subset-Family of X , C be Subset-Family of Y ;
reconsider p = p as Element of NAT ;
let v , w be Point of X ;
let s be State of SCM+FSA , a be Int-Location ;
p is FinSequence of ( the InstructionsF of SCM+FSA ) -valued Function ;
stop I ( ) c= PGij ( a , I ( ) , J ( ) , J ( ) , 3 ( ) ) ;
set ci = ( f /. i ) `1 , ci = ( f /. i ) `1 , ci = ( f /. i ) `1 , ci = ( f /. i ) `1 , c
w ^ t ^ t ^ s ^ t ^ s ^ t ^ t ^ s ^ t ^ t ^ s ^ t ^ t ^ t ^ s ^ t ^ t ^ t ^ s ^ t ^
W1 /\ W = W1 /\ W ` ;
f . j is Element of J . j ;
let x , y be \rm \rm \rm \hbox { - } of T2 ;
ex d st a , b // b , d ;
a <> 0 & b <> 0 & c <> 0 ;
ord x = 1 & x is \sum & y is \sum implies x is \sum
set g2 = lim ( seq ^\ k ) , g1 = lim ( seq ^\ k ) ;
2 * x >= 2 * ( 1 / 2 ) ;
assume ( a 'or' c ) . z <> TRUE ;
f (*) g in Hom ( c , c ) ;
Hom ( c , c + d ) <> {} ;
assume 2 * Sum ( q | m ) > m ;
L1 . F-21 = 0 & L1 . Fk1 = 0 ;
x1 \/ R1 = x1 & y1 = x2 ;
( sin . x ) <> 0 & ( sin . x ) <> 0 ;
( ( #Z 2 ) . x ) ^2 > 0 ;
o1 in ( X /\ O2 ) /\ ( X /\ O2 ) ;
e , v6 be set ;
r3 > ( 1 - 2 * 0 ) / 2 ;
x in P .: ( F -ideal ( L ) ) ;
let J be closed Ideal of R ;
h . p1 = f2 . O & h . O = g2 ;
Index ( p , f ) + 1 <= j ;
len ( q * M ) = width M & width ( q * M ) = width M ;
the carrier of meets ( CK ) ;
dom f c= union rng ( F | X ) ;
k + 1 in support ( support ( n ) ) ;
let X be ManySortedSet of the carrier of S ;
[ x `1 , y `2 ] in an \/ ( the InternalRel of R ) ;
i = D1 or i = D2 or i = D1 ;
assume a mod n = b mod n ;
h . x2 = g . x1 & h . x2 = h . x2 ;
F c= 2 -tuples_on the carrier of X ;
reconsider w = |. s1 .| as Real_Sequence ;
( 1 / m * m + r ) < p ;
dom f = dom ( I --> ( 0 , 1 ) ) ;
[#] P-17 = [#] ( ( ( TOP-REAL 2 ) | K1 ) | K1 ) ;
cluster - x -> ExtReal for ExtReal ;
then { d1 } c= A & A is closed ;
cluster ( TOP-REAL n ) | A -> finite-ind for Subset of TOP-REAL n ;
let w1 be Element of M ;
let x be Element of dyadic ( n ) ;
u in W1 & v in W3 implies u in W2
reconsider y = y as Element of L2 ;
N is full SubRelStr of ( T |^ the carrier of S ) ;
sup { x , y } = c "\/" c ;
g . n = n to_power 1 .= n ;
h . J = EqClass ( u , J ) ;
let seq be -> -> -> -> summable summable sequence of X ;
dist ( x `1 , y ) < ( r / 2 ) ;
reconsider mm = m , mm = n as Element of NAT ;
( - x0 ) < r1 - x0 & ( - r2 ) < x0 ;
reconsider P ` = P ` as strict Subgroup of N ;
set g1 = p * idseq ( q `1 , q `2 ) ;
let n , m , k be non zero Nat ;
assume that 0 < e and f | A is lower ;
D2 . ( I8 . I ) in { x } ;
cluster subcondensed -> subcondensed for Subset of T ;
let P be compact non empty Subset of TOP-REAL 2 , p be Point of TOP-REAL 2 ;
Gik in LSeg ( cos , 1 ) /\ LSeg ( cos , 1 ) ;
let n be Element of NAT , x be Element of X ;
reconsider S8 = S , S8 = T as Subset of T ;
dom ( i .--> X ` ) = { i } ;
let X be non-empty ManySortedSet of S ;
let X be non-empty ManySortedSet of S ;
op ( 1 ) c= { [ {} , {} ] } ;
reconsider m = mm - 1 as Element of NAT ;
reconsider d = x as Element of C ( ) ;
let s be 0 -started State of SCMPDS , a be Int-Location ;
let t be 0 -started State of SCMPDS , Q ;
b , b , b , x , y ;
assume that i = n \/ { n } and j = k \/ { k } ;
let f be PartFunc of X , Y ;
N1 >= ( sqrt c / sqrt 2 ) * ( 2 * n ) ;
reconsider t7 = T-1 as TopSpace of ( TOP-REAL 2 ) | P ;
set q = h * p ^ <* d *> ;
z2 in U . ( y2 , z2 ) /\ Q2 ;
A |^ 0 = { <%> E } & A |^ 0 = { <%> E } ;
len W2 = len W + 2 & len W2 = len W + 2 ;
len h2 in dom h2 & len h2 in dom h2 ;
i + 1 in Seg ( len s2 ) & j + 1 in Seg ( len s2 ) ;
z in dom g1 /\ dom f & z in dom g1 ;
assume p2 `1 = ( E-max ( K ) ) `1 & p2 `2 = ( E-max ( K ) ) `2 ;
len G + 1 <= i1 + 1 ;
f1 (#) f2 is convergent & lim ( f1 (#) f2 ) = x0 ;
cluster ( seq + seq ) - ( seq + seq1 ) -> summable ;
assume j in dom ( M1 * ( i , j ) ) ;
let A , B , C be Subset of X ;
let x , y , z be Point of X , r be Real ;
b ^2 - ( 4 * a * c ) >= 0 ;
<* xx : <* y *> ^ <* y *> ^ <* x *> ^ <* y *> ^ <* x *> ^ <* x *> ^ <* y *> ^ <* x *> ^ <* x *> ^ <* x *> ^ <* x *>
a , b in { a , b } ;
len p2 is Element of ( len p1 ) -tuples_on the carrier of K ;
ex x being element st x in dom R & y = R . x ;
len q = len ( K (#) G ) & len q = width G ;
s1 = Initialize Initialized s , P1 = P +* I , P2 = P +* stop I ;
consider w being Nat such that q = z + w ;
x ` ` is Element of x & y ` is Element of L ;
k = 0 & n <> k or k > n ;
then X is discrete for A is closed ;
for x st x in L holds x is FinSequence ;
||. f /. c .|| <= r1 & ||. f /. c .|| <= g ;
c in uparrow p & not c in { p } ;
reconsider V = V as Subset of the topology of \hbox { 0 } ;
N , M be being being being being \hbox { N } : not contradiction } ;
then z is_>=_than waybelow x & z is_>=_than compactbelow y ;
M \lbrack f , g .] = f & M \lbrack g , g .] = g ;
( ( TOP-REAL 1 ) /. 1 ) = TRUE ;
dom g = dom f & dom g = X ;
mode : of G is \cal : for W being Walk of G holds W is : trivial
[ i , j ] in Indices M & [ i , j ] in Indices M ;
reconsider s = x " , t = y as Element of H ;
let f be Element of ( dom ( Subformulae p ) ) -tuples_on Subformulae ( f ) ;
F1 . ( a1 , - a2 ) = G1 & F1 . ( a2 , - a2 ) = G1 ;
redefine func thesis ( a , b , r ) -> compact ;
let a , b , c , d be Real ;
rng s c= dom ( 1 / f ) & rng s c= dom f ;
curry ( F-19 , k ) is additive & curry ( F-19 , k ) is additive ;
set k2 = card dom B , k1 = card dom C , k2 = card dom C ;
set G = the Sorts of Free ( X , X ) ;
reconsider a = [ x , s ] as of G ;
let a , b be Element of ML , M be Matrix of L ;
reconsider s1 = s , s2 = t as Element of ( the carrier of S ) * ;
rng p c= the carrier of L & p . 0 = 0. L ;
let d be Subset of the Sorts of A ;
( x .|. x = 0 iff x = 0. W ) ;
I-21 in dom stop I & Ik in dom stop I ;
let g be continuous Function of X | B , Y ;
reconsider D = Y as Subset of ( TOP-REAL n ) | P ;
reconsider i0 = len p1 , i2 = len p2 as Integer ;
dom f = the carrier of S & rng f c= the carrier of S ;
rng h c= union ( ( the carrier of J ) --> { x } ) ;
cluster All ( x , H ) -> non \widetilde LSeg ;
d * N1 / 2 > N1 * 1 / 2 ;
]. a , b .[ c= [. a , b .] ;
set g = f " | D1 , h = f " | D2 ;
dom ( p | mm1 ) = mm1 .= dom ( p | mm1 ) ;
3 + - 2 <= k + - 2 ;
tan is_differentiable_in ( ( arccot * arccot ) `| Z ) . x ;
x in rng ( f /^ ( k -' 1 ) ) ;
let f , g be FinSequence of D ;
cp in the carrier of S1 & cp in the carrier of S2 ;
rng f " = dom f & rng f = dom f ;
( the Target of G ) . e = v ;
width G - 1 < width G - 1 ;
assume v in rng ( S | E1 ) & v in rng ( S | E1 ) ;
assume x is root or x is root & y is root ;
assume 0 in rng ( g2 | A ) & 0 < g2 . A ;
let q be Point of ( TOP-REAL 2 ) | K1 , r be Real ;
let p be Point of ( TOP-REAL 2 ) | K1 , q be Point of ( TOP-REAL 2 ) | K1 ;
dist ( O , u ) <= |. p2 .| + 1 ;
assume dist ( x , b ) < dist ( a , b ) ;
<* S7 *> is_in the carrier of C-20 & <* S7 *> is_\! ] ;
i <= len ( G * ( i1 -' 1 , j1 ) ) ;
let p be Point of ( TOP-REAL 2 ) | K1 , q be Point of ( TOP-REAL 2 ) | K1 ;
x1 in the carrier of [: I[01] , I[01] :] & x2 in the carrier of I[01] ;
set p1 = f /. i , p2 = f /. ( i + 1 ) ;
g in { g2 : r < g2 } ;
Q2 = Sp2 " * ( Q * P ) .= ( Q * P ) " * Q ;
( ( 1 / 2 ) to_power ( n + 1 ) ) to_power k is summable ;
- p + I c= - p + A ;
n < LifeSpan ( P1 , s1 ) & I /. ( n + 1 ) = P1 . n ;
CurInstr ( p1 , s1 ) = i & CurInstr ( p2 , s2 ) = halt SCMPDS ;
A /\ Cl { x } \ { x } <> {} ;
rng f c= ]. r , r + 1 .[ ;
let g be Function of S , V ;
let f be Function of L1 , L2 , g be Function of L2 , L1 ;
reconsider z = z as Element of CompactSublatt L ;
let f be Function of S , T ;
reconsider g = g as Morphism of c opp , b opp ;
[ s , I ] in S ~ ( the carrier' of A ) ;
len ( the connectives of C ) = 4 & len ( the connectives of C ) = 5 ;
let C1 , C2 be subFunctor of C , D ;
reconsider V1 = V as Subset of X | B ;
attr p is valid means : Def1 : All ( x , p ) is valid ;
assume that X c= dom f and f .: X c= dom g ;
H |^ a " * H is Subgroup of H & H |^ a = H |^ a ;
let A1 be assume that A1 : E on E1 , A2 ;
p2 , r3 , q2 is_collinear & p2 , q2 , p3 is_collinear ;
consider x being element such that x in v ^ K ;
not x in { 0. TOP-REAL 2 } or not x in { 0. TOP-REAL 2 } ;
p in [#] ( ( I[01] | B11 ) | B11 ) ;
0 . 0 < M . E8 ;
^ ( c , c ) @ = c ;
consider c being element such that [ a , c ] in G ;
a1 in dom ( F . s2 ) & a2 in dom ( F . s2 ) ;
cluster -> 0. for \mathbin { -| } the carrier of L is e -| ;
set i1 = the Nat , i2 = the Element of NAT ;
let s be 0 -started State of SCM+FSA , a be Int-Location ;
assume y in ( f1 \/ f2 ) .: A ;
f . ( len f ) = f /. len f .= f /. 1 ;
x , f . x '||' f . x , f . y ;
pred X c= Y means : Def1 : cos ( X ) c= cos ( Y ) ;
let y be upper Subset of Y , x be Element of X ;
cluster -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> -> of Nat ;
set S = <* Bags n , i *> , T = <* i *> , S = <* i *> , T = <* i *> , S = <* i *> , T = <* i *> , T = <* i *> , S = <* i
set T = [. 0 , 1 / 2 .] , G = [. 0 , 1 .] ;
1 in dom mid ( f , 1 , 1 ) ;
( 4 * PI ) / 2 < ( 2 * PI ) / 2 ;
x2 in dom f1 /\ dom f & x2 in dom f1 /\ dom f ;
O c= dom I & { {} } = { {} } ;
( the Target of G ) . x = v & ( 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 , z , t be Element of G opp ;
h19 . i = f . ( h . i ) ;
( p `1 ) ^2 = ( p1 `1 ) ^2 + ( p2 `2 ) ^2 ;
i + 1 <= len Cage ( C , n ) ;
len <* P *> @ = len P & len <* P *> = 1 ;
set N-26 = the \subseteq of N , N-26 = the Element of N ;
len gfunction + ( x + 1 ) - 1 <= x ;
a on B & b on B implies a on B ;
reconsider rv = r * I . v as FinSequence of REAL ;
consider d such that x = d and a is_less_than d ;
given u such that u in W and x = v + u ;
len f /. ( \downharpoonright n ) = len ( p /^ n ) ;
set q2 = ( Int C ) `2 , q2 = ( E-max C ) `2 ;
set S =
MaxADSet ( b ) c= MaxADSet ( P /\ Q ) ;
Cl ( G . q1 ) c= F . r2 & Cl ( G . q2 ) c= G . r2 ;
f " D meets h " V & f " D meets h " V ;
reconsider D = E as non empty directed Subset of L1 ;
H = ( the_left_argument_of H ) '&' ( the_right_argument_of H ) & H = ( the_left_argument_of H ) '&' ( the_right_argument_of H ) ;
assume t is Element of ( the Sorts of Free ( S , X ) ) . s ;
rng f c= the carrier of S2 & rng g c= the carrier of S2 ;
consider y being Element of X such that x = { y } ;
f1 . ( a1 , b1 ) = b1 & f2 . ( a2 , b2 ) = b2 ;
the carrier' of G opp = E \/ { E } .= { E } ;
reconsider m = len thesis - k as Element of NAT ;
set S1 = LSeg ( n , UMP C ) , S2 = LSeg ( n , UMP C ) ;
[ i , j ] in Indices M1 & [ i , j ] in Indices M1 ;
assume that P c= Seg m and M is \HM { i } is } is { i } ;
for k st m <= k holds z in K . k ;
consider a being set such that p in a and a in G ;
L1 . p = p * L /. ( 1 + 1 ) ;
p-7 . i = pp1 . i & pp2 . i = pp2 . i ;
let PA , PA , G be a_partition of Y , a be Element of Y ;
pred 0 < r & r < 1 & 1 < r & r < 1 ;
rng ( ( a , X ) --> ( a , b ) ) = [#] X ;
reconsider x = x , y = y , z = z as Element of K ;
consider k such that z = f . k and n <= k ;
consider x being element such that x in X \ { p } ;
len ( canFS ( s ) ) = card s .= card ( { 1 } ) ;
reconsider x2 = x1 , y2 = x2 as Element of L2 ;
Q in FinMeetCl ( ( the topology of X ) \/ the topology of Y ) ;
dom ( f . 0 ) c= dom ( u . 0 ) & dom ( f . 0 ) c= dom ( u . 0 ) ;
pred n divides m & m divides n implies n = m ;
reconsider x = x as Point of [: I[01] , I[01] :] ;
a in ; ( the carrier of the carrier of T2 , T2 ) ;
not y0 in the still of f & not y0 in the carrier' of f ;
Hom ( ( a \times b ) \times c , c ) <> {} ;
consider k1 such that p " < k1 and k1 < len f ;
consider c , d such that dom f = c \ d ;
[ x , y ] in [: dom g , dom k :] ;
set S1 = Let ( x , y , z ) , S2 = { x , y , z } ;
l1 = m2 & l1 = i2 & l2 = i2 & l2 = j2 implies E = i2
x0 in dom ( u /\ A ) & x0 in dom ( u + v ) ;
reconsider p = x as Point of ( TOP-REAL 2 ) | K1 ;
m01 = [: the carrier of I[01] , the carrier of I[01] :] & c01 = [: the carrier of I[01] , the carrier of I[01] :] ;
f . p4 <= f . p1 & f . p2 <= f . p3 ;
( ( F . x ) `1 <= ( F . x ) `1 ;
x `2 = ( W `2 ) * ( W `2 ) ;
for n being Element of NAT holds P [ n ] implies P [ n + 1 ]
let J , K be non empty Subset-Family of I ;
assume 1 <= i & i <= len <* a " *> ;
0 |-> a = <*> ( the carrier of K ) .= ( 0 |-> a ) * a ;
X . i in 2 -tuples_on A . i \ B . i ;
<* 0 *> in dom ( e --> [ 1 , 0 ] ) ;
then P [ a ] & P [ succ a ] & P [ succ a ] ;
reconsider sp2 = sp2 as N of D , the carrier' of D ;
( k - 1 ) <= len thesis & ( k - 1 ) <= len thesis ;
[#] S c= [#] ( the TopStruct of T ) & [#] T c= [#] ( the TopStruct of T ) ;
for V being strict real linear space holds V in the carrier of V implies V in the carrier of W
assume k in dom mid ( f , i , j ) & k + 1 in dom mid ( f , i , j ) ;
let P be non empty Subset of TOP-REAL 2 , p be Point of TOP-REAL 2 ;
let A , B be Matrix of n1 , K , n be Nat ;
- a * - b * a = a * b ;
for A being Subset of AS holds A // A implies A // A
( for o2 being Element of B holds o2 in <^ o2 , o2 ^> implies <^ o2 , o1 ^> = <^ o2 , o1 ^>
then ||. x .|| = 0 & x = 0. X ;
let N1 , N2 be strict normal Subgroup of G , N be normal Subgroup of G ;
j >= len upper_volume ( g , D1 ) & 1 <= j & j <= len upper_volume ( g , D1 ) ;
b = Q . ( len Qk - 1 ) & b = Q . ( len Qk - 1 ) ;
f2 * f1 /* s is divergent_to+infty & f2 * f1 is divergent_to+infty ;
reconsider h = f * g as Function of [: N1 , N2 :] , G ;
assume that a <> 0 and Let a , b , c ;
[ t , t ] in the Relation of A & [ t , t ] in the InternalRel of A ;
( v |-- E ) | n is Element of ( T | n ) | ( ( T | n ) | n ) ;
{} = the carrier of L1 + L2 & {} = the carrier of L1 + L2 ;
Directed I is_closed_on Initialized s , P & Directed I is_halting_on Initialized s , P ;
Initialized p = Initialize ( p +* q ) , s1 = p +* q , s2 = p +* q , s3 = p +* q , s3 = p +* q , s3 = p +* q , P3 = p +* q , s4 = p +* q , P4 =
reconsider N2 = N1 , N2 = N2 as strict net of R2 ;
reconsider Y = Y as Element of [: Ids L , Ids L :] ;
"/\" ( uparrow p \ { p } , L ) <> p ;
consider j being Nat such that i2 = i1 + j and j in dom f ;
not [ s , 0 ] in the carrier of S2 & not [ s , 0 ] in the carrier of S2 ;
m9 in ( B '&' C ) '/\' D \ { {} } ;
n <= len ( P + ( len P ) ) & n <= len ( P + ( len P ) ) ;
( x1 `1 ) ^2 = ( x2 `1 ) ^2 + ( x1 `2 ) ^2 ;
InputVertices S = { x1 , x2 , x3 , x4 , x5 , x5 , x5 } ;
let x , y be Element of FTT1 ( n , m ) ;
p = |[ p `1 , p `2 ]| & p `2 = |[ p `1 , p `2 ]| ;
g * 1_ G = h " * g * h * h ;
let p , q be Element of V , a be Element of V ;
x0 in dom x1 /\ dom x2 & x0 in dom x1 /\ dom x2 ;
( R qua Function ) " = R " & ( R " ) " = R " ;
n in Seg len ( f /^ ( i -' 1 ) ) & n in Seg ( i -' 1 ) ;
for s being Real st s in R holds s <= s2 implies s <= 1
rng s c= dom ( f2 * f1 ) & rng s c= dom ( f2 * f1 ) ;
synonym for for for for for for for for for for for for X being Subset of \mathop { X } for X is finite set holds X is finite ;
1. ( K , n ) * 1. ( K , n ) = 1. ( K , n ) ;
set S = Segm ( A , P1 , Q1 ) , T = Segm ( A , P1 , Q1 ) ;
ex w st e = ( w - f ) / ( w - f ) & w in F ;
curry ( P+* ( i , k ) , x ) # x is convergent ;
cluster open open open for Subset of T7 , F be Subset-Family of T ;
len f1 = 1 .= len f3 .= len f2 .= len f3 + 1 ;
( i * p ) / p < ( 2 * p ) / p ;
let x , y be Element of [: the carrier of U0 , the carrier of U0 :] ;
b1 , c1 // b9 , c9 & o , c1 // o , c ;
consider p be element such that c1 . j = { p } ;
assume that f " { 0 } = {} and f is total and f is total ;
assume IC Comput ( F , s , k ) = n & IC Comput ( F , s , k ) in dom I ;
Reloc ( J , card I ) does not destroy a ;
( goto ( card I + 1 ) ) does not destroy c ;
set m3 = LifeSpan ( p3 , s3 ) , s3 = Comput ( p3 , s3 , 1 ) , P4 = P3 ;
IC SCMPDS in dom Initialize ( p +* I ) & IC SCMPDS in dom ( p +* I ) ;
dom t = the carrier of SCM & dom t = the carrier of SCM ;
( ( E-max L~ f ) .. f ) .. f = 1 ;
let a , b be Element of V , c be Element of V ;
Cl Int ( union F ) c= Cl Int ( union F ) ;
the carrier of X1 union X2 misses ( A \/ B ) ;
assume not LIN a , f . a , g . a ;
consider i being Element of M such that i = d6 and i in K ;
then Y c= { x } or Y = {} or Y = { x } ;
M , v |= H1 / ( ( y , x ) / ( y , x ) ) ;
consider m be element such that m in Intersect ( FF , B ) and m in X ;
reconsider A1 = support u1 , A2 = support v1 as Subset of X ;
card ( A \/ B ) = k-1 + ( 2 * 1 ) ;
assume that a1 <> a3 and a2 <> a4 and a3 <> a4 and a3 <> a4 and a3 <> a4 ;
cluster s -\bf -> $ S for string of S ;
LG2 /. n2 = LG2 . n2 & LG2 /. n2 = LG2 . n2 ;
let P be compact non empty Subset of TOP-REAL 2 , p be Point of TOP-REAL 2 ;
assume r-7 in LSeg ( p1 , p2 ) /\ LSeg ( p1 , p2 ) ;
let A be non empty compact Subset of TOP-REAL n , x be Point of TOP-REAL n ;
assume [ k , m ] in Indices ( D1 | Seg n ) ;
0 <= ( ( 1 / 2 ) |^ ( p / 2 ) ) * ( 1 / 2 ) ;
( F . N | E8 ) . x = +infty ;
pred X c= Y & Z c= V & X \ V c= Y \ Z ;
( y `2 * ( z `2 * z `2 ) - 1 ) * ( y `2 * z `2 ) <> 0. I ;
1 + card X-18 <= card u & card X-18 <= card X ;
set g = z \circlearrowleft ( ( E-max L~ z ) .. z ) , M = z .. z , N = ( ( E-max L~ z ) .. z ) .. z , S = ( ( E-max L~ z ) .. z ) .. z , N = ( ( E-max L~ z
then k = 1 & p . k = <* x , y *> . k ;
cluster -> total for Element of C -O ( X , Y ) * ;
reconsider B = A as non empty Subset of ( TOP-REAL n ) | A ;
let a , b , c be Function of Y , BOOLEAN , p be Function of Y , BOOLEAN ;
L1 . i = ( i .--> g ) . i .= g . i .= g . i ;
Plane ( x1 , x2 , x3 ) c= P & Plane ( x2 , x3 , x4 ) c= P ;
n <= indx ( D2 , D1 , j1 ) & 1 <= indx ( D2 , D1 , j1 ) ;
( ( ( g2 . O ) `1 ) / ( 1 + ( g2 . O ) `2 ) ^2 ) = - 1 ;
j + p .. f - len f <= len f - len f ;
set W = W-bound C , E = E-bound C , N = E-bound C , S = E-bound C , N = E-bound C , S = E-bound C , N = E-bound C , N = E-bound C , S = E-bound C , N = E-bound C , S = E-bound
S1 . ( a `1 , e `2 ) = a + e .= a `1 ;
1 in Seg width ( M * ( ColVec2Mx p ) ) & 1 in Seg width ( M * ( ColVec2Mx p ) ) ;
dom ( i (#) Im f ) = dom Im f /\ dom Im f ;
that that ^2 . x = W . ( a , *' ( a , p ) ) ;
set Q = _ _ { > g , f , h } ;
cluster -> topological for ManySortedSet of U1 * -valued Relation of U1 * ;
attr ex A st F = { A } & F is discrete ;
reconsider z9 = \hbox { y where y is Element of product G : y in F } as finite set ;
rng f c= rng f1 \/ rng f2 & f . 0 = f1 . 0 \/ f2 . 0 ;
consider x such that x in f .: A and x in f .: C ;
f = <*> ( the carrier of F_Complex ) & f is FinSequence of the carrier of F_Complex ;
E , j |= All ( x1 , x2 , H ) & E , j |= All ( x2 , x1 , H ) ;
reconsider n1 = n , n2 = m as Morphism of o1 , o2 ;
assume that P is idempotent and R is idempotent and P ** R = R ** P ;
card ( B2 \/ { x } ) = k-1 + 1 ;
card ( ( x \ B1 ) /\ B1 ) = 0 ;
g + R in { s : g-r < s & s < g + r } ;
set q0S = ( q , <* s *> ) -\hbox { [ p , q ] } ;
for x being element st x in X holds x in rng f1 ;
h0 /. ( i + 1 ) = h0 . ( i + 1 ) ;
set mw = max ( B , o ) , mw = max ( B , o ) ;
t in Seg width ( I ^ ( n , n ) ) & t in Seg n ;
reconsider X = dom f /\ C as Element of Fin NAT ;
IncAddr ( i , k ) = <% l . k %> + k .= i + k ;
( ( E-max L~ f ) `2 <= ( q `2 ) / 2 ) `2 ;
attr R is condensed means : Def1 : Int R is condensed & Cl R is condensed & Int R is condensed ;
pred 0 <= a & b <= 1 & a * b <= 1 ;
u in ( ( c /\ ( ( d /\ b ) /\ e ) /\ f ) /\ j ;
u in ( ( c /\ ( ( d /\ e ) /\ b ) /\ f ) /\ j ;
len C + - 2 >= 9 + - 3 & len C + - 3 >= 0 ;
x , z , y is_collinear & x , z , x is_collinear & x , z , y is_collinear ;
a |^ ( n1 + 1 ) = a |^ n1 * a ;
<* \underbrace ( 0 , \dots , 0 ) *> in Line ( x , a * x ) ;
set y9 = <* y , c *> ;
FF2 /. 1 in rng Line ( D , 1 ) & FF2 /. len FF2 = F /. 1 ;
p . m Joins r /. m , r /. ( m + 1 ) , G ;
( p `2 ) = ( f /. i1 ) `2 .= ( f /. i1 ) `2 .= ( f /. i1 ) `2 ;
W-bound ( X \/ Y ) = W-bound ( X \/ Y ) & W-bound ( X \/ Y ) = W-bound ( X \/ Y ) ;
0 + ( p `2 / |. p .| - sn ) <= 2 * r + ( p `2 / |. p .| - sn ) ;
x in dom g & not x in g " { 0 } ;
f1 /* ( seq ^\ k ) is divergent_to+infty & f2 /* ( seq ^\ k ) is divergent_to+infty ;
reconsider u2 = u as VECTOR of P`1 ( X , Y ) ;
p |-count ( Product Sgm ( X11 ) ) = 0 & p |-count ( Product Sgm ( X11 ) ) = 0 ;
len <* x *> < i + 1 & i + 1 <= len c ;
assume that I is non empty and { x } /\ { y } = { 0. I } ;
set ii2 = card I + 4 .--> goto 0 , ii2 = goto 0 , ii2 = goto 0 , ii2 = goto 2 ;
x in { x , y } & h . x = {} T implies x = y
consider y being Element of F such that y in B and y <= x `1 ;
len S = len ( the charact of ( ( the charact of ( A ) ) * ( the charact of B ) ) ;
reconsider m = M , i = I , n = N as Element of X ;
A . ( j + 1 ) = B . ( j + 1 ) \/ A . j ;
set N8 = : G : not ( G is finite & G is finite ) ;
rng F c= the carrier of gr { a } & rng F c= the carrier of gr { a } ;
P is & P is & Q is C & Q is a every -valued FinSequence of D ;
f . k , f . ( Let ( m -' n ) ) in rng f ;
h " P /\ [#] ( T1 | P ) = f " P /\ [#] ( T1 | P ) ;
g in dom f2 \ f2 " { 0 } & ( f2 " ) . g in dom f2 ;
g+ X /\ dom f1 = g1 " X & X /\ dom f1 = dom g1 ;
consider n being element such that n in NAT and Z = G . n ;
set d1 = being elements of dist ( x1 , y1 ) , d2 = dist ( x2 , y2 ) ;
b `2 / ( 1 - sn ) < ( 1 - sn ) / ( 1 - sn ) ;
reconsider f1 = f as VECTOR of the carrier of X , Y ;
pred i <> 0 means i / ( i + 1 ) mod ( i + 1 ) = 1 ;
j2 in Seg len ( ( g2 . i2 ) `2 ) & j2 in Seg ( len g2 ) ;
dom ( i * ( i , j ) ) = dom ( i * ( i , j ) ) .= a ;
cluster sec | ]. PI / 2 , PI / 2 .[ -> one-to-one ;
Ball ( u , e ) = Ball ( f . p , e ) .= Ball ( u , r ) ;
reconsider x1 = x0 , y1 = x1 as Function of S , IC ;
reconsider R1 = x , R2 = y , R2 = z as Relation of L , L ;
consider a , b being Subset of A such that x = [ a , b ] ;
( <* 1 *> ^ p ) ^ <* n *> in RK ;
S1 +* S2 = S2 +* S1 +* S2 & S2 +* S2 = S2 +* S2 +* S2 ;
( ( #Z 2 ) * ( cos * ( f1 + f2 ) ) `| Z ) = f ;
cluster -> continuous for Function of C , REAL , a be Real ;
set C7 = 1GateCircStr ( <* z , x *> , f3 ) , C8 = 1GateCircStr ( <* z , x *> , f3 ) ;
EE . e2 = EE . e2 -carrier of T & EE . e2 = EE . e2 ;
( ( ( - 1 / 2 ) (#) ( ln * f ) ) `| Z ) = f ;
upper_bound A = ( PI * 3 / 2 ) * 2 & lower_bound A = 0 ;
F . ( dom f , - F . ( cod f , - F . ( cod f , - F . ( cod f , - F . ( cod f , - F . ( cod f , - F . ( cod f , - F . ( cod f , - F . ( cod f , - F . ( cod f
reconsider p8 = q8 , p8 = q8 as Point of Euclid 2 ;
g . W in [#] ( Y0 ) & [#] ( Y0 ) c= [#] ( Y ) ;
let C be compact non vertical non horizontal non empty compact Subset of TOP-REAL 2 ;
LSeg ( f ^ g , j ) = LSeg ( f , j ) /\ LSeg ( g , i ) ;
rng s c= dom f /\ ]. -infty , x0 + r .[ & f . ( n + k ) = f . ( n + k ) ;
assume x in { idseq ( 2 ) , Rev ( idseq ( 2 ) , Rev ( 2 ) , Rev ( 2 ) , 2 ) } ;
reconsider n2 = n , m2 = m , n1 = n , n2 = m as Element of NAT ;
for y being ExtReal st y in rng seq holds g <= y ;
for k st P [ k ] holds P [ k + 1 ] ;
m = m1 + m2 .= m1 + m2 .= m1 + m2 .= m1 + m2 ;
assume for n holds H1 . n = G . n -H . n ;
set B-1 = f .: ( the carrier of X1 ) , B-1 = f .: the carrier of X2 ;
ex d being Element of L st d in D & x << d ;
assume R " ( a ) c= R " ( b ) & R " ( a ) c= R " ( b ) ;
t in ]. r , s .] or t = r or t = s or t = s ;
z + v2 in W & x = u + ( z + v2 ) ;
x2 |-- y2 iff P [ x2 , y2 ] & P [ x2 , y2 ] & P [ x2 , y2 ] ;
pred x1 <> x2 & |. x1 - x2 .| > 0 & |. x1 - x2 .| > 0 ;
assume p2 - p1 , p3 - p1 - p2 , p3 - p1 - p2 , p3 - p1 - p2 - p3 is_collinear ;
set q = ( \mathbb f ) ^ <* 'not' 'not' A *> ;
let f be PartFunc of REAL-NS 1 , REAL-NS n , x be Point of REAL-NS 1 , r be Real ;
( n mod ( 2 * k ) ) + 1 = n mod k ;
dom ( T * ( succ t ) ) = dom ( T * ( succ t ) ) ;
consider x be element such that x in wc iff x in c ;
assume ( F * G ) . ( v . x3 ) = v . x3 ;
assume that the Sorts of D1 c= the Sorts of D2 and the Sorts of D2 c= the Sorts of D1 and the Sorts of D1 c= the Sorts of D2 ;
reconsider A1 = [. a , b .[ , A2 = [. 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 L~ Cage ( C , n ) , q = W-min L~ Cage ( C , n ) , G = Gauge ( C , n ) * ( i , 1 ) , G = Gauge ( C , n ) * ( i , 1 ) , G = Gauge ( C , n ) * ( i , 1 ) , G
n1 - len f + 1 <= len ( - 1 ) + 1 - len f ;
\lbrace q , O1 , a , b , b , a , b , b , c } = { u , v , w } ;
set C-2 = ( ( `1 ) | ( G .order() -' 1 ) ) . ( k + 1 ) ;
Sum ( L (#) p ) = 0. R * Sum p .= 0. V * Sum p .= 0. V ;
consider i be element such that i in dom p and t = p . i ;
defpred Q [ Nat ] means 0 = Q ( $1 ) & $1 <= n implies $1 <= n ;
set s3 = Comput ( P1 , s1 , k ) , P3 = Comput ( P2 , s2 , k ) , P4 = P2 , P4 = Comput ( P2 , s2 , k ) , P4 = Comput ( P2 , s2 , k ) , P4 = P2 , P4 = Comput ( P2 , s2 , k )
let l be variable of k , A , A-30 be S -|^ k ;
reconsider U2 = union G-24 , G-24 = union G-24 as Subset-Family of ( T | A ) | A ;
consider r such that r > 0 and Ball ( p `1 , r ) c= Q ` ;
( h | ( n + 2 ) ) /. ( i + 1 ) = p2 ;
reconsider B = the carrier of X1 , C = the carrier of X2 as Subset of X ;
por = <* - c9 , 1 *> & pS = <* - c9 , 1 *> ;
synonym f is real-valued means : Def1 : rng f c= NAT & rng f c= NAT ;
consider b being element such that b in dom F and a = F . b ;
xx < card X0 + card Y0 & xx in card ( Y0 \/ Y0 ) & xx in card ( Y0 \/ Y0 ) ;
pred X c= B1 means : Def1 : for B st X c= succ B holds X c= succ B & X c= B ;
then w in Ball ( x , r ) & dist ( x , w ) <= r ;
angle ( x , y , z ) = angle ( x , y , z ) ;
pred 1 <= len s means : Def1 : for s being Element of ( the carrier of S ) * holds s . ( s , 0 ) = s . ( s , 0 ) ;
f-47 c= f . ( k + ( n + 1 ) ) ;
the carrier of { 1_ G } = { 1_ G } & the carrier of G = { 1_ G } ;
pred p '&' q in to & q '&' p in WFF & q '&' p in WFF ;
- ( t `1 / t `2 ) < ( t `2 / t `2 ) / t `2 ;
U2 . 1 = U2 /. 1 .= ( U2 /. 1 ) `1 .= ( U2 /. 1 ) `1 .= ( U2 /. 1 ) `1 ;
f .: ( the carrier of x ) = the carrier of x & f .: ( the carrier of x ) = the carrier of x ;
Indices ( O * ( i , j ) ) = [: Seg n , Seg n :] & Indices ( O * ( i , j ) ) = [: Seg n , Seg n :] ;
for n being Element of NAT holds G . n c= G . ( n + 1 ) ;
then V in M @ ;
ex f being Element of F-9 st f is \cup ( A , B ) & f is \cup ( B , C ) ;
[ h . 0 , h . 3 ] in the InternalRel of G & [ h . 2 , h . 3 ] in the InternalRel of G ;
s +* Initialize ( ( intloc 0 ) .--> 1 ) = s3 +* Initialize ( ( intloc 0 ) .--> 1 ) ;
|[ w1 , v1 ]| - |[ w1 , v1 ]| <> 0. TOP-REAL 2 & |[ w1 , v1 ]| - |[ w1 , v1 ]| = 0. TOP-REAL 2 ;
reconsider t = t as Element of ( the carrier of INT ) * ;
C \/ P c= [#] ( ( G | ( [#] ( ( ( G | A ) \ A ) ) \ A ) ) ;
f " V in ( the topology of X ) /\ D & f " V in D /\ ( the topology of X ) ;
x in [#] ( ( the carrier of ( F . m ) /\ A ) ) /\ the carrier of ( ( F . m ) /\ A ) ;
g . x <= h1 . x & h . x <= h1 . x ;
InputVertices S = { xy , y , z } & InputVertices S = { xy , y , z } ;
for n being Nat st P [ n ] holds P [ n + 1 ] ;
set R = Line ( M , i , a * Line ( M , i ) ) ;
assume that M1 is being_line and M2 is being_line and M3 is being_line and M3 is being_line and M3 is being_line and M3 is being_line ;
reconsider a = f4 . ( i0 -' 1 ) , b = f4 . ( i0 -' 1 ) as Element of K ;
len B2 = Sum ( Len ( F1 ^ F2 ) ) .= len ( Len ( F1 ^ F2 ) ) + len ( Len ( F1 ^ F2 ) ) ;
len ( ( the ` of n ) * ( i , j ) ) = n & len ( ( i , j ) * ( i , j ) ) = n ;
dom max ( - ( f + g ) , f + g ) = dom ( f + g ) ;
( for n holds seq . n = upper_bound Y1 ) implies seq is convergent & lim seq = upper_bound ( seq * ( seq * ( seq * ( seq * ( seq * ( seq * ( seq * ( seq * ( seq * ( seq * ( seq * ( seq * ( seq * ( seq * seq1 ) ) ) ) )
dom ( p1 ^ p2 ) = dom ( f ^ p2 ) .= dom ( f ^ p1 ) /\ dom ( f ^ p2 ) ;
M . [ 1 / y , y ] = 1 / y * v1 .= 1 / y * v1 .= 1 / y ;
assume that W is non trivial and W .vertices() c= the carrier' of G2 and W is trivial and W is trivial ;
C6 * ( i1 , i2 ) = G1 * ( i1 , i2 ) .= G1 * ( i1 , i2 ) ;
C8 |- 'not' Ex ( x , p 'or' p ) ;
for b st b in rng g holds lower_bound rng f\lbrace b - a , b + a .[ <= b
- ( ( q1 `1 / |. q1 .| - cn ) / ( 1 + cn ) ) = 1 ;
( LSeg ( c , m ) \/ [: l , k :] ) \/ LSeg ( l , k ) c= R ;
consider p be element such that p in ( such that p in S and p in L~ f and x = f /. p ;
Indices ( X @ ) = [: Seg n , Seg 1 :] & Indices ( X @ ) = [: Seg n , Seg 1 :] ;
cluster s => ( q => p ) => ( q => ( s => p ) ) -> valid ;
Im ( ( Partial_Sums F ) . m , ( Partial_Sums F ) . n ) is_measurable_on E ;
cluster f . ( x1 , x2 ) -> Element of D ( ) * ;
consider g being Function such that g = F . t and Q [ t , g ] ;
p in LSeg ( ( Int Z ) , ( E-max Z ) `2 ) /\ LSeg ( ( E-max Z ) , ( E-max Z ) `2 ) ;
set R8 = R / ( 1 / 2 ) , R8 = ( 1 / 2 ) (#) ( R / 2 ) ;
IncAddr ( I , k ) = SubFrom ( da , db ) .= SubFrom ( da , db ) .= IncAddr ( da , db ) ;
seq . m <= ( ( the Sorts of seq ) . k ) . ( ( the Sorts of seq ) . k ) ;
a + b = ( a ` *' b ) ` + ( a ` *' b ) ` .= ( a ` ` ) ` + ( a ` ` ) ` ;
id ( X /\ Y ) = id X /\ id ( Y /\ X ) .= 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 , U1 , U2 be non empty Subset of U0 ;
u in ( ( c /\ ( ( d /\ e ) /\ b ) /\ f ) /\ m ;
consider y being element such that y in Y and P [ y , inf B ] ;
consider A being finite stable set of R such that card A = ( the carrier of R ) \ A ;
p2 in rng ( f |-- p1 ) \ rng <* p1 *> & p2 in rng ( f |-- p1 ) \ { p2 } ;
len s1 - 1 > 0 & len s2 - 1 > 0 & len s2 - 1 > 0 ;
( ( N-min ( P ) ) `2 = N-bound ( P ) & ( ( E-max ( P ) ) `2 ) = N-bound ( P ) ;
Ball ( e , r ) c= LeftComp Cage ( C , k + 1 ) & Ball ( e , r ) c= LeftComp Cage ( C , k + 1 ) ;
f . a1 ` = f . a1 ` & f . a2 = f . a2 ` ;
( seq ^\ k ) . n in ]. -infty , x0 + r .[ & ( seq ^\ k ) . n in ]. x0 , x0 + r .[ ;
gg . s0 = g . s0 | G . s0 .= g . s0 .= g . s0 ;
the InternalRel of S is \lbrace x , y } & the InternalRel of S is transitive ;
deffunc F ( Ordinal , Ordinal ) = phi . ( $1 + 1 ) & $2 = phi . ( $1 + 1 ) ;
F . s1 . a1 = F . s2 . a1 .= F . s2 . a1 .= F . s2 . a1 ;
x `2 = A . a .= Den ( o , A . a ) . x ;
Cl ( f " P1 ) c= f " ( Cl P1 ) & Cl ( f " P1 ) c= f " ( Cl P1 ) ;
FinMeetCl ( ( the topology of S ) \/ the topology of T ) c= the topology of T ;
synonym o is \bf means : Def1 : o <> \ast & o <> {} & o <> {} & o <> {} ;
assume that X c= Y and card X <> card Y and card Y <> card Z and card X <> card Z ;
the { F ( s ) -> 1 + ( the *> , ( the ) -\geq 1 + ( the <* F ( s ) , ( the carrier' of S ) . ( s , n + 1 ) ) ) ;
LIN a , a1 , d or b , c // b1 , c1 or b , c // c1 , c1 ;
e / 2 . 1 = 0 & e / 2 . 2 = 1 & e / 2 . 3 = 0 ;
Ef in SS1 & ES2 in { NS1 } & ES2 in { NS2 } ;
set J = ( l , u ) If , K = I " ;
set A1 = } , A2 = } , A2 = { A1 , A2 , p3 } ;
set c9 = [ <* c , d *> , '&' ] , d9 = [ <* d , c *> , '&' ] , I = [ <* c , d *> , '&' ] , T = [ <* d , c *> , '&' ] , T = [ <* c , d *> , '&' ] , D = [ <* c , d *> , '&' ] , E =
x * z `2 * x " in x * ( z * N ) * x " ;
for x being element st x in dom f holds f . x = f3 . x & f . x = f . x
Int cell ( f , 1 , G ) c= RightComp f \/ RightComp f \/ L~ f \/ L~ f \/ L~ f ;
U2 is_an_arc_of W-min ( C ) , E-max ( C ) , E-max ( C ) , E-max ( C ) ;
set f-17 = f @ "/\" g @ ;
attr S1 is convergent means : Def1 : S2 is convergent & lim ( S1 - S2 ) = 0 & ( for n holds S1 . n = S2 . n ) ;
f . ( 0 + 1 ) = ( 0 qua Ordinal ) + a .= a ;
cluster -> } -be be be be be be be be } transitive reflexive transitive non empty reflexive transitive RelStr , F be Function of F , G -symmetric Function ;
consider d being element such that R reduces b , d and R reduces c , d and R reduces d , b ;
not b in dom Start-At ( ( card I + 2 ) , SCMPDS ) & not b in dom Start-At ( ( card I + 2 ) , SCMPDS ) ;
( z + a ) + x = z + ( a + y ) .= z + a + y ;
len ( l \lbrack a |^ 0 , x |^ 0 .] ) = len l .= len l ;
t4 ^ {} is ( {} \/ rng t4 ) -valued FinSequence of ( {} \/ rng t4 ) * * * \ { {} } ;
t = <* F . t *> ^ ( C . ( p ^ q ) ) .= <* F . ( p ^ q ) *> ^ q ;
set p-2 = W-min L~ Cage ( C , n ) , p-2 = W-min L~ Cage ( C , n ) , p-2 = W-min L~ Cage ( C , n ) , p-2 = W-bound L~ Cage ( C , n ) , p-2 = W-bound L~ Cage ( C , n ) , p-2 = W-bound L~ Cage ( C , n )
( k -' ( i + 1 ) ) - ( i + 1 ) = ( k - ( i + 1 ) ) - ( i + 1 ) ;
consider u being Element of L such that u = u ` and u in D and u in D ;
len ( ( width E ) |-> a ) = width E & width ( ( len E ) |-> a ) = width E ;
FM . x in dom ( ( G * the_arity_of o ) . x ) & FM . x in dom ( G * the_arity_of o ) ;
set cH2 = the carrier of H2 , cH2 = the carrier of H2 ;
set cH1 = the carrier of H1 , cH2 = the carrier of H2 ;
( Comput ( P , s , 6 ) ) . intpos m = s . intpos m .= Comput ( P , s , 6 ) . intpos m ;
IC Comput ( Q2 , t , k ) = ( l + 1 ) + 1 .= IC Comput ( Q2 , t , k ) ;
dom ( ( cos * sin ) `| Z ) = REAL & dom ( ( cos * sin ) `| Z ) = dom ( ( cos * sin ) `| Z ) ;
cluster <* l *> ^ phi -> ( 1 + 1 ) -element for string of S ;
set b9 = [ <* \setminus ( p , q ) , '&' ] , c9 = [ <* p , q *> , '&' ] , S ] ;
Line ( Segm ( M @ , P , Q ) , x ) = L * Sgm Q ;
n in dom ( ( the Sorts of A ) * ( the_arity_of o ) ) & n in dom ( ( the Sorts of A ) * ( the_arity_of o ) ) ;
cluster f1 + f2 -> continuous for PartFunc of REAL , the carrier of S , the carrier of T ;
consider y be Point of X such that a = y and ||. y - x .|| <= r ;
set x3 = t2 . DataLoc ( s2 . SBP , 2 ) , x4 = s2 . DataLoc ( s2 . SBP , 2 ) , P4 = Comput ( P2 , s2 , 2 ) , P4 = Comput ( P2 , s2 , 2 ) , P4 = P2 . DataLoc ( s2 . SBP , 2 ) , P4 = Comput ( P2 , s2
set p-3 = stop I , pE = stop I , pE = stop I ;
consider a being Point of D2 such that a in W1 and b = g . a and a in W2 ;
{ A , B , C , D , E } = { A , B , C } \/ { D , E , F , J , M }
let A , B , C , D , E , F , J , M , N , N , M , N , N , M , N , N , M , N , N , N , M , N , N , M , N , N , N , M , N , N , N , M , N , N ,
|. p2 .| ^2 - ( p2 `2 ) ^2 - ( p2 `2 ) ^2 >= 0 ;
l - 1 + 1 = n-1 * ( m + 1 ) + ( 1 + 1 ) ;
x = v + ( a * w1 + b * w2 ) + ( c * w2 ) + ( c * w2 ) ;
the TopStruct of L = |. ( the TopStruct of L ) . ( the Scott of L ) .| .= the TopStruct of L ;
consider y being element such that y in dom H1 and x = H1 . y and y in H ;
f9 \ { n } = ( \mathop { v1 , v2 } ) \ { v1 , v2 } .= ( the Sorts of Free ( C , n ) ) \ { v2 } ;
for Y being Subset of X st Y is summable holds Y is iff Y is non empty & X is Seg implies Y is Seg k
2 * n in { N : 2 * Sum ( p | N ) = N & N > 0 } ;
for s being FinSequence holds len ( the { 0 } --> \rm seq ( s ) ) = len s & for i being Nat st i in dom s holds s . i = F ( i )
for x st x in Z holds exp_R * f is_differentiable_in x & ( exp_R * f ) . x > 0 ;
rng ( h2 * f2 ) c= the carrier of ( ( TOP-REAL 2 ) | ( the carrier of ( TOP-REAL 2 ) | K1 ) ) | K1 ;
j + ( - len f ) <= len f + ( len f - len f ) - len f ;
reconsider R1 = R * I as PartFunc of REAL , REAL-NS n , REAL-NS n ;
C8 . x = s1 . a .= C8 . x .= C8 . x .= C8 . x ;
power ( F_Complex ) . ( z , n ) = 1 .= x |^ n .= x |^ n ;
t at ( C , s ) = f . ( the connectives of S ) . t & t at ( C , s ) = f . t ;
support ( f + g ) c= support f \/ C & support ( f + g ) c= support f \/ support g ;
ex N st N = j1 & 2 * Sum ( seq1 | N ) > N & N > 0 ;
for y , p st P [ p ] holds P [ All ( y , p ) ] & P [ All ( y , p ) ]
{ [ x1 , x2 ] where x1 is Point of [: X1 , X2 :] , x2 is Point of X2 } is Subset of X ;
h = ( j , j ) |-- ( id B , id B ) . i .= H . i ;
ex x1 being Element of G st x1 = x & x1 * N c= A & N c= A ;
set X = ( ( |. q .| ) * ( ( q , O1 ) `1 ) / ( 2 , 4 ) ) ;
b . n in { g1 : x0 < g1 & g1 < x0 } & ( for n st n >= k holds g1 . n < x0 ) implies f . n < f . x0
f /* s1 is convergent & f /. x0 = lim ( f /* s1 ) implies f /* s1 is convergent & f /. x0 = lim ( f /* s1 )
the lattice of Y = the lattice of the lattice of Y & the carrier of Y = the carrier of Y & the carrier of Y = the carrier of Z ;
'not' ( a . x ) '&' b . x 'or' a . x '&' 'not' ( b . x ) = FALSE ;
2 = len ( ( q ^ r1 ) ^ ( r1 ^ r2 ) ) + len ( ( q ^ r2 ) ^ ( r1 ^ r2 ) ) ;
( 1 / a ) (#) ( sec * f1 ) - id Z * ( ( 1 / a ) (#) ( sec * f1 ) ) is_differentiable_on Z ;
set K1 = integral ( ( lim ( H , A ) || ( A , B ) ) , D2 = integral ( H , A ) || ( B , B ) ;
assume e in { ( w1 - w2 ) / ( w1 - w2 ) : w1 in F & w2 in G } ;
reconsider d7 = dom a `1 , d6 = dom F `1 , d6 = dom F `1 , d6 = dom F `1 , d6 = dom F `1 , d6 = dom F `1 , d6 = dom F `1 , d6 = dom F `1 , d6 = dom F `1 , d6 = dom F `1 , d6 = dom F `1
LSeg ( f /^ j , q ) = LSeg ( f , j + q .. f -' 1 + q .. f -' 1 ) ;
assume X in { T . ( N2 , K ) : h . ( N2 , K ) = N2 } ;
assume that Hom ( d , c ) <> {} and <* f , g *> * f1 = <* f , g *> * f2 ;
dom S29 = dom S /\ Seg n .= dom ( L29 | Seg n ) .= dom ( L29 | Seg n ) .= Seg n /\ Seg n .= Seg n /\ Seg n .= Seg n ;
x in H |^ a implies ex g st x = g |^ a & g in H & a in H
* ( 0. ( Z , n ) , a ) = a `1 - ( 0 * n ) .= a `1 - a `1 ;
D2 . j in { r : lower_bound A <= r & r <= D1 . i } ;
ex p being Point of TOP-REAL 2 st p = x & P [ p ] & p `2 <= 0 & p <> 0. TOP-REAL 2 ;
for c holds f . c <= g . c implies f @ @ = g @ @ c
dom ( f1 (#) f2 ) /\ X c= dom ( f1 (#) f2 ) /\ X & dom ( f1 (#) f2 ) /\ X c= dom f1 /\ X ;
1 = ( p * p ) * p .= p * ( p * p ) .= p * 1 .= p * 1 ;
len g = len f + len <* x + y *> .= len f + 1 .= len f + 1 .= len f + 1 ;
dom ( F-11 = dom ( F | [: N1 , S :] ) .= [: N1 , S :] .= [: N1 , S :] ;
dom ( f . t * I . t ) = dom ( f . t * g . t ) .= dom ( f . t * g . t ) ;
assume a in ( "\/" ( ( T |^ the carrier of S ) , F ) ) .: D ;
assume that g is one-to-one and ( the carrier' of S ) /\ rng g c= dom g and g is one-to-one ;
( ( x \ y ) \ z ) \ ( ( x \ z ) \ ( y \ z ) ) = 0. X ;
consider f such that f * f opp = id b and f * f = id a and f * f = id b ;
( cos | [. 2 * PI * 0 , PI * 0 + 2 * PI * 0 .] ) is increasing ;
Index ( p , co ) <= len LS - Gij .. LS & Index ( Gij , LS ) + 1 <= len LS ;
let t1 , t2 , t2 , t2 , t1 , t2 , t2 , t2 , t2 , t2 , t2 , t1 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2 , t2
& > & j <= "/\" ( ( Frege ( ( ( curry G ) . j ) ) , L ) & j <= j implies j <= i
then P [ f . i0 , f . ( i0 + 1 ) ] & F ( f . i0 , f . ( i0 + 1 ) ) < j ;
Q [ [ D ( x ) , 1 ] , F ( D ( x ) , 1 ) ] ;
consider x being element such that x in dom ( F . s ) and y = F . s . x ;
l . i < r . i & [ l . i , r . i ] is for i being Nat holds r . i is f of G . i ;
the Sorts of A2 = ( the carrier of S2 ) --> the carrier of S2 .= the carrier of S2 ;
consider s being Function such that s is one-to-one and dom s = NAT and rng s = F and for n being Nat st n in NAT holds s . n = F ( n ) ;
dist ( b1 , b2 ) <= dist ( b1 , a ) + dist ( a , b2 ) & dist ( a , b2 ) <= dist ( a , b2 ) + dist ( b , b1 ) ;
( <* Cage ( C , n ) /. len ( C /. 1 ) *> /. 1 ) `1 = W-bound L~ Cage ( C , n ) ;
q `2 <= ( UMP ( Upper_Arc ( C ) ) `2 & p `2 <= ( UMP ( C ) ) `2 ;
LSeg ( f | i2 , i ) /\ LSeg ( f | i2 , j ) = {} & LSeg ( f | i2 , j ) /\ LSeg ( f , i ) = {} ;
given a being ExtReal such that a <= II and A = ]. a , II .] and a <= b ;
consider a , b be complex number such that z = a & y = b & z + y = a + b ;
set X = { b |^ n where n is Element of NAT : n <= m } , Y = { b |^ n where m is Element of NAT : m <= n } ;
( ( x * y * z \ x ) \ z ) \ ( x * y \ x ) = 0. X ;
set xy = [ <* xy , y *> , f1 ] , yz = [ <* y , z *> , f2 ] , yz = [ <* z , x *> , f3 ] , zx = [ <* z , x *> , f3 ] , zx = [ <* z , x *> , f3 ] , zx = [ <* z , x *> , f3 ] ;
( l /. len ( l /. 1 ) ) `1 = ( l /. len ( l /. 1 ) ) `1 .= ( l /. 1 ) `1 ;
( ( q `2 / |. q .| - sn ) / ( 1 - sn ) ) * ( 1 - sn ) = 1 ;
( ( p `2 / |. p .| - sn ) / ( 1 - sn ) ) * ( 1 - sn ) < 1 ;
( ( ( ( S \/ Y ) `2 ) / 2 ) * ( ( S \/ Y ) / 2 ) = ( ( ( S \/ Y ) / 2 ) * ( ( S \/ Y ) / 2 ) ) * ( ( S \/ Y ) / 2 ) ;
( seq - seq ) . k = seq . k - seq . ( k + 1 ) .= seq . k - seq . ( k + 1 ) ;
rng ( ( h + c ) ^\ n ) c= dom SVF1 ( 1 , f , u0 ) /\ dom SVF1 ( 1 , f , u0 ) ;
the carrier of X = the carrier of X & the carrier of X = the carrier of X & the carrier of X = the carrier of X ;
ex p4 st p3 = p4 & |. p4 - |[ a , b ]| .| = r & |. p4 - |[ a , b ]| .| = r ;
set ch = chi ( X , A5 ) , c5 = chi ( X , A5 ) ;
R |^ ( 0 * n ) = I\HM ( X , X ) .= R |^ n |^ 0 .= R |^ n ;
( Partial_Sums ( ( curry ( F1 , n ) ) . n ) . m is nonnegative & ( ( ( ( , n ) to_power k ) to_power k ) to_power k ) . m <= ( ( ( ( , n ) to_power k ) to_power k ) to_power k ) to_power k ) to_power k ;
f2 = C7 . ( E7 , len ( V , K ) ) .= V . ( len ( V , K ) ) ;
S1 . b = s1 . b .= s2 . b .= s2 . b .= ( s2 * ( s1 * ( s2 * ( s2 * ( s2 * ( s2 * ( s2 * ( s2 * ( s2 * ( s2 * ( s1 * ( s2 * ( s2 * ( s2 * ( s2 * ( s2 * ( s2 * ( s2 * ( s2 * ( s2 * ( s2 * ( s2 * (
p2 in LSeg ( p2 , p1 ) /\ LSeg ( p1 , p2 ) \/ LSeg ( p1 , p2 ) \/ LSeg ( p2 , p1 ) ;
dom ( f . t ) = Seg n & dom ( I . t ) = Seg n & rng ( I . t ) c= Seg n ;
assume o = ( the connectives of S ) . 11 & o in ( the carrier' of S ) . 11 ;
set phi = ( l1 , l2 ) \mathop { l1 , l2 } , F = ( l1 , l2 ) \mathop { l1 , l2 } , G = ( l1 , l2 ) \mathop { l1 , l2 } , F = ( l1 , l2 ) \mathop { l1 , l2 } , G = ( l1 , l2 ) \mathop { l1 , l2 } , D = ( l1 , l2 ) \mathop { l1 , l2 } , F =
synonym p is invertible means : Def1 : ex q being Polynomial of n , L st q = ( f *' ) . ( p , q ) ;
( Y1 `2 = - 1 & 0. ( ( TOP-REAL 2 ) | ( Y1 ) ) <> 0. ( ( TOP-REAL 2 ) | ( Y1 ) ) ;
defpred X [ Nat , set , set ] means P [ $1 , $2 , , , , , , , , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 , $2 is_collinear
consider k being Nat such that for n being Nat st k <= n holds s . n < x0 + g ;
Det ( I ^ ( m -' n ) ) * ( m -' n ) = 1. ( K , n ) * ( m -' n ) ;
( - b - sqrt ( b ^2 - 4 * a * c ) ) / 2 < 0 ;
CK . d = C7 . d mod C7 . d & C8 . d = C8 . d mod C7 . d ;
attr X1 is dense means : Def1 : X2 is dense dense & X1 /\ X2 is dense SubSpace of X & X1 /\ X2 is dense SubSpace of X ;
deffunc F6 ( Element of E , Element of I ) = $1 * ( $2 * ( $1 , $2 ) ) ;
t ^ <* n *> in { t ^ <* i *> : Q [ i , T . t ] } ;
( x \ y ) \ x = ( x \ x ) \ y .= y ` \ 0. X .= 0. X ;
for X being non empty set for Y being Subset-Family of X holds for X being Subset-Family of [: X , product Y :] holds X is Basis of [: X , product Y :]
synonym A , B are_separated means : Def1 : Cl ( A , B ) misses Cl B & A misses B ;
len ( M @ ) = len p & width ( M @ ) = width ( M @ ) & width ( M @ ) = width ( M @ ) ;
J . v = { x where x is Element of K : 0 < v . x & v . x = 0. K } ;
( Sgm Seg m ) . d - ( Sgm Seg m ) . e <> 0 ;
lower_bound divset ( D2 , k + k2 ) = D2 . ( k + k2 - 1 ) .= lower_bound divset ( D1 , k + ( 1 + 1 ) - 1 ) ;
g . r1 = - 2 * r1 + 1 & dom h = [. 0 , 1 .] & rng h c= [. 0 , 1 .] ;
|. a .| * ||. f .|| = 0 * ||. f .|| .= ||. a * f .|| .= ||. a * f .|| .= ||. a * f .|| .= ||. a * f .|| ;
f . x = ( h . x ) `1 & g . x = ( h . x ) `2 & h . y = ( h . y ) `2 ;
ex w st w in dom B1 & <* 1 *> ^ s = <* 1 *> ^ w & for i st i in dom B1 holds w . i = <* 1 *> ^ w ;
[ 1 , {} , <* d1 *> ] in ( { [ 0 , {} , {} ] } \/ S1 ) \/ S2 ;
IC Exec ( i , s1 ) + n = IC Exec ( i , s2 ) .= IC Exec ( i , s2 ) .= IC Exec ( i , s2 ) ;
IC Comput ( P , s , 1 ) = IC Comput ( P , s , 9 ) .= 5 + 9 .= 5 ;
( IExec ( W6 , Q , t ) ) . intpos ( e + 2 ) = t . intpos ( e + 2 ) .= t . intpos ( e + 2 ) ;
LSeg ( f /^ q , i ) misses LSeg ( f /^ q , j ) \/ LSeg ( f /^ q , j ) ;
assume for x , y being Element of L st x in C & y in C holds x <= y or y <= x ;
integral ( integral ( C , f , X ) , x ) = f . ( upper_bound C ) - lower_bound C ;
for F , G being one-to-one FinSequence st rng F misses rng G holds F ^ G is one-to-one & F ^ G is one-to-one
||. R /. ( L . h ) - R /. ( L . h ) .|| < e1 * ( K . h ) ;
assume a in { q where q is Element of M : dist ( z , q ) <= r } ;
set p4 = [ 2 , 1 ] .--> [ 2 , 0 , 1 ] ;
consider x , y being Subset of X such that [ x , y ] in F and x c= d and y \not c= d ;
for y , x being Element of REAL st y ` in Y & x in X holds y ` <= x ` + x ` ;
func |. p \bullet q .| -> variable of A means : Def1 : for i being Nat st i in dom it holds it . i = min ( NBI . i , p . i ) ;
consider t being Element of S such that x `1 , y `2 '||' z `1 , t `2 and x `2 , z `2 '||' y , t `2 ;
dom x1 = Seg ( len x1 ) & len x1 = len l1 & for i st i in Seg ( len x1 ) holds x1 . i = x1 . i ;
consider y2 being Real such that x2 = y2 and 0 <= y2 & y2 <= 1 / 2 and y2 <= 1 / 2 ;
||. f | X .|| /* s1 = ||. f .|| /* s1 & ||. f .|| /* s1 = ||. f /. s1 .|| & ||. f /. s1 .|| = ||. f /. s1 .|| ;
( the InternalRel of A ) ` /\ Y ` = {} \/ {} .= {} \/ {} .= {} \/ {} .= {} \/ {} .= {} \/ {} .= {} ;
assume i in dom p implies for j being Nat st j in dom q holds P [ i , j ] & i + 1 in dom p & j + 1 in dom q ;
reconsider h = f | X ( ) as Function of X ( ) , rng f , rng f , rng f , rng f , rng f , rng f , rng f , rng f , rng f :] ;
u1 in the carrier of W1 & u2 in the carrier of W2 implies ( ( for v st v in the carrier of W1 holds v1 . v = v2 ) & ( ( v1 is 0. V ) + v2 ) & ( v2 is 0. V implies v1 is 0. V )
defpred P [ Element of L ] means M <= f . $1 & f . $1 <= f . $1 & f . $1 <= f . $1 ;
l . ( u , a , v ) = s * x + ( - ( s * x + y ) ) * y .= b ;
- ( - ( - x ) ) = - x + - ( - y ) .= - x + - y .= - x + y .= - x + y ;
given a being Point of GX such that for x being Point of GX holds a , x are_\HM { a } and a , b are_\HM { a } ;
fSet = [ [ dom ( @ f2 ) , cod ( @ f2 ) ] , cod ( @ f2 ) ] , [ cod ( @ f2 ) , cod ( f ) ] ] ;
for k , n being Nat st k <> 0 & k < n & k is prime holds k , n are_relative_prime & k , n are_relative_prime & k , n are_relative_prime
for x being element holds x in A |^ d iff x in ( ( A ` ) ` ) ` & ( ( A ` ) ` ) ` = ( A ` ) `
consider u , v being Element of R , a being Element of A such that l /. i = u * a and u in A ;
- ( ( p `1 / |. p .| - cn ) / ( 1 - cn ) ) ^2 > 0 ;
L-13 . k = LF . ( F . k ) & F . k in dom ( LF . k ) ;
set i2 = SubFrom ( a , i , - n ) , i1 = goto - ( n + 1 ) ;
attr B is } is \frac means : Def1 : for S being SubSub\mathop of B holds S = ( B , S ) `1 ;
a9 "/\" D = { a "/\" d where d is Element of N : d in D } & a "/\" b = a "/\" b ;
|( \square , \square - q )| * |( q , q )| + |( q , q )| * |( q , q )| >= |( q , q )| + |( q , q )| ;
( - f ) . ( upper_bound A ) = ( ( - f ) | A ) . ( upper_bound A ) .= f . ( upper_bound A ) ;
G * ( len G , k ) `1 = G * ( len G , k ) `1 .= G * ( len G , k ) `1 .= G * ( len G , k ) `1 ;
( Proj ( i , n ) . LM ) . LM = <* ( proj ( i , n ) . ( LM ) ) . ( LM ) *> ;
f1 + f2 * reproj ( i , x ) is_differentiable_in ( ( the - 1 ) (#) ( f1 + f2 ) ) . x ;
pred ( for x st x in Z holds ( tan . x ) <> 0 & ( tan . x ) <> 0 & ( tan . x ) <> 0 ) ;
ex t being SortSymbol of S st t = s & h1 . t = h2 . t & ( for x being set st x in dom h1 holds h1 . x = F ( x ) ) ;
defpred C [ Nat ] means P8 . $1 is non empty & P8 . $1 is non empty & A8 . $1 is non empty ;
consider y being element such that y in dom ( p9 . i ) and q9 . i = p9 . y and ( p9 . i ) . y = x ;
reconsider L = product ( { x1 } +* ( index B , l ) ) as Basis of A ;
for c being Element of C ex d being Element of D st T . ( id c ) = id d & for c being Element of C st c in dom T holds T . ( id c ) = id d
not ( f , n , p ) = ( f | n ) ^ <* p *> .= f ^ <* p *> .= f ^ <* p *> ;
( f * g ) . x = f . ( g . x ) & ( f * h ) . x = f . ( h . x ) ;
p in { ( 1 - 2 ) * ( G * ( i + 1 , j ) + G * ( i + 1 , j + 1 ) ) } ;
f `2 - p `2 = ( f | ( n , L ) ) *' - ( f . ( - p ) ) .= ( f . ( - p ) ) *' - ( f . ( - p ) ) ;
consider r be Real such that r in rng ( f | divset ( D , j ) ) and r < m + s ;
f1 . ( |[ r2 , r3 ]| , |[ r2 , r3 ]| ) in f1 .: ( W1 /\ W2 ) & f2 . ( r1 , r2 ) = f2 .: ( W1 /\ W2 ) ;
eval ( a | ( n , L ) , x ) = eval ( a | ( n , L ) , x ) .= a * eval ( b , x ) .= a * eval ( b , x ) ;
z = DigA ( tk , x9 ) .= DigA ( tk , ( k + 1 ) + 1 ) .= DigA ( tk , ( k + 1 ) + 1 ) .= DigA ( tk , ( k + 1 ) + 1 ) ;
set H = { Intersect S where S is Subset-Family of X : S c= G } , G = { Intersect G where G is Subset-Family of X : G c= F } , H = { Intersect G where G is Subset-Family of X : G c= F } , G = { Intersect G where G is Subset-Family of X : G c= F } ;
consider S19 being Element of D * , d being Element of D * such that S `1 = S19 ^ <* d *> and S `2 = d ;
assume that x1 in dom f and x2 in dom f and f . x1 = f . x2 and f . x2 = f . x2 ;
- 1 <= ( ( q `2 / |. q .| - sn ) / ( 1 - sn ) ) / ( 1 - sn ) ;
1. ( K , L ) is Linear_Combination of A & Sum ( 1. ( K , L ) ) = 0. K implies Sum ( L ) = Sum ( L )
let k1 , k2 , k2 , k2 , k2 , k1 , k2 , k2 , k2 , k2 , k2 , k2 , k2 , \in dom p & I = p +* ( k1 , k2 , k2 ) ;
consider j being element such that j in dom a and j in g " { k `2 } and x = a . j ;
H1 . x1 c= H1 . x2 or H1 . x2 c= H1 . x1 or H1 . x2 c= H1 . x2 or H1 . x1 c= H1 . x2 & H1 . x2 c= H1 . x2 ;
consider a being Real such that p = L~ ( f * p1 + ( a * p2 ) * p2 ) and 0 <= a and a <= 1 ;
assume that a <= c & c <= d & [' a , b '] c= dom f and [' a , b '] c= dom g ;
cell ( Gauge ( C , m ) , m -' 1 , 0 ) is non empty & cell ( Gauge ( C , m ) , m -' 1 , 0 ) is non empty ;
Ax in { ( S . i ) `1 where i is Element of NAT : i in dom S } ;
( T * b1 ) . y = L * b2 /. y .= ( F /. y ) * ( F /. y ) .= ( F /. y ) * ( F /. y ) ;
g . ( s , I ) . x = s . y & g . ( s , I ) . y = |. s . x - s . y .| ;
( log ( 2 , k + 1 ) ) ^2 >= ( log ( 2 , k + 1 ) ) ^2 ;
then that p => q in S and not x in the still of p and not p => All ( x , q ) in S ;
dom ( the InitS of r-10 ) misses dom ( the InitS of rM ) & dom ( the InitS of rM ) misses dom ( the InitS of rM ) ;
synonym f is ExtReal means : Def1 : for x being set st x in rng f holds x is ExtReal ;
assume for a being Element of D holds f . { a } = a & for X being Subset-Family of D holds f . ( f .: X ) = f . union X ;
i = len p1 .= len p3 + len <* x *> .= len p1 + len <* x *> .= len p1 + 1 .= len p1 + 1 ;
( l /. 1 , 3 ) `1 = ( g /. 3 , k ) `1 + ( k + 1 ) - ( g /. 3 , k + 1 ) `1 ;
CurInstr ( P2 , Comput ( P2 , s2 , l ) ) = halt SCM+FSA .= CurInstr ( P2 , Comput ( P2 , s2 , l ) ) .= halt SCM+FSA ;
assume for n be Nat holds ||. seq .|| . n <= ( ||. seq .|| . n ) & ( ||. seq .|| . n ) . n <= ( ||. seq .|| . n ) . n ;
sin . ( 0. ) = sin . ( r * PI ) .= cos . ( - cos . ( r * PI ) ) .= 0 ;
set q = |[ g1 `1 . t0 , g2 `2 . t0 ]| , g1 `2 = |[ g1 `1 . t0 , g2 `2 . t0 ]| , g2 = |[ g2 `1 . t0 , g2 `2 . t0 ]| ;
consider G being sequence of S such that for n being Element of NAT holds G . n in holds G in WL~ Assume ( F . n ) ;
consider G such that F = G and ex G1 st G1 in S3 & G = ( the carrier of G1 ) --> ( G1 , G2 ) ;
the root of [ x , s ] in ( the Sorts of Free ( C , X ) ) . s & the Sorts of C = ( the Sorts of Free ( C , X ) ) . s ;
Z c= dom ( exp_R * ( f + ( #Z 3 ) * f1 + ( #Z 3 ) * f2 ) ) ;
for k being Element of NAT holds seq1 . k = ( sum ( Im ( f , S ) ) . k ) * ( ( Im ( f , S ) . k ) ) * ( ( Im ( f , S ) . k ) * ( ( Im ( f , S ) . k ) ) ) ;
assume that - 1 < n and q `2 > 0 and ( q `2 / |. q .| - sn ) / ( 1 + sn ) < 0 and q `2 / |. q .| - sn ;
assume that f is continuous one-to-one and a < b and c < d and f . a = g and f . b = c and f . c = d ;
consider r being Element of NAT such that sd = Comput ( P1 , s1 , r ) and r <= q and q <= r ;
LE f /. ( i + 1 ) , f /. j , f /. ( len f + 1 ) , f /. ( len f + 1 ) ;
assume that x in the carrier of K and y in the carrier of K and inf { x , y } = inf { x , y } and x <= y ;
assume f +* ( i1 , \xi ) . 1 in ( proj ( F , i2 ) * ( i1 , j1 ) ) " { 0 } & f . ( i1 , j1 ) = ( proj ( F , i2 ) * ( i1 , j1 ) ) . 1 ;
rng ( ( ( ( Flow M ) ~ | ( the carrier of M ) ) * ( id the carrier' of M ) ) c= the carrier' of M ;
assume z in { ( the carrier of G ) \/ { t } where t is Element of T : t in A } ;
consider l be Nat such that for m be Nat st l <= m holds ||. s1 . m - x0 .|| < g / 2 ;
consider t be VECTOR of product G such that mt = ||. D5 . t .|| and ||. t .|| <= 1 ;
assume that the carrier of v = 2 and v ^ <* 0 *> in dom p and v ^ <* 1 *> in dom p and p . 1 = p . 2 and p . 2 = p . 3 ;
consider a being Element of the Points of X39 , A being Element of the Points of X39 such that 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 holds p . i is FinSequence of D
defpred R [ element ] means ex x , y st [ x , y ] = $1 & P [ x , y ] & P [ x , y ] ;
L~ f2 = union { LSeg ( p0 , p1 ) , LSeg ( p1 , p2 ) } \/ LSeg ( p1 , p2 ) \/ LSeg ( p1 , p2 ) ;
i - len h11 + 2 - 1 < i - len h11 + 2 - 1 + 1 - 1 + 1 & i - len h11 + 2 - 1 < i - len h11 + 2 - 1 ;
for n being Element of NAT st n in dom F holds F . n = |. ( nX . ( n -' 1 ) ) .| * |. F . n .| ;
for r , s1 , s2 , r , s st r in [. s1 , s2 .] & s1 <= s2 & r <= s2 holds r <= s & s <= r
assume v in { G where G is Subset of T2 : G in B2 & G c= z1 } & v in { z1 } ;
let g be } is \vert S -valued Function of A , INT & ( g | X ) | ( b , b ) <> 0 ;
min ( g . [ x , y ] , k ) = ( min ( g , k , x ) ) . y .= min ( g , k , x ) ;
consider q1 being sequence of CK such that for n holds P [ n , q1 . n ] and P [ n , q1 . n ] ;
consider f being Function such that dom f = NAT & for n being Element of NAT holds f . n = F ( n ) and for n being Element of NAT holds f . n = F ( n ) ;
reconsider B-6 = B /\ O , Od = O /\ Z , Od = { Z , W , Z } as Subset of B ;
consider j being Element of NAT such that x = ( the ` of n ) * j and 1 <= j and j <= n and n <= len f ;
consider x such that z = x and card ( x . O2 ) in card ( x . O2 ) and x in L1 and x in L2 ;
( C * : T . ( k , n2 ) ) . 0 = C . ( ( <> <> ( T . ( k + 1 ) ) . 0 ) ) & ( C * T . ( k + 1 ) ) . 0 = C . ( ( T . ( k + 1 ) ) . 0 ) ;
dom ( X --> rng f ) = X & dom ( X --> f ) = dom ( X --> f ) & rng ( X --> f ) = dom f ;
( N-bound L~ SpStSeq C ) `2 <= ( ( /. i ) `2 & ( S-bound L~ Cage ( C , i + 1 ) ) `2 <= N-bound L~ Cage ( C , i + 1 ) `2 ;
synonym x , y are_collinear means : Def1 : x = y or ex l being \HM of S st { x , y } c= l & l is \overline of A ;
consider X be 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 , a , b being Element of Im k st a = x & b = y & x << y holds a << b ;
( 1 / 2 * ( ( ( - 1 / 2 ) * ( ( #Z 2 ) * ( ( #Z 2 ) * ( 1 / 2 ) * ( 1 / 2 ) ) ) ) ) `| REAL ) = ( ( - 1 / 2 ) * ( ( #Z 2 ) * ( 1 / 2 ) ) ) / 2 ;
defpred P [ Element of omega ] means ( for n holds ( ( the Sorts of A1 ) . n = A1 . n ) implies ( ( the Sorts of A2 ) . n = A2 . ( n + 1 ) ) ;
IC Comput ( P , s , 2 ) = succ IC Comput ( P , s , 1 ) .= 6 + 1 .= 6 + 1 ;
f . x = f . g1 * f . g2 .= f . g1 * ( g . g2 ) .= f . g1 * ( g . g2 ) .= f . g2 * ( g . g2 ) .= f . g2 * ( g . g2 ) ;
( M * F-4 ) . n = M . ( F-4 . n ) .= M . ( { ( canFS ( Omega ( Omega ) ) . n } ) ) .= M . ( { ( canFS ( Omega ) ) . n } ) ;
the carrier of L1 + L2 c= ( the carrier of L1 ) \/ ( the carrier of L2 ) & the carrier of L1 /\ ( the carrier of L1 ) c= the carrier of L2 ;
pred a , b , c , x , y , z , x , y , z , y , z , x , y , z , x , y , z , y , z , x , y , z , x , y , z , x , y , z , x , y , z , x , y , z , z , x , y , z , z , x , y , z , x , y , z , x , y , z , x , y , z , y , z , z , x
( the PartFunc of s ) . n <= ( the Sorts of s ) . n * ( the Sorts of A ) . ( n + 1 ) & ( the Sorts of A ) . n <= ( the Sorts of A ) . n ;
pred - 1 <= r & r <= 1 & ( - 1 ) * ( ( - 1 ) / r ) = - ( 1 / r ) * ( r / r ) ;
seq in { p ^ <* n *> where n is Nat : p ^ <* n *> in T1 } or for n being Nat st n in T1 holds p . n in T1 & p . n in T2 } ;
|[ x1 , x2 , x3 ]| . 2 - |[ y1 , y2 ]| . 2 - |[ y2 , y2 ]| . 3 - |[ y1 , y2 ]| . 2 - |[ y1 , y2 ]| . 3 - |[ y1 , y2 ]| . 2 - |[ y1 , y2 ]| . 3 - |[ y1 , y2 ]| . 2 - |[ y1 , y2 ]| . 3 - |[ y1 , y2 ]| . 3 ]| ;
attr for m being Nat holds F . m is nonnegative & ( Partial_Sums F ) . m is nonnegative & ( Partial_Sums F ) . m is nonnegative ) implies ( Partial_Sums F ) . m is nonnegative & ( Partial_Sums F ) . n is nonnegative ;
len ( w . z ) = len ( ( G . ( xx + 1 ) ) + ( G . ( xx + 1 ) ) ) .= len ( G . ( xx + 1 ) ) ;
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 W3 ;
given F be FinSequence of NAT such that F = x and dom F = n and rng F c= { 0 , 1 } and Sum F = k and Sum F = k ;
0 = 1 * 0 * 0 -uon iff 1 = ( 1 - ( 1 - ( - 1 ) * ( - 1 ) * ( - 1 ) ) * ( - 1 - ( - ( - ( 1 - ( - 1 ) * ( - 1 ) * ( - 1 ) ) * ( - 1 ) ) ) ;
consider n be Nat such that for m be Nat st n <= m holds |. ( f # x ) . m - ( f # x ) . n .| < e / 2 ;
cluster } is being } -\mathbin { \rm \hbox { - } \frac 1 , ( w + 1 ) -\mathbin { - } 1 , ( w + 1 ) -\mathbin { - 1 } , ( w + 1 ) -{ - 1 } , ( w + 1 ) -{ - 1 } , L ) is Boolean
"/\" ( BB , {} ) = Top B .= the carrier of S .= "/\" ( [#] S , {} ) .= "/\" ( I , {} ) .= "/\" ( I , {} ) ;
( r / 2 ) ^2 + ( r / 2 ) ^2 <= ( r / 2 ) ^2 + ( r / 2 ) ^2 ;
for x being element st x in A /\ dom ( f `| X ) holds ( f `| X ) . x >= r2 & ( f `| X ) . x >= r2
2 * r1 - ( 2 * r1 - ( 2 * r1 - ( 2 * r2 - ( 2 * r2 - ( 2 * r2 - ( 2 * r2 - ( 2 * r2 - ( 2 * r2 - ( 2 * r2 - ( 2 * r2 - ( 2 * r2 - ( 2 * r2 - ( 2 * r2 - ( 2 * r2 - ( 2 * r2 - ( 2 * r2 - 1 ) ) ) ) / 2 ) ) / 2 ) ) ) / 2 ) )
reconsider p = P * ( \square , 1 ) , q = a " * ( ( - ( K , n , 1 ) ) * ( Q , 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 y = [ x1 , x2 ] ;
for n be Nat st 1 <= n & n <= len q1 holds q1 . n = ( upper_volume ( g , M7 ) ) . n & ( upper_volume ( g , M7 ) ) . n = ( upper_volume ( g , M7 ) ) . n
consider y , z being element such that y in the carrier of A and z in the carrier of A and i = [ y , z ] and i = [ y , z ] ;
given H1 , H2 being strict Subgroup of G such that x = H1 & y = H2 and H1 , H2 are_Subgroup of H2 and H2 is Subgroup of H1 and H2 is Subgroup of H2 ;
for S , T being non empty < T , d being Function of T , S st T is complete holds d is directed-sups-preserving & d is monotone
[ a + 0 , i + b2 ] in ( the carrier of F_Complex ) /\ ( the carrier of F_Complex ) & [ a + b , i + b2 ] in [: the carrier of F_Complex , the carrier of F_Complex :] ;
reconsider m9 = max ( len F1 , len ( p . n ) * ( <* x *> |^ n ) ) as Element of NAT ;
I <= width GoB ( ( GoB h ) * ( 1 , width GoB h ) `1 , ( GoB h ) * ( 1 , width GoB h ) `2 ) & I <= width GoB ( ( GoB h ) * ( 1 , width GoB h ) `2 , ( GoB h ) * ( 1 , width GoB h ) `2 ) `2 ;
f2 /* q = ( f2 /* ( f1 /* s ) ) ^\ k .= ( ( f2 * f1 ) /* s ) ^\ k .= ( ( ( f2 * f1 ) /* s ) ^\ k .= ( ( ( f2 * f1 ) ^\ k ) / ( f2 * f2 ) ) ^\ k ;
pred A1 \/ A2 is linearly-independent means : Def1 : A1 misses A2 & A2 misses A1 & Lin ( A1 \/ A2 ) = Lin ( A1 \/ A2 ) & Lin ( A2 \/ A1 ) = Lin ( A2 \/ Lin ( A1 \/ A2 ) ) ;
func A -carrier of C -> set means : Def1 : it in union { A . s where s is Element of R : s in C } & for x being Element of R st x in A holds it . x = F ( x ) ;
dom ( Line ( v , i + 1 ) ^ ( Line ( p , m ) ) * ( \square , 1 ) ) = dom ( F ^ G ) .= dom ( F ^ G ) ;
cluster [ x `1 , 4 ] -> [ x `1 , 4 ] , [ x `2 , 4 ] ] -> [ x `1 , 4 ] , [ x `1 , 4 ] ] -> [ x `1 , 4 ] , [ x `1 , 4 ] ] -> [ x `1 , 4 ] , [ x , 4 ] ] -> [ x `1 , 4 ] , [ x , 4 ] ] ;
E , All ( x2 , ( x2 => ( x1 => x2 ) ) => ( x1 '&' x2 ) => ( x2 '&' x3 ) ) |= All ( x2 , ( x1 '&' x2 ) => ( x2 '&' x3 ) ) ;
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 . m ) - ( h . m ) .= ( F . m ) - ( F . m ) - ( F . m ) ;
cell ( G , ( X -' 1 , Y -' 1 ) \ ( X -' 1 ) \ ( X -' 1 ) ) meets ( ( L~ f ) \ ( X -' 1 ) ) ;
IC Comput ( P2 , s2 , i ) = IC Comput ( P2 , s2 , i ) .= IC Comput ( P2 , s2 , i ) .= IC Comput ( P2 , s2 , i ) .= ( card I + 1 ) + 1 .= ( card I + 1 ) + 1 ;
sqrt ( ( - ( ( q `1 / |. q .| - cn ) / ( 1 + cn ) ) ^2 ) > 0 ;
consider x0 being element such that x0 in dom a and x0 in g " { k `2 } and y = a . x0 and x0 in { k } and x0 in { k } ;
dom ( r1 (#) chi ( A , A ) ) = dom chi ( A , A ) /\ dom chi ( A , A ) .= dom ( r1 (#) chi ( A , A ) ) /\ dom ( r2 (#) chi ( A , A ) ) .= dom ( r1 (#) chi ( A , A ) ) /\ dom ( r2 (#) chi ( A , A ) ) .= dom ( r1 (#) chi ( A , A ) ) ;
d-7 . [ y , z ] = ( ( y `1 ) * ( y `2 ) - ( y `2 ) * ( y `2 ) ) * ( y `2 ) ;
pred for i being Nat holds C . i = A . i /\ B . i & L~ C c= A /\ ( B /\ C ) ;
assume that x0 in dom f and f is_continuous_in x0 and f is_continuous_in x0 and f is_continuous_in x0 and f /. x0 = ( f /. x0 ) * ( f /. x0 ) * ( f /. x0 ) * ( f /. x0 ) + ( f /. x0 ) * ( f /. x0 ) * ( f /. x0 ) * ( f /. x0 ) * ( f /. x0 ) * ( f /. x0 ) * ( f /. x0 ) * ( f /. x0 ) * ( f /. x0 ) + ( f /. x0 ) * ( f /. x0 ) * ( f /. x0 ) * ( f /.
p in Cl A implies for K being Basis of p , Q being Subset of T st Q in K & K meets Q holds A meets Q
for x being Element of REAL n st x in Line ( x1 , x2 ) holds |. y1 - y2 .| <= |. y1 - y2 .| + |. y2 - x2 .|
func /. ( <*> the carrier of a ) -> Ordinal means : Def1 : a in it & for b being Ordinal st b in it holds it . b c= b ;
[ a1 , a2 , a3 ] in ( the carrier of A ) /\ ( the carrier of B ) & [ a1 , a2 , a3 ] in [: the carrier of A , the carrier of B :] /\ [: the carrier of B , the carrier of B :] ;
ex a , b being element st a in the carrier of S1 & b in the carrier of S2 & x = [ a , b ] & [ a , b ] in the InternalRel of S2 ;
||. ( ( vseq . n ) - vseq . m ) * ||. x - y .|| < ( e / ( ||. x .|| + ||. y .|| ) * ||. x - y .|| ) * ||. x - y .|| ;
then for Z being set st Z in { Y where Y is Element of I7 : F c= Y & Y in Z } holds z in x & z in Z ;
sup compactbelow [ s , t ] = [ sup { 1 } , sup ( compactbelow [ s , t ] ) ] .= [ sup { 1 } , sup { 1 } ] .= [ sup { 1 } , sup { 1 } ] ;
consider i , j being Element of NAT such that i < j and [ y , f . j ] in II and [ f . i , f . j ] in II and [ i , j ] in II ;
for D being non empty set , p , q being FinSequence of D st p c= q holds ex p being FinSequence of D st p ^ q = q & p ^ q = q ^ p
consider e19 being Element of the affine of X such that c9 , a9 // a9 , e and not LIN a9 , b9 , c9 and not LIN c9 , a9 , e and LIN c9 , a9 , e and LIN c9 , a9 , e ;
set U2 = I \! \mathop { \vert I .| where I is Element of U : not contradiction } ;
|. q2 .| ^2 = ( ( |. q2 .| ) ^2 + ( ( |. q2 .| ) ^2 + ( |. q2 .| ) ^2 ) * ( |. q2 .| ) ^2 .= |. q .| ^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 implies x "/\" y = x /\ y
dom signature U1 = dom ( the charact of U1 ) & Args ( o , MSAlg U1 ) = dom ( the charact of U1 ) & Args ( o , MSAlg U1 ) = dom ( the charact of U1 ) & dom ( the charact of U2 ) = dom ( the charact of U2 ) ;
dom ( h | X ) = dom h /\ X .= dom ( ||. h .|| | X ) /\ X .= dom ( ||. h .|| | X ) /\ X .= dom ( ||. h .|| | X ) /\ X .= dom ( ||. h .|| | X ) .= X /\ X .= X /\ X .= X /\ X .= dom ( ( ||. h .|| | X ) | X ) ;
for N1 , N2 being Element of G8 , h being Element of ( the carrier of G ) * , N1 , N2 being Element of ( the carrier of G ) * st dom h = N & rng h c= N1 & h . N1 = N2 holds h . N2 = h . N1
( mod ( u , m ) + mod ( v , m ) ) . i = ( mod ( u , m ) + mod ( v , m ) ) . i .= ( mod ( v , m ) + mod ( v , m ) ) . i ;
- ( q `1 / |. q .| - cn ) < - ( q `2 / |. q .| - cn ) & - ( q `2 / |. q .| - cn ) <= - ( q `2 / |. q .| - cn ) ;
pred r1 = f9 & r2 = g9 & r1 * r2 = f9 * ( f * ( f * ( f * g ) ) ) & for i st i in dom f holds r1 * ( f * g ) = f9 * ( f * ( f * g ) ) ;
( vseq . m is bounded Function of X , the carrier of Y & xx . m = ( vseq . m ) . x & ( vseq . m ) . x = ( vseq . m ) . x ;
pred a <> b & b <> c & angle ( a , b , c ) = PI & angle ( b , c , a ) = 0 & angle ( b , c , a ) = PI ;
consider i , j , r being Nat such that p1 = [ i , r ] and p2 = [ j , r ] and i < j and r < j and j < i ;
|. p .| ^2 - ( 2 * |( p , q )| ) ^2 + |. q .| ^2 = |. p .| ^2 + |. q .| ^2 - ( 2 * |( p , q )| ) ^2 ;
consider p1 , q1 being Element of X such that y = p1 ^ q1 and q1 ^ q1 = p1 ^ q1 and p1 ^ q1 = p2 ^ q2 and p1 ^ q1 = p2 ^ q2 and q1 ^ q2 = p2 ^ q2 ;
1. ( K , r1 , r2 , s1 , s2 , s2 , Amp ) = ( s2 * gcd ( A , B , s1 , s2 ) ) * ( r2 * gcd ( B , B , s2 , Amp ) ) ;
( UMP A ) `2 = lower_bound ( proj2 .: ( A /\ Vertical_Line w ) ) & proj2 .: ( A /\ Vertical_Line w ) is non empty & proj2 .: ( A /\ Vertical_Line w ) is non empty ;
s |= ( ( k , k1 ) \cap ( H2 , k2 ) ) iff s |= ( ( H , k2 ) \cap ( H , k2 ) ) & s |= ( ( H , k2 ) /\ ( H , k2 ) ) ;
len ( s + 1 ) = card ( support b1 ) + 1 .= card ( support b2 ) + 1 .= len ( s + 1 ) + 1 .= len ( s + 1 ) + 1 .= len ( s + 1 ) + 1 ;
consider z being Element of L1 such that z >= x and z >= y and for z being Element of L1 st z >= x & z >= y holds z `1 >= y & z `2 >= x ;
LSeg ( UMP D , |[ W-bound D , E-bound D ]| ) /\ LSeg ( |[ W-bound D , E-bound D ]| , ( E-bound D ) / 2 ) = { UMP D } /\ LSeg ( UMP D , ( E-bound D ) / 2 ) ;
lim ( ( ( f `| N ) / g ) /* b ) = lim ( ( f `| N ) / g ) / ( g `| N ) .= lim ( ( f `| N ) / g ) / ( g `| N ) ;
P [ i , pr1 ( f ) . i , pr1 ( f ) . ( i + 1 ) , pr1 ( f ) . ( i + 1 ) ] ;
for r be Real st 0 < r ex m be Nat st for k be Nat st m <= k holds ||. ( seq . k - R /. ( k + 1 ) ) - ( seq . k - R /. ( k + 1 ) ) .|| < r
for X being set , P being a_partition of X , x , a , b being set st x in a & a in P & b in P & x in P & a = b holds a = b
Z c= dom ( ( - 1 / 2 ) (#) ( ( #Z 2 ) * f ) \ ( ( #Z 2 ) * f ) " { 0 } ) & Z c= dom ( ( #Z 2 ) * f ) \ ( ( #Z 2 ) * f ) " { 0 } " { 0 } ;
ex j being Nat st j in dom ( l ^ <* x *> ) & j < i & i = ( l ^ <* x *> ) . j & i = 1 + len l & j = i + len l & j = i + len <* x *> & j = i + 1 ;
for u , v being VECTOR of V , r being Real st 0 < r & u in N & v in N holds r * u + ( 1-r * v ) in N
A , Int A , Cl Int A , Int Cl A , Int Cl Int A , Int Cl Int Cl Int A , Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl A , Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl Int Cl A , Int Cl Int Cl A , Int Cl Int Cl A , Int Cl Int Cl A , Int Cl A , Int Cl Int Cl
- Sum <* v , u , w *> = - ( v + u + w ) * v .= - ( v + u ) * u + u * w .= - ( v + u ) * w ;
Exec ( a := b , s ) . IC SCM R = ( Exec ( a := b , s ) ) . IC SCM .= Exec ( ( a := b ) , s ) . IC SCM R .= succ IC s .= IC s .= IC s .= IC s .= IC s .= IC s .= IC s .= 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 reflexive RelStr , D being non empty directed Subset of [: S1 , S2 :] , S being Subset of [: S2 , S2 :] , T being non empty directed Subset of [: S1 , S2 :] , T holds cos ( D ) is directed
card X = 2 implies ex x , y st x in X & y in X & x <> y or z = x & y = y or z = x & z = y or z = y & x = z or z = y & z = x or z = y & z = x or z = y & z = x & z = y ;
E-max L~ Cage ( C , n ) in rng ( Cage ( C , n ) \circlearrowleft Cage ( C , n ) ) & W-min L~ Cage ( C , n ) in rng ( Cage ( C , n ) \circlearrowleft Cage ( C , n ) ) ;
for T , T being DecoratedTree , p , q being Element of dom T st p element T & q in dom T holds ( T -\hbox { p } ) . q = T . q & ( T -\hbox { p } ) . q = T . q
[ i2 + 1 , j2 ] in Indices G & [ i2 , j2 ] in Indices G & f /. k = G * ( i2 + 1 , j2 ) & f /. k = G * ( i2 + 1 , j2 ) ;
cluster that not ( k divides ( k , n ) and k divides m & k divides n & k divides n & k divides n & k divides m implies k divides n ) & k divides m ;
dom F " = the carrier of X2 & rng F = the carrier of X1 & F " = the carrier of X2 & F " = the carrier of X2 & F " = the carrier of X1 & F " = the carrier of X2 ;
consider C being finite Subset of V such that C c= A and card C = n and the VectSpStr of V = Lin ( BM \/ C ) and C is linearly-independent of Lin ( BM \/ C ) ;
V is prime implies for X , Y being Element of [: the topology of T , the topology of T :] st X /\ Y c= V & X c= V holds X c= Y or Y c= V
set X = { F ( v1 ) where v1 is Element of B ( ) : P [ v1 ] } , Y = { F ( v1 ) where v1 is Element of B ( ) : P [ v1 ] } ;
angle ( p1 , p3 , p4 ) = 0 .= angle ( p2 , p3 , p2 ) .= angle ( p2 , p3 , p3 ) .= angle ( p2 , p3 , p2 ) .= angle ( p2 , p3 , p2 ) ;
- sqrt ( ( - ( q `1 / |. q .| - cn ) / ( 1 - cn ) ) ^2 ) = - ( - ( q `1 / |. q .| - cn ) / ( 1 - cn ) ) ^2 .= - ( - ( q `1 / |. q .| - cn ) / ( 1 - cn ) ) / ( 1 - cn ) ;
ex f being Function of I[01] , ( TOP-REAL 2 ) | P st f is continuous one-to-one & rng f = P & f . 0 = p1 & f . 1 = p2 & f . 0 = p2 & f . 1 = p3 & f . 1 = p2 & f . 0 = p4 ;
pred f is_is_is_is_differentiable on u0 means : Def1 : SVF1 ( 2 , pdiff1 ( f , 1 ) , u0 ) . ( u0 + 1 ) - SVF1 ( 2 , pdiff1 ( f , 3 ) , u0 ) . ( u0 + 1 ) = ( proj ( 2 , 3 ) . u0 ) . ( u0 + 1 ) ;
ex r , s st x = |[ r , s ]| & G * ( len G , 1 ) `1 < r & r < G * ( 1 , 1 ) `1 & G * ( len G , 1 ) `2 < s & s < G * ( 1 , 1 ) `2 ;
assume that f is_sequence_on G and 1 <= t & t <= len G and G * ( t , width G ) `2 >= N-bound L~ f and G * ( t , width G ) `2 >= S-bound L~ f and f /. len f = f /. len f and f /. len f = f /. len f ;
pred i in dom G means : Def1 : r (#) ( f * reproj ( i , x ) ) = r (#) f * reproj ( i , x ) ;
consider c1 , c2 being bag of o1 + o2 such that ( decomp c ) /. k = <* c1 , c2 *> and c = ( O /. k ) + ( O /. k ) and c1 <> c2 and c2 <> c1 and c1 <> c2 and c2 <> c2 ;
u0 in { |[ r1 , s1 ]| : r1 < G * ( 1 , 1 ) `1 & G * ( 1 , 1 ) `2 < s1 } & |[ G * ( 1 , width G ) `2 , width G * ( 1 , width G ) `2 ]| `2 < s1 } ;
Cl ( X ^ Y ) . k = the carrier of X . k2 .= C4 . k .= C4 . k .= ( C ^ C4 ) . k .= ( C ^ C4 ) . k .= ( C ^ C4 ) . k ;
pred len M1 = len M2 & width M1 = width M2 & width M1 = width M2 & width M1 = width M2 & width M1 = width M2 & width M1 = width M2 & width M1 = width M2 & width M1 = width M2 & width M1 = width M2 & width M1 = width M2 & width M1 = width M2 ;
consider g2 be Real such that 0 < g2 and { y where y is Point of S : ||. y - x0 .|| < g2 & y in dom f } c= N2 & f . ( y - x0 ) < f . ( y - x0 ) ;
assume x < ( - b + sqrt ( delta ( a , b , c ) ) / ( 2 * a ) or x > - b - sqrt ( delta ( a , b , c ) ) / ( 2 * a ) ;
( G1 '&' G2 ) . i = ( <* 3 *> ^ G1 ) . i & ( H1 '&' H2 ) . i = ( <* 3 *> ^ G1 ) . i & ( H1 '&' H2 ) . i = ( <* 3 *> ^ G1 ) . i ;
for i , j st [ i , j ] in Indices ( M3 + M1 ) holds ( M3 + M1 ) * ( i , j ) < M2 * ( i , j ) + M2 * ( i , j )
for f being FinSequence of NAT , i being Element of NAT st i in dom f & i divides j holds i divides f /. j & i divides f /. ( j + 1 ) & i divides f /. ( j + 1 )
assume F = { [ a , b ] where a , b is Subset of X : for c being set st c in B\bf 1 & a c= c holds b c= c } & a c= c ;
b2 * q2 + ( b3 * q3 ) + - ( ( a * q2 ) * q3 + ( - ( a * q2 ) * q3 ) ) * ( ( a * q2 ) * q2 + ( - ( a * q2 ) * q3 ) * q3 ) = 0. TOP-REAL n ;
Cl ( Cl F ) = { D where D is Subset of T : ex B being Subset of T st D = Cl B & B in F & D in F } & F is closed & B is closed & F is closed & Cl B is closed } ;
attr seq is summable means : Def1 : seq is summable & seq is summable & Sum ( seq ) = Sum ( seq ) & Sum ( seq ) = Sum ( seq ) & Sum ( seq ) = Sum ( seq ) & Sum ( seq ) = Sum ( seq ) ;
dom ( ( ( ( ( ( TOP-REAL 2 ) | D ) | D ) | D ) ) = ( the carrier of ( ( TOP-REAL 2 ) | D ) /\ D ) /\ D .= the carrier of ( ( TOP-REAL 2 ) | D ) | D ) .= D ;
[: X , Z :] is full non empty full SubRelStr of ( Omega Z ) |^ the carrier of Z & [ X , Y ] is full SubRelStr of ( Omega Z ) |^ the carrier of Z ;
G * ( 1 , j ) `2 = G * ( i , j ) `2 & G * ( 1 , j ) `2 <= G * ( i , j ) `2 & G * ( i , j ) `2 <= G * ( i , j + 1 ) `2 ;
synonym m1 c= m2 means : Def1 : for p being set st p in P holds the non empty \HM { m1 + 1 where m1 is Nat : m1 in dom ( m2 . p ) } & ( m1 + 1 ) in the carrier' ] & m2 in the carrier' of ( m2 . p ) ;
consider a being Element of B ( ) such that x = F ( a ) and a in { G ( b ) where b is Element of A ( ) : P [ b ] } and P [ a ] ;
attr IT is $1 -loop loop Str means : Def1 : the carrier of IT , the carrier of IT #) = [ the carrier of IT , the carrier of IT ] & the multF of IT , the carrier of IT ] in the carrier of the carrier of IT ;
sequence ( a , b , 1 ) + sequence ( c , d ) = b + sequence ( c , d ) .= b + ( a + c ) .= b + ( a + c ) .= b + ( a + c ) ;
cluster + ( - ( - ( i , j ) ) ) -> natural for Element of INT , i , j be Element of INT , j be Element of INT ;
- ( s2 * p1 + ( s2 * p2 - ( s2 * p2 - ( s2 * p1 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2 * p2 - ( s2
eval ( ( a | ( n , L ) ) *' p , x ) = eval ( a | ( n , L ) , x ) * eval ( p , x ) .= a * eval ( p , x ) * eval ( q , x ) .= a * eval ( p , x ) * eval ( q , x ) ;
assume that the TopStruct of S = the TopStruct of T and for D being non empty directed Subset of Omega S , V being open Subset of Omega S st V in V & V is open & V is open holds V meets V ;
assume that 1 <= k & k <= len w + 1 and T-7 . ( ( q11 , w ) -) . k = ( T-7 . ( q11 , w ) ) . k and T21 . k = ( T21 . ( q11 , w ) ) . k ;
2 * a |^ ( n + 1 ) + ( 2 * b |^ ( n + 1 ) ) >= a |^ ( n + 1 ) + ( 2 * a |^ ( n + 1 ) ) + ( 2 * b |^ ( n + 1 ) ) ;
M , v2 |= All ( x. 3 , All ( x. 0 , All ( x. 4 , All ( x. 0 , All ( x. 4 , x. 0 , x. 4 4 4 4 4 4 4 4 4 4 4 5 5 5 5 5 5 , x. 0 ) ) ) ) ;
assume that f is_differentiable_on l and for x0 st x0 in l holds 0 < f . x0 and for x0 st x0 in l holds f . x0 - f . x0 < f . x0 & f . x0 < 0 ;
for G1 being _Graph , W being Walk of G1 , e being set , G2 being Walk of G2 , e being Vertex of G2 st e in W & G2 is_Walk_from e , e holds not e Joins ( G2 | e ) , ( G2 | e ) , ( G2 | e ) , ( G2 | e ) , ( G2 | e ) , ( G2 | e ) , ( G2 | e ) , ( G2 | e )
not c9 is not empty iff not ( ( not ( ( ( not ( ( ( not ( ex y is not empty & not ( y is not empty & not ( y is not empty & not ( y is not empty & not ( y is not true ) & not ( y is not true ) & not ( y is not empty ) & not ( y is not empty ) & not ( y is not empty ) ) ) ) & not ( y is not empty ) ) ) & not ( not ( y is not empty ) & not ( y is not empty ) & not ( not ( not y is not empty ) & not ( not ( y is not empty ) & not ( y is not empty ) & not ( not y is not empty ) & not ( not ( y is
Indices GoB f = [: dom GoB f , Seg width GoB f :] & i + 1 in dom GoB f & j + 1 in dom GoB f & i + 1 in dom GoB f & j + 1 in dom GoB f & f /. i = ( GoB f ) * ( i + 1 , j + 1 ) ;
for G1 , G2 , G2 , G3 being strict Subgroup of O , O being stable Subgroup of O st G1 is_stable of G2 & G2 is_stable & G1 is_stable of G2 holds G1 * ( G1 , G2 ) is stable Subgroup of G2 & G2 is stable Subgroup of G2
UsedIntLoc ( int -in4 ) = { intloc 0 , intloc 1 , intloc 2 , intloc 3 , intloc 4 , intloc 4 , intloc 5 , 6 , 7 , 8 , 8 , 8 , 8 , 8 , 8 , 9 , 7 , 8 , 8 , 8 , 9 } \/ UsedIntLoc I \/ UsedIntLoc J \/ UsedIntLoc I \/ UsedIntLoc J \/ UsedIntLoc J \/ UsedIntLoc J \/ UsedIntLoc 6 ;
for f1 , f2 being FinSequence of F st f1 ^ f2 is p -element & Q [ p ^ <* p *> ] & Q [ p ^ <* p *> ] holds Q [ f1 ^ f2 ^ <* p *> ] & Q [ p ^ f2 ] & Q [ f1 ^ f2 ] & Q [ p ^ f2 ]
( p `1 / sqrt ( 1 + ( p `2 / p `1 ) ^2 ) ) * ( ( p `1 / sqrt ( 1 + ( p `2 / p `1 ) ^2 ) ) = ( q `1 / sqrt ( 1 + ( q `2 / q `1 ) ^2 ) ) * ( ( q `2 / sqrt ( 1 + ( q `2 / q `1 ) ^2 ) ) ;
for x1 , x2 , x3 , x4 being Element of REAL n holds |( x1 - x2 , x3 - x4 )| = |( x1 , x2 - x3 )| + |( x2 , x3 )| + |( x2 , x3 )| + |( x2 , x3 )| + |( x2 , x3 )| + |( x2 , x3 )| + |( x2 , x3 )| + |( x2 , x3 )| + |( x2 , x3 )| + |( x2 , x3 )| + |( x2 , x3 )| + |( x2 , x3 )| + |. x3 , x3 )| + |. x3 , x3 )| + |. x3 , x3 )| + |. x3 - x3 )| + x2 , x3 )| + |. x3 , x3 )| + x2 )| + x2 , x3 )| + x2 )| + |. x3 - x3 )| + |. x3 - x3 )| +
for x st x in dom ( ( ( ( ( ( ( ( x - x ) | A ) | A ) ^ <* x *> ) ^ ( ( x - x ) | A ) | A ) ) ) holds ( ( ( ( ( x - x ) | A ) ^ ( x - x ) ) | A ) ^ ( x - x ) ) | A = - ( ( x - x ) | A ) . x
for T being non empty TopSpace , P being Subset-Family of T , B being Basis of T st P c= the topology of T for x being Point of T st P c= B ex B being Basis of x st B c= P & B is Basis of x
( a 'or' b 'imp' c ) . x = 'not' ( ( a 'or' b ) . x 'or' c . x ) 'or' c . x .= 'not' ( ( a . x 'or' b . x ) 'or' c . x ) 'or' c . x .= TRUE ;
for e being set st e in A8 ex X1 being Subset of [: X , Y :] , Y1 being Subset of [: Y , Y :] st e = [: X1 , Y1 :] & Y1 is open & Y1 is open & Y1 is open & Y1 is open & Y1 is open & Y1 is open & Y1 is open
for i be set st i in the carrier of S for f be Function of [: S , S :] , S1 . i st f = H . i & F . i = f | [: S , S . i :] holds F = G
for v , w st for y st x <> y holds w . y = v . y holds Valid ( VERUM ( Al , J ) , J ) . ( v . y ) = Valid ( VERUM ( Al , J ) , J ) . ( v . y )
card D = card D1 + card D1 - card { i , j } - card D1 + 1 - 1 .= c1 + 1 - 1 + 1 - 1 .= c1 + 1 - 1 + 1 - 1 .= c1 + 1 - 1 + 1 - 1 .= 2 + 1 - 1 ;
IC Exec ( i , s ) = ( s +* ( 0 .--> succ ( s . 0 ) ) ) . 0 .= ( 0 .--> ( s . 0 ) ) . 0 .= Exec ( i , s ) . 0 .= succ IC s .= succ IC s .= IC s .= IC s .= IC s .= IC s .= IC Exec ( i , s ) ;
len f -' ( i1 -' 1 ) + 1 - 1 = len f -' ( i1 -' 1 ) + 1 - 1 .= len f -' ( i1 -' 1 ) + 1 - 1 .= len f -' ( i1 -' 1 ) + 1 - 1 .= len f -' ( i1 -' 1 ) + 1 - 1 ;
for a , b , c being Element of NAT st 1 <= a & 2 <= b & k <= a or k = a & k <= b + b-2 or k = a + b-2 or k = b + b-2 or k = a + b or k = a + b + a ;
for f being FinSequence of TOP-REAL 2 , p being Point of TOP-REAL 2 , i being Nat st i in LSeg ( f , i ) & p in LSeg ( f , i ) holds Index ( p , f ) <= Index ( p , f )
lim ( curry ' ( ( P , k + 1 ) # x ) = lim ( ( curry ' ( ( P , k ) # x ) ) + ( ( curry ' ( ( P , k ) # x ) ) # x ) ) ) ;
z2 = g /. ( ( i -' n1 + 1 ) + 1 ) .= g . ( i -' n1 + 1 + 1 ) .= g . ( i -' n1 + 1 + 1 ) .= g /. ( i -' n1 + 1 + 1 ) .= g /. ( i -' n1 + 1 + 1 ) .= g /. ( i -' n1 + 1 + 1 ) ;
[ f . 0 , f . 3 ] in id ( the carrier of G ) \/ ( the InternalRel of G ) or [ f . 0 , f . 3 ] in the InternalRel of G & [ f . 0 , f . 2 ] in the InternalRel of G & [ f . 2 , f . 3 ] in the InternalRel of G ;
for G being Subset-Family of B st G = { R [ X ] where R is Subset of A , B is Subset of B : R in F } & ( for X being Subset of A holds X in G iff X in F ) holds ( for X being Subset of A holds X in G iff X in F ) & X is finite )
CurInstr ( P1 , Comput ( P1 , s1 , m1 + m2 ) ) = CurInstr ( P1 , Comput ( P1 , s1 , m1 ) ) .= CurInstr ( P1 , Comput ( P1 , s1 , m2 ) ) .= CurInstr ( P1 , Comput ( P1 , s1 , m2 ) ) .= CurInstr ( P1 , Comput ( P1 , s1 , m2 ) ) .= halt SCMPDS ;
assume that a on M and b on M and c on N and d on N and p on M and a on N and c on N and d on P and p on P and p on Q and a on P and b on Q and c on Q and d on P and p on Q and c on Q and d on Q and c on Q and d on Q and d on Q ;
assume that T is \hbox -Z of 4 and F is closed and ex F be Subset-Family of T st F is closed & ind F <= 0 & ind F <= 0 & ind F <= 0 and ind T <= 0 and ind T <= 0 ;
for g1 , g2 st g1 in ]. r - g , r + g .[ & |. f . g1 - f . g2 .| <= ( g1 - g2 ) / ( |. r - g .| ) holds |. ( f - g ) . g1 - f . g2 .| <= ( f - g ) / ( |. r - g .| ) / ( |. r - g .| )
( ( - 1 / 2 ) * ( ( - 1 / 2 ) * ( ( - 1 / 2 ) * ( ( - 1 / 2 ) * ( - 1 / 2 ) * ( - 1 / 2 ) * ( - 1 / 2 ) * ( - 1 / 2 ) * ( - 1 / 2 ) * ( - 1 / 2 ) * ( - 1 / 2 ) * ( - 1 / 2 ) * ( - 1 / 2 ) * ( - 1 / 2 * ( - 1 / 2 ) ) ) = ( - 1 / 2 * ( - 1 / 2 * ( - 1 / 2 * ( - 1 / 2 * ( - 1 / 2 * ( - 1 / 2 * ( - 1 / 2 * ( - 1 / 2 * ( - 1 / 2 * ( - 1 / 2 * ( - 1 / 2 ) * ( - 1 / 2 ) * ( - 1 / 2
F . i = F /. i .= 0. R + r2 .= ( b |^ n + r2 ) * ( a |^ n ) .= <* ( ( n + 1 ) / a ) * ( a |^ n + b |^ n ) * ( a |^ n ) * ( a |^ n ) *> .= <* ( n + 1 ) / a |^ ( n + 1 ) * a * b |^ n *> ;
ex y being set , f being Function st y = f . n & dom f = A ( ) & f . 0 = R ( ) & for n holds f . ( n + 1 ) = R ( n , f . n ) & f . n = R ( n , f . n ) & f . n = f . ( n + 1 ) ;
func f (#) F -> FinSequence of V means : Def1 : len it = len F & for i be Nat st i in dom it holds it . i = F . i * ( F /. i ) * ( F /. i ) ;
{ 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 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x6 } = { x1 , x2 , x3 , x4 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x6 , x5 , x6 , 6 , x5 , 7 , 7 , 7 , x5 , x5 , 6 , 6 , x5 , x5 , x5 , 7 , x5 , x5 , 6 , 7 , 7 , 7 , x5 , 6 , 7 , x5 , 6 , 7 , 8 , 7 , 6 , 6
for n being Nat , x being set st x = h . n holds h . ( n + 1 ) = o ( x , n ) & x in InputVertices S ( x , n ) & o . ( n + 1 ) in InnerVertices S ( x , n ) & o . ( n + 1 ) in InnerVertices S ( x , n )
ex S1 being Element of CQC-WFF ( Al ( ) ) st SubP ( P , l , e ) = S1 & ( for S being Element of CQC-WFF ( Al ( ) ) holds S . S is Element of CQC-WFF ( Al ( ) , e , e ) ) & ( S . S ) `1 = e ) & ( S . S ) `1 = e & ( S . S ) `1 = e ;
consider P being FinSequence of Gs2 such that p9 = Product P and for i st i in dom P ex t7 being Element of the carrier of K st P . i = t & P . i = Q . i & P . i = t . i & P . i = t . i & P . i = t . i ;
for T1 , T2 being strict non empty TopSpace , P being Basis of T1 , T2 being Basis of T2 st the carrier of T1 = the carrier of T2 & P = the topology of T2 & P = the topology of T2 holds P is Basis of T1 & P is Basis of T2
assume that f is_is_is_is_differentiable , u0 and r (#) pdiff1 ( f , 3 ) is_partial_differentiable_in u0 , 2 and partdiff ( r (#) pdiff1 ( f , 3 ) , u0 , 3 ) = r * pdiff1 ( f , u0 ) . 3 and partdiff ( r (#) pdiff1 ( f , 3 ) , u0 , 3 ) = r * partdiff ( f , u0 , 3 ) ;
defpred P [ Nat ] means for F , G being FinSequence of ( Seg $1 ) * , G be Permutation of Seg $1 st len F = $1 & G = F * s holds Sum F = Sum G & Sum G = Sum F ;
ex j st 1 <= j & j < width GoB f & ( ( GoB f ) * ( 1 , j ) ) `2 < s & s < ( ( GoB f ) * ( 1 , j + 1 ) ) `2 & s < ( ( GoB f ) * ( 1 , j + 1 ) ) `2 ;
defpred U [ set , set ] means ex Fi1 being Subset-Family of T st $2 = Fi1 & union Fi1 is open & union Fi1 is open & union Fi1 is open & union Fi1 is open & union Fi1 is open & union Fi1 is NAT & union Fi1 is <= & union Fi1 is <= ;
for p4 being Point of TOP-REAL 2 st LE p4 , p4 , P & LE p1 , p2 , P & LE p2 , p3 , P & LE p3 , p4 , P holds LE p4 , p4 , P & LE p4 , p1 , P & LE p4 , p2 , P & LE p4 , p1 , P & LE p4 , p1 , P & LE p4 , p2 , P & LE p4 , p2 , P & LE p4 , p1 , P holds LE p4 , p2 , P
f in \rbrace & for g st g in D & for y st g . y <> f . y holds g in ( the Sorts of Free ( S , X ) ) . ( f . y ) = f . ( All ( x , X ) ) ;
ex 8 being Point of TOP-REAL 2 st x = 8 & ( ( ( - 1 ) * ( ( p `2 / |. p .| - sn ) / ( 1 - sn ) ) / ( 1 - sn ) ) * ( 1 - sn ) + sn ) / ( 1 - sn ) * ( 1 - sn ) <= 0 & 0 <= 8 & 8 <= 1 ;
assume for d7 being Element of NAT st d7 <= d7 holds s1 . ( ( n + 1 ) -\hbox { d } ) = s2 . ( ( n + 1 ) -\hbox { d } ) & s2 . ( ( n + 1 ) -\hbox { d } ) = s2 . ( ( n + 1 ) -\hbox { d } ) ;
assume that s <> t and s is Point of Sphere ( x , r ) and s is not Point of Sphere ( x , r ) and ex e being Point of Sphere ( x , r ) st e = Ball ( s , r ) /\ Sphere ( x , r ) & e in Sphere ( x , r ) /\ Sphere ( y , r ) ;
given r such that 0 < r and for s st 0 < s ex x1 be Point of CNS st x1 in dom f & ||. x1 - x0 .|| < s & |. f /. x1 - f /. x0 .| < r & |. f /. x1 - f /. x0 .| < r ;
( p | x ) | ( p | ( x | x ) ) = ( ( ( ( x | x ) | x ) | ( x | x ) ) | ( p | ( x | x ) ) ) | p ;
assume that x , x + h / 2 in dom sec and ( for x st x in dom sec holds sin . x = ( 4 * sin ( x + h / 2 ) * sin ( x + h / 2 ) ) / ( sin ( x + h / 2 ) * sin ( x + h / 2 ) ) and sin . x = sin ( x + h / 2 ) / ( cos ( x + h / 2 ) * sin ( x + h / 2 ) ) ;
assume that i in dom A and len A > 1 and for i , j st i > 1 & j > 1 & i < len B & j < len A holds A * ( i , j ) = ( i , j ) * ( i , j ) and i < j and j < len A and j < len A and i < j ;
for i be non zero Element of NAT st i in Seg n holds i divides n or i = n or i = n or i = n & i <> n & i <> n & i <> n & i <> n implies h . i = 1. ( F_Complex , n ) & i <> n & i <> n implies h . i = 1. ( F_Complex _ n , n )
( ( ( b1 'imp' b2 ) '&' ( c1 'imp' c2 ) '&' ( ( b1 'or' c2 ) '&' ( c1 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 ) '&' 'not' ( a2 '&' c2 )
assume that for x holds f . x = ( ( - cot * sin ) . x ) & for x st x in dom ( ( - cot * sin ) `| Z ) holds ( ( - cot * sin ) `| Z ) . x = - cos . ( x + h ) / ( sin . ( x + h ) ) / ( sin . ( x + h ) ) / ( sin . ( x + h ) ) ^2 ) ;
consider R8 , I8 be Real such that R8 = Integral ( M , Re ( F . n ) ) and I8 = Integral ( M , Im ( F . n ) ) and Integral ( M , Im ( F . n ) ) = Integral ( M , Im ( F . n ) ) + Integral ( M , Im ( F . n ) ) ;
ex k be Element of NAT st k = k & 0 < d & for q be Element of product G st q in X & ||. q- partdiff ( f , q , k ) .|| < r holds ||. partdiff ( f , q , k ) - partdiff ( f , x , k ) .|| < r ;
x in { x1 , x2 , x3 , x4 , x5 , x5 , x5 , x5 , x5 , x5 , 6 , 7 , 8 , 8 , 8 , 7 , 8 , 8 , 8 , 8 , 7 , 8 , 8 , 8 , 7 , 8 , 8 , 8 , 7 , 8 , 8 , 8 , 7 , 8 , 8 , 8 , 8 , 7 , 8 , 8 , 8 , 7 , 8 , 8 , 8 , 8 , 8 , 8 , 8 , 7 , 8 , 8 , 8 , 8 , 8 , 8 , 7 , 8 , 7 , 8 , 8 , 8 , 7 , 8 , 8 , 8 , 8 , 8 , 8 , 7 , 7 , 8 , 7 , 8 , 7 , 8 , 8 , 7 , 8 , 8 , 8 , 8 , 8 , 8 , 8 , 8 , 7 , 8 , 8 , 7 , 7 , 7 , 8 , 8 , 8 , 7 ,
G * ( j , i ) `2 = G * ( 1 , i ) `2 .= G * ( 1 , j ) `2 .= G * ( 1 , j ) `2 .= G * ( 1 , j ) `2 .= G * ( 1 , j ) `2 .= G * ( 1 , j + 1 ) `2 .= G * ( 1 , j + 1 ) `2 .= G * ( 1 , j + 1 ) `2 .= p `2 ;
f1 * p = p .= ( ( the Arity of S1 ) * ( the Arity of S2 ) ) . o .= ( the Arity of S1 ) . ( g . o ) .= ( the Arity of S1 ) . ( g . o ) .= ( the Arity of S2 ) . ( g . o ) .= ( the Arity of S1 ) . ( g . o ) .= ( the Arity of S1 ) . ( g . o ) .= ( the Arity of S1 ) . ( g . o ) ;
func tree ( T , P , T1 ) -> DecoratedTree means : Def1 : q in it iff q in T & for p st p in P holds p in T or p in T1 & q in T1 & p in T1 & q in T1 & p = T ;
F /. ( k + 1 ) = F . ( k + 1 -' 1 ) .= Fholds ( F /. ( k + 1 -' 1 ) ) * ( F /. ( k + 1 -' 1 ) ) = Fx0 * ( F /. k , k -' 1 ) .= Fx0 * ( F /. k , k -' 1 ) * F /. ( k + 1 -' 1 ) .= Fx0 * ( F /. k , k -' 1 ) ;
for A , B , C being Matrix of K st len B = len C & width B = width C & len B = width C & len A > 0 & width B > 0 & len B > 0 & width B > 0 & len B > 0 & width B > 0 & width B > 0 & width B > 0 & width B > 0 holds A * ( B * C ) = B * ( C * C )
seq . ( k + 1 ) = 0. F_Complex + seq . ( k + 1 ) .= ( Partial_Sums ( seq ) ) . ( k + 1 ) + seq . ( k + 1 ) .= ( Partial_Sums ( seq ) ) . ( k + 1 ) + seq . ( k + 1 ) .= ( Partial_Sums ( seq ) ) . ( k + 1 ) + seq . ( k + 1 ) ;
assume that x in ( the carrier of Cq ) /\ ( the carrier of Cq ) and y in ( the carrier of Cq ) /\ the carrier of Cq and z = [ x , y ] and [ x , y ] in the InternalRel of Cq ;
defpred P [ Element of NAT ] means for f st len f = $1 holds ( VAL g ) . ( ( f /. ( k + 1 ) ) '&' ( VAL g ) . ( ( f /. ( k + 1 ) ) '&' ( VAL g ) . ( ( f /. ( k + 1 ) ) '&' ( VAL g ) . ( k + 1 ) ) ) = ( VAL g ) . ( ( f /. ( k + 1 ) ) '&' ( VAL g ) ) ;
assume that 1 <= k and k + 1 <= len f and f is_sequence_on G and [ i , j ] in Indices G and f /. k = G * ( i , j ) and f /. ( k + 1 ) = G * ( i , j ) and f /. k = G * ( i + 1 , j ) ;
assume that sn < 1 and ( q `1 > 0 & q `2 / |. q .| - sn ) / ( 1 + sn ) >= 0 and p `2 / |. q .| - sn and q `2 / |. q .| - sn and q `2 / |. q .| - sn and q `2 / |. q .| - sn and q `2 / |. q .| - sn and q `2 / |. q .| - sn and q `2 / |. q .| - sn and q `2 / |. q .| - sn and q `2 / |. q .| - sn and q `2 / |. q .| - sn and q `2 / |. q .| - sn and q `2 / |. q .| / |. q .| >= sn and q `2 / |. q .| / |. q .| - sn and q `2 / |. q .| / |. q .| / |. q .| >= sn and q `2 / |. q .| >= sn and q `2 / |. q .| - sn and q `2 / |. q .| - sn
for M being non empty dist , x being Point of M , f being Point of M , x being Point of M st x = x `1 holds ex f being sequence of L~ f st f is sequence of ( the carrier of M ) & for n being Element of NAT holds f . n = dist ( x `1 , n )
defpred P [ Element of omega ] means f1 is_differentiable_on Z & f2 is_differentiable_on Z & for x st x in Z holds ( ( f1 - f2 ) `| Z ) . x = ( f1 - f2 ) . x - ( f1 - f2 ) . x ;
defpred P1 [ Nat , Point of CNS ] means $2 in Y & ||. ( f /. $1 ) - ( f /. ( $1 + 1 ) ) .|| < r & ||. ( f /. $1 ) - ( f /. ( $1 + 1 ) ) .|| < r ;
( f ^ mid ( g , 2 , len g ) ) . i = ( mid ( g , 2 , len f -' 1 ) ) . ( i -' 1 ) .= g . ( i -' 1 + 1 ) .= g . ( i -' 1 + 1 ) .= g . ( i -' 1 + 1 ) .= g . ( i -' 1 + 1 ) .= f . ( i -' 1 + 1 ) ;
( 1 / 2 * n0 + 2 * ( 2 * n0 + 2 * ( 2 * n0 + 1 ) ) * ( 2 * n0 + 2 * ( 2 * n0 + 1 ) ) * ( 2 * n0 + 1 ) * ( 2 * n0 + 1 ) * ( 2 * n0 + 1 ) * ( 2 * n0 + 1 ) * ( 2 * n0 + 1 ) * ( 2 * n0 + 1 ) * ( 2 * n0 + 1 ) * ( 2 * n0 + 1 ) * ( 2 * n0 + 1 ) = ( 1 / 2 * n0 + 1 ) * ( 2 * n0 + 1 ) * ( 2 * n0 ) * ( 2 * n0 + 1 ) * ( 2 * n0 + 1 ) * ( 2 * n0 + 1 ) * ( 2 * n0 + 1 ) * ( 2 * n0 + 1 ) * ( 2 * n0 + 1 ) * ( 2 * n0 + 1 ) * ( 2 * n0 + 1 ) * ( 2 * n0 + 1 ) * ( 2 *
defpred P [ Nat ] means for G being non empty finite strict finite strict RelStr , H being strict strict symmetric RelStr st G is \mathop { H , G } & the carrier of H = the carrier of G & the carrier of H = the carrier of G & the InternalRel of H = the InternalRel of H & the InternalRel of H = the InternalRel of G & the InternalRel of H = the InternalRel of H ;
assume that f /. 1 in Ball ( u , r ) and 1 <= m & m <= len f and LSeg ( f , i ) /\ LSeg ( f , m ) <> {} and LSeg ( f , i ) /\ LSeg ( f , m ) <> {} and LSeg ( f , i ) /\ LSeg ( f , m ) <> {} and f /. m in Ball ( f , n ) /\ LSeg ( f , m ) ;
defpred P [ Element of NAT ] means ( Partial_Sums ( ( cos * ( ( cos * ( ( 1 / 2 ) * ( cos * ( ( 1 / 2 ) * ( cos * ( ( 1 / 2 * ( ( 1 / 2 * ( ( 1 / 2 * ( n / 2 * ( n / 2 * n ) ) ) ) / 2 ) ) ) ) ) ) . $1 = ( Partial_Sums ( ( cos * ( n / 2 * ( n / 2 * ( n / 2 * ( n / 2 * ( n / 2 * ( n / 2 * ( n / 2 ) ) ) ) ) ) . ( 2 * ( n / 2 * ( n / 2 * ( n / 2 ) ) ) ) . ( 2 * ( n / 2 * ( n / 2 * ( n / 2 ) ) ) ) . ( $1 / 2 * ( ( n / 2 ) ) ) . ( x / 2 ) ) ) . ( x / 2 ) ) ) . ( x / 2 ) ) = ( Partial_Sums
for x being Element of product F holds x is FinSequence of I & dom x = I & for i being set st i in dom x holds x . i = ( the Sorts of F ) . i & for i being set st i in dom x holds x . i = ( the Sorts of F ) . i
( x " ) |^ ( n + 1 ) = ( x " ) * x * x " .= ( x * x ) |^ n * x .= ( x |^ n ) * x .= ( x |^ n ) * x .= ( x |^ n ) * x .= ( x |^ n ) * x .= ( x |^ n ) * x .= ( x |^ n ) * x .= ( x |^ n ) * x ;
DataPart Comput ( P +* I , ( Initialized s ) , ( Initialized s ) +* I , ( Initialized s ) +* I , ( Initialized s ) +* I , ( Initialized s ) +* I ) = DataPart Comput ( P +* I , ( Initialized s ) +* I , ( Initialized s ) +* I , ( Initialized s ) +* I ) ;
given r such that 0 < r and ]. x0 - r , x0 .[ c= ( dom f1 /\ dom f2 ) /\ dom ( f1 - f2 ) and for g st g in ]. x0 - r , x0 .[ /\ dom ( f1 - f2 ) & g in ]. x0 - r , x0 .[ /\ dom ( f1 - f2 ) ;
assume that X c= dom f1 /\ dom f2 and f1 | X is continuous and f2 | X is continuous and ( f1 + f2 ) | X is continuous and ( f1 - f2 ) | X is continuous and ( f1 - f2 ) | X is continuous and ( f1 - f2 ) | X is continuous and f2 | X is continuous ;
for L being continuous complete LATTICE for l being Element of L ex X being Subset of L st l = sup X & for x being Element of L st x in X holds x is directed & for x being Element of L st x in X holds x = "\/" ( waybelow l /\ ( { x } , L ) )
Support e8 in { m *' p where m is Polynomial of n , L : ex i being Element of NAT st i in dom ( m *' p ) & p . i = ( m *' q ) . i & ex n being Nat st n in dom ( m *' p ) & q . i = ( m *' p ) . ( i + 1 ) ;
( f1 - f2 ) /. ( lim s1 ) = lim ( f1 /* s1 - f2 /* s1 ) .= lim ( ( f1 /* s1 ) - ( f2 /* s1 ) ) .= lim ( ( f1 /* s1 ) - ( f2 /* s1 ) ) .= lim ( ( f1 /* s1 ) - ( f2 /* s1 ) ) .= lim ( ( f1 /* s1 ) - ( f2 /* s1 ) ) ;
ex p1 being Element of CQC-WFF ( Al ) st p1 = g . p1 & for g being Function of [: [: D , D :] , D :] , D st P [ g , ( len g ) , ( len g ) ] holds P [ g , ( len g ) , ( len g ) ] ;
( mid ( f , i , len f -' 1 ) ^ <* f /. ( len f -' 1 ) *> ) /. j = ( mid ( f , i , len f -' 1 ) ) /. j .= ( mid ( f , i , len f -' 1 ) ) /. j .= f /. ( j + 1 ) .= f /. ( j + 1 ) ;
( ( p ^ q ) . ( len p + k ) ) . ( len p + k ) = ( ( ( p ^ q ) . ( len p + k ) ) . ( k + 1 ) ) . ( ( p ^ q ) . ( len p + k ) ) .= ( ( p ^ q ) . ( len p + k ) ) . ( k + 1 ) .= ( ( p ^ q ) . ( k + 1 ) ) . ( k + 1 ) .= ( ( p ^ q ) . ( k + 1 ) .= ( ( p ^ q ) . ( k + 1 ) . ( k + 1 ) . ( k + 1 ) . ( k + 1 ) . ( k + 1 ) . ( k + 1 ) . ( k + 1 ) . ( len p + 1 ) .= ( ( ( k + 1 ) .= ( ( p ^ q ) . ( len p + 1 ) . ( len p + 1 ) . ( len p + 1 ) .= ( ( p ^ q ) . ( k + 1 ) . ( len p + 1 ) . ( len p + 1 ) .=
len mid ( upper_volume ( f , D2 ) , 1 , indx ( D2 , D1 , j1 ) + 1 ) = indx ( D2 , D1 , j ) - indx ( D2 , D1 , j1 ) + 1 .= indx ( D2 , D1 , j1 ) + 1 - 1 ;
x * y * z = Mf . ( ( y * z ) * ( y * z ) ) .= ( x * ( y * z ) ) * ( ( y * z ) * ( y * z ) ) .= ( x * ( y * z ) ) * ( y * z ) .= ( x * ( y * z ) ) * ( y * z ) .= ( x * y ) * ( y * z ) ;
v . <* x , y *> - ( <* x0 , y0 *> - ( x - y ) * i ) = partdiff ( v , ( x - y ) * ( x - y ) + ( y - x0 ) * ( x - y ) * i ) + ( proj ( 1 , ( x - y ) * i ) * ( x - y ) * i ) ;
i * i = [* 0 * ( - 1 ) - ( 0 * 0 ) * 0 + 0 * 0 .= - 1 * 0 + 0 * 0 .= - 1 * 0 + 0 * 0 .= - 1 * 0 + 0 * 0 .= - 1 * 0 + 0 * 0 .= - 1 * 0 + 0 * 0 .= - 1 * 0 + 0 * 0 .= - 1 * 0 + 0 * 0 .= - 1 * 0 + 0 * 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 +
Sum ( L (#) F ) = Sum ( L (#) ( F1 ^ F2 ) ) .= Sum ( L (#) F1 ) + Sum ( L (#) F2 ) .= Sum ( L (#) F1 ) + Sum ( L (#) F2 ) .= Sum ( L (#) F1 ) + Sum ( L (#) F2 ) .= Sum ( L (#) F1 ) + Sum ( L (#) F2 ) .= Sum ( L (#) F1 ) + Sum ( L (#) F2 ) ;
ex r be Real st for e be Real st 0 < e ex Y1 be finite Subset of X st Y1 is non empty & for Y be finite Subset of X st Y c= Y & Y c= Y holds |. Sum ( the carrier of X , Y ) - Sum ( the carrier of Y , Y ) .| < r
( GoB f ) * ( i , j ) = f /. ( k + 2 ) & ( GoB f ) * ( i , j + 1 ) = f /. ( k + 2 ) or ( GoB f ) * ( i , j + 1 ) = f /. ( k + 2 ) & ( GoB f ) * ( i , j + 1 ) = f /. ( k + 2 ) ;
( ( cos - sin ) / ( cos - sin ) ) / ( cos - sin ) = ( - ( cos - sin ) / ( cos - sin ) ) / ( cos - sin ( - ( sin - cos ) / ( cos - sin ( - ( cos - sin ( - ( sin - cos ) / ( sin - cos ) ) ) ) ) .= ( - ( cos - sin ( - ( cos - / sin ) ) / ( cos - sin ( - ( sin - cos ( - ( sin - cos ( - ( sin - cos ( - ( sin - cos ( - ( sin ( - ( sin ( - ( - ( - ( sin - cos ( - ( sin - cos ( - ( sin - ( sin - ( sin - ( sin - ( sin - ( sin - ( sin ( - ( sin ( - ( sin ( - ( sin ( - ( sin ( - ( sin ( - ( sin ( - ( sin ( - ( sin ( - ( sin ( - ( sin ( - ( - ( - ( sin ( - ( sin ( - ( sin ( - ( - ( sin ( - ( sin ( -
( - b + sqrt ( delta ( a , b , c ) ) / ( 2 * a ) < 0 & - ( - b - sqrt ( delta ( a , b , c ) ) / ( 2 * a ) ) / ( 2 * a ) > 0 or - ( - b - sqrt ( delta ( a , b , c ) ) / ( 2 * a ) ) / ( 2 * a ) > 0 ;
assume that ex_inf_of uparrow "\/" ( X /\ C , L ) and ex_sup_of X , L and "\/" ( X , L ) = "/\" ( X , L ) and "\/" ( X , L ) = "/\" ( X , L ) and "\/" ( X , L ) = "/\" ( X , L ) and "\/" ( X , L ) = "/\" ( X , L ) ;
( for j being Element of Oed ( B ) ) . ( j , i ) = ( j , i ) |-- ( i , j ) & j = i implies ( j = i & j = i & j = j implies i = j ) & j = i & j = j implies i = j & j = i & j = i & j = j implies j = i & j = i & j = j