thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
contradiction ;
contradiction ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
contradiction ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
assume not thesis ;
assume not thesis ;
B ;
a <> c
T c= S
D c= B
c in X ;
b in X ;
X ;
b in D ;
x = e ;
let m ;
h is onto ;
N in K ;
let i ;
j = 1 ;
x = u ;
let n ;
let k ;
y in A ;
let x ;
let x ;
m c= y ;
F is one-to-one ;
let q ;
m = 1 ;
1 < k ;
G is cyclic ;
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 ;
k be Nat ;
K ` is being_line ;
assume n >= N ;
assume n >= N ;
assume X is \rm _ \sum ;
assume x in I ;
q is limit_ordinal ;
assume c in x ;
p > 0 ;
assume x in Z ;
assume x in Z ;
1 <= k12 ;
assume m <= i ;
assume G is cyclic ;
assume a divides b ;
assume P is closed ;
O > 0 ;
assume q in A ;
W is non empty ;
f is IC one-to-one ;
assume A is boundary ;
g is special ;
assume i > j ;
assume t in X ;
assume n <= m ;
assume x in W ;
assume r in X ;
assume x in A ;
assume b is even ;
assume i in I ;
assume 1 <= k ;
X is non empty ;
assume x in X ;
assume n in M ;
assume b in X ;
assume x in A ;
assume T c= W ;
assume s is 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 ;
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 invertible ;
Q halts_on s ;
x in such that x in \in \in \in \in \in such
M < m + 1 ;
T2 is open ;
z in b \frac a ;
R2 is well-ordering ;
1 <= k + 1 ;
i > n + 1 ;
q1 is one-to-one ;
let x be non trivial set ;
P3 is one-to-one ;
n <= n + 2 ;
1 <= k + 1 ;
1 <= k + 1 ;
let e be Real ;
i < i + 1 ;
p3 in P ;
p1 in K ;
y in C1 ;
k + 1 <= n ;
let a be Real , x be Point of TOP-REAL 2 ;
X |- r => p ;
x in { A } ;
let n be Nat ;
let k be Nat ;
let k be Nat ;
let m be Nat ;
0 < 0 + k ;
f is_differentiable_in x ;
let x0 ;
let E be Ordinal ;
o OperSymbol o1 ;
O <> O2 ;
let r be Real ;
let f be FinSeq-Location ;
let i be Nat ;
let n be Nat ;
Cl A = A ;
L c= Cl L ;
A /\ M = B ;
let V be RealUnitarySpace , M be Subset of V ;
not s in Y |^ 0 ;
rng f <= w
b "/\" e = b ;
m = m1 ;
t in h . D ;
P [ 0 ] ;
assume z = x * y ;
S . n is bounded ;
let V be RealUnitarySpace , A be Subset of V ;
P [ 1 ] ;
P [ {} ] ;
C1 is connected ;
H = G . i ;
1 <= i `2 + 1 ;
F . m in A ;
f . o = o ;
P [ 0 ] ;
aa <= b ;
R [ 0 ] ;
b in f .: X ;
assume q = q2 ;
x in [#] V ;
f . u = 0 ;
assume e1 > 0 ;
let V be RealUnitarySpace , A be Subset of V ;
s is trivial & s is non empty ;
dom c = Q ;
P [ 0 ] ;
f . n in T ;
N . j in S ;
let T be complete LATTICE , f be Function of T , 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 ;
v^ < n ;
S5 is bounded ;
assume p = p2 ;
len f = n ;
assume x in P1 ;
i in dom q ;
let U0 ;
pp = c ;
j in dom h ;
let k ;
f | Z is continuous ;
k in dom G ;
UBD C = B ;
1 <= len M ;
p in Ball x ;
1 <= jj ;
set A = \overline Reconsider an ;
card a [= c ;
e in rng f ;
cluster B \oplus A -> non empty ;
H has the means : Let : H is Set ;
assume that n <= m and m <= n ;
T is increasing ;
e2 <> e2 ;
Z c= dom g ;
dom p = X ;
H is proper of G ;
i + 1 <= n ;
v <> 0. V ;
A c= Affin A ;
S c= dom F ;
m in dom f ;
X0 be set ;
c = sup N ;
R is connected & union M is connected ;
assume not x in REAL ;
Im f is complete ;
x in Int y ;
dom F = M ;
a in On W ;
assume e in [: A , B :] ;
C c= C1. ( K , n ) ;
m1 <> {} ;
let x be Element of Y ;
let f be Int oriented Chain , x be Element of f ;
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 in v \overline ( X ) ;
- y in I ;
let A be non empty set , B be Subset of A ;
P0 = 1 ;
assume r in F . k ;
assume f is simple ;
let A be Incountable set ;
rng f c= NAT ;
assume P [ k ] ;
f6 <> {} ;
let o be Ordinal ;
assume x is sum of squares ;
assume not v in { 1 } ;
let I1 ;
assume that 1 <= j and j < l ;
v = - u ;
assume s . b > 0 ;
d1 in NAT ;
assume t . 1 in A ;
let Y be non empty TopSpace , f be Function of Y , TOP-REAL 2 ;
assume a in ]. s , t .[ ;
let S be non empty RelStr ;
a , b // b , a ;
a * b = p * q ;
assume x , y are_the space ;
assume x in Omega ( f ) ;
[ a , c ] in X ;
m1 <> {} ;
M + N c= M + M ;
assume M is \llangle h\rbrace ;
assume f is inintn\ast ;
let x , y be element ;
let T be non empty TopSpace ;
b , a // b , c ;
k in dom Sum p ;
let v be Element of V ;
[ x , y ] in T ;
assume len p = 0 ;
assume C in rng f ;
k1 = k2 & k2 = k2 ;
m + 1 < n + 1 ;
s in S \/ { s } ;
n + i >= n + 1 ;
assume Re y = 0 ;
k1 <= j1 & k2 <= j2 ;
f | A is element ;
f . x be Real ;
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 ;
CP ;
q2 c= C1 & q2 in C2 ;
a2 < c2 & c2 < c2 ;
s2 is 0 -started ;
IC s = 0 ;
s4 = s4 . 5 ;
let V ;
let x , y be element ;
let x be Element of T ;
assume a in rng F ;
x in dom T ` ;
let S be verify of L ;
y " <> 0 ;
y " <> 0 ;
0. V = uw ;
y2 , y , w is_collinear ;
RQ ;
let a , b be Real , r be Real ;
let a be Object of C ;
let x be Vertex of G ;
let o be Object of C , a be Element of A ;
r '&' q = P \lbrack l , r .] ;
let i , j be Nat ;
let s be State of A , P be State of A , Q be Subset of A ;
s4 . n = N ;
set y = ( x `1 ) / 2 ;
NAT in dom g & m 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 phi in NH ;
reconsider i = i as Ordinal ;
r * v = 0. X ;
rng f c= INT ;
G = 0 .--> goto 0 ;
let A be Subset of X ;
assume that A9 is dense and A9 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 ) ;
let o be OperSymbol of S ;
let R be connected non empty RelStr ;
n + 1 = succ n ;
xY c= Z1 & xY c= Z1 ;
dom f = C1 & rng g c= C2 ;
assume [ a , y ] in X ;
Re ( seq ) is convergent ;
assume a1 = b1 & a2 = b2 ;
A = Int ( A ) ;
a <= b or b <= a ;
n + 1 in dom f ;
let F be Instruction of S , s be State of S ;
assume r2 > x0 & x0 < r2 ;
let Y be non empty set , f be Function of Y , BOOLEAN ;
2 * x in dom W ;
m in dom g2 & n + 1 in dom g2 ;
n in dom g1 & m + 1 in dom g2 ;
k + 1 in dom f ;
not the still not bound in { s } ;
assume x1 <> x2 & x2 <> x3 ;
v2 in V1 & v2 in V1 ;
not [ b `1 , b `2 ] in T ;
ii + 1 = i ;
T c= FinSequence ( T ) ;
( l - 1 ) * ( l - 1 ) = 0 ;
n be Nat ;
( t `2 ) ^2 = r ;
AA is integrable & f | A is bounded ;
set t = Top t ;
let A , B be real-membered set ;
k <= len G + 1 ;
[: V , C :] misses [: V , C :] ;
Product ( seq ) is non empty ;
e <= f or f <= e ;
cluster -> non empty for normal Function ;
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 v-4 is Cauchy and for n be Nat holds vK . n is convergent ;
IC Comput ( P3 , s3 , k ) = 0 ;
k in N or k in K ;
F1 \/ F2 c= F ;
Int G1 <> {} & Int G1 <> {} ;
( z `2 ) ^2 = 0 ;
p1 <> p1 & p2 <> p3 ;
assume z in { y , w } ;
MaxADSet ( a ) c= F ;
ex_sup_of ]. s , t .[ , S ;
f . x <= f . y ;
let T be up-complete non empty reflexive antisymmetric RelStr ;
q |^ m >= 1 ;
a >= X & b >= Y ;
assume <* a , c *> <> {} ;
F . c = g . c ;
G is one-to-one ;
A \/ { a } c= B ;
0. V = 0. Y ;
let I be as as as <= Instruction of S , s be State of 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 REAL & x2 in REAL ;
p1 = K1 & p2 = K1 ;
M . k = <*> REAL ;
phi . 0 in rng phi ;
MMMit is closed ;
assume z0 <> 0. L & z0 <> 0. L ;
n < Nk . n ;
0 <= seq . 0 - seq . 0 ;
- q + p = v ;
{ v } is Subset of B ;
set g = f /. 1 ;
[: R , S :] is stable
set RR = Vertices R , S = Vertices R ;
pp c= P1 & p2 in P2 ;
x in [. 0 , 1 .] ;
f . y in dom F ;
let T be Scott Scott Scott Scott Scott Scott TopAugmentation of S ;
inf the carrier of S in S ;
sup downarrow a = downarrow b ;
P , C , K is_collinear ;
assume x in F ( s , r ) ;
2 to_power i < 2 to_power m ;
x + z = x + z ;
x \ ( a \ x ) = x ;
||. \mathclose { 0 } .|| <= r ;
assume that Y c= field Q and Y <> {} ;
a ~ , b ~ are_isomorphic ;
assume a in A ( ) ;
k in dom ( q | k ) ;
p is FinSequence of S ;
i -' 1 = i-1 - 1 ;
f | A is one-to-one ;
assume x in f .: [: X , Y :] ;
i2 - i1 = 0 & i2 = 0 ;
j2 + 1 <= i2 ;
g " * a in N ;
K <> { [ {} , {} ] } ;
cluster -> strict for strict for strict non empty doubleLoopStr ;
|. q .| ^2 > 0 ;
|. p4 .| = |. p .| ;
s2 - s1 > 0 ;
assume x in { Gij } ;
W-min C in C & W-min C in C ;
assume x in { Gij } ;
assume i + 1 = len G ;
assume i + 1 = len G ;
dom I = Seg n & dom I = Seg n ;
assume that k in dom C and k <> i ;
1 + 1-1 <= i + 1-1 ;
dom S = dom F & dom F = Seg n ;
let s be Element of NAT ;
let R be ManySortedSet of A ;
let n be Element of NAT ;
let S be non void non empty holds holds cluster non void for \it 0. S ;
let f be ManySortedSet of I ;
let z be Element of COMPLEX , x be Element of COMPLEX ;
u in { [: -' g , g :] } ;
2 * n < ( 2 * n ) ;
x , y are_set ;
B-11 c= V1 & B-15 c= V2 ;
assume I is_closed_on s , P & I is_halting_on s , P ;
U = U . ( len U ) ;
M /. 1 = z /. 1 ;
x11 = x22 & x22 = x22 ;
i + 1 < n + 1 + 1 ;
x in { {} , <* 0 *> } ;
f7 <= f6 & f7 <= len f ;
let l be Element of L ;
x in dom ( F | X ) ;
let i be Element of NAT ;
rr is ( len rr ) -element ;
assume <* o2 , o *> <> {} ;
s . x |^ 0 = 1 ;
card ( K1 ) in M & card ( K1 ) in M ;
assume that X in U and Y in U ;
let D be Subset-Family of Omega ;
set r = { q + 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 an interval ;
|. <*> A .| . a = 0 ;
cluster strict for SubLattice of L ;
a1 in B . s1 & a2 in B . s1 ;
let V be finite RealUnitarySpace , F be Function of V , W ;
A * B on B & A on A ;
f-3 = NAT --> 0 ;
let A , B be Subset of V ;
z1 = P1 . 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 ;
sqrt ( PI / 2 ) < Arg z ;
reconsider z9 = 0 as Nat ;
LIN a , d , c ;
[ y , x ] in [: I , I :] ;
( Q /. 3 ) `2 = 0 ;
set j = x0 gcd m , m = x0 gcd m ;
assume a in { x , y , c } ;
j2 - ( j2 - 1 ) > 0 ;
I -TruthEval phi = 1 ;
[ y , d ] in F-8 ;
let f be Function of X , Y ;
set A2 = ( B |^ C ) * ( B |^ C ) ;
s1 , s2 are_] & s1 , s2 are_] implies s1 , s2 are_lim s1 , s2
j1 -' 1 = 0 & j1 - 1 = 1 ;
set m2 = 2 * n + j ;
reconsider t = t as bag of n ;
I2 . j = m . j ;
i |^ s , n are_congruent_mod p ;
set g = f | DY , h = f | DY ;
assume that X is lower bounded and 0 <= r ;
( p1 `1 ) ^2 = 1 ;
a < ( p3 `2 ) ^2 / ( p3 `1 ) ^2 ;
L \ { m } c= UBD C ;
x in Ball ( x , 10 ) ;
not a in LSeg ( c , m ) ;
1 <= i1 -' 1 + 1 ;
1 <= i1 -' 1 + 1 ;
i + i2 <= len h ;
x = W-min ( P ) .= P ;
[ x , z ] in X ~ ;
assume y in [. x0 , x .] ;
assume p = <* 1 , 2 , 3 *> ;
len <* A1 *> = 1 ;
set H = h . ( g . O ) ;
card b * a = |. a .| ;
Shift ( w , 0 ) |= v ;
set h = h2 ** h1 ;
assume x in X0 /\ ( X1 union X2 ) ;
||. h .|| < d1 & ||. h .|| < d ;
not x in the carrier of f .: the carrier of f ;
f . y = F ( y ) ;
for n holds X [ n ] ;
k - l = kk1 + 1 ;
<* p , q *> /. 2 = q ;
let S be Subset of the lattice of Y ;
let P , Q be Initialize s of S ;
Q /\ M c= union ( F | M )
f = b * ( canFS ( S ) ) ;
let a , b be Element of G ;
f .: X <= f . sup X ;
let L be non empty reflexive RelStr , X be Subset of L ;
S-20 is x -One -by i ;
let r be non positive Real ;
M , v |= x \hbox { y } ;
v + w = 0. ( V , w ) ;
P [ len F ] implies P [ F ] ;
assume InsCode i = 8 ;
the carrier of M = 0 & the carrier of M = { 0 } ;
cluster z * seq -> summable ;
let O be Subset of the carrier of C ;
||. f .|| | X is continuous ;
x2 = g . ( j + 1 ) ;
cluster -> non empty for Element of S ;
reconsider l1 = lk - 1 as Nat ;
v4 is Vertex of r2 & v4 is Vertex of r2 ;
T3 is SubSpace of T2 & T3 is SubSpace of T2 ;
Q1 /\ Q1 <> {} & Q1 /\ [#] ( TOP-REAL 2 ) <> {} ;
k be Nat ;
q " is Element of X & q " is Element of X ;
F . t is set of M & F . t is non empty ;
assume that n <> 0 and n <> 1 ;
set e = EmptyBag n , f = EmptyBag n , g = EmptyBag n , h = EmptyBag n , e = EmptyBag n , e = EmptyBag n , h = EmptyBag n , e = EmptyBag n ,
let b be Element of Bags n ;
assume for i holds b . i is commutative ;
x is root implies x `2 = ( p `1 ) / 2
not r in ]. p , q .[ ;
let R be FinSequence of REAL , r be Real ;
S7 does not destroy b1 & S7 does not destroy b2 ;
IC SCM ( R ) <> a ;
|. p - x .| >= r ;
1 * ( s * ( 1 - s ) ) = s * ( 1 - s ) ;
let x be FinSequence of NAT , n be Nat ;
let f be Function of C , D , g be Function of C , D ;
for a holds 0. L + a = a
IC s = s . NAT .= n ;
H + G = F-FL ;
C1 . x = x2 & C1 . x = y2 ;
f1 = f . x .= f2 . x .= f2 . x ;
Sum <* p . 0 *> = p . 0 ;
assume v + W = v + u + W ;
{ a1 } = { a2 } ;
a1 , b1 _|_ b , a ;
a3 , o _|_ o , a3 & a3 , o _|_ a3 , a4 ;
I1 is reflexive & I2 is reflexive & I2 is transitive implies f .: I is reflexive
I1 is antisymmetric & I2 is antisymmetric implies C is antisymmetric
sup rng H1 = e & sup rng H1 = e ;
x = ( a * a9 ) * ( a * b ) ;
|. p1 .| ^2 >= 1 ;
assume j2 -' 1 < 1 & j2 < len f ;
rng s c= dom f1 & rng s c= dom f2 ;
assume support a misses support b & not b in support b ;
let L be associative non empty doubleLoopStr , p be Polynomial of L ;
s " + 0 < n + 1 ;
p . c = ( f " ) . 1 ;
R . n <= R . ( n + 1 ) ;
Directed I1 = I1 & card I2 = card I1 ;
set f = + ( x , y , r ) ;
cluster Ball ( x , r ) -> bounded ;
consider r be Real such that r in A ;
cluster non empty for NAT -defined Function ;
let X be non empty directed Subset of S ;
let S be non empty full full SubRelStr of L ;
cluster <* F1 . N , F . N *> -> complete for non trivial Real ;
sqrt ( 1 - a " ) = a ;
( q . {} ) `1 = o ;
n - ( i -' 1 ) > 0 ;
assume sqrt ( 1 - 2 ) <= t `2 ;
card B = k + 1-1 ;
x in union rng ( f | X ) ;
assume x in the carrier of R & y in the carrier of R ;
d in D ;
f . 1 = L . ( F . 1 ) ;
the vertices of G = { v } ;
let G be : w: G is \times ;
e , v6 , v6 , v1 , v2 , v1 , v2 , v1 , v2 , V ;
c . i9 in rng c & c . i9 in rng c ;
f2 /* q is divergent_to+infty & f2 /* q is divergent_to+infty ;
set z1 = - z2 * z1 , z2 = - z2 * z1 , z2 = - z2 * z1 , z2 = - z2 * z1 , z1 = - z2 * z1 , z2 = - z2 ;
assume w is llas of S , G ;
set f = p \! \mathop { t } , g = p \! \mathop { t } , h = p \! \mathop { t } , f = p \! \mathop { t } , f = t \! \mathop
let c be Object of C ;
assume ex a st P [ a ] ;
let x be Element of REAL m , m be Element of REAL m ;
let I1 be Subset-Family of X , I2 be Subset-Family of X ;
reconsider p = p as Element of NAT ;
let v , w be Point of X ;
let s be State of SCM+FSA , P be Initialize s of SCM+FSA ;
p is FinSequence of NAT & p is FinSequence of NAT implies p . 1 = p . 1
stop I c= P +* I ;
set ci = f^ ( i , n ) ;
w ^ t ^ s seq ( n ) ^ s in rng w ;
W1 /\ W = W1 /\ W2 ;
f . j is Element of J . j ;
let x , y be Element of T2 , T be Subset of T2 ;
ex d st a , b // b , d ;
a <> 0 & b <> 0 ;
ord ( x ) = 1 & x is positive ;
set g2 = lim ( seq ^\ k ) , g1 = lim ( seq ^\ k ) ;
2 * x >= 2 * sqrt ( 1 + x ^2 ) ;
assume ( a 'imp' c ) . z <> TRUE ;
f (*) g in Hom ( c , c ) ;
Hom ( c , c + d ) <> {} ;
assume 2 * Sum ( q | m ) > m ;
L1 . ( F . ( F . k ) ) = 0 ;
: R1 \/ R1 = ( id X ) \/ ( id X ) ;
( ( ( - 1 ) (#) sin ) `| Z ) . x <> 0 ;
( ( ( exp_R * exp_R ) `| Z ) . x > 0 ;
o1 in ( X /\ O2 ) /\ ( X /\ O2 ) ;
e , v6 , v6 , v1 , v2 , v1 , v2 , v1 , v2 , V ;
r3 > ( 1 / 2 ) * 0 ;
x in P .: ( F " I ) ;
let J be closed Subset of R , I be Subset of R ;
h . p1 = f2 . O .= f . O ;
Index ( p , f ) + 1 <= j ;
len ( q * M ) = width M & width ( q * M ) = width M ;
the carrier of \mathbb K c= A & the carrier of \mathbb K c= A ;
dom f c= union rng ( F | X ) ;
k + 1 in support ( ( support ( n ) ) --> x ) ;
let X be ManySortedSet of the carrier of S ;
[ x `1 , y `2 ] in ( ( field R ) * ( R ~ ) ) ;
i = D1 or i = D2 ;
assume a mod n = b mod n ;
h . x2 = g . x1 .= x2 ;
F c= 2 |^ ( the carrier of X )
reconsider w = |. s1 .| as Real_Sequence of TOP-REAL 2 ;
sqrt ( 1 - m * r ) < p ;
dom f = dom I-4 & dom g = Seg len I-4 ;
[#] ( ( TOP-REAL 2 ) | K1 ) = [#] ( ( TOP-REAL 2 ) | K1 ) ;
cluster - x -> ExtReal for ExtReal ;
then { d } c= A ;
cluster [: TOP-REAL n , TOP-REAL n :] -> finite-ind ;
let w1 be Element of M ;
let x be Element of dyadic ( n ) ;
u in W1 & v in W2 implies u + v 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 / 1 .= n ;
h . J = EqClass ( u , J ) ;
let seq be \mathclose sequence of X ;
dist ( x `1 , y ) < r / 2 ;
reconsider mm = m - 1 as Element of NAT ;
x- x0 < r1 - x0 & r1 < x0 + r ;
reconsider P = P ` as strict Subgroup of N ;
set g1 = p * ( idseq ( q `1 ) ) ;
let n , m , k be non zero Nat ;
assume that 0 < e and f | A is lower ;
D2 . I2 in { x } ;
cluster -> subcondensed for Subset of T ;
let P be compact non empty Subset of TOP-REAL 2 , p , q be Point of TOP-REAL 2 ;
Gik in LSeg ( \pi , 1 ) /\ LSeg ( Gik , Gij ) ;
let n be Element of NAT , x be Element of NAT ;
reconsider ST = S as Subset of T ;
dom ( i .--> X ) = { i } ;
let X be non-empty ManySortedSet of S ;
let X be non-empty ManySortedSet of S ;
op ( 1 , {} ) c= { [ {} , {} ] } ;
reconsider m = m2 - 1 as Element of NAT ;
reconsider d = x as Element of [: C , D :] ;
let s be 0 -started State of SCMPDS , P be Initialize s of SCMPDS ;
let t be 0 -started State of SCMPDS , Q ;
b , b , x , y is_collinear & a , b , x , y is_collinear ;
assume that i = n \/ { n } and j = k \/ { n } ;
let f be PartFunc of X , Y ;
N2 >= sqrt ( ( sqrt c ) ^2 ) / sqrt ( ( N ^2 ) ^2 ) ;
reconsider t7 = T" as TopSpace ;
set q = h * p ^ <* d *> ;
z2 in U . ( y2 ) /\ Q2 . ( y2 ) ;
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 & i + 1 in Seg len s2 ;
z in dom g1 /\ dom f & z in dom f /\ dom g ;
assume p2 = W-min ( K ) & p1 = W-min ( K ) ;
len G + 1 <= i1 + 1 ;
f1 * f2 is convergent & f2 * f1 is convergent & lim ( f2 * f1 ) = x0 ;
cluster seq + ( seq + k ) -> summable ;
assume j in dom M1 /. i & j in dom M1 ;
let A , B , C be Subset of X ;
x , y , z is_collinear & x , y , z is_collinear ;
b ^2 - ( 4 * a * c ) >= 0 ;
<* xy *> ^ <* y *> divides x ;
a , b in { a , b } ;
len p2 is Element of NAT & len p1 = len p2 ;
ex x being element st x in dom R & y = R . x ;
len q = len ( K * G ) ;
s1 = Initialize Initialized s , P1 = P +* I , P2 = P +* I , P3 = P +* I , s4 = P +* I , s4 = P +* I , s4 = P +* I , s4 = P +* I
consider w being Nat such that q = z + w ;
x ` is Ideal of x & x ` is Element of L ;
k = 0 & n <> k or k > n ;
then X is discrete for X being Subset of X ;
for x st x in L holds x is FinSequence
||. f /. c - f /. c .|| <= r1 ;
c in ]. p , q .[ & not c in { p } ;
reconsider V = V as Subset of the carrier of TOP-REAL n ;
let N , M be being being being being being being being being being being being being being being being being void net of L ;
then z >= waybelow x ;
M | [. f , g .] = f & M | [. g , f .] = g ;
( to_power 1 ) /. 1 = TRUE ;
dom g = dom f .: X .= X ;
mode ^ of G is \cal : Let of G ;
[ i , j ] in Indices M & [ i , j ] in Indices M ;
reconsider s = x " as Element of H ( ) ;
let f be Element of Subformulae p , x be Element of Subformulae p ;
F1 . ( a1 , - a2 ) = G1 * ( a1 , a2 ) ;
cluster rectangle ( a , b , r ) -> compact ;
let a , b , c , d be Real ;
rng s c= dom ( 1 / ( f . x ) ) ;
curry ( ( curry F-19 ) . k ) is additive ;
set k2 = card ( dom B ) , k2 = card ( dom B ) , s4 = card ( dom B ) ;
set G = coprod ( X , X ) ;
reconsider a = [ x , s ] as terminal of G ;
let a , b be Element of [: M , M :] ;
reconsider s1 = s as Element of S0 ( S ) ;
rng p c= the carrier of L & p is one-to-one implies p is one-to-one
let d be Subset of the Sorts of A ;
( x .|. x ) = 0 iff x = 0. W
I1 in dom stop I & I2 in dom stop I ;
let g be continuous Function of X | B , Y ;
reconsider D = Y as Subset of TOP-REAL n ;
reconsider i0 = len p1 - 1 as Integer ;
dom f = the carrier of S & rng f c= the carrier of S ;
rng h c= union ( the carrier of J ) ;
cluster All ( x , H ) -> One -] ;
d * N1 > N1 * 1 / ( 1 - d ) ;
]. a , b .[ c= [. a , b .[ ;
set g = f " D1 | D1 , f = f " D2 ;
dom ( p | ( m + 1 ) ) = NAT ;
3 + - 2 <= k + - 2 ;
tan is_differentiable_in ( ( tan * arccot ) . x ) ;
x in rng ( f /^ ( p -' 1 ) ) ;
let f , g be FinSequence of D ;
[: p , q :] in the carrier of S1 & [: p , q :] in the carrier of S2 ;
rng f " { 0 } = dom f \ { 0 } ;
( the Target of G ) . e = v ;
width G -' 1 < width G -' 1 ;
assume v in rng ( S | E1 ) ;
assume x is root & x is root implies x is root & x is root ;
assume 0 in rng ( ( g2 ) | A ) ;
let q be Point of TOP-REAL 2 , a , b be Real ;
let p be Point of TOP-REAL 2 , a , b be Real ;
dist ( O , u ) <= |. p2 .| + 1 ;
assume dist ( x , b ) < dist ( a , b ) ;
<* S7 *> is_in the carrier of C-20 & <* S7 *> is Element of C-20 ;
i <= len G -' 1 + 1 & i + 1 <= len G -' 1 ;
let p be Point of TOP-REAL 2 , a , b be Real ;
x1 in the carrier of I[01] & x2 in the carrier of I[01] ;
set p1 = f /. i , p2 = f /. j ;
g in { g2 : r < g2 & g2 < x0 } ;
Q2 = Sp2 " . ( Q " ) .= Q " . ( Q " ) ;
( ( 1 / 2 ) to_power n ) is summable ;
- p + I c= ( - p + A ) + A ;
n < LifeSpan ( P1 , s1 ) + 1 ;
CurInstr ( p1 , s1 ) = i & CurInstr ( p1 , s1 ) = i ;
A /\ Cl { 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 , L2 ;
reconsider z = z as Element of InclPoset ( L ) ;
let f be Function of S , T ;
reconsider g = g as Morphism of c opp , b opp ;
[ s , I ] in S ~ ;
len ( the connectives of C ) = 4 & len ( the connectives of C ) = 5 ;
let C1 , C2 be subfunctor of C , o be object of C ;
reconsider V1 = V as Subset of X | B ;
attr p is valid means : Def6 : All ( x , p ) is valid ;
assume that X c= dom f and f .: X c= dom g and g .: X c= dom g ;
H |^ a " is Subgroup of H & H |^ a is Subgroup of H ;
let A1 be |^ of O , E be Element of O ;
p2 , r1 , q2 is_collinear & q2 , r1 , q2 is_collinear ;
consider x being element such that x in v ^ K and y = v . x ;
not x in { 0. TOP-REAL 2 } & x in { 0. TOP-REAL 2 } ;
p in [#] ( ( TOP-REAL 2 ) | B11 ) ;
0 . E < M . ( EE ) ;
^ ( c / d ) = c ;
consider c being element such that [ a , c ] in G ;
a1 in dom ( F . s2 ) & a2 = ( F . s2 ) `2 ;
cluster -> -> \uparrow for distributive distributive distributive distributive non empty Poset ;
set i1 = the Nat of G , i2 = the carrier of G , i1 = the carrier of G , i2 = the carrier of G , i2 = the carrier of G , i1 = the carrier of G , i2 = the carrier
let s be 0 -started State of SCM+FSA , P be s of P ;
assume y in ( f1 \/ f2 ) .: A ;
f . len f = f /. len f ;
x , f . x '||' f . x , f . y ;
attr X c= Y means : Def6 : cos .: X c= cos .: Y ;
let y be upper Subset of Y , x be Element of Y ;
cluster ( x `1 ) / 2 -> non inininininini2 ;
set S = <* Bags n , i9 *> ;
set T = [. 0 , 1 / 2 .] , G = [. 0 , 1 .] ;
1 in dom mid ( f , 1 , 1 ) ;
sqrt 4 * PI < sqrt 2 * PI ;
x2 in dom f1 /\ dom f2 & x1 in dom f2 /\ dom ( f1 + f2 ) ;
O c= dom I & { {} } c= { {} } ;
( 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 be Element of G ` ;
h19 . i = f . ( h . i ) ;
( p `1 ) ^2 = ( p1 `1 ) ^2 / ( p1 `1 ) ^2 ;
i + 1 <= len Cage ( C , n ) ;
len <* P *> = len P & len <* P *> = len P ;
set NN = the Element of the connectives of N , v be Element of the carrier of N ;
len g\mathopen ( x + 1 , x ) - 1 <= x ;
a on B & b on B implies a on B
reconsider r-12 = r * I . v as FinSequence ;
consider d such that x = d and a [= d and a [= c ;
given u such that u in W and x = v + u ;
len f /. ( \downharpoonright n ) = len f -' n ;
set q2 = q2 `2 / ( q2 `2 / ( q2 `2 ) ^2 ) ;
set S = { 1 , S2 } , T = { 2 } , f = the Element of S ;
MaxADSet ( b ) c= MaxADSet ( P /\ Q ) ;
Cl ( G . q1 ) c= F . r2 ;
f " D meets h " V & h " V c= h " V ;
reconsider D = E as non empty directed Subset of L1 ;
H = the_left_argument_of H '&' ( H '&' F ) ;
assume t is Element of ( S . s ) . X ;
rng f c= the carrier of S2 & rng g c= the carrier of S2 ;
consider y being Element of X such that x = { y } ;
f1 . ( a1 , b1 ) = b1 . a1 ;
the carrier' of G = E \/ { E } ;
reconsider m = len , k = len \mathbb k - 1 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 with_\mathbb \rbrace ;
for k st m <= k holds z in K . k ;
consider a being set such that p in a and a in G ;
L1 . p = p * L /. 1 .= p * L /. 1 ;
pp . i = p1 . i .= p1 . i ;
let PA , G be a_partition of Y , BOOLEAN ;
attr 0 < r & 1 < 1 & r < 1 implies r < 1 ;
rng ( AffineMap ( a , X ) ) = [#] X ;
reconsider x = x , y = y as Element of K ;
consider k such that z = f . k and n <= k ;
consider x being element such that x in X \ { p } ;
len ( ( canFS s ) | ( card s ) ) = card s ;
reconsider x2 = x1 , y2 = x2 as Element of L2 ;
Q in FinMeetCl ( ( the topology of X ) \ { 0 } ) ;
dom f0 c= dom u & dom f0 = dom u & dom f0 = dom v ;
attr n divides m & m divides n implies n = m ;
reconsider x = x as Point of [: I[01] , I[01] :] ;
a in ;
not y0 in the still of f . ( x , y ) ;
Hom ( ( a \times b ) , c ) <> {} ;
consider k1 such that p " < k1 and k1 < k and p . k1 < k ;
consider c , d such that dom f = c \ d and rng f c= c ;
[ x , y ] in dom g & [ y , k ] in dom g ;
set S1 = that is that x = : y = 0. S1 and z = y ;
l1 = m2 & l2 = i2 & l1 = j2 & l2 = i2 ;
x0 in dom u /\ ( ( 1 - B ) * ( 1 - B ) ) ;
reconsider p = x as Point of ( TOP-REAL 2 ) | K1 ;
I[01] = ( ( TOP-REAL 2 ) | B01 ) | B01 .= ( ( TOP-REAL 2 ) | B01 ) | B01 ;
f . p4 <= f . p1 & f . p2 <= f . p3 ;
( ( F . x ) `1 <= ( F . x ) `1 ;
( x `2 ) ^2 = ( ( Wq ) * ( x `1 ) ) ^2 ;
for n being Element of NAT holds P [ n ] ;
let J , K be non empty Subset of I ;
assume 1 <= i & i <= len <* a " *> ;
0 |-> a = <*> ( the carrier of K ) ;
X . i in 2 |^ A ( ) \ B . i ;
<* 0 *> in dom ( e --> [ 1 , 0 ] ) ;
then P [ a ] ;
reconsider s^ = s/. ( s , t ) as terminal of D * ;
( - i -' 1 ) <= len , - j ;
[#] S c= [#] T & [#] T c= [#] T ;
for V being strict RealUnitarySpace holds V in (0). V implies V is Subspace of V
assume k in dom mid ( f , i , j ) ;
let P be non empty Subset of TOP-REAL 2 , p , q be Point of TOP-REAL 2 ;
let A , B be Matrix of n1 , n2 , k be Nat ;
- a * b = a * b ;
for A being Subset of A9 holds A // A & A // B implies A // B
( id o2 ) in <* o2 , o2 *> & ( id o2 ) . ( x , o2 ) = o2 ;
then ||. x .|| = 0 & x = 0. X ;
let N1 , N2 be strict normal Subgroup of G , a be Element of G ;
j >= len upper_volume ( g , D1 ) & j <= len upper_volume ( g , D1 ) ;
b = Q . ( len Q - 1 ) + 1 ;
f2 * f1 /* s is divergent_to+infty & f2 * f1 /* s is divergent_to+infty ;
reconsider h = f * g as Function of [: N2 , H :] , G ;
assume that a <> 0 and Polynom ( a , b , c ) >= 0 ;
[ t , t ] in the InternalRel of A & [ t , t ] in the InternalRel of A ;
( v |-- E ) | n is Element of ( T | n ) | n ;
{} = the carrier of L1 + L2 & the carrier of L1 = { 0 } ;
Directed I is_closed_on Initialized s , P & Initialized s , P & Initialized s , P +* I is_halting_on Initialized s , P ;
Initialized p = Initialize ( p +* q ) .= p +* q ;
reconsider N2 = N1 as strict net of R1 , R2 ;
reconsider Y = Y as Element of <* Ids L , \subseteq \rangle ;
"/\" ( { p } , L ) <> p ;
consider j be Nat such that i2 = i1 + j and j in dom f ;
not [ s , 0 ] in the carrier of S2 & [ s , 0 ] in the carrier of S2 ;
m1 in ( B '&' C ) /\ D \ { {} } ;
n <= len ( ( P + Q ) | ( len P + 1 ) ) ;
( x1 - x2 ) `1 = ( x2 - x3 ) `1 ;
InputVertices S = { x1 , x2 } & InputVertices S = { x1 , x2 } ;
let x , y be Element of FT1 ( n ) ;
p = |[ p `1 , p `2 ]| ;
g * 1_ G = h " * g * h .= h " * g " * h " ;
let p , q be Element of PFuncs ( V , C ) ;
x0 in dom x1 /\ dom x2 & x1 in dom x2 /\ dom x2 ;
( R qua Function ) " = R " * ( R * ( R * ( R * ( R * S ) ) ) ) ;
n in Seg len ( f /^ ( len p -' 1 ) ) ;
for s be Real st s in R holds s <= s2 & s <= s2 ;
rng s c= dom ( f2 * f1 ) /\ dom f2 ;
synonym for for for for for for for for for X being Subset of for X being Subset of \rm Fin X holds X is non empty ;
1_ K * 1_ K = 1_ K * 1_ K .= 1_ K * 1_ K ;
set S = Segm ( A , P1 , Q1 ) , Q1 = Seg ( n + 1 ) ;
ex w st e = ( w - f ) * w & w in F ;
curry ( ( P+* ( k , X ) ) # x ) is convergent ;
cluster -> open for Subset of TT ;
len f1 = 1 .= len f3 + len f3 .= len f3 + len f3 ;
sqrt i * p < sqrt 2 * p / p ;
let x , y be Element of [: U0 , U0 :] ;
b1 , c1 // b1 , c1 & b1 , c1 // c1 , c2 ;
consider p being 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 ;
Reloc ( J , card I ) does not destroy a ;
Macro ( ( card I + 1 ) + 1 ) does not destroy c ;
set m1 = LifeSpan ( p3 , s3 ) , m2 = P +* I , P4 = P +* I , P4 = P +* I , P4 = P +* I , P4 = P +* I , P4 = Comput ( p3 , s3 , 1 ) , P4 = Comput
IC Comput ( P , s , k ) in dom Initialize ( p +* I ) ;
dom t = the carrier of SCM & dom t = the carrier of SCM R ;
( E-max L~ f ) .. f = 1 ;
let a , b be Element of V ( ) , C be Element of V ( ) ;
Cl ( union F ) c= Cl ( Int union F ) ;
the carrier of X1 union X2 misses ( A1 \/ A2 ) ;
assume not LIN a , f . a , g . a , f . b ;
consider i being Element of M such that i = d6 and d in M ;
then Y c= { x } or Y = { x } ;
M , v / ( y , x ) |= H1 / ( y , x ) ;
consider m be element such that m in Intersect ( F0 ) and x = Intersect ( F0 ) ;
reconsider A1 = support u1 as Subset of X ;
card ( A \/ B ) = k-1 + ( 2 * 1 ) ;
assume that a1 <> a3 and a2 <> a4 and a3 <> a4 and a4 <> a4 and a4 <> a4 and a4 <> a4 ;
cluster s \! \mathop { \rm \hbox { - } such that V is .| for string of S ;
LL2 /. ( n + 2 ) = LL2 . ( n + 1 ) ;
let P be compact non empty Subset of TOP-REAL 2 , p , q be Point of TOP-REAL 2 ;
assume that r-7 in LSeg ( p1 , p2 ) and rppppppc1 = LSeg ( p1 , p2 ) ;
let A be non empty compact Subset of TOP-REAL n , a , b be Real ;
assume [ k , m ] in Indices ( D1 * D2 ) ;
0 <= ( ( 1 / 2 ) to_power p ) . p ;
( F . N | E8 ) . x = +infty ;
attr X c= Y & Z c= V & X \ V c= Y \ Z ;
( y `2 ) * ( z `2 ) <> 0. I ;
1 + card ( X \/ Y ) <= card u + card ( X \/ Y ) ;
set g = z \circlearrowleft ( E-max L~ z ) , h = z /. ( len z + 1 ) ;
then k = 1 & p . k = <* x , y *> ;
cluster -> total for Element of C -NAT -defined Function of X , Y ;
reconsider B = A as non empty Subset of TOP-REAL n , P be Subset of TOP-REAL n ;
let a , b , c be Function of Y , BOOLEAN ;
L1 . i = ( i .--> g ) . i .= g . i ;
Plane ( x1 , x2 , x3 ) c= P & P c= Q ;
n <= indx ( D2 , D1 , j1 ) + 1 - 1 ;
( ( ( g2 ) . O ) `1 = - 1 ;
j + p .. f - len f <= len f - len f ;
set W = W-min C , S = TOP-REAL 2 , E = TOP-REAL 2 , N = TOP-REAL 2 , N = TOP-REAL 2 , S = TOP-REAL 2 , E = TOP-REAL 2 , W = TOP-REAL 2 , E = TOP-REAL 2 , N = TOP-REAL 2 , E = TOP-REAL
S1 . ( a , e ) = a + e .= a + e ;
1 in Seg width ( M * ( p * ( len p ) ) ) ;
dom ( i * Im f ) = dom Im f ;
Dz1 . x = W . ( a *' ( a , p ) ) ;
set Q = i2 ( g , f , h ) ;
cluster -> \mathclose for an sorted ManySortedSet of U1 ;
attr F = { A } means : Def6 : F is discrete ;
reconsider z9 = *> as Element of product G ;
rng f c= rng f1 \/ rng f2 & rng ( f ^ ) c= rng f1 \/ rng f2 ;
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 ) implies E , j |= H
reconsider n1 = n as Morphism of o1 , o2 ;
assume that P is idempotent and R is idempotent and P (*) R = R .: P ;
card ( B2 \/ { x } ) = k-1 + 1 ;
card ( x \ B1 ) /\ B1 = 0 ;
g + R in { s : g-r < s & s < g + r } ;
set q9 = ( q , <* s *> ) -q , q9 = ( q , <* s *> ) -q , q = ( q , <* s *> ) -q , s = ( q , <* s *> ) -q , s = ( q ,
for x being element st x in X holds x in rng f1 ;
h1 /. ( i + 1 ) = h1 . ( i + 1 ) ;
set mw = max ( B , min ( B , m ) ) ;
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 .= l ;
( E-max L~ f ) `2 <= ( q `2 ) / ( |. q .| - sn ) ;
attr R is condensed means : Def6 : R is condensed & R is condensed & R is condensed ;
attr 0 <= a & b <= 1 & a * b <= 1 ;
u in ( ( c /\ ( d /\ e ) ) /\ f ) /\ j ;
u in ( ( c /\ ( ( d /\ e ) /\ b ) /\ f ) /\ j ) /\ j ;
len C + - 2 >= 9 + - 3 ;
x , z , y is_collinear & x , y , z is_collinear implies x , y , z is_collinear
a |^ ( n1 + 1 ) = a |^ n1 * a |^ ( n1 + 1 ) ;
<* \underbrace ( 0 , \dots , 0 ) *> in Line ( x , a ) ;
set y9 = <* y , c *> ;
F2 /. 1 in rng Line ( D , 1 ) & F2 . len F2 = Line ( D , 1 ) ;
p . m Joins r /. m , r /. ( m + 1 ) , G ;
( p `2 ) ^2 = ( f /. i1 ) ^2 .= ( f /. i1 ) ^2 ;
W-min ( X \/ Y ) = W-bound ( X \/ Y ) .= W-bound ( X \/ Y ) ;
0 + ( p `2 ) ^2 <= 2 * r * ( p `2 ) + ( p `2 ) ^2 ;
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 \mathop { \rm Preal } ;
p \! \mathop { \rm \hbox { - } count ( X ) = 0 ;
len <* x *> < i + 1 & i + 1 <= len c + 1 ;
assume that I is non empty and { x } /\ { y } = { 0. I } ;
set ii = ( card I + 4 ) .--> goto 0 , goto 0 = goto 0 , goto 0 = goto 0 , goto 0 = goto 0 , goto 0 = goto 0 , goto 0 = goto 0 , goto 0 = goto 0 , goto 0 = goto 0 , goto 0 = goto
x in { x , y } & h . x = {} & h . y = {} ;
consider y being Element of F such that y in B and y <= x `2 ;
len S = len ( the charact of A1 ) .= len the charact of A1 .= len the charact of A2 ;
reconsider m = M , n = I , n = N as Element of X ;
A . ( j + 1 ) = B . j \/ A . j ;
set Nmin = : : G2 in : G2 `1 <= ( G * ( 1 , j ) `1 ) `1 ;
rng F c= the carrier of gr { a } & F is one-to-one ;
^ ( p2 , K ) . ( K , n ) is a every FinSequence ;
f . k , f . ( mod n ) are_congruent_mod rng f ;
h " P /\ [#] ( T | P ) = f " P " P /\ [#] ( T | P ) ;
g in dom f2 \ f2 " { 0 } & f2 " { 0 } c= dom f2 \ f2 " { 0 } ;
gX /\ dom f1 = g1 " ( ( g1 " ) * f1 ) .= g1 " ( ( g2 ) * f1 ) ;
consider n being element such that n in NAT and Z = G . n ;
set d1 = being element of being Function of REAL , REAL n , REAL n , r be Real ;
b `1 + sqrt ( 1 + ( - 1 ) ^2 ) < ( 1 + sqrt ( 1 + ( - 1 ) ^2 ) ;
reconsider f1 = f as VECTOR of the carrier of X , Y ;
attr i <> 0 implies i ^2 mod ( i + 1 ) = 1 ;
j2 in Seg len ( ( g2 . i2 ) * ( ( g2 . i2 ) * ( ( g2 . i2 ) * ( ( g2 . i2 ) * ( ( g2 . i2 ) * ( ( g2 . i2 ) * ( ( g2 . i2 ) * ( ( g2 ) i1 ) *
dom ( i --> ( x . i ) ) = dom ( i --> a ) .= a ;
cluster sec | ]. PI / 2 , PI / 2 .[ -> one-to-one ;
Ball ( u , e ) = Ball ( f . p , e ) ;
reconsider x1 = x0 as Function of S , T . I ;
reconsider R1 = x , R2 = y as Relation of L , L ;
consider a , b being Subset of A such that x = [ a , b ] ;
( <* 1 *> ^ p ) ^ <* n *> in R1 ;
S1 +* S2 +* S2 = S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2 +* S2
( ( ( ( exp_R * exp_R ) `| Z ) * ( ( exp_R * exp_R ) `| Z ) ) . x = exp_R . x / ( exp_R . x ) ^2 ) ;
cluster -> continuous for Function of C , REAL ;
set C7 = 1GateCircStr ( <* z , x *> , f3 ) , C7 = 1GateCircStr ( <* z , x *> , f3 ) , C7 = 1GateCircStr ( <* z , x *> , f3 ) , C7 = 1GateCircStr ( <* z , x *> , f3 ) , C7 = <* x , y *> , '&' )
E8 . e2 = ( E . e2 ) -T . ( e2 + 1 ) ;
( ( arctan * arctan ) `| Z ) . x = ( arctan * arccot ) . x .= ( ( arctan * arccot ) `| Z ) . x ;
sup A = ( cos * 3 ) . ( lower_bound A ) & lower_bound A = 0 ;
F . ( dom f , - g ) is Morphism of F . ( cod f , - g ) ;
reconsider p9 = q9 , q9 = q as Point of TOP-REAL 2 ;
g . W in [#] Y & [#] Y c= [#] Y ;
let C be compact non vertical non horizontal Subset of TOP-REAL 2 , D be non empty Subset of TOP-REAL 2 ;
LSeg ( f ^ g , j ) = LSeg ( f , j ) ;
rng s c= dom f /\ ]. x0 - r , x0 .[ & rng s c= dom f /\ ]. x0 , x0 + r .[ ;
assume x in { idseq ( 2 ) , Rev ( idseq ( 2 ) ) } ;
reconsider n2 = n , m2 = m - 1 as Element of NAT ;
for y being ExtReal st y in rng seq holds g . y <= y
for k st P [ k ] holds P [ k + 1 ] ;
m = m1 + m2 .= m1 + m2 .= m1 + m2 ;
assume for n holds H1 . n = G . n -H . n ;
set BY = f .: ( the carrier of X1 ) , BY = f .: the carrier of X2 ;
ex d being Element of L st d in D & x << d ;
assume R ~ c= R ~ & R ~ c= R ~ & R ~ c= R ~ ;
t in ]. r , s .[ or t = s or t = s ;
z + v2 in W & x = u + ( z + v2 ) ;
x2 |-- y2 iff P [ x2 , y2 ] & P [ x2 , y2 ] ;
attr x1 <> x2 means : Def6 : |. x1 - x2 .| > 0 & |. x1 - x2 .| > 0 ;
assume p2 - p1 , p3 - p1 , p2 - p3 is_collinear ;
set q = \cal f ^ <* 'not' 'not' A *> ;
let f be PartFunc of \langle REAL-NS 1 , REAL-NS 1 *> , REAL-NS 1 , REAL-NS 1 ;
( n mod ( 2 * k ) ) ! = n mod k ;
dom ( T * ( \rm succ t ) ) = dom ( T * ( x , t ) ) ;
consider x being element such that x in wX and x in c and y = c . x ;
assume ( F * G ) . v = v . x3 & ( F * G ) . x3 = v . x4 ;
assume that the carrier of D1 c= the carrier of D2 and for x being Element of D1 holds x in the carrier of D1 iff x in the carrier of D2 ;
reconsider A1 = [. a , b .[ as Subset of REAL n ;
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 ) , r = W-min L~ Cage ( C , n ) , s = Cage ( C , n ) , s = Gauge ( C , n ) , w = Gauge ( C , n ) , G = Gauge ( C , n )
n1 -' len f + 1 <= len f + ( len f -' 1 ) - 1 ;
|. |. |. q , O1 .| .| = [ u , v , a ] ;
set C-2 = ( \mathclose { ]| : G . ( k + 1 ) ) `1 = G * ( k , 1 ) `1 ;
Sum ( L * p ) = 0. R * Sum p .= 0. V ;
consider i being element such that i in dom p and t = p . i ;
defpred Q [ Nat ] means 0 = Q ( ) & $1 < 0 implies P [ $1 ] ;
set s3 = Comput ( P1 , s1 , k ) , s4 = P1 +* I , P4 = P1 +* I , P4 = P1 +* I , s4 = P3 +* I , P4 = P3 +* I , s4 = P3 +* I , P4 = P3 +* I , s4 = P3 ;
let l be variable of k , A , A be non empty Subset of k , x be element ;
reconsider U1 = union ( G . k ) as Subset-Family of ( T . k ) | ( T . k ) ;
consider r such that r > 0 and Ball ( p `1 , r ) c= Q ` ;
( h | ( n + 2 ) ) /. i = p9 /. ( n + 1 ) ;
reconsider B = the carrier of X1 , C = the carrier of X2 as Subset of X ;
pA1 = <* - 1 , - 1 , - 1 , - 1 , - 1 , - 1 , - 1 , - 1 , - 1 , - 1 , - 1 , - 1 , - 1 , - 1 , - 1 , - 1 , - 1 , - 1 , - 1 , - 1 , - 1 , -
synonym f is real-valued means : \overline rng f c= NAT & rng f c= NAT ;
consider b being element such that b in dom F and a = F . b ;
x12 < card ( X0 \/ Y2 ) & card ( Y2 \/ Y2 ) < card ( Y1 \/ Y2 ) ;
attr X c= B1 means : Def6 : for B st B in B1 holds X in succ B & X c= B1 ;
then w in Ball ( x , r ) & dist ( x , w ) <= r ;
angle ( x , y , z ) = angle ( x , 0 , z ) ;
attr 1 <= len s means : Let : for i st i in dom s holds ( the \mathopen { - } s . i } ) . i = s . i ;
fm c= f . ( k + ( n + 1 ) ) ;
the carrier of { 1_ G } = { 1_ G } & { 1_ G } c= { 1_ G } ;
attr p '&' q in TAUT ( Al ) means : Def6 : q '&' p in TAUT ( Al ) ;
- ( t `2 / t `1 ) < ( ( t `1 / t `1 ) / t `1 ;
U . 1 = U /. 1 .= ( U /. 1 ) `1 .= ( U /. 1 ) `1 ;
f .: ( the carrier of x ) = the carrier of x & f .: ( the carrier of x ) = the carrier of x ;
Indices ( ( n + 1 ) * ( p + q ) ) = [: Seg n , Seg n :] ;
for n being Element of NAT holds G . n c= G . ( n + 1 )
then V in M .: { x } ;
ex f being Element of F-9 st f is \cup ( A * ) & f is onto ;
[ h . 0 , h . 3 ] in the InternalRel of G ;
s +* Initialize ( ( intloc 0 ) .--> 1 ) = s3 +* ( ( intloc 0 ) .--> 1 ) ;
|[ w1 , v1 ]| - |[ w1 , w2 ]| <> 0. TOP-REAL 2 ;
reconsider t = t as Element of ( INT \ { 0 } ) -tuples_on ( ( INT \ { 0 } ) \ { 0 } ) ;
C \/ P c= [#] ( ( G \ A ) \ A ) & C /\ ( G \ A ) c= [#] ( ( G \ A ) \ A ) ;
f " V in ( ( ( X /\ Y ) /\ D ) . ( ( the carrier of X ) /\ D ) . ( the carrier of X ) ) ;
x in [#] ( ( A /\ B ) ` ) /\ ( ( A /\ B ) ` ) ;
g . x <= h1 . x & h . x <= h1 . x ;
InputVertices S = { xy , yz , zx , zx , zx , zx , zx , zx } ;
for n being Nat st P [ n ] holds P [ n + 1 ] ;
set R = ( Line ( M , i ) ) * Line ( M , i ) ;
assume that M1 is being_line and M2 is being_line and M1 is being_line and M2 is being_line and M1 <> M2 ;
reconsider a = f2 . ( i0 -' 1 ) as Element of K ( ) ;
len ( B2 ^ ( F ^ F2 ) ) = Sum ( ( Len F1 ) ^ ( F ^ F2 ) ) ;
len ( ( the R of n ) * ( i , j ) ) = n & i = j ;
dom max ( - ( f + g ) , - ( f + g ) ) = dom ( f + g ) ;
( the Sorts of seq ) . n = sup Y1 & ( the Sorts of seq ) . n = sup Y1 ;
dom ( p1 ^ p2 ) = dom ( f ^ p2 ) .= dom ( f ^ p2 ) .= dom ( f ^ p2 ) ;
M . [ 1 , y ] = 1 / ( 1 - y ) .= y * v .= y ;
assume that W is non trivial and W .vertices() c= the carrier of G2 and W .vertices() c= the carrier of G2 ;
C6 /. i1 = G1 * ( i1 , i2 ) .= G1 * ( i1 , i2 ) ;
CQ |- 'not' All ( x , p ) 'or' ( 'not' p ) ;
for b st b in rng g holds lower_bound rng fa <= b & b <= sup rng fa
- sqrt ( ( ( q `1 / |. q .| - sn ) / ( 1 + sn ) ) ^2 ) = 1 ;
( LSeg ( c , m ) \/ LSeg ( l , k ) ) c= R ;
consider p be element such that p in Ball ( x , r ) and p in L~ f and x = f /. p ;
Indices X = [: Seg n , Seg n :] & len X = n & width X = n ;
cluster s => ( q => p ) -> valid ;
Im ( ( Partial_Sums F ) . m ) 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 ( N-min L~ Cage ( C , n ) , NW-corner L~ Cage ( C , n ) ) /\ LSeg ( NW-corner L~ Cage ( C , n ) , NW-corner L~ Cage ( C , n ) ) ;
set R8 = R / ( 1 - R . x ) , R8 = R / ( 1 - R . x ) , R8 = R / ( 1 - R . x ) , R8 = R / ( 1 - R . x ) , R8 = R / ( 1 - R . x ) , R8
IncAddr ( I , k ) = AddTo ( da , db ) .= I . ( m + k ) ;
seq . m <= ( the Sorts of seq ) . ( ( seq ^\ k ) . n ) ;
a + b = ( a ` *' ) ` .= ( a ` ) ` .= a ` ;
id ( X /\ Y ) = id ( X /\ Y ) .= id ( X /\ Y ) ;
for x being element st x in dom h holds h . x = f . x ;
reconsider H = U1 \/ U2 as non empty Subset of U0 ;
u in ( ( ( c /\ ( ( d /\ e ) /\ b ) /\ f ) /\ j ) /\ m /\ j ) /\ m ;
consider y being element such that y in Y and P [ y , lower_bound B ] ;
consider A being finite Subset of R such that card A = card ( R * A ) and card A = card ( R * A ) ;
p2 in rng ( f |-- p1 ) \ rng <* p1 *> & rng <* p1 *> c= rng ( f |-- p1 ) \ rng <* p1 *> ;
len s1 - 1 > 0 & len s2 - 1 > 0 ;
( E-max L~ Cage ( C , n ) ) `2 = ( E-max L~ Cage ( C , n ) ) `2 ;
Ball ( e , r ) c= LeftComp Cage ( C , k + 1 ) ;
f . a1 ` = f . a1 ` .= ( f . a1 ) ` .= ( f . a1 ) ` ;
( seq ^\ k ) . n in ]. - r , x0 .[ & ( seq ^\ k ) . n in ]. x0 - r , x0 .[ ;
gg . x0 = g . ( x0 ) | G . x0 .= f . x0 ;
the InternalRel of S is transitive & the InternalRel of S is transitive ;
deffunc F ( Ordinal , Ordinal ) = phi . ( $2 , $2 ) ;
F . s1 . a1 = F . s2 . a1 .= ( s2 . a1 ) . a1 ;
x `2 = A . ( o . a ) .= Den ( o , A . a ) ;
Cl ( f " P1 ) c= f " ( ( f " P1 ) " P1 ) ;
FinMeetCl ( the topology of S ) c= the topology of T & the topology of S c= the topology of T ;
synonym o is " means : by by : by \mathclose : by 7 : Let the carrier of S <> {} & o <> {} & o <> {} ;
assume that X + Y = Y + 1 and card X <> card Y and card Y <> card X and card Y <> card X ;
the such that s <= 1 + ( the such that s <= 1 + ( the such that s = the card of s ) * ( ( the card s ) * ( the Arity of S ) ) ;
LIN a , a1 , d or b , c // b1 , c1 ;
e /. 1 = 0 & e /. 2 = 1 & e /. 3 = 0 ;
EI in SI & not E in { NI } ;
set J = ( l , u ) \mathop { I } ;
set A1 = \cal m ( ) , A2 = Following ( <* a1 , a2 *> , '&' ) , A2 = Following ( <* a1 , a2 *> , '&' ) , A1 = Following ( s , 2 ) , A2 = Following ( s , 2 ) , A2 = Following ( s , 2 ) , A1 = Following ( s , 2 ) ;
set vs = [ <* vs , A1 *> , and2a ] , xy = [ <* xy , yz *> , and2a ] , yz = [ <* yz , yz *> , and2a ] , zx = [ <* xy , yz *> , and2a ] , zx = [ <* xy , yz *> , and2a ] , zx = [ <* xy , yz *> , and2a ] , zx =
x * z `1 * x " in x * ( z * N ) " ;
for x being element st x in dom f holds f . x = g2 . x & f . x = g2 . x ;
Int cell ( f , 1 , G ) c= RightComp f \/ RightComp f \/ L~ f ;
U is an arc of W-min L~ Cage ( C , n ) , W-min L~ Cage ( C , n ) ;
set f-17 = f .: @ g "/\" @ @ f ;
attr S1 is convergent means : Def6 : S2 is convergent & S1 is convergent & for n st n >= m holds S1 . n <> 0. S ;
f . ( 0 + 1 ) = ( 0 qua Ordinal ) + a .= a ;
cluster -> \mathclose -> reflexive for reflexive transitive RelStr ;
consider d being element such that R reduces b , d and R reduces c , d and R reduces c , d ;
not b in dom Start-At ( ( card I + 2 ) , SCMPDS ) ;
( z + a ) + x = z + ( a + y ) .= z + a ;
len ( l | A ) = len l .= len l ;
t4 \/ {} is ( {} \/ rng t4 ) -valued FinSequence ;
t = <* F . t *> ^ ( C . p ) *> ^ q ;
set pp = W-min L~ Cage ( C , n ) , p = W-min L~ Cage ( C , n ) , q = W-min L~ Cage ( C , n ) , r = Cage ( C , n ) /. len p , s = Cage ( C , n ) /. len p , s = G * ( 1 , 1 ) , t = G *
( ( k -' 1 ) + 1 ) = ( k -' 1 ) + 1 .= ( k -' 1 ) + 1 ;
consider u being Element of L such that u = u ` and u in D and u in D and u in D ;
len ( width ( ( b |-> a ) |-> ( b * a ) ) ) = width ( ( b --> a ) ) ;
F3 . x in dom ( ( G * the_arity_of o ) . x ) ;
set H2 = the carrier of H2 , H1 = the carrier of H2 , H2 = the carrier of H2 ;
set H1 = the carrier of H1 , H2 = the carrier of H2 , H2 = the carrier of H2 ;
( Comput ( P , s , 6 ) ) . intpos m = s . intpos m .= s . intpos m ;
IC Comput ( P3 , t , k ) = ( l + 1 ) .= ( l + 1 ) ;
dom ( ( ( ( - 1 ) (#) ( ( #Z 2 ) * ( ( #Z 2 ) * ( ( #Z 2 ) * ( #Z 2 ) ) ) ) `| REAL ) = REAL ;
cluster <* l *> ^ phi -> ( 1 + 2 ) -element for string of S ;
set b5 = [ <* A1 , cin *> , and2a ] , x5 = [ <* cin , c *> , and2a ] , x5 = [ <* A1 , cin *> , '&' ] , x5 = [ <* A1 , cin *> , '&' ] , x5 = [ <* A1 , cin *> , '&' ] , x5 = [ <* cin , \cal *> , '&'
Line ( Segm M , P , Q ) = L * Sgm Q * Sgm Q ;
n in dom ( ( the Sorts of A ) * the_arity_of o ) ;
cluster f1 + f2 -> continuous for PartFunc of REAL , REAL n ;
consider y be Point of X such that a = y and ||. \mathclose { y } - g /. y .|| <= r ;
set x3 = Q . DataLoc ( s . a , i ) , x4 = Q . DataLoc ( s . a , i ) , P4 = Comput ( P , s , 2 ) , P4 = Comput ( P , s , 2 ) , P4 = Comput ( P , s , 2 ) , P4 = P . intpos ( i + 1
set pp = stop I , p1 = P +* I , p2 = P +* I , p1 = Comput ( p1 , s1 , 1 ) , p2 = P +* I , s4 = Comput ( p1 , s1 , 1 ) , P4 = p1 ;
consider a being Point of D2 such that a in W1 and b = g . a and a < b ;
{ A , B , C , D } = { A , B , C , D , E , F , J , M , N , M , N , N , M , N , N , M , N , N , F , M , N , N , M , N , N , M , N , N , M ,
let A , B , C , D , E , F , J , M , N , N , M , N , N , F , M , N , N , M , N , N , F , M , N , N , N , M , N , N , F , J , M , N , N , M ,
|. p2 .| ^2 - ( p2 `2 ) ^2 >= 0 ;
l -' 1 + 1 = n-1 * ( l + 1 ) + 1 ;
x = v + ( a * w1 + b * w2 ) + ( c * w2 ) ;
the TopStruct of L = TopSpaceMetr ( ( the Scott of L ) | the carrier of L ) ;
consider y being element such that y in dom H1 and x = H1 . y and y = H1 . y ;
fv \ { n } = ( Free ( { v } ) \/ { m } ) \/ { n } ;
for Y being Subset of X st Y is summable \ { x } holds Y is summable & Y is summable implies Y is summable
2 * n in { N : 2 * Sum ( p | N ) = N & N > 0 } ;
for s being FinSequence holds len ( Subset the Sorts of A ) = len s & len ( the Sorts of A ) = len s implies s = s
for x st x in Z holds exp_R . ( exp_R . x ) <> 0 & exp_R . x > 0
rng ( h2 * f2 ) c= the carrier of ( TOP-REAL 2 ) | K1 & rng ( g2 * f2 ) c= the carrier of ( TOP-REAL 2 ) | K1 ;
j + ( len f ) <= len f + ( len f - len f ) - len f ;
reconsider R1 = R * I as PartFunc of REAL , REAL-NS n , REAL-NS n ;
C8 . x = s1 . ( a . intloc 0 ) .= C8 . x .= C8 . x ;
power F_Complex . ( z , n ) = 1 / ( z |^ n ) .= x |^ n ;
t at ( C , s ) = f . ( the connectives of S ) . t ;
support ( f + g ) c= support f \/ ( C + D ) & support ( f + g ) c= support f \/ ( C + D ) ;
ex N st N = j1 & 2 * Sum ( ( r | N ) | N ) > N ;
for y , p st P [ p ] holds P [ All ( y , p ) ]
{ [ x1 , x2 ] } is Subset of [: X1 , X2 :] ;
h . i = j |-- ( h , id B ) . i .= H . i ;
ex x1 being Element of G st x1 = x & x1 * N c= A & x1 * N c= A ;
set X = ( ( ConsecutiveSet ( q , O1 ) ) . ( x , y ) ) `1 , Y = ( ( ConsecutiveSet ( q , O1 ) ) . ( x , y ) ) `2 ;
b . n in { g1 : x0 - r < g1 & g1 < x0 } ;
f /* s1 is convergent & f /. ( lim s1 ) = lim ( f /* s1 ) ;
the lattice of Y = the lattice of ( the carrier of Y ) & the carrier of ( the carrier of X ) = the carrier of Y ;
'not' ( a . x ) '&' b . x = FALSE ;
2 = ( len ( q ^ r1 ) ) + len ( q ^ r1 ) .= len ( q ^ r1 ) + len ( q ^ r1 ) ;
sqrt ( 1 - ( sec * f1 ) ^2 ) * ( ( sec * f1 ) ^2 ) is_differentiable_on Z ;
set K1 = upper ( lim ( f | A ) , H ) , D2 = lim ( f | A ) , D1 = dom ( f | A ) , D2 = dom ( f | A ) , D2 = dom ( f | A ) , D1 = dom ( f | A ) , D2 = dom ( f | A ) ;
assume e in { |[ w1 , w2 ]| : w1 in F & w2 in G & w1 in F & w2 in G & w1 <> w2 } ;
reconsider da = dom a `1 , db = dom F `1 , db = dom F `1 , db = dom F `1 , db = dom F `1 , db = dom F `1 , db = dom F , db = dom F , db = dom G , db = dom F , db = dom F , db = dom
LSeg ( f /^ j , j ) = LSeg ( f , j ) \/ LSeg ( q , j + 1 ) ;
assume X in { T . ( N2 , K1 ) : h . ( N2 , K1 ) = N2 } ;
assume that Hom ( d , c ) <> {} and <* f , g *> * f1 = <* f , g *> * f2 ;
dom S[. S , n .] = dom S /\ 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
a * ( ( n , 1 ) * n ) = a `2 - ( 0 * n ) * n .= a `2 ;
D2 . j in { r : lower_bound A <= D1 . i & D1 . i <= D2 . i } ;
ex p being Point of TOP-REAL 2 st p = x & P [ p ] & P [ p ] ;
for c holds f . c <= g . c implies f ^ @ c , g ^ @ c |= f ;
dom ( f1 (#) f2 ) /\ X c= dom ( f1 (#) f2 ) /\ X .= dom ( f1 (#) f2 ) /\ X .= dom ( f1 (#) f2 ) /\ X .= dom ( f1 (#) f2 ) /\ X ;
1 = ( p * p ) * ( p * q ) .= p * ( q * p ) .= p * ( q * p ) ;
len g = len f + len <* x *> .= len f + len <* y *> .= len f + 1 ;
dom F-11 = dom ( F | ( N1 \/ Si1 ) ) .= dom ( F | ( N1 \/ Si1 ) ) .= ( dom F ) /\ ( S1 \/ Si1 ) ;
dom ( f . t ) * I . t = dom ( f . t ) * ( g . t ) ;
assume a in ( "\/" ( ( T |^ the carrier of S ) , T |^ the carrier of S ) ) .: D ;
assume that g is one-to-one and ( the carrier' of S ) /\ rng g c= dom g and rng g c= dom g and rng g c= dom g ;
( ( x \ y ) \ z ) \ ( ( x \ y ) \ z ) = 0. X ;
consider f such that f * f = id b and f * f = id b and f * f = id b and f * f = id b ;
( ( ( ( - 1 ) (#) cos ) `| ]. 0 , PI / 2 .[ ) . ( x - x0 ) ) | ]. 0 , PI / 2 .[ is increasing ;
Index ( p , co ) <= len LS - LS .. LS + 1 .= len LS -' Index ( Gij , LS ) ;
t1 , t2 , t1 , t2 , t2 , t2 , t1 , t2 , t2 , t1 , t2 , t2 , t2 , t1 , t2 , t2 , t2 , t2 , t1 , t2 , t2 , t2 , t2 , t1 , t2 , t2 , t2 , t1 , t2 , t2 , t2 , t2 , t1 , t2 , t2 , t2 , t2 , t2 , t1 ,
( Frege ( Frege ( Frege ( Frege ( H ) ) ) ) . h <= ( Frege ( Frege ( G ) ) ) . h ;
then P [ f . i0 , f . i0 ] & F ( f . i0 , F . i0 ) < j ;
Q [ ( D . ( x , 1 ) ) `1 , F . ( D . ( x , 1 ) ) `2 ] ;
consider x being element such that x in dom ( F . s ) and y = F . s ;
l . i < r . i & [ l . i , r . i ] is ] of G . i ;
the Sorts of A2 = ( the Sorts of S2 ) * ( the Arity of S2 ) ;
consider s being Function such that s is one-to-one and dom s = NAT and rng s = F and rng s c= F ;
dist ( b1 , b2 ) <= dist ( b1 , a1 ) + dist ( a1 , a2 ) ;
( for n holds ( Cage ( C , n ) /. len Cage ( C , n ) ) /. ( len Cage ( C , n ) ) = W-min L~ Cage ( C , n ) ;
q `2 <= ( ( UMP L~ Cage ( C , n ) ) / 2 ) * ( ( E-max L~ Cage ( C , n ) ) / 2 ) `2 ;
LSeg ( f | i2 , i ) /\ LSeg ( f | i2 , j ) = {} ;
given a being ExtReal such that a <= I1 and A = ]. a , I1 .[ and B = ]. a , I1 .[ ;
consider a , b be complex number such that z = a & y = b and z + y = a + b ;
set X = { b } where b is Element of NAT : b in n & a < b } ;
( ( x * y ) \ z ) \ ( x * y ) = 0. X ;
set xy = [ <* xy , yz *> , and2a ] , yz = [ <* xy , yz *> , and2a ] , yz = [ <* yz , yz *> , and2a ] , zx = [ <* xy , yz *> , and2a ] , zx = [ <* xy , yz *> , and2a ] , zx = [ <* xy , yz *> , '&' ] , xy = [ <* xy , yz *>
lq /. len lq = lq . len ( l | k ) .= lq . ( len l + k ) ;
sqrt ( ( ( |. q .| ) ^2 - ( |. q .| ) ^2 ) = 1 ;
sqrt ( ( p `1 / |. p .| - sn ) / ( 1 + sn ) ) < 1 ;
( ( ( S \/ Y ) | ( S \/ T ) ) | ( S \/ T ) ) . x = ( ( S \/ Y ) | ( S \/ T ) ) . x ;
( s1 - s1 ) . k = s1 . ( k + 1 ) - s1 . ( k + 1 ) ;
rng ( ( h + c ) ^\ n ) c= dom SVF1 ( 1 , f , u0 ) ;
the carrier of X = the carrier of X & the carrier of X = the carrier of X & the carrier of X = the carrier of X ;
ex p3 st p3 = p4 & |. p3 - |[ a , b ]| .| = r & |. p3 - |[ a , d ]| .| = r ;
set ch = [: X , ( A \/ B ) :] , Ah = [: X , ( A \/ B ) :] ;
R |^ ( 0 * n ) = I\times ( X , X ) .= R |^ ( 0 * n ) .= R |^ ( 0 * n ) ;
( Partial_Sums ( ( curry F ) . n ) ) . x is nonnegative & ( Partial_Sums ( ( curry F ) . n ) ) . x is nonnegative ;
f2 = C7 . ( E7 , len ( V , len ( K , len ( K , len ( K , len ( K , len ( K , len ( K , len ( K , len ( K , len ( K , len ( K , len ( K , len ( K , len ( K ) ) ) ) ) ) ) ) ) ) ;
S1 . b = s1 . b .= S2 . b .= S2 . b .= S2 . b .= S2 . b ;
p2 in LSeg ( p2 , p1 ) /\ LSeg ( p1 , p2 ) \/ LSeg ( p1 , p2 ) /\ LSeg ( p1 , p2 ) ;
dom ( f . t ) = Seg n & dom ( I . t ) = Seg n & dom ( I . t ) = Seg n ;
assume o = ( the connectives of S ) . 11 & o <> ( the connectives of S ) . 12 ;
set phi = ( l1 , l2 ) , phi = ( X , l2 ) , phi = X , l = X , F = X . l , F = X . l , F = X . l , phi = X . l , phi = X . l , phi = X . l , phi = X . l , phi = X . l , phi = X . l , phi = X . l , phi =
synonym p is invertible means : where p , T st HT ( p , T ) = 1 & HT ( p , T ) = 0. L ;
( Y1 `2 ) ^2 = - 1 & ( Y1 `2 ) ^2 = ( Y1 `1 ) ^2 & ( Y1 `2 ) ^2 = ( Y1 `2 ) ^2 ;
defpred X [ Nat , set , set ] means P [ $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 , $2 , $2 , $2 , $2 , $2
consider k be Nat such that for n be Nat st k <= n holds s . n < x0 + g / 2 ;
Det I = ( m |^ ( ( m -' n ) -' n ) ) * ( m |^ ( m -' n ) ) .= 1_ K ;
sqrt ( - b ^2 ) < 0 & sqrt ( - 4 * a * c ) < 0 ;
CP . d = CP . ( d1 , d2 ) mod CP . ( d2 , d2 ) .= CP . ( d1 , d2 ) mod CP . ( d2 , d2 ) ;
attr X1 is dense means : Def6 : X1 is dense & X2 is dense & X1 /\ X2 is dense implies X1 /\ X2 is dense ;
deffunc F6 ( Element of E , Element of I ) = ( 2 * $1 ) * ( $2 , $2 ) ;
t ^ <* n *> in { t ^ <* i *> : Q [ i , T . t ] } ;
( x \ y ) \ x = ( x \ x ) \ y .= y ` \ x ` .= 0. X ;
for X being non empty set holds X is Basis of <* X , Y *> iff X is Basis of <* X , Y *>
synonym A , B are_separated for A \/ B for A \/ B ;
len ( ML * p ) = len p & width ( ML * p ) = width ( ML * p ) ;
as Element of K ( ) , v be Element of K ( ) , a , b be Element of K ( ) ;
( Sgm ( m ) ) . d - ( Sgm ( m ) ) . e <> 0 ;
lower_bound divset ( D2 , k + k2 ) = D2 . ( k + k2 + 1 ) - D2 . ( k + k2 + 1 ) ;
g . r1 = ( 2 * r1 + 1 ) * h . r1 & dom h = [. 0 , 1 .] ;
|. a .| * ||. f /. x .|| = 0 * ||. f /. x .|| .= ||. a * f /. x .|| ;
f . x = ( h . x ) `1 & g . x = ( h . x ) `2 ;
ex w st w in dom B1 & <* 1 *> ^ s = <* 1 *> ^ w ^ w ^ w ^ w ;
[ 1 , {} , <* d1 *> ] in ( { [ 0 , {} ] } \/ ( { 0 } \/ { 1 } ) \/ { 1 } ) ;
IC Exec ( i , s1 ) + n = IC Exec ( i , s2 ) + n .= IC Exec ( i , s2 ) + n ;
IC Comput ( P , s , 1 ) = succ IC s .= ( 0 + 1 ) .= ( 0 + 1 ) ;
( IExec ( W6 , Q , t ) ) . intpos ( m + 1 ) = t . intpos ( m + 1 ) ;
LSeg ( f /^ q , i ) misses LSeg ( f /^ q , j ) \/ LSeg ( f /^ q , j ) ;
assume for x , y being Element of L st x in C holds x <= y or x <= y or y <= x & y <= y ;
Integral ( C , f | X ) . x = f . ( upper_bound C ) - f . ( upper_bound C ) ;
for F , G being one-to-one st rng F misses rng G & rng F misses rng G holds F ^ G is one-to-one
||. R /. ( L . h ) - R /. ( L . h ) .|| < e1 * ( K + 1 ) ;
assume a in { q where q is Element of M : dist ( z , q ) < r } ;
set p4 = [ 2 , 1 ] .--> [ 2 , 1 ] ;
consider x , y being Subset of X such that [ x , y ] in F and x c= d and y c= d and x in d and y in d and x in d and y in d ;
for y , x being Element of REAL m st y in Y ` & x in X ` holds y ` <= x ` + y ` ;
func |. p .| -> \rbrack means : Def6 : for n being Nat holds it . n = min ( p . n , p . n ) ;
consider t being Element of S such that x `1 , y `1 '||' z `1 , t `2 and x `1 , y `2 '||' z `1 , t `2 ;
dom x1 = Seg len x1 & len x2 = len x1 & len x1 = len x2 & for i st i in Seg len x1 holds x1 . i = x2 . i * x1 . i ;
consider y2 being Real such that x2 = y2 and 0 <= y2 and y2 <= 1 and x2 <= 1 / 2 ;
||. f /* ( s1 /* s1 ) - f /. ( s1 /* s1 ) .|| = ||. f /. ( s1 + lim s1 ) - f /. ( s1 + lim s1 ) .|| ;
( the InternalRel of A ) ~ /\ Y = {} \/ ( the InternalRel of A ) ~ .= {} \/ ( the InternalRel of A ) ~ .= {} ;
assume that i in dom p and for j being Nat st j in dom q holds P [ i , j ] and for j being Nat st j in dom p holds P [ j , p . j ] ;
reconsider h = f | [: X , Y :] as Function of [: X , Y :] , [: Y , X :] ;
u1 in the carrier of W1 & u2 in the carrier of W2 implies u1 + u2 in the carrier of W1 & u2 + u2 in the carrier of W2
defpred P [ Element of L ] means M <= f . $1 & f . $1 <= f . $1 & f . $1 <= f . $1 ;
T . ( u , a , v ) = s * x + ( - ( s * x ) + y ) .= b * x + y ;
- ( - ( - 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__ 2 , T ;
fm = [ [ dom ( f ^ ) , cod ( f ^ ) ] , [ cod ( f ^ ) , cod ( g ^ ) ] ] , [ cod ( f ^ ) , cod ( g ^ ) ] ] ;
for k , n being Nat st k <> 0 & k < n & n < k holds ( k * n ) * ( k * n ) = ( k * n ) * ( k * n )
for x being element holds x in A |^ d iff x in ( A ` ) ` & x in ( ( A ` ) ` ) `
consider u , v being Element of R , a being Element of A such that l /. i = u * a * v ;
( - sqrt ( 1 - ( p `2 / |. p .| - sn ) / ( 1 - sn ) ) ^2 ) > 0 ;
L-13 . k = Lk . ( F . k ) & F . k in dom ( Lk | dom ( Lk | dom ( L | dom ( L | dom F ) ) ) ) ;
set i2 = AddTo ( a , i , - n ) , i1 = goto ( - n ) , i2 = goto ( - n ) , i2 = goto ( - n ) , i2 = goto ( - n ) , i2 = goto ( - n ) , i2 = goto ( - n ) , i2 = goto ( - n ) ;
attr B is number means : Def6 : for S being Nat holds holds holds -\mathop { S . ( S , x ) } = ( B . S ) `1 ;
a9 " D = { a "/\" d where d is Element of N : d in D & a in D & d in D } ;
|( \square , REAL . ( q9 - q ) , REAL . ( b - q ) )| >= |( \square , REAL . ( b - q ) )| ;
( - f ) . sup A = ( - f ) . sup A .= ( - f ) . sup A .= f . sup A ;
( G * ( len G , k ) ) `1 = ( G * ( len G , k ) ) `1 .= ( G * ( len G , k ) ) `1 ;
( Proj ( i , n ) . LL = <* ( proj ( i , n ) . LL ) . ( LL . ( LL . ( LL ) ) ) *> ;
f1 + f2 * reproj ( i , x ) is_differentiable_in ( ( reproj ( i , x ) ) . x0 + f2 * reproj ( i , x ) ) . x0 ;
attr IT is 0 & ( for x st x in Z holds tan . x = tan . x ) implies tan is differentiable ;
ex t being SortSymbol of S st t = s & h1 . t = h2 . t & h2 . t = h2 . t ;
defpred C [ Nat ] means ( ( P . $1 ) `1 is non empty & ( P . $1 ) `2 is } & ( ( P . $1 ) `1 is non empty & ( P . $1 ) `2 is non empty & ( P . $1 ) `1 is non empty ) ;
consider y being element such that y in dom ( p9 | i ) and q9 . i = ( p9 | i ) . y ;
reconsider L = product ( { x1 } --> ( index B ) ) as Basis of product A ;
for c being Element of C ex d being Element of D st T . ( id c ) = id d & T . ( id c ) = id d
& ( f | n , p ) = ( f | n ) ^ <* p *> .= f | n ^ <* p *> ;
( f * g ) . x = f . ( g . x ) & ( f * h ) . x = f . ( h . x ) ;
p in { 1 / 2 * ( G * ( i , j ) + G * ( i , j ) + G * ( i , j ) + G * ( i , j ) + G * ( i , j + 1 ) + G * ( i , j + 1 ) + G * ( i , j + 1 ) + G * ( i , j ) ) } ;
f `2 - p = ( f | ( n , L ) ) *' ( f | ( n , L ) ) .= f . ( ( n , L ) *' ) .= f . ( ( n , L ) *' ) ;
consider r be Real such that r in rng ( f | divset ( D , j ) ) and r < m + s ;
f1 . ( |[ ( ( ( ( ( r - r ) / 2 ) / 2 ) / 2 , ( ( r - r ) / 2 ) / 2 ]| ) `1 ) in f1 .: ( ( r - r ) / 2 ) ) ;
eval ( a | ( n , L ) , x ) = ( a | ( n , L ) ) . x .= a * ( x | ( n , L ) ) . x ;
z = DigA ( tw , x ) .= DigA ( tw , x ) .= DigA ( tw , x ) .= ( DigA ( tw , x ) ) . z ;
set H = { Intersect S where S is Subset-Family of X : S c= G & S c= G } ;
consider S19 being Element of D ( ) , d being Element of D ( ) such that S = S19 ^ <* d *> and S = S19 ^ <* d *> ;
assume that x1 in dom f and x2 in dom f and f . x1 = f . x2 and f . x2 = f . x2 and f . x1 = f . x2 ;
- 1 <= ( sqrt ( ( q `1 / |. q .| - sn ) / ( 1 + sn ) ) ^2 ) / ( 1 + sn ) ;
(0). V is Linear_Combination of A & Sum ( { 0. V } ) = 0. V implies for x being VECTOR of V holds x in A & x in A
let k1 , k2 , k2 , x4 , k2 , x4 , x5 , x6 , x6 , 7 , 8 , 8 , 8 , 7 , 8 , 8 , 8 , 8 , 8 , 7 , 8 , 8 , 7 , 8 , 7 , 8 , 8 , 8 , 7 be Element of NAT ;
consider j being element such that j in dom a and j in g " { k } and x = a . j ;
H1 . x1 c= H1 . x2 or H1 . x2 c= H1 . x2 & H1 . x1 c= H1 . x2 ;
consider a being Real such that p = a * p1 + ( a * p2 ) and 0 <= a and a <= 1 and a <= 1 ;
assume that a <= c and d <= b and [ a , b ] c= dom f and [ a , b ] in dom g and g . a = g . b ;
cell ( Gauge ( C , m ) , len Gauge ( C , m ) -' 1 , 0 ) is non empty ;
A-1 in { ( S . i ) `1 where i is Element of NAT : 1 <= i & i <= len ( S . i ) `1 } ;
( T * b1 ) . y = L * ( b2 `1 ) .= ( F `1 ) . y .= ( F `1 ) . y ;
g . ( s , I ) . x = s . y & g . ( s , I ) . y = |. s . x + s . y .| ;
( log ( 2 , k ) ) / ( 2 |^ ( k + 1 ) ) >= ( log ( 2 , ( k + 1 ) ) / ( 2 |^ ( k + 1 ) ) ) / ( 2 |^ ( k + 1 ) ) ) ;
then that p => q in S and not x in the carrier of S and not p => q in S and not p => q in S ;
dom ( the initial of r-10 ) misses dom ( the initial of r-10 ) & dom ( the initial of r-10 ) = dom ( the initial of r-10 ) ;
synonym f is extended real-valued means : Def6 : for x being set st x in rng f holds x is ExtReal ;
assume for a being Element of D holds f . { a } = a & f . ( f .: X ) = f . union X ;
i = len p1 .= len p1 + len <* x *> .= len p1 + len <* x *> .= len p1 + len <* x *> .= len p1 + len <* x *> ;
( l /. 1 ) `1 = ( g /. ( 1 + 1 ) ) `1 .= ( g /. ( 1 + 1 ) ) `1 .= ( g /. ( 1 + 1 ) ) `1 ;
CurInstr ( P2 , Comput ( P2 , s2 , l ) ) = halt SCM+FSA .= halt SCM+FSA ;
assume for n be Nat holds ||. ( seq . n ) - ( seq . n ) .|| <= R . ( ( seq . n ) - ( seq . n ) ) ) & ( for n be Nat holds ( seq . n ) - ( seq . n ) ) < R ;
sin . ( *> - cos . ( - PI * sin ) ) = sin . ( - PI * cos . ( - PI * sin . ( - PI * sin . ( - PI * cos . ( - PI * sin . ( - PI * cos . ( - PI * sin . ( - PI * sin . ( - PI * sin ) ) ) ) ) ) .= 0 ;
set q = |[ g1 `1 / ( t `2 ) , g2 `2 / ( t `1 ) / ( t `2 ) ]| , g1 = |[ g2 `1 / ( t `1 ) / ( t `2 ) , g2 `2 / ( t `2 ) / ( t `2 ) ]| ;
consider G being sequence of S such that for n being Element of NAT holds G . n in : G . n in : G . n = F ( F . n ) } ;
consider G such that F = G and ex G1 , G2 st G1 in SX & G2 in SX & G = ( X --> G2 ) . ( G . ( G . ( G . ( G . ( G , H ) ) ) ) ) ;
the root of [ x , s ] in ( the Sorts of Free ( C , X ) ) . s & ( the Sorts of Free ( C , X ) ) . s in ( the Sorts of Free ( C , X ) ) . s ;
Z c= dom ( exp_R * ( ( exp_R * f1 ) + ( exp_R * f2 ) ) `| Z ) ;
for k being Element of NAT holds ( r . k ) . x = ( ( Im f ) . k ) . x
assume that - 1 < n and ( q `2 / |. q .| - sn ) < 0 and ( |. q .| ) < 0 and ( |. q .| ) < 0 ;
assume that f is continuous one-to-one and a < b and c < d and f . a = g . c and f . b = d and f . c = g . d and f . d = g . c and f . c = d ;
consider r being Element of NAT such that sY. = Comput ( P1 , s1 , i ) and r <= q and r <= q ;
LE f /. ( i + 1 ) , L~ f , L~ f , L~ f , L~ f , L~ f , P , f /. ( i + 1 ) , L~ f ;
assume that x in the carrier of K and y in the carrier of K and inf { x , y } in the carrier of K and inf { x , y } in K ;
assume f /^ ( i1 , j2 ) in ( proj ( F , i2 ) ) " ( ( proj ( F , i2 ) ) " ( ( proj ( F , i1 ) ) " ) ) " ( ( proj ( F , i2 ) ) " ( ( proj ( F , i2 ) ) " ) ) ;
rng ( ( Flow M ) | ( the carrier of M ) ) c= the carrier' of M & rng ( ( Flow M ) | ( the carrier of M ) ) c= the carrier' of M ;
assume z in { ( the carrier of G ) \ { t } where t is Element of T : t in { s where s is Element of T : s in X } ;
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 NAT = ||. DD . t .|| and ||. t .|| <= 1 / 2 ;
assume that the carrier of v = 2 and v ^ <* 0 *> in dom p and v ^ <* 1 *> in dom p and v ^ <* 1 *> in dom p and v ^ <* 1 *> in dom p and v ^ <* 1 *> in dom p ;
consider a being Element of the Points of X , A such that a on the Points of X and not a on A and not b on A ;
( - x ) |^ ( k + 1 ) * ( ( - x ) |^ ( k + 1 ) ) " = 1 / ( ( - x ) |^ k ) ;
for D being set st for i st i in dom p holds p . i in D . i iff p . i in D . i
defpred R [ element ] means ex x , y st [ x , y ] = $1 & P [ x , y ] ;
L~ f2 = union { LSeg ( p1 , p2 ) where p1 , p2 is Point of TOP-REAL 2 : LSeg ( p1 , p2 ) /\ LSeg ( p1 , p2 ) = { LSeg ( p1 , p2 ) where p1 , p2 is Real : p1 `1 < s1 & p2 `1 < s2 } ;
i -' len h11 + 2 - 1 < i -' len h11 + 1 - 1 + 1 + 1 - 1 + 1 ;
for n being Element of NAT st n in dom F holds F . n = |. ( ( n -' 1 ) * ( n -' 1 ) ) .|
for r , s1 , s2 , s3 st r in [. s1 , s2 .] & s1 < s2 & s2 < s3 holds s1 <= s2 & s1 <= s2 & s2 <= s3
assume v in { G where G is Subset of T2 : G in ( B \/ C ) & G c= { z } & G c= { z } & z in { z } & G c= { z } & G c= { z } ;
let g be meets T be meets Function of A , ( X --> b ) , ( X --> b ) , ( X --> c ) , ( X --> d ) , X , b , c , d being Element of A , f , g being Function of A , ( X --> b ) , ( X --> d ) , ( X --> d ) , ( X --> d ) , ( X --> d ) --> c , ( X --> d ) --> c , (
min ( g . [ x , y ] , k ) = ( min ( g . [ y , z ] , k ) ) . y ;
consider q1 being sequence of CH such that for n holds P [ n , q1 . n ] ;
consider f being Function such that dom f = NAT and for n being Element of NAT holds f . n = F ( n ) ;
reconsider B-6 = B /\ B , id Z = O /\ Z , id O = O /\ O as Subset of B ;
consider j being Element of NAT such that x = the FinSequence of n and 1 <= j and j <= n and 1 <= n and n <= len f and 1 <= j and j <= n ;
consider x such that z = x and card ( x . O2 ) in card ( x . O2 ) and x in L1 . O and x in L2 . O ;
( C * _ ( k , n2 ) ) . 0 = C . ( ( C * _ ( k , n2 ) ) . 0 ) .= C . ( ( C * _ ( k , n2 ) ) . 0 ) ;
dom ( X --> rng f ) = X & dom ( X --> f ) = dom ( X --> f ) ;
( E-max L~ Cage ( C , n ) ) `2 <= ( ( E-max L~ Cage ( C , n ) ) `2 ;
synonym x , y means : Def6 : { x , y } = y or ex l being bag of S st { x , y } c= l ;
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 st a = x & b = y holds x << y iff x << y ;
sqrt ( 1 - ( ( ( - ( ( #Z n ) * ( #Z n ) ) ) * ( ( #Z n ) * ( #Z n ) ) ) ) is_differentiable_on REAL ;
defpred P [ Element of omega ] means ( the partial of A1 ) . $1 = A1 . ( $1 + 1 ) & ( the partial of A1 ) . $1 = A2 . ( $1 + 1 ) ;
IC Comput ( P , s , 2 ) = succ IC Comput ( P , s , 1 ) .= 6 + 1 .= 6 ;
f . x = f . ( g1 . ( g2 . x ) ) * f . ( g2 . x ) .= ( f . ( g1 . x ) ) * f . ( g2 . x ) .= ( f . ( g1 . x ) ) * f . ( g2 . x ) ;
( M * ( F-4 ) ) . n = M . ( ( ( ( ( -1 ) * ( ( ( canFS ) . n ) ) ) . n ) ) .= M . ( ( ( ( ( ( ( P ) . n ) ) ) . x ) ) . n ) ;
the carrier of L1 + L2 c= ( the carrier of L1 ) \/ ( the carrier of L2 ) & the carrier of L1 + L2 c= ( the carrier of L1 ) \/ ( the carrier of L2 ) ;
attr a , b , c , x , y , z is_collinear means : Def6 : a , b , c , x , y is_collinear & a , b , c , x is_collinear & a , c , y is_collinear & x , y , z is_collinear & x , y , z is_collinear ;
( the Sorts of s ) . n <= ( the Sorts of A ) . ( n + 1 ) * ( the Sorts of A ) . n ;
attr - 1 <= r & r <= 1 implies ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) (#) ( ( - 1 ) * ( ( - 1 ) * ( ( - 1 ) * ( ( - 1 ) * ( ( - 1 ) * ( ( - 1
sT in { p ^ <* n *> where n is Nat : p ^ <* n *> in T1 & p ^ <* n *> in T1 } ;
|[ x1 , x2 , x3 , x4 , x5 , x5 , x5 , x6 , x5 , x6 , x6 , x6 , x6 , x4 , x5 , x6 , x5 , x6 , x6 , x6 , x6 , x6 , x6 , x5 , product , W , W , N , b9 , 7 , 8 , 8 , 8 , 8 , 8 , 8 , 8 , 8 , 8 , 8 , 8 , 8 , 8 , 8 , 8 , 8 , 8 , 8 , 8 , 8 ,
attr for m being Nat holds F . m is nonnegative means : Def6 : ( Partial_Sums F ) . m is nonnegative & ( Partial_Sums F ) . m is nonnegative ;
len ( proj ( G , z ) ) = len ( ( reproj ( G , y ) ) . ( x , y ) ) + ( \overline ( G , y ) ) . ( y , z ) ;
consider u , v being VECTOR of V such that x = u + v and u in W1 /\ W2 and v in W2 /\ W3 ;
given F being FinSequence of NAT such that F = x and dom F = n and rng F = { 0 , 1 } and for k st k in n holds Sum F = k * ( F . k ) ;
0 = 1 * a2 & 1 = 1 * a2 * a3 + ( 1 - a2 ) * a3 ;
consider n be Nat such that for m be Nat st n <= m holds |. ( f # x ) . m - lim ( f # x ) .| < e / 2 ;
cluster non empty for Boolean \mathclose { \rm c } for ` ` ` ` ` ` ;
"/\" ( B , L ) = Top ( B , L ) .= "/\" ( [#] ( S , L ) , L ) .= "/\" ( [#] ( S , L ) , L ) .= "/\" ( [#] ( S , L ) , L ) ;
sqrt ( r ^2 + ( r ^2 ) / 2 ) + ( r ^2 + ( r ^2 ) / 2 ) <= sqrt ( r ^2 + ( r ^2 ) / 2 ) ;
for x being element st x in A /\ dom ( f `| X ) holds ( f `| X ) . x >= r2
2 * r1 - ( 2 * |[ a , c ]| - ( 2 * |[ b , c ]| - ( 2 * |[ b , c ]| ) ) = 0. TOP-REAL 2 ;
reconsider p = P /. ( \square , 1 ) = a " * ( ( ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( - ( K ) ) ) ) ) ) ) ) ) ) * ( ( ( ( - ( - ( K ) ) ) * ( ( - ( K ) ) * ( ( - ( K ) ) * ( ( K ) ) * ( ( K ) ) ) ) ) ) as FinSequence of K ;
consider x1 , x2 being element such that x1 in uparrow s and x2 in uparrow t and x = [ x1 , x2 ] and x = [ x1 , x2 ] ;
for n be Nat st 1 <= n & n <= len q1 holds q1 . n = ( upper_volume ( g , M1 ) ) . n
consider y , z being element such that y in the carrier of A and z in the carrier of A and i = [ y , z ] and i = [ y , z ] ;
given H1 , H2 being strict Subgroup of G such that x = H1 and y = H2 and for x , y being Element of G st x = H1 & y = H2 holds x * y = y * x ;
for S , T being non empty RelStr , d being Function of T , S st T is complete holds d is directed-sups-preserving & d is monotone & d is monotone & d is monotone
[ a + i , b ] in ( the carrier of F_Complex ) \ ( the carrier of V ) & [ a , b ] in ( the carrier of F_Complex ) \ ( the carrier of V ) ;
reconsider m1 = max ( len F1 , len ( F1 . n ) * ( p . n ) ) as Element of NAT ;
I <= width GoB ( GoB ( h , k ) , GoB ( h , k ) ) & I <= len GoB ( h , k ) ;
f2 /* q = ( f2 /* ( f1 /* s ) ) ^\ k .= ( f2 * f1 ) /* ( f2 /* s ) .= ( f2 * f1 ) /* s ;
attr A1 : for A , B , C being Subset of V st A \/ B is linearly-independent & A /\ B = { 0. V } holds Lin ( A /\ B ) = Lin ( A \/ B ) ;
func A -Ccarrier C -> set means : Def6 : union it = union { A . s where s is Element of R : s in A & s in C } ;
dom ( ( Line ( v , i + 1 ) ) (#) ( ( ( 1. ( K , m ) ) (#) ( 1. ( K , n ) ) ) ) = dom ( F ^ ) ) ;
cluster [ x `1 , x `2 ] -> real & [ x `1 , x `2 ] in [: x `1 , x `2 :] ;
E , All ( x , H ) |= All ( x , H ) => All ( x , H ) '&' All ( x , H ) ;
F .: ( ( id X ) . x , g ) = F . ( id X , g . x ) .= F . ( id X , g . x ) .= F . ( ( id X ) . x , g . x ) ;
R . ( h . m ) = F . x0 + h . ( m + 1 ) - h . x0 .= ( F . x0 + F . x0 ) + ( F . x0 ) ;
cell ( G , ( X1 -' 1 , Y1 ) , ( Y -' 1 ) \ L~ f ) \ L~ f meets UBD L~ f \/ ( L~ f ) ;
IC Comput ( P2 , s2 , LifeSpan ( P2 , s2 , LifeSpan ( P2 , s2 ) ) ) = IC Comput ( P2 , s2 , LifeSpan ( P2 , s2 , LifeSpan ( P2 , s2 ) ) ) .= ( card I + 1 ) + 1 .= ( card I + 1 ) + 1 ;
sqrt ( 1 - ( ( ( q `2 / |. q .| - sn ) / ( 1 + sn ) ) ^2 ) > 0 ;
consider x0 being element such that x0 in dom a and x0 in g " { k } and y = ( g " { x0 } ) . x0 and x0 = a . x0 ;
dom ( r1 * ( chi ( A , A ) . m ) ) = dom ( ( chi ( A , A ) . m ) * ( ( chi ( A , A ) . m ) ) ) .= dom ( ( ( A * ( B * ( A * ( B * ( B * C ) ) ) ) ) | ( ( A * ( B * ( B * C ) ) ) ) .= C ;
dZ . [ y , z ] = ( ( ( y - z ) / ( y - z ) ) / ( y - z ) ) / ( y - z ) ;
attr for i being Nat holds C . i = A . i /\ B . i & C . i = ( A . i ) /\ ( B . i ) ;
for x0 st x0 in dom f & f . x0 in dom f & f . x0 in dom f & for r st x0 in dom f holds ||. f /. x0 - f /. x0 .|| < r ) implies f | X is continuous
p in Cl A implies for K being Basis of p , Q being Subset of T st Q in K & A /\ Q c= Q holds A meets Q
for x being Element of REAL n st x in Line ( x1 , x2 ) holds |. y1 - y2 .| <= |. y1 - y2 .|
func Sum <* a *> -> Ordinal means : Def6 : a in it & for b being Ordinal st a in it holds it c= b ;
[ a1 , a2 , a3 ] in ( the carrier of A ) ~ & [ a1 , a2 , a3 ] in ( the carrier of A ) ~ ;
ex a , b being element st a in the carrier of S1 & b in the carrier of S2 & x = [ a , b ] ;
||. ( ( v . n ) - ( v . m ) ) * ( ( v . n ) - ( v . m ) ) * ( ( v . n ) + ( v . m ) ) * ( ( v . n ) - ( v . m ) ) ) * ( ( v . n ) - ( v . m ) ) ) < e / 2 ;
then for Z being set st Z in { Y where Y is Element of I1 : F c= Y & z in Z } holds z in Z ;
sup compactbelow ( [ s , t ] , sup { s } ) = [ sup { s } , sup { t } ] .= sup { s . ( ( sup { s } ) , t ) where t is Element of L : not contradiction } ;
consider i , j being Element of NAT such that i < j and [ y , f . i ] in [: I , J :] and [ y , f . j ] in [: I , J :] ;
for D being non empty set , p , q being FinSequence of D st p c= q & p ^ q = q holds p ^ q = q
consider e1 being Element of the carrier of X such that c , a // a9 , b9 and not a , c // a9 , b9 and not a , c // a9 , b9 and not a , c // a9 , b9 and not a , c // a9 , b9 and a , c // c9 , c9 ;
set U = I \! \mathop { \rm \hbox { - } ^ F } ;
|. q2 .| ^2 = ( ( |. q2 .| ) ^2 + ( |. q2 .| ) ^2 ) / ( |. q2 .| ) ^2 .= |. q2 .| ^2 / ( |. q2 .| ) ^2 ;
for T being non empty TopSpace , x , y being Element of [: the topology of T , the topology of T :] holds x "\/" y = x "\/" y & x "/\" y = x & x "/\" y = x
dom ( ( the charact of U1 ) * the charact of U2 ) = dom ( ( the charact of U1 ) * the charact of U2 ) & dom ( ( the charact of U1 ) * the charact of U2 ) = dom ( the charact of U1 ) ;
dom ( h | X ) = dom h /\ X .= dom ( ( ||. h .|| | X ) | X ) .= dom ( ( ||. h .|| | X ) | X ) .= dom ( ( h | X ) | X ) .= dom ( ( h | X ) | X ) .= dom ( ( h | X ) | X ) ;
for N1 , N1 being Element of [: G , H :] holds dom ( h . K ) = N . N1 & rng ( h . K ) = [: N , I :]
( mod ( u , m ) + mod ( v , m ) ) . i = ( mod ( u , m ) ) . i + ( mod ( v , m ) ) . i ;
- ( - 1 ) < ( - 1 ) / ( |. q .| - sn ) & ( - 1 ) / ( |. q .| - sn ) >= 0 ;
attr r1 = f & r2 = f & f = g implies for x , y st x in dom f & y in dom f & x <> y holds r1 * f . x = r2 * ( f . y ) ;
( for m be bounded Function of X , Y holds xK . m = ( seq_id ( vseq . m ) ) . x ) & ( x = ( seq_id ( vseq . m ) ) . x ) implies x = ( seq_id ( vseq . m ) ) . x
attr a <> b & b <> c & angle ( a , b , c ) = PI & angle ( b , c , d ) = PI ;
consider i , j being Nat , r being Real such that p1 = [ i , r ] and r < j and j < n and r < j and not f . ( i + 1 ) = f . ( j + 1 ) ;
|. p .| ^2 - ( 2 * ( p `2 ) ^2 + |. p `2 .| ^2 ) = |. p .| ^2 + |. p `2 .| ^2 ;
consider p1 , q1 being Element of [: X , Y :] such that y = p1 ^ q1 and q1 ^ q2 = p1 ^ q1 and p1 ^ q1 = q1 ^ q2 ;
L1 . ( ( r , r1 ) , ( r , r2 ) ) = ( ( r , ( r , r1 ) ) , ( r , r2 ) ) / ( ( r , r1 ) ) / ( ( r , r2 ) ) * ( ( r , r2 ) / ( ( r , r2 ) / ( r , r1 ) ) ) ;
( for w st w = lower_bound ( proj2 .: ( A /\ B ) ) holds proj2 .: ( A /\ B ) is non empty & proj2 .: ( A /\ B ) is non empty & proj2 .: ( A /\ B ) is non empty ;
s , ( ( H , 1 ) |= H1 iff s , ( H , 1 ) |= H2 ) implies s , ( H , 1 ) |= H2
len ( s + t ) + 1 = card ( support b1 ) + 1 .= card ( support b1 ) + card ( support b2 ) .= card ( support b1 ) + card ( support b1 ) .= card ( support b1 ) + card ( support b2 ) ;
consider z being Element of L1 such that z >= x and z >= y and for z being Element of L1 st z >= y holds z >= y ;
LSeg ( UMP D , ( ( ( TOP-REAL 2 ) / ( 2 |^ ( m + 1 ) ) / 2 ) ) /\ D ) = { UMP D , ( ( ( TOP-REAL 2 ) / ( m + 1 ) ) / 2 ) ) / 2 } ;
lim ( ( ( f `| N ) /* ( g `| N ) /* b ) ) = lim ( ( f `| N ) /* b ) .= lim ( ( f `| N ) /* b ) ;
P [ i , pr1 ( f , i ) . ( pr1 ( f , i ) . ( pr1 ( f , i ) . ( pr1 ( f , i ) . ( o + 1 ) ) ) ] ;
for r be Real st 0 < r ex m be Nat st for k be Nat st m <= k holds ||. ( seq . k ) - ( lim seq ) .|| < r
for X being set , P , Q being Subset of X , x , y being set st x in P & y in P & x in P & y in P & x in P & y in P & x in P & y in P & x in P & y in P & x in P & y in P & x in P & y in P & x in P & y in P & x in P & y in P & x in P & y in P & y in P & x in P & y in P & x in P & y in P & y in P & x in P & y
Z c= dom ( ( ( ( ( ( exp_R * f ) `| Z ) / ( exp_R * f ) ) `| Z ) \ ( ( exp_R * f ) `| Z ) " { 0 } ) ;
ex j being Nat st j in dom ( l ^ <* x *> ) & j < i & i < j & y = ( l ^ <* x *> ) . j & z = ( l ^ <* x *> ) . j ;
for u , v being VECTOR of V for r being Real st 0 < r & r < 1 holds r * u + ( r * v ) in N * N
A , Int A , Int ( A , B ) , Int ( A , C ) , Int ( A , D ) , Int ( A , B ) , Int ( A , C ) , Int ( A , D ) , A , B ) , A , C , D , E , F , J , M , N , N , M , N , N , f , J , M , N , f , M , N , N , f , J , M , M , N , N , N , f , J , M , N , N , N , N , f , M , N , N , N , N
- Sum <* v , u *> = - ( v + u ) .= - ( v + u ) .= - ( v + u ) .= - ( v + u ) ;
( Exec ( a := b , s ) ) . IC SCM = ( Exec ( a := b , s ) ) . IC SCM .= succ IC s .= succ IC s .= succ IC s ;
consider h being Function such that f . a = h and dom h = I and for x being element st x in I holds h . x = ( the Sorts of J ) . x ;
for S1 , S2 being non empty reflexive RelStr for D being non empty Subset of S1 , f being Function of S1 , S2 holds cos ( f , D ) is directed & cos ( f , D ) is directed
card X = 2 implies ex x , y st x in X & y in X & for z st z in X & z in X & x <> y holds z = x or z = y & z = x & z = y ;
E-max L~ Cage ( C , n ) in rng ( Cage ( C , n ) \circlearrowleft W-min L~ Cage ( C , n ) ) ;
for T , T , p , q being Element of dom T st p ^ q , T holds ( T , p , q ) . ( q , p ) = T . ( q , p )
[ i2 + 1 , j2 ] in Indices G & [ i2 + 1 , j2 ] in Indices G & f /. k = G * ( i2 , j2 ) & f /. k = G * ( i2 + 1 , j2 ) ;
cluster the _ of ( k , n ) -> commutative & ( for m being Nat st k divides m holds ( k divides m ) & ( k divides n implies ( k divides m ) implies ( k divides n ) implies ( k divides m ) implies ( k divides m ) & ( k divides m ) implies ( k divides m ) implies ( k divides m ) & ( k divides m ) implies ( k divides m ) implies ( k divides m ) implies ( k divides m ) implies ( k divides m ) implies ( k divides m ) implies ( k divides m ) implies ( k divides m ) implies ( k divides m ) implies ( k divides
dom F " = the carrier of X1 & rng F = the carrier of X2 & F " = the carrier of X2 & F " = the carrier of X1 & F " = the carrier of X2 ;
consider C be finite Subset of V such that C c= A and card C = m and the carrier of V = Lin ( B \/ C ) and the carrier of V = Lin ( B \/ C ) and A c= B ;
V is prime implies for X , Y being Subset of [: the carrier of T , the carrier of T :] st X /\ Y 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 , p4 ) .= angle ( p3 , p4 , p4 ) .= angle ( p3 , p4 , p4 ) ;
- sqrt ( 1 - ( ( q `1 / |. q .| - sn ) / ( 1 - sn ) ) ^2 ) = - ( - ( q `1 / |. q .| - sn ) / ( 1 - sn ) ) ^2 ) .= - ( q `1 / |. q .| - sn ) / ( 1 - sn ) ;
ex f being Function of I[01] , TOP-REAL 2 st f is continuous one-to-one & rng f = P & f . 0 = p1 & f . 1 = p2 & f . 1 = p4 & f . 0 = p4 & f . 1 = p3 ;
attr f is partial means : Def6 : for u , v st u in dom f & v in dom f holds SVF1 ( 2 , f , u ) . ( u - v ) = ( SVF1 ( 2 , f , u0 ) ) . ( u - v ) ;
ex r , s st x = |[ r , s ]| & G * ( len G , 1 ) `2 < s & s < G * ( 1 , 1 ) `2 & s < G * ( 1 , 1 ) `2 ;
assume that f is FinSequence which and 1 <= len G and t <= width G and G * ( t , width G ) `2 >= N-bound L~ f and G * ( t , width G ) `2 >= N-bound L~ f ;
attr i in dom G means : Def6 : r * ( reproj ( i , x ) ) . x = r * reproj ( i , x ) . x ;
consider c1 , c2 being bag of o1 + o2 such that ( ( decomp c ) /. k = <* c1 , c2 *> and c = c1 + c2 and c = c2 + c2 and c1 = c2 + c2 ;
u in { |[ r1 , s1 ]| : r1 < G * ( 1 , 1 ) `1 & s1 < G * ( 1 , 1 ) `2 & s1 < G * ( 1 , 1 ) `2 & s1 < G * ( 1 , 1 ) `2 } ;
Cl ( X ^ Y ) = the carrier of X . ( k2 + 1 ) .= C4 . ( C . ( k2 + 1 ) ) .= C4 . ( C . ( k2 + 1 ) ) .= C4 . ( C . ( k2 + 1 ) ) ;
attr M1 = len M2 means : Def6 : 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 ;
consider g2 be Real such that 0 < g2 and for y be Point of S st ||. y - x0 .|| < g2 & ||. y - x0 .|| < g2 holds g2 . ( y - x0 ) < g2 . ( y - x0 ) ;
assume x < ( - b + sqrt ( a , b ) ) / 2 * ( 2 * a ) or x > - b ;
( G1 '&' G2 ) . i = ( <* 3 *> ^ G1 ) . i & ( G1 '&' G2 ) . i = ( <* 3 *> ^ G1 ) . i & ( G1 '&' G2 ) . i = ( <* 3 *> ^ G1 ) . i ;
for i , j st [ i , j ] in Indices M1 holds ( M2 + M1 ) * ( i , j ) < M2 * ( i , j )
for f being FinSequence of NAT , i being Element of NAT st i in dom f & i in dom f holds i divides Sum f & i divides Sum f implies i divides Sum f
assume F = { [ a , b ] where a , b is Subset of X : for c st c in B holds a c= c & b c= c & c c= d & a c= b & b c= c & c c= d & d c= c & b c= d ;
b2 * q2 + ( b3 * q2 + b3 * q2 ) = 0. TOP-REAL n + ( - ( a1 * q2 ) * q2 ) .= ( 0. TOP-REAL n + ( p1 * q2 ) * q2 .= ( 0. TOP-REAL n ) * q2 ;
Cl ( F .: D ) = { D where D is Subset of T : ex B being Subset of T st D = Cl B & B in F & D in F & B c= D & B c= D & C c= D & B c= D & C in D & B in D & C in D & D in D & C in D ;
attr IT is summable means : Def6 : for s st s is summable holds ( for n st n >= 1 holds ( s + 1 ) * ( s . n ) = Sum ( s ) * ( s . n ) ;
dom ( ( cn " ) | D ) = ( the carrier of ( TOP-REAL 2 ) | D ) /\ D .= ( the carrier of ( TOP-REAL 2 ) | D ) /\ ( the carrier of ( TOP-REAL 2 ) | D ) .= the carrier of ( ( TOP-REAL 2 ) | D ) | D ;
[ X \to Z ] is full full non empty full SubRelStr of ( Omega Z ) |^ the carrier of X , the carrier of Y |^ the carrier of Y ] is full full SubRelStr of ( Omega Z ) |^ the carrier of X ;
( G * ( 1 , j ) ) `2 = ( G * ( 1 , j ) ) `2 & ( G * ( 1 , j ) ) `2 = ( G * ( 1 , j ) ) `2 ;
synonym m1 c= m2 means : Def6 : for p , q being ( the carrier of L ) st p in P & q in the carrier of L holds the InternalRel of p <= ( the InternalRel of L ) | ( m , n ) ;
consider a being Element of B ( ) such that x = F ( a ) and a in { G ( b ) where b is Element of B ( ) : P [ b ] } and P [ a ] ;
func multiplicative Let L -> RelStr means : where s being multiplicative means : Let : the carrier of it = [ the carrier of it , the carrier of it #) = { [ the carrier of L , the carrier of L ] where s is Element of L : s in the carrier of it & it = [ s , the carrier of L ] } ;
( the carrier of not a , b , c ) + ( the carrier of not c , d ) = b + ( the carrier of C ) + ( the carrier of D ) .= the carrier of D + ( the carrier of C ) .= the carrier of D ;
cluster strict for non empty RelStr means : Let : for i , j being Element of NAT holds it . ( i , j ) = ( i , j ) * ( i , j ) ;
( ( 2 * p1 ) + ( 2 * p2 ) ) * ( ( 2 * p1 ) + ( 2 * p2 ) ) = ( ( 2 * p1 ) + ( 2 * p2 ) ) * ( ( 2 * p2 ) + ( 2 * p1 ) * ( ( 2 * p2 ) + ( 2 * p2 ) ) * ( ( 2 * p1 ) + ( 2 * p2 ) * ( ( 2 * p2 ) + ( 2 * p2 ) ) * ( ( 2 * p1 ) ) ;
eval ( ( a | ( n , L ) ) *' p , x ) = eval ( a | ( n , L ) ) * eval ( p , x ) .= a * eval ( p , x ) .= a * eval ( p , x ) ;
assume that the TopStruct of S = the TopStruct of T and for V being Subset of S , V being Subset of T st V in V & V in the topology of S holds V meets V and for V being Subset of T st V in V holds V /\ V is open & V is open & V is open & V is open & V is open & V is open & p in V ;
assume that 1 <= k and k <= len w + 1 and T . ( ( ( k + 1 ) + 1 ) , w . ( k + 1 ) ) = ( ( T . ( k + 1 ) , w . ( k + 1 ) ) , w . ( k + 1 ) ) ) `2 ;
2 * ( a |^ ( n + 1 ) ) + ( 2 * ( b |^ ( n + 1 ) ) >= ( a |^ ( n + 1 ) ) + ( b |^ ( n + 1 ) ) ;
M , v / ( x. 3 , m ) / ( x. 4 , m ) / ( x. 4 , m ) / ( x. 4 , m ) / ( x. 0 , m ) / ( x. 4 , m ) / ( x. 0 , m ) / ( x. 4 , m ) / ( x. 0 , m ) / ( x. 4 , m ) ) |= M ;
assume that f is_differentiable_on l and for x0 st x0 in l holds 0 < f . x0 & for x0 st x0 < x0 holds f . x0 < f . x0 & f . x0 < 0 ;
for G1 , G2 being _Graph , W being Walk of G1 , e being set st e in W \overline ( the carrier of G2 ) holds W is Walk of G2 iff W is Walk of G2
not c01 is not empty iff empty is not empty & empty is not empty & empty is not empty & empty is not empty & empty is not empty & empty is not empty & empty is not empty & empty is not empty & not empty is not empty & empty is not empty & empty is not empty & not empty is not empty & not empty is not empty & not empty is not empty & not empty is not empty & not empty is not empty & not empty & not empty is not empty & not empty is not empty & not empty & not empty is not empty & not empty is not empty & not empty & not empty & not empty is not empty & not empty is not empty & not empty is not empty & not empty is not empty & not empty & not empty is not empty
Indices GoB f = [: dom GoB f , Seg width GoB f :] & 1 + 1 in dom GoB f & 1 <= len GoB f & 1 <= len GoB f & 1 <= len GoB f & 1 <= len GoB f & 1 <= len GoB f & 1 <= len GoB f & 1 <= len GoB f & 1 <= len GoB f & 1 <= len GoB f & 1 <= len GoB f & 1 <= len GoB f & 1 <= j & j + 1 <= len GoB f & j + 1 <= len GoB f & j + 1 <= len GoB f & j + 1 <= len GoB f & j + 1 <= len GoB f & j + 1 <= len GoB f & j + 1 <= len GoB f & j + 1 <= len GoB f & j + 1 <=
for G1 , G2 , G2 , G1 , G2 being stable Subgroup of O st G1 is stable & G2 is stable holds G1 is stable & G2 is stable & G2 is stable & G2 is stable & G1 is stable & G2 is stable & G2 is stable & G2 is stable & G2 is stable & G2 is stable & G2 is stable
UsedIntLoc ( ( int ) . intloc 0 , f ) = { intloc 0 , intloc 0 , intloc 0 , 1 , 1 , 1 , 1 , 2 , 3 , 4 , 5 , 5 , 6 , 7 , 8 , 8 , 8 , 7 , 8 , 8 , 7 , 8 , 8 , 7 , 8 , 8 , 7 , 8 , 8 , 7 , 8 , 8 , 8 , 7 , 8 , 8 , 8 , 8 , 7 , 8 , 8 , 7 , 8 , 8 , 8 , 8 , 8 , 8 , 7 , 8 , 8 , 8 , 7 , 8 , 8 , 8 , 8 , 8 , 8 , 8 , 7 , 7 , 7 , 8 , 8 , 8 , 7 , 8 , 8 , 7
for f1 , f2 being FinSequence of F st f1 ^ f2 is p -element & Q [ f1 ^ f2 ] holds Q [ f1 ^ f2 ]
sqrt ( ( p `1 ) ^2 + ( p `2 ) ^2 ) = sqrt ( ( q `1 ) ^2 + ( q `2 ) ^2 ) .= sqrt ( ( q `1 ) ^2 + ( q `2 ) ^2 ) ;
for x1 , x2 , x3 , x4 , x5 , x5 , x6 , x6 , x6 , x5 , x6 , x6 , x6 , x4 , x5 , x6 , x6 , x6 , x6 , x6 , x6 , x6 , x6 , x6 , x1 , x2 , x3 , x4 , x4 , x4 , x5 , x5 , x2 , x3 , x4 , x4 , x5 , x5 , x5 , x1 , x2 , x3 , x4 , x4 , x5 , x5 , x1 , x2 , x2 , x3 , x4 , x4 , x5 , x2 , x3 , x4 , x4 , x4 , x5 , x2 , x4 , x4 , x5 , x5 , x2 , x4 , x4 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x4 , x5 , x4 , x5
for x st x in dom ( ( - F ) | A ) holds ( ( - F ) | A ) . x = - ( ( - F ) | A ) . x )
for T being non empty TopSpace , P being Subset of T , B being Basis of T , x being Point of T st P c= the topology of T holds P is Basis of x
( a 'imp' b ) . x = 'not' ( ( a 'or' b ) . x ) 'or' c . x .= TRUE 'or' TRUE .= TRUE ;
for e being set st e in AZ ex X1 , X2 being Subset of Y st e = X1 & X1 = Y1 & X2 = Y2 & X1 is open & X2 is open & Y1 is open & Y2 is open & Y2 is open & Y1 is open & Y2 is open & Y2 is open & Y1 is open & Y2 is open & Y2 is open & Y2 is open & Y2 is open & Y2 is open
for i be set st i in the carrier of S for f being Function of [: S1 , S2 :] , the carrier of S2 st f = H . i holds F . i = f | ( F . i )
for v , w st for x st x <> y holds J . ( v . x ) = J . ( ( VERUM ( Al , J ) ) . v ) holds Valid ( All ( x , J ) , J ) . v = Valid ( VERUM ( Al , J ) , J ) . v
card D = card D1 + card D2 - card D1 + card D1 .= ( i + 1 ) - card D1 + 1 - 1 .= 2 * ( i + 1 ) - 1 .= 2 * ( i + 1 ) - 1 .= 2 * ( i + 1 ) - 1 .= 2 * ( i + 1 ) - 2 * ( i + 1 ) ;
IC Exec ( i , s ) = ( s +* ( 0 .--> 1 ) ) . 0 .= ( s +* ( 0 .--> 1 ) ) . 0 .= succ IC s .= succ IC s .= succ IC s ;
len f /. ( i1 -' 1 ) = len f -' ( i1 -' 1 ) + 1 .= len f -' ( i1 -' 1 ) + 1 .= len f -' ( i1 -' 1 ) + 1 .= len f -' ( i1 -' 1 ) + 1 .= len f -' ( i1 -' 1 ) ;
for a , b , c being Element of NAT st 1 <= a & a < b & b < d holds a < b + c or a = b + c
for f being FinSequence of TOP-REAL 2 , p being Point of TOP-REAL 2 st p in LSeg ( f , i ) & p in LSeg ( f , p ) holds Index ( p , f /. i , f /. ( p .. f ) ) = i + 1
lim ( ( curry ( P , ( k + 1 ) ) # x ) ) = lim ( ( curry ( P , ( k + 1 ) ) # x ) ) + lim ( ( curry ( P , ( k + 1 ) ) # x ) ) ;
z2 = g /. ( i -' n1 + 1 ) .= g /. ( i -' n1 + 1 ) .= g /. ( i -' n1 + 1 ) .= g /. ( i -' n1 + 1 ) .= g /. ( i -' n1 + 1 ) .= g /. ( i -' n1 + 1 ) ;
[ f . 0 , f . 3 ] in id ( the carrier of G ) or [ f . 0 , f . 3 ] in id the carrier of G & [ f . 0 , f . 3 ] in the InternalRel of G ;
for G being Subset-Family of B st G = { R [ X ] where X is Subset of A ( ) : R [ X ] } holds ( for X being Subset of A ( ) st X in F ( ) holds X in G ( ) ) & ( for x being Element of A ( ) holds X [ x , x ] implies x in F ( x ) )
CurInstr ( P1 , Comput ( P1 , s1 , m ) ) = CurInstr ( P1 , Comput ( P1 , s1 , m ) ) .= halt SCMPDS .= CurInstr ( P1 , Comput ( P1 , s1 , m ) ) .= halt SCMPDS ;
assume that a on M and b on M and c on N and d on N and p on M and p on M and d on M and p on M and c on N and p on M and d on N and p on M and d on N and p on M and p on N and d on N and p on M and d on N and p on N and d on N and p on N and d on N and d in N and p in N and d in N and p in M and d in N and d in N and d in N and p in N and d in N and d in N and p in N and p in N and p in N and p in M and d in N and d in N and d in N and p in N and d in N and p in M and d in N and p in N and d in N and p in N and d in M
for T be \hbox { T _ 4 } , F being Subset-Family of T ex B being Subset-Family of T st F is closed & B is finite-ind & F is finite-ind & ( for n being Nat holds F . n = 0 ) & ( for n being Nat holds F . n = 0 ) & ( for n being Nat holds F . n = 0 ) implies F is finite-ind & for n being Nat st n in dom F holds F . n is finite-ind ) implies F is finite-ind
for g1 , g2 st g1 in ]. x0 - r , x0 .[ & g2 in ]. x0 - r , x0 .[ holds |. ( f . g1 ) - ( f . g2 ) .| <= ( ( f1 . x0 ) - ( f2 . x0 ) ) / ( ( f . x0 ) - ( f . x0 ) )
/ ( ( Re z ) / ( |. z .| + |. z .| ) * ( |. z .| ) = ( Re z ) / ( |. z .| + |. z .| ) * ( |. z .| + |. z .| ) / ( |. z .| + |. z .| ) * ( |. z .| + |. z .| ) ;
F . i = F /. i + ( 0 + 1 ) .= <* b *> /. ( n + 1 ) .= <* b *> /. ( n + 1 ) .= b /. ( n + 1 ) .= b /. ( n + 1 ) ;
ex y being set , f being Function st y = f . n & dom f = NAT & for n being Nat holds f . n = R ( n , f . n ) & f . n = F ( n , f . n ) ;
func f (#) F -> FinSequence of V means : Def6 : len it = len F & for i being Nat st i in dom F holds it . i = F . i * f . ( F . i ) ;
{ x1 , x2 , x3 , x4 , x5 , x5 , x6 , x6 , x6 , x5 , x6 , x6 , x6 , x5 , x6 , x6 , x5 , x6 , x6 , x5 , x6 , x6 , x6 , x5 , x6 , x5 , x6 , x5 , x5 , x5 , x5 , x5 , x6 , x5 , x5 , x5 , x5 , x6 , x5 , x5 , x5 , x6 , x5 , x6 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x6 , x5 , x5 , x5 , x5 , x5 , x6 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x5 , x6 , x5 , x5 , x6 , x6 , x6 , x6 , x6 , x6 , x6 , x5 , x5 , x5 , x6 , x5 , x5 , x6 , x9
for n being Nat for x being set st x = h . n holds 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 ( Al ( ) ) ) . ( S1 , e ) = S1 & ( ( S ( ) . ( S1 , e ) ) . ( S1 , e ) ) = S1 . ( S1 , e ) ;
consider P being FinSequence of G such that p9 = Product P and for i being Element of NAT st i in dom P ex t1 , t2 being Element of G st P . i = t1 * t2 & P . i = t2 * t1 & P . i = t2 * t1 ;
for T1 , T2 being strict non empty TopSpace , P being Subset of T1 , T being Basis of T2 , f being Function of T1 , T2 st the carrier of T1 = the carrier of T2 & f .: P = the carrier of T2 holds f .: P = the topology of T2
assume that f is_partial differentiable on u0 and r (#) pdiff1 ( f , 3 ) is_differentiable_in u0 and SVF1 ( r (#) f , u0 ) . u = r * pdiff1 ( f , 3 ) . u and SVF1 ( r (#) f , u0 ) . u = r * SVF1 ( 1 , f , u0 ) . u ;
defpred P [ Nat ] means for F , G being FinSequence of REAL st len F = $1 & rng F = rng G & G = F * s holds Sum ( F , G ) = Sum ( F , G ) * Sum ( G , G ) ;
ex j st 1 <= j & j < width GoB f & ( GoB f ) * ( 1 , j ) `2 <= s & s * ( 1 , j ) `2 <= ( GoB f ) * ( 1 , j + 1 ) `2 ;
defpred U [ set , set ] means ex F\times Y st $2 = F\times Y & ( for n being Nat holds F\times Y , F\times Y , F\times Y st n = F . n ) & ( for n being Nat holds F\times Y , F\times Y :] is open & ( for n being Nat holds F\times Y , F\times Y is open ) ;
for p4 being Point of TOP-REAL 2 st LE p4 , p2 , P , p1 , p2 & LE p4 , p2 , P , p1 , p2 holds LE p4 , p2 , P , p1 , p2
f in St ( E , H ) & for y st y <> f . y holds x in rng ( the Sorts of U1 ) implies f . y = y & f . x = y
ex p2 being Point of TOP-REAL 2 st x = p2 & |. p2 .| >= sn & |. p2 .| >= sn & |. p2 .| >= sn & |. p2 .| >= sn & p2 <> 0. TOP-REAL 2 & |. p2 .| >= sn & p2 <> 0. TOP-REAL 2 & p2 <> 0. TOP-REAL 2 & p2 <> 0. TOP-REAL 2 & p2 <> 0. TOP-REAL 2 & p2 <> 0. TOP-REAL 2 & p2 <> 0. TOP-REAL 2 ;
assume for d1 being Element of NAT st d1 <= ( n implies ( n <= ( n + 1 ) implies s . ( n + 1 ) = ( n + 1 ) * ( n + 1 ) ) & ( n + 1 ) <= ( n + 1 ) * ( n + 1 ) ;
assume that s <> t and s is Point of Sphere ( x , r ) and not ex e being Point of Ball ( x , r ) st e = Ball ( x , r ) /\ Ball ( y , r ) & not e in Ball ( x , r ) ;
given r such that 0 < r and for s st 0 < s ex x1 , x2 be Point of C st ||. x1 - x2 .|| < s & ||. x1 - x2 .|| < s & ||. x1 - x2 .|| < s & ||. x1 - x2 .|| < s ;
( p | x ) | ( ( x | x ) | ( x | x ) ) = ( ( ( x | x ) | ( x | x ) ) | ( x | x ) ) | ( x | x ) ;
for x , h st x + h in dom sec holds ( AffineMap ( 2 * PI , x ) ) . ( x + h ) = ( 4 * PI * ( x + h ) ) / ( 2 * PI * ( x + h ) )
assume that i in dom A and len A > 1 and B is Matrix of len A , len B and len A = len B and len B > 0 and len A > 0 and len A > 0 and len B > 0 and len A > 0 and len A > 0 and len A > 0 ;
for i being non zero Element of NAT st i in Seg n holds ( i divides n implies h . i = ( 1_ F_Complex ) * ( i , j ) ) & ( h . i = ( 1_ F_Complex ) * ( i , j ) ) & ( h . j = ( 1_ F_Complex ) * ( i , j ) ) * ( h . j )
( ( b1 'imp' b2 ) '&' ( ( b2 '&' c2 ) '&' ( ( b2 '&' c2 ) '&' ( ( b2 '&' c2 ) '&' ( ( b2 '&' c2 ) '&' ( ( b2 '&' c2 ) '&' ( ( b2 '&' c2 ) '&' ( ( b2 '&' c2 ) '&' ( ( b2 '&' c2 ) '&' ( ( b2 '&' c2 ) '&' ( ( b2 '&' c2 ) '&' ( ( b2 '&' c2 ) '&' ( b2 '&' c2 ) ) ) ) ) ) ) '&' ( ( ( ( b2 '&' c2 ) '&' ( ( b2 '&' c2 ) '&' ( ( b2 '&' c2 ) '&' ( ( b2 '&' c2 ) '&' ( ( b2 '&' c2 ) '&' ( ( b2 '&' c2 ) '&' ( ( b2 '&' c2 ) '&' ( b2 '&' c2 ) '&' ( ( b2 '&' c2 ) '&' ( ( ( b2 '&' c2 ) '&' ( ( ( ( b2 '&' c2 ) '&' ( ( b2 '&' c2 ) ) ) ) ) ) '&' ( ( b2 ) '&'
assume that for x holds f . x = ( ( - 1 ) (#) ( ( cot * cot ) `| Z ) . x ) and for x st x in Z holds ( ( ( cot * cot ) `| Z ) . x ) = ( ( ( cot * cot ) `| Z ) . x ) / ( ( ( cot * cot ) `| Z ) . x ) ^2 ;
consider RI , II be Real such that RI = Integral ( M , F . n ) and RI = Integral ( M , F . n ) and I = Integral ( M , F . n ) and for i be Nat holds I . i = Integral ( M , F . i ) ;
ex k being Element of NAT st ' = k & 0 < k & for q be Element of product G st q in X & ||. qZ - f /. x .|| < r holds ||. partdiff ( f , q , x ) - diff ( f , x ) .|| < r
x in { x1 , x2 , x3 , x4 , x5 , x5 , x6 , x6 , x6 , x6 , x6 , x6 , x6 , x6 , x6 , x6 , x6 , x6 , x6 , x6 , x6 , x6 , x5 , 7 , 8 , 8 , 7 , 8 , 8 , 8 , 8 , 7 , 8 , 8 , 8 , 8 , 7 } ;
( G * ( j , i ) ) `2 = ( G * ( 1 , i ) ) `2 .= ( G * ( 1 , i ) ) `2 .= ( G * ( 1 , i ) ) `2 .= ( G * ( 1 , j ) ) `2 ;
f1 * p = p . ( ( the Arity of S1 ) . o ) .= ( the Arity of S2 ) . ( ( the Arity of S2 ) . o ) .= ( the Arity of S1 ) . ( ( the Arity of S1 ) . o ) .= ( the Arity of S1 ) . ( ( the Arity of S1 ) . o ) ;
func // T , P , T1 , T2 , T2 , T2 , T2 , T2 , T2 , T1 , T2 , T2 , T2 , T2 , T , p , q , r , r , s , s , r , q , r , s , p , q , r , s , r , s , r , q , r , s , r , s , r , s , r , q ;
F /. ( k + 1 ) = F . ( p . ( k + 1 ) , F /. ( k + 1 ) ) .= Fx0 . ( p . ( k + 1 ) , p /. ( k + 1 ) ) .= Fx0 . ( p . ( k + 1 ) , p /. ( k + 1 ) ) ;
for A , B , C , D being Matrix of K st len B = len C & len A = len C & len B > 0 & len A > 0 & len A > 0 & len B > 0 & len A > 0 & len B > 0 holds A * ( BC ) = B * ( BC )
seq . ( k + 1 ) = 0. ( ( seq . k ) * seq . ( k + 1 ) ) .= ( Partial_Sums ( seq ) ) . ( k + 1 ) .= ( Partial_Sums ( seq ) ) . ( k + 1 ) ;
assume that x in ( the carrier of CP ) and y in ( the carrier of CP ) and z in ( the carrier of CP ) and x = [ x , y ] ;
defpred P [ Element of NAT ] means for f st len f = $1 holds ( for k st k in $1 holds ( ( VAL g ) . k ) . ( f . k ) = ( ( VAL g ) . ( f . k ) ) '&' ( ( VAL g ) . ( f . k ) ) ;
assume that 1 <= k and k + 1 <= len f and f /. k = G * ( i , j ) and [ i , j ] in Indices G and [ i + 1 , j ] in Indices G and [ i + 1 , j ] in Indices G and G * ( i + 1 , j ) = G * ( i , j ) ;
assume that cn < 1 and ( |. q .| ) ^2 > 0 and ( |. q .| ) ^2 >= 0 and ( |. q .| ) ^2 >= 0 and ( |. q .| ) ^2 >= 0 and ( |. q .| ) ^2 >= 0 ;
for M being non empty TopSpace , x being Point of M , f being Function of M , M st x = f . x ex n being Element of M st for x being Element of M holds f . x = F ( x ) & f . x = F ( x ) holds f . x = F ( x )
defpred P [ Element of omega ] means f1 . $1 in Z & f2 . ( $1 + 1 ) in Z & f2 . ( $1 + 1 ) in Z & f2 . ( $1 + 1 ) = f1 . ( $1 + 1 ) / f2 . ( $1 + 1 ) ;
defpred P1 [ Nat , element ] means ( for r st r in Y & r in Y holds ||. ( f /. $1 ) - f /. $2 .|| < r ) implies ||. ( f /. $1 ) - f /. x0 .|| < r ) & ||. ( f /. $1 ) - f /. x0 .|| < r
( f ^ mid ( g , 2 , len g ) ) . i = ( mid ( g , 2 , len g ) ) . i .= g . ( i -' 1 ) .= g . ( i -' 1 ) .= g . ( i -' 1 ) ;
sqrt ( 1 - 2 * ( n + 1 ) ) * ( 2 * ( n + 1 ) ) = ( sqrt ( 1 - 2 * ( n + 1 ) ) / 2 ) * ( 2 * ( n + 1 ) ) ) .= 1 * ( 2 * ( n + 1 ) ) ;
defpred P [ Nat ] means for G being finite non empty RelStr st G is finite non empty & card G = $1 holds the carrier of G = { the carrier of G , the carrier of G } ;
assume that not f /. 1 in Ball ( u , r ) and not 1 <= m and m <= len f and for i st 1 <= i & i <= len f holds LSeg ( f /. i , f /. m ) /\ LSeg ( f , i ) <> {} ;
defpred P [ Element of NAT ] means ( Partial_Sums ( cos * ( $1 + 1 ) ) ) . ( 2 * $1 + 1 ) = ( Partial_Sums ( cos * ( $1 + 1 ) ) ) . ( 2 * $1 + 1 ) * ( ( Partial_Sums ( cos * ( $1 + 1 ) ) ) . ( 2 * $1 + 1 ) ) ;
for x being Element of product F holds x is FinSequence of product F & dom x = I & for i being set st i in dom F holds x . i = ( the Sorts of F ) . i ) & ( for i being set st i in I holds x . i = ( the Sorts of F ) . i ) implies x = ( the Sorts of F ) . i
( x " ) |^ ( n + 1 ) = ( x " ) * x " .= ( x " ) * x " .= ( x " ) * x " .= x " * x " * x " .= x " * x " * x " * x " * x " ;
DataPart Comput ( P +* I , Initialized s ) = DataPart Comput ( P +* I , Initialized s ) +* ( I +* I , Initialized s ) +* I +* I +* J +* J ) ;
given r such that 0 < r and ]. x0 - r , x0 + r .[ c= dom ( f1 | ]. x0 - r , x0 .[ ) and for g st g in ]. x0 , x0 + r .[ holds f1 . g <= x0 + r / ( g . g ) ;
assume that X c= dom f1 /\ dom f2 and f2 | X is continuous and for r st r in X /\ dom f2 holds ( f1 + f2 ) | X is continuous and for r st r in X /\ dom f2 holds f1 . r = r * ( f1 . r ) + ( f2 | X ) . r ;
for l being continuous continuous LATTICE for X being Subset of L ex L being Subset of L st l = sup ( { l where l is Element of L : for x being Element of L st x in X holds x in X } holds x is Ideal
Support ( A *' p ) = { m *' p where m is Element of NAT : m in dom ( m *' p ) } & ex m being Element of NAT st p = ( m *' p ) *' p & ex n being Element of NAT st n < m & m < n & p . n = ( m *' p ) . ( n + 1 ) ;
( f1 - f2 ) /* ( ( f1 /* ( f1 /* s ) ) ) = lim ( ( f1 /* s ) - f2 /* ( f1 /* s ) ) .= lim ( f2 * f1 ) ;
ex p1 being Element of CQC-WFF ( Al ( ) ) st F . p = g . p1 & for g being Function of D ( ) , D ( ) st P [ g , f . ( len f ) ] holds P [ g , f . ( len f ) ] ;
( mid ( f , i , len f -' 1 ) ) /. j = ( mid ( f , i , len f -' 1 ) ) /. j .= f /. ( j + 1 -' 1 ) .= f /. ( j + 1 -' 1 ) ;
( p ^ q ) . ( len p + k ) = ( ( p ^ q ) . ( len p + k ) ) . ( len p + k ) .= ( ( p ^ q ) . ( len p + k ) ) . ( len p + k ) .= ( p ^ q ) . ( len p + k ) ;
len mid ( D2 , D1 , j1 ) + 1 = indx ( D2 , D1 , j1 ) + 1 .= indx ( D2 , D1 , j1 ) + 1 .= indx ( D2 , D1 , j1 ) + 1 + 1 .= indx ( D2 , D1 , j1 ) + 1 ;
x * y = Mz . ( ( y * z ) * z ) .= ( x * y ) * ( z * z ) .= ( x * y ) * ( z * x ) .= ( x * y ) * ( z * x ) ;
v . ( <* x , y *> - ( y * i ) ) * y . ( reproj ( i , y ) + ( y * i ) ) = diff ( u , y ) + diff ( u , y ) ;
i * i = <* 0 * ( 1 - i ) * ( 1 - i ) *> .= <* 0 * ( 1 - i ) * ( 1 - i ) * ( 1 - i ) * ( 1 - i ) * ( 1 - i ) *> .= <* 0 * ( 1 - i ) * ( 1 - i ) * ( 1 - i ) ;
Sum ( L * F ) = Sum ( L * F ) + 0. V .= Sum ( L * F ) + 0. V .= Sum ( L * F ) + 0. V .= Sum ( L * F ) + 0. V .= L * F + L * F ;
ex r be Real st 0 < r & for Y1 be Subset of X st Y1 is non empty & Y1 c= Y holds |. Sum ( Y1 ) - 0 .| < r
( GoB f ) * ( i , j ) = f /. ( k + 2 ) & ( GoB f ) * ( i + 1 , j ) = f /. ( k + 1 ) or ( GoB f ) * ( i + 1 , j ) = f /. ( k + 2 ) ;
( ( - 1 ) / ( r * ( x - r ) ) ) / ( r * ( x - r ) ) = ( ( - 1 ) / ( r * ( x - r ) ) ) / ( r * ( x - r ) ) ) / ( r * ( x - r ) ) .= ( ( 1 - r ) / ( r * ( x - r ) ) ) / ( r * ( x - r ) ) ;
( - b + sqrt ( a , b ) ) / 2 > 0 & ( - b + sqrt ( b , c ) ) / 2 > 0 implies ( - b ) / 2 < 0 & ( - b ) / 2 < 0
assume that inf ( ( the carrier of L ) /\ C ) in X and for X st X in C holds not sup ( ( the carrier of L ) /\ C ) = "/\" ( ( the carrier of L ) /\ C , L ) and not "\/" ( ( the carrier of L ) /\ C , L ) = "/\" ( ( the carrier of L ) /\ C , L ) ;
( ( ( B , B ) . i ) (*) ( ( the Sorts of B ) . j ) = ( i |-> ( ( the Sorts of B ) . j ) ) (*) ( ( the Sorts of A ) . j ) ) .= ( i |-> ( ( the Sorts of B ) . j ) ) . ( ( the Sorts of A ) . j ) ;