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 ;
hence thesis ;
hence thesis ;
assume not thesis ;
assume not thesis ;
let B ;
a <> c
T c= S
D c= B
let G , c ;
let a , b ;
let n , 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 injective ;
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 ;
let G , n , m ;
f is meet-preserving ;
not x in Y ;
z = +infty ;
k be Nat ;
K9 is being_line ;
assume n >= N ;
assume n >= N ;
assume X is positive-implicative ;
assume x in I ;
q is dominated_by_0 ;
assume c in x ;
1 - p > 0 ;
assume x in Z ;
assume x in Z ;
1 <= k2a ;
assume m <= i ;
assume G is cyclic ;
assume a divides b ;
assume P is closed ;
d - c > 0 ;
assume q in A ;
W is not bounded ;
f is weakly-one-to-one ;
assume A is boundary ;
g is being_S-Seq ;
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 ;
b9 <=' c9 ;
A meets W ;
i9 <= j9 ;
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 - 2 ;
let X be set ;
let X be set ;
let y be element ;
let x be element ;
P [ 0 ]
let E be set ;
let C be Category ;
let x be element ;
let k be Nat ;
let x be element ;
let x be element ;
let e be element ;
let x be element ;
P [ 0 ]
let c be element ;
let y be element ;
let x be element ;
let a be Real ;
let x be element ;
let X be element ;
P [ 0 ]
let x be element ;
let x be element ;
let y be element ;
r in REAL ;
let e be element ;
n1 is epi ;
Q halts_on s ;
x in ICC ;
M < m + 1 ;
T2 is open ;
z in b U+ a ;
R2 is well-ordering ;
1 <= k + 1 ;
i > n + 1 ;
q1 is one-to-one ;
let X , Y ;
PR 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 |- 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 ~= o4 ;
O <> O3 ;
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 ComplexNormSpace ;
not s in Y ^0 ;
rng f is_<=_than w
b "/\" e = b ;
m = m4 ;
t in h . D ;
P [ 0 ] ;
z = x * y ;
S . n is bounded ;
let V be RealLinearSpace ;
P [ 1 ] ;
P [ {} ] ;
C1 is a_component ;
H = G . i ;
1 <= i9 + 1 ;
F . m in A ;
f . o = o ;
P [ 0 ] ;
a - a <= r - a ;
R [ 0 ] ;
b in f .: X ;
q = q2 ;
x in [#] V ;
f . u = 0 ;
e1 > 0 ;
let V be RealUnitarySpace ;
s is trivial non empty ;
dom c = Q ;
P [ 0 ] ;
f . n in T ;
N . j in S ;
let T be complete LATTICE ;
the ObjectMap of F is one-to-one
sgn x = 1 ;
k in support a ;
1 in Seg 1 ;
rng f = X ;
len T in X ;
va < n ;
SI is bounded ;
assume p = p2 ;
len f = n ;
assume x in P1 ;
i in dom q ;
let UN ;
pc = c ;
j in dom h ;
let n be non zero Nat , k ;
f | Z is continuous ;
k in dom G ;
UBD C = B ;
1 <= len M ;
p in north_halfline x ;
1 <= j19 ;
set A = KurExSet ;
a *' [= c ;
e in rng f ;
cluster B ++ A -> empty ;
not H is Until ;
assume n0 <= m ;
T is increasing Ordinal-Sequence ;
e2 <> e4
Z c= dom g ;
dom p = X ;
H is_proper_subformula_of G ;
( i + 1 ) <= n ;
not v = 0. V ;
A c= Affin A ;
S c= dom F ;
m in dom f ;
let X0 be set ;
c = sup N ;
R is_connected_in union M ;
assume not x in REAL ;
Image f is complete ;
x in Int y ;
dom F = M ;
a in On W ;
assume e in A ( ) ;
C c= Cy ;
mbcd <> {} ;
let x be Element of Y ;
let f be ConwayGameChain ;
not n in Seg 3 ;
assume X in f .: A ;
p <= m ;
assume not u in { v } ;
d is Element of A ;
A ^b misses B ;
e in v .edgesOut() ;
- y in I ;
let A be non empty set ;
Pk = 1 ;
assume r in F . k ;
assume f is_simple_func_in S ;
let A be uncountable set ;
rng f c= NAT
assume P [ k ] ;
fC1 <> {} ;
let X be set , o be Ordinal ;
assume x is being_a_sum_of_amalgams_of_squares ;
assume not v in { 1 } ;
let IPS ;
j < l ;
v = - u ;
assume s . b > 0 ;
let d1 , d2 , d3 , d4 ;
assume t . 1 in A ;
let Y be non empty TopSpace ;
assume a in uparrow s ;
let S be non empty Poset ;
a , b // b , a ;
a * b = p * q ;
assume Gen x , y ;
assume x in Big_Omega ( f ) ;
[ a , c ] in X ;
mbcde <> {} ;
M +^ N c= M +^ M ;
assume M is strongly_Mahlo ;
f is union-distributive ;
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 ;
m + 1 < n + 1 ;
s in S \/ { s } ;
n + i >= n + 1 ;
assume Re ( y ) = 0 ;
k1 <= j1 ;
f | A is uniformly_continuous ;
f . x - a <= b ;
assume y in dom h ;
x * y in B1 ;
set X = Seg n ;
1 <= i2 + 1 ;
k + 0 <= k + 1 ;
p ^ q = p ;
j |^ y divides m ;
set m = max A ;
[ x , x ] in R ;
assume x in succ 0 ;
a ( ) in sup phi ;
let S , z , CH ;
q2 c= C1 ;
a2 < c2 ;
s2 is 0 -started ;
IC s = 0 ;
s6 = s5 ;
let v be 0 -started State of SCMPDS , V ;
let x , y be element ;
let x be Element of T ;
assume a in rng F ;
then x in dom T9 ;
let S be System of L ;
y " <> 0 ;
y " <> 0 ;
0. V = u - w ;
are_Prop y2 , y ;
let X , G , K , RK ;
let a , b be Real ;
let a be Object of C ;
let x be Vertex of G ;
let o be Object of C ;
r '&' q = P ! l ;
let i , j be Nat ;
let s be State of A ;
s4 . n = N ;
let x ;
mi in dom g ;
l . 2 = y1 ;
|. g . y .| <= r ;
f . x in C0 ;
VP is non empty ;
let x be Element of X ;
0 <> f . g2 ;
f2 /* q is convergent ;
f . i is_measurable_on E ;
assume xi in Nx0 ;
reconsider i9 = i as Ordinal ;
r * v = 0. X ;
rng f c= INT ;
G = 0 .--> goto 0 ;
let A be Subset of X ;
assume A0 is dense open ;
|. f . x .| <= r ;
addLoopStr , x be Element of R ;
let b be Element of L ;
assume x in Wy ;
P [ k , a ] ;
let X be Subset of L ;
let b be object of B ;
let A , B be AltCatStr ;
set X = MSVars C ;
let o be OperSymbol of S ;
let R be connected non empty Poset ;
n + 1 = succ n ;
xx c= Z1 ;
dom f = C1 ;
assume [ a , y ] in X ;
Re seq is convergent ;
assume a1 = b1 ;
A = sInt A ;
a <= b or b <= a ;
n + 1 in dom f ;
let F be Instruction-Sequence of S ;
assume r2 > x0 ;
let X be set , Y be non empty set ;
2 * x in dom W ;
m in dom g2 ;
n in dom g1 ;
k + 1 in dom f ;
still_not-bound_in { s } is finite ;
assume x1 <> x2 ;
v4 in VG ;
not [ b9 , b ] in T ;
ii + 1 = i ;
T c= CnCPC ( T ) ;
l `1 = 0 ;
let f be sequence of TOP-REAL N , n be Nat ;
t `2 = r ;
AF is_integrable_on M ;
set v = VAL g , t = TVERUM ;
let A , B be real-membered set ;
k <= len G + 1 ;
MP-conectives misses MP-variables
product so is non empty ;
e <= f or f <= e ;
cluster non empty normal for Sequence ;
assume c2 = b2 ;
assume h in [. q , p .] ;
1 + 1 <= len C ;
not c in B . m1 ;
cluster R .: X -> empty ;
p . n = H . n ;
vseq is Cauchy_sequence_by_Norm ;
IC s3 = 0 ;
k in N or k in K ;
F1 \/ F2 c= F
Int G1 <> {} ;
z `2 = 0 ;
p01 <> p1 ;
assume z in { y , w } ;
MaxADSet ( a ) c= F ;
ex_sup_of downarrow s , S ;
f . x <= f . y ;
TopRelStr ;
( q |^ m ) >= 1 ;
a is_>=_than X & b is_>=_than Y ;
assume <^ a , c ^> <> {} ;
F . c = g . c ;
G is one-to-one faithful full onto ;
not A \/ { a } c= B ;
0. V = 0. Y ;
I being IC-relocable Instruction of S ;
fn1 . 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+ ;
p1 = KD1 ;
M . k = <*> REAL ;
phi . 0 in rng phi ;
OSMSubSort ( A ) is opers_closed
assume z0 <> 0. L ;
n < NS . k ;
0 <= seq . 0 ;
- q + p = v ;
{ v } is Subset of B ;
g = Del ( f , 1 ) ;
cR is StableSet of R ;
set cR = Vertices R ;
pWH c= P4 ;
x in [. 0 , 1 .[ ;
f . y in dom F ;
let T be Scott TopAugmentation of S ;
ex_inf_of the carrier of S , S ;
types a = types b ;
P , C , K is_coplanar ;
let x be element ;
2 to_power i < 2 to_power m ;
x + z = x + z + q ;
x \ ( a \ x ) = x ;
||. x - y .|| <= r ;
Y <> {} ;
a [x] b , b [x] a are_isomorphic
assume a in A ( ) . i ;
k in dom qq ;
p is distProbFinS of S ;
i -' 1 = i - 1 ;
reconsider A = [: {} , D :] as empty set ;
assume x in f .: X ( ) ;
i2 - i1 = 0 ;
j2 + 1 <= i2 ;
g " * a in N ;
K <> { [ {} , {} ] } ;
cluster strict for EuclidianRing ;
( |. q .| ) ^2 > 0 ;
|. p4 .| = |. p .| ;
s2 - s1 > 0 ;
assume x in { Gij } ;
W-min C in C ;
assume x in { Gij } ;
assume i + 1 = len G ;
assume i + 1 = len G ;
dom I = Seg n ;
k <> i ;
1 + 1 - 1 <= i + j - 1 ;
dom S = dom F ;
let s be Element of NAT ;
let R be ManySortedRelation of A ;
let n be Element of NAT ;
TopStruct ;
let f be ManySortedSet of I ;
let z be Element of COMPLEX ;
u in { bg } ;
2 * n < 2tpk ;
let f be finite-support Function , x , y be set ;
BF c= Vc1
assume I is_halting_on s , P ;
UIL = UIL1 ;
M /. 1 = z /. 1 ;
x11 = x22 ;
i + 1 < n + 1 + 1 ;
x in { {} , <* 0 *> } ;
fx <= fy ;
let L be LATTICE , l be Element of L ;
x in dom Fp ;
let i be Element of NAT ;
rF is COMPLEX -valued ;
<^ o2 , o ^> <> {} ;
( s . x ) to_power 0 = 1 ;
card K1 in M ;
assume that X in U and Y in U ;
let D be Dynkin_System of Omega ;
set r = q - { k + 1 } ;
y = W . ( 2 * x - 1 ) ;
dom g = cod f ;
let X , Y be non empty TopSpace ;
for A being Interval , x being Real holds x ++ A is Interval
|. <*> A .| . a = 0
cluster strict for SubLattice of L ;
a1 in B . s1 ;
let V be finite-dimensional VectSp of F ;
A * B on B , A ;
fd = 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 ;
q in A \/ ( B "\/" C ) ;
dom ( F * C ) = o ;
set S = Funcs ( X , INT ) ;
z in dom ( A --> y ) ;
P [ y , h . y ] ;
{ x0 } c= dom f ;
let B be non-empty ManySortedSet of I ;
PI / 2 < Arg z ;
reconsider zz = 0 as Nat ;
LIN a9 , d9 , c9 ;
[ y , x ] in IR ;
Q `3_3 = 0 ;
set j = x0 div m ;
assume a in { x , y , c } ;
j2 - jn2 > 0 ;
hence I -TruthEval phi = 1 ;
[ y , d ] in FSG ;
let f be Function of X , Y ;
set A2 = B / C ;
s1 , s2 are_co-prime ;
j1 -' 1 = 0 ;
set m2 = 2 * n + j ;
reconsider t9 = t as bag of n ;
I2 . j = m . j ;
i |^ s , n are_relative_prime ;
set g = f | DD1 ;
assume that X is bounded_below and 0 <= r ;
p1 `1 = 1 ;
a < p3 `1 ;
L \ { m } c= UBD C ;
x in Ball ( x , 10 ) ;
not a in LSeg ( c , m ) ;
1 <= i1 -' 1 ;
1 <= i1 -' 1 ;
i + i2 <= len h ;
x = W-min ( P ) ;
[ x , z ] in [: X , Z :] ;
assume y in [. x0 , x .] ;
assume p = <* 1 , 2 , 3 *> ;
len <* A1 *> = 1 ;
set H = h . gfB ;
b *' * a = |. a .| ;
Shift ( w , 0 ) |= v ;
set h = h2 ** h1 ;
assume x in X3 /\ X4 ;
||. h .|| < d0 ;
not x in Carrier f ;
f . y = F ( y ) ;
for n holds X [ n ] ;
then k -' l = k - l ;
<* p , q *> /. 2 = q ;
let S be Subset of Domains_Lattice Y ;
let P , Q be Loop of s ;
Q /\ M c= union ( F | M )
f = b * canFS ( S ) ;
let a , b be Element of G ;
f .: X is_<=_than f . sup X
let L be non empty transitive reflexive RelStr ;
SF is x -quasi_basis
let r be non positive Real , s be non negative Real ;
M , v |= x '=' y ;
v + w = 0. ZS ;
then P [ len cF ] ;
InsCode ins = 8 ;
the ZeroF of M = 0 ;
cluster z * seq -> summable ;
let O be Subset of the carrier of C ;
( abs f ) | X is continuous
x2 = g . ( j + 1 ) ;
cluster -> 0wff for Element of AtomicFormulasOf S ;
reconsider l1 = l - 1 as Nat ;
vs2 is_vertex_seq_of r2 ;
T3 is SubSpace of T2 ;
Q1 /\ Q19 <> {} ;
let X be non empty set , t be FinSequence of X , k be Nat ;
q " is Element of X ;
F . t is thin of M ;
assume that not n = 0 and not n = 1 ;
set eb = EmptyBag n ;
let b be Element of Bags n ;
for i holds b . i is commutative ;
x is_a_root_of p `2 ;
not r in ]. p , q .[ ;
let R be FinSequence of REAL ;
SS does not destroy b1 ;
IC SCM R <> a ;
|. p - |[ x , y ]| .| >= r ;
1 * seq = seq
NAT , x be FinSequence of NAT ;
let f be Function of C , D ;
for a holds 0. L + a = a
IC s = s . NAT ;
H + G = F - ( G - G ) ;
Ch2 . x = x2 ;
f1 = f .= f2 ;
Sum <% p . 0 %> = p . 0 ;
assume v + W = ( v + u ) + W ;
{ a1 } = { a2 } ;
a1 , b1 _|_ b , a ;
d3 , o _|_ o , a3 ;
IR is_reflexive_in CR ;
IR is_antisymmetric_in CR ;
upper_bound rng H1 = e ;
x = aa1 * aa1 ;
( |. p1 .| ) ^2 >= 1 ;
assume j2 -' 1 < 1 ;
rng s c= dom f1 ;
assume support a misses support b ;
let L be associative well-unital non empty doubleLoopStr ;
s " + 0 < n + 1 ;
p . c = fd . 1 ;
R . n <= R . ( n + 1 ) ;
Directed I0 = I0 ;
set f = + ( x , y , r ) ;
cluster Ball ( x , r ) -> bounded ;
consider r being Real such that r in A ;
cluster non empty NAT -defined for Function ;
let X be non empty filtered Subset of S ;
let S be non empty full SubRelStr of L ;
cluster InclPoset lambda N -> complete non trivial ;
1 / a " = a ;
( q . {} ) `1 = o ;
n - ( i -' 1 ) > 0 ;
assume 1 / 2 <= t9 & t9 <= 1 ;
card B = ( k + 1 ) - 1 ;
x in union ( rng fIp ) ;
assume x in the carrier of R ;
let Y , Z , M , o , a , b , c , a1 , b1 , c1 , d ;
f . 1 = L . ( F . 1 ) ;
the_Vertices_of G = { v } ;
let G be nonnegative-weighted WEGraph , e , x be set ;
let G be VGraph , e , val be set ;
c . ic in rng c ;
f2 /* q is divergent_to-infty ;
set z1 = - z2 ;
assume w is_atlas_of S , G ;
set f = p |-count t ;
let S be Functor of C opp , B , c be Object of C ;
assume ex a st P [ a ] ;
let x be Element of REAL m ;
let IT be Subset-Family of X ;
reconsider p9 = p as Element of NAT ;
let X be RealLinearSpace , v , w be Point of X ;
let s be State of SCM+FSA ;
p is FinPartState of SCM+FSA ;
stop I ( ) c= PI ;
set ci = fc1 /. i ;
then w ^ t is_a_prefix_of w ^ s ;
W1 /\ W = W1 /\ W9 ;
f . j is Element of J . j ;
let x , y be type of T2 ;
ex d st a , b // b , d ;
a <> 0 & b <> 0 & c <> 0
ord x = 1 & x is nilpotent ;
set g2 = lim seq2 ;
2 * x >= 2 * ( 1 / 2 ) ;
assume ( a 'or' c ) . z <> TRUE ;
f (*) g in Hom ( c , c ) ;
Hom ( c , c + d ) <> {} ;
assume 2 * Sum ( q | m ) > m ;
L1 . ( Fbm ) = 0 ;
nabla X \/ R1 = nabla X ;
sin . x <> 0 ;
exp_R . x > 0 ;
o1 in XX /\ O2 ;
let G be EGraph , e , val be set ;
r3 > ( 1 / 2 ) * 0 ;
x in P .: ( F -Ideal ) ;
left-ideal non empty Subset of R ;
h . p1 = f2 . O ;
Index ( p , f ) + 1 <= j ;
len qK = width M ;
Carrier ( L - K ) c= A ;
dom f c= union rng FG
k + 1 in support pfexp n ;
let X be ManySortedSet of the carrier of S ;
[ x9 , y9 ] in EqCl R ;
i = D1 or i = D2 ;
assume a mod n = b mod n ;
h . x2 = g . x1 ;
F c= bool the carrier of X
reconsider w = |. s1 .| as Real_Sequence ;
1 / ( m * m + r ) < p ;
dom f = dom Ip ;
[#] PY = [#] KX ;
redefine func - x -> R_eal ;
{ d0 } c= A implies A is closed
cluster TOP-REAL n -> finite-ind ;
let w be Element of N , w1 be Element of M ;
let x be Element of dyadic ( n ) ;
u in W1 & v in W3 ;
reconsider y9 = y as Element of L2 ;
N is full SubRelStr of T opp ;
sup { x , y } = c "\/" c ;
g . n = n to_power 1 .= n ;
h . J = EqClass ( u , J ) ;
let seq be norm_summable sequence of X ;
dist ( x9 , y ) < r / 2 ;
reconsider mm = m as Element of NAT ;
x - x0 < r1 - x0 ;
reconsider P99 = P9 as strict Subgroup of N ;
set g1 = p * idseq q9 ;
let n , m , k be non zero Nat ;
assume 0 < e & f | A is bounded_below ;
D2 . ID1 in { x } ;
cluster subcondensed -> semi-open for Subset of T ;
2 ;
Gik in LSeg ( pion1 , 1 ) ;
let f be FinSequence of TOP-REAL 2 , n be Element of NAT ;
reconsider SS = S as Subset of T ;
dom ( i .--> X9 ) = { i } ;
let S be locally_directed OrderSortedSign , X be non-empty ManySortedSet of S ;
let S be locally_directed OrderSortedSign , X be non-empty ManySortedSet of S ;
op1 c= { [ {} , {} ] } ;
reconsider m9 = m - 1 as Element of NAT ;
reconsider d9 = x as Element of C ( ) ;
let s be 0 -started State of SCMPDS ;
let t be 0 -started State of SCMPDS ;
parallelogram b , b9 , x , y ;
j = k \/ { k } ;
let Y be complex-functions-membered set , f be PartFunc of X , Y ;
N0 >= sqrt c / sqrt 2 ;
reconsider tr = TR as TopSpace ;
set q = h * ( p ^ <* d *> ) ;
z2 in U_FT y4 /\ Q2 ;
A |^ 0 = { <%> E } ;
len W2 = len W + 2 ;
len h2 in dom h2 ;
i + 1 in Seg len s2 ;
z in dom g1 /\ dom f ;
assume p2 = E-max ( K ) ;
( len G ) + 1 <= i1 + 1 ;
f1 (#) f2 is_convergent_in x0 ;
cluster seq1 + seq2 -> summable ;
assume j in dom ( M1 /. i ) ;
let A , B , C be Subset of X ;
let x , y , z be Point of X ;
b ^2 - 4 * a * c >= 0 ;
<* x /" y *> ^ <* y *> ==>. x ;
a in { a , b } & b in { a , b } ;
len p2 is Element of NAT ;
ex x being element st x in dom R ;
len q = len ( K (#) G ) ;
s1 = Initialize Initialized s ;
consider w being Nat such that q = z + w ;
x `# is_a_complement'_of x ;
k = 0 & n <> k or k > n ;
X is discrete implies for A being Subset of X holds A is closed
for x st x in L holds x is FinSequence
||. f /. c .|| <= r1 ;
c in uparrow p & not c in { p } ;
reconsider V9 = V as Subset of Sierpinski_Space ;
let L be non empty 1-sorted , N , M be net of L ;
z is_>=_than waybelow x implies z is_>=_than compactbelow x
M ! f = f & M ! g = g ;
( Bin1 1 ) /. 1 = TRUE ;
dom g = dom Funcs ( X , f ) ;
mode Trail of G is Trail-like Walk of G ;
[ i , j ] in Indices M ;
reconsider s = x " as Element of H ;
let f be Element of dom Subformulae p ;
F1 ?- a1 = G1 ;
cluster circle ( a , b , r ) -> compact ;
let a , b , c , d be Real ;
rng s c= dom ( f ^ ) ;
ProjMap2 ( FF2 , k ) is additive ;
set k2 = card dom B ;
set X = ( the Sorts of A ) (\/) V , G = DTConMSA X ;
reconsider a = [ x , s ] as Terminal of G ;
let a , b be Element of MPS ;
reconsider s1 = s as Element of S0 ;
rng p c= the carrier of L ;
let p be QC-formula of A , d be Subset of bound_QC-variables ( A ) ;
x .|. x = 0 iff x = 0. W ;
Ik in dom stop ( I ) ;
let g be continuous Function of X | B , Y ;
reconsider D = Y as Subset of Euclid n ;
reconsider i0 = len p1 as Integer ;
dom f = the carrier of S ;
rng h c= Union Carrier J
cluster All ( x , H ) -> ZF-formula-like ;
d * N1 ^2 > N1 * 1 ;
]. a , b .[ c= [. a , b .] ;
set g = ( f " ) | D1 ;
dom ( p | mm ) = mm ;
3 + - 2 <= k + - 2 ;
tan is_differentiable_in arccot . x ;
x in rng ( f :- p ) ;
let D be non empty set , f , g be FinSequence of D ;
cp in the carrier of S1 ;
rng ( f " ) = dom f ;
( the_Target_of G ) . e = v ;
width G -' 1 < width G ;
assume v in rng ( S | E1 ) ;
assume x is_a_root_of g or x is_a_root_of h ;
assume 0 in rng ( g2 | A ) ;
let q be Point of TOP-REAL 2 ;
let p be Point of TOP-REAL 2 ;
dist ( O , u ) <= |. p2 .| + 1 ;
assume dist ( x , b ) < dist ( a , b ) ;
<* Smax *> is_in_the_area_of Ca ;
i <= len Ga -' 1 ;
let p be Point of TOP-REAL 2 ;
x1 in the carrier of I[01] ;
set p1 = f /. i , p2 = f /. ( i + 1 ) ;
g in { g2 : r < g2 } ;
Q2 = SQ1 " Q ;
( 1 / 2 ) GeoSeq is summable ;
- p + I c= - p + A ;
n < LifeSpan ( P1 , s1 ) ;
CurInstr ( p1 , s1 ) = i ;
( A /\ Cl { x } ) \ { x } <> {} ;
rng f c= ]. r , r + 1 .[
let f be Function of T , S , g be Function of S , V ;
let f be Function of L1 , L2 ;
reconsider z9 = z as Element of CompactSublatt L ;
let S , T be complete Scott TopLattice , f be Function of S , T ;
reconsider g9 = g as Morphism of c9 , b9 ;
[ s , I ] in [: S , ElementaryInstructions A :] ;
len the connectives of C = 4 ;
let C1 , C2 be Subcategory of C ;
reconsider V1 = V as Subset of X | B ;
p is valid implies All ( x , p ) is valid
f .: X c= dom g ;
H |^ a " is Subgroup of H ;
let A1 be Action of O , E1 ;
p2 , r3 , q2 is_collinear ;
consider x be element such that x in v ^ K ;
not x in { 0. TOP-REAL 2 } ;
p in [#] ( I[01] | B11 ) ;
In ( 0 , REAL ) < M . EE ;
for c being Object of C holds opp ( c opp ) = c ;
consider c being element such that [ a , c ] in G ;
a1 in dom ( F . s2 ) ;
cluster -> Orthocomplemented for naturally_sup-generated CLatAugmentation of L ;
set i1 = the Nat , a = the Int-Location ;
let s be 0 -started State of SCM+FSA ;
assume y in ( f1 union f2 ) .: A ;
f . len f = f /. len f ;
x , f . x '||' f . x , f . y ;
X c= Y implies proj2 X c= proj2 Y
let X , Y be ext-real-membered set , x be UpperBound of X , y be UpperBound of Y ;
redefine func x `1 -> quasi-loci ;
set S = RelStr (# Bags n , iln #) ;
set T = Closed-Interval-TSpace ( 0 , 1 / 2 ) ;
1 in dom mid ( f , 1 , 1 ) ;
4 * PI / PI < 2 * PI / PI ;
x2 in dom f1 /\ dom f ;
O c= dom I & { {} } = { {} } ;
( the Source of G ) . x = v ;
{ HT ( f , T ) } c= Support f ;
reconsider h = R . k as Polynomial of n , L ;
ex b being Element of G st y = b * H ;
let x9 , y9 , z9 be Element of G9 ;
h19 . i = f . ( h . i ) ;
p `1 = p1 `1 ;
i + 1 <= len Cage ( C , n ) ;
len ( <* P *> @ ) = len P ;
set NX = the LTLnext of N ;
len g - y + ( x + 1 ) - 1 <= x ;
( not a on B ) & not b on B ;
reconsider rIv = r * I . v as FinSequence ;
consider d such that x = d and a [*] d [= c ;
given u such that u in W & x = v + u ;
len ( f /^ n ) = len f - n ;
set q1 = SW-corner C , q2 = NW-corner C ;
set S = Sub_& ( S1 , S2 ) ;
MaxADSet ( b ) c= MaxADSet ( P /\ Q ) ;
Cl ( G . q1 ) c= F . r2 ;
f " D meets h " V ;
reconsider D = E as non empty directed Subset of L1 ;
H = ( the_left_argument_of H ) '&' ( the_right_argument_of H ) ;
assume t is Element of Free ( S , X ) ;
rng f c= the carrier of S2 ;
consider y being Element of X such that x = { y } ;
f1 . ( a1 , b1 ) = b1
the carrier' of G9 = E \/ { E } ;
reconsider m = len p - k as Element of NAT ;
set S1 = LSeg ( n , UMP C ) ;
[ i , j ] in Indices M1 ;
assume that P c= Seg m and M is without_repeated_line ;
for k st m <= k holds z in K . k ;
consider a be set such that p in a and a in G ;
L1 . p = p * ( L /. 1p ) ;
prodi1 . i = prodi . i ;
let PA , PB be a_partition of Y ;
0 < r & r < 1 implies 1 < 1 / r
rng transl ( a , X ) = [#] X ;
reconsider x9 = x , y9 = y as Element of K ;
consider k such that z = f . k & n <= k ;
consider x be element such that x in ( X \ { p } ) ;
len canFS ( s ) = card s ;
reconsider x2 = x1 as Element of L2 ;
Q in FinMeetCl the topology of X ;
dom ff c= dom ufs ;
for n , m st n divides m & m divides n holds n = m
reconsider x9 = x as Point of [: I[01] , I[01] :] ;
a in DiffElems ( T2 , T2 ) ;
not y0 in still_not-bound_in f ;
Hom ( ( a [x] b ) [x] c , c ) <> {} ;
consider k1 such that p " < k1 ;
consider c , d such that dom f = c \ d ;
[ x , y ] in [: dom g , dom k :] ;
set S1 = GFA3AdderStr ( x , y , z ) ;
l3 = m2 & l4 = i2 ;
x0 in dom u01 /\ AB ;
reconsider p = x as Point of TOP-REAL 2 ;
I[01] = ( R^1 ) | B01 ;
hence LE f . p4 , f . p1 , P ;
FiP `1 <= x `1 ;
x `2 = Wmin `2 ;
for n being Element of NAT holds P [ n ] ;
let F be ManySortedSigmaField of I , Sigma , J , K be non empty Subset of I ;
assume 1 <= i & i <= len <* a " *> ;
0 |-> a = <*> ( the carrier of K ) ;
X . i in bool ( A . i \ B . i ) ;
<* 0 *> in dom ( e --> [ 1 , 0 ] ) ;
P [ a ] implies P [ succ a ]
reconsider sy1 = sy as Terminal of D ;
k - ( i -' 1 ) <= len p - j ;
[#] S c= [#] the TopStruct of T ;
for V being strict RealLinearSpace holds V in Subspaces ( V )
assume k in dom mid ( f , i , j ) ;
let P be non empty Subset of TOP-REAL 2 ;
let A , B be Matrix of n1 , K ;
( - a ) * ( - b ) = a * b ;
for A being being_line Subset of AS holds A // A
idm o2 in <^ o2 , o2 ^> ;
||. x .|| = 0 implies x = 09 ( X )
let N1 , N2 be strict normal Subgroup of G ;
j >= len lower_volume ( g , D1 ) ;
b = Q . ( len Qr - 1 + 1 ) ;
( f2 * f1 ) /* s is divergent_to+infty ;
reconsider h = f * g as Function of N4 , G ;
assume that a <> 0 and delta ( a , b , c ) >= 0 ;
[ t , t ] in the Relation of A ;
( v |-- E ) | n is Element of TRn ;
{} = Carrier ( L1 + L2 ) ;
Directed I is_pseudo-closed_on Initialized s , P ;
Initialized p = Initialize ( p +* q ) ;
reconsider N2 = N1 as strict net of R2 ;
reconsider Y9 = Y as Element of InclPoset Ids L ;
"/\" ( ( uparrow p ) \ { p } , L ) <> p ;
consider j being Nat such that i2 = i1 + j ;
not [ s , 0 ] in the carrier of S2 ;
mbcd in INTERSECTION ( B '/\' C , D ) \ { {} } ;
n <= len PR1 + len PR ;
x1 `1 = x2 `1 ;
InputVertices S = { x1 ( ) , x2 ( ) } ;
let x , y be Element of FTSC1 n ;
p = |[ p `1 , p `2 ]| ;
g * 1_ G = h " * g * h ;
let p , q be Element of SubstLatt ( V , C ) ;
x0 in dom x1 /\ dom x2 ;
R qua Function " = R " ;
n in Seg len ( f -: p ) ;
for s being Real st s in R holds s <= s2 ;
rng s c= dom ( f2 * f1 ) ;
synonym 2Set ( X ) for TWOELEMENTSETS ( X ) ;
1_ K * 1_ K = 1_ K ;
set S = Segm ( A , P1 , Q1 ) ;
ex w st e = w / f & w in F ;
( ProjMap2 ( PP2 , k9 ) ) # x is convergent ;
cluster open -> F_sigma for Subset of TM ;
len f1 = 1 .= len f3 ;
( i * p ) / p < ( 2 * p ) / p ;
let x , y be Element of OSSub ( U0 ) ;
b1 , c1 // b19 , c19 ;
consider p being element such that c1 . j = { p } ;
assume that f " { 0 } = {} and f is total ;
assume IC Comput ( F , s , k ) = n ;
Reloc ( J , card I ) does not destroy a ;
Goto ( card I + 1 ) does not destroy c ;
set m3 = LifeSpan ( p3 , s3 ) ;
IC SCMPDS in dom ( Initialize p ) ;
dom t = the carrier of SCM R ;
( S-max L~ f ) .. f = 1 ;
let a , b be Element of SubstLatt ( V , C ) ;
Cl ( union Int F ) c= Cl Int ( union F ) ;
( the carrier of ( X1 union X2 ) ) misses A0 ;
assume not LIN a , f . a , g . a ;
consider i being Element of M such that i = dD9 ;
Y c= { x } implies Y = {} or Y = { x }
M , v |= H1 / ( y , x ) ;
consider m being element such that m in Intersect FF ;
reconsider A1 = support ( u1 ) as Subset of X ;
card ( A \/ B ) = ( k - 1 ) + 2 * 1 ;
assume that a1 <> a3 and a2 <> a4 ;
cluster s -compound ( V ) -> termal for string of S ;
Li /. n2 = Li . n2 ;
let P be compact non empty Subset of TOP-REAL 2 ;
assume rl in LSeg ( p1 , p2 ) ;
let A be non empty compact Subset of TOP-REAL n ;
[ k , m ] in Indices DT ;
0 <= ( ( 1 / 2 ) GeoSeq ) . p ;
( ( F . N ) | EE ) . x = +infty ;
X c= Y & Z c= V implies X (\) V c= Y (\) Z
y `2 * z `2 <> 0. I ;
1 + card Xu <= card u ;
set g = Rotate ( z , S-max L~ z ) ;
k = 1 implies p . k = <% x , y %> . k ;
cluster -> total for Element of ( C ) -States ( X ) ;
reconsider B = A as non empty Subset of TOP-REAL n ;
let a , b , c be Function of Y , BOOLEAN ;
L1 . i = ( i .--> g ) . i .= g ;
plane ( x1 , x2 , x3 ) c= P ;
n <= indx ( D2 , D1 , j1 ) ;
( ( g2 ) . O ) `1 = - 1 ;
j + p .. f -' len f <= len f ;
set W = W-bound C , S = S-bound C , E = E-bound C , N = N-bound C ;
S1 . ( a9 , e9 ) = a + e .= a9 ;
1 in Seg width ( M * ( ColVec2Mx p ) ) ;
dom ( <i> (#) ( Im f ) ) = dom Im f ;
Phi ( x9 ) = W . ( a , *' ( a , p9 ) ) ;
set Q = SIGMA ( Foax ( g , f , h ) ) ;
cluster MSCongruence-like for MSEquivalence-like ManySortedRelation of U1 ;
for F st ( ex A st F = { A } ) holds F is discrete
reconsider zyMm = y - x as Element of product carr G ;
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 ) ;
E , j |= All ( x1 , x2 , 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 qsa = ( q , <* s *> ) -admissible ;
for x being element st x in X holds x in rng f1
h0 /. ( i + 1 ) = h0 . ( i + 1 ) ;
set mw = max ( B , InvLexOrder NAT ) ;
t in Seg width ( 1. ( K , n ) ) ;
reconsider X = findom C as Element of Fin NAT ;
IncAddr ( i , k ) = a =0_goto ( l + k ) ;
S-bound L~ f <= q `2 ;
R is condensed implies Int R is condensed & Cl R is condensed
0 <= a & a <= 1 & b <= 1 implies a * b <= 1
u in c /\ ( ( d /\ b ) /\ e ) /\ f /\ j ;
u in c /\ ( ( d /\ e ) /\ b ) /\ f /\ j ;
len C + ( - 2 ) >= 9 + ( - 3 ) ;
x , z , y is_collinear & x , z , x is_collinear ;
a |^ ( n1 + 1 ) = a |^ n1 * a ;
0* n in Line ( x , a * x ) ;
set xy = <* x , y *> , yc = <* y , c *> , xc = <* x , c *> ;
FF /. 1 in rng Line ( D , 1 ) ;
p . m orientedly_joins r /. m , r /. ( m + 1 ) ;
p `2 = ( f /. i1 ) `2 ;
W-bound ( X \/ Y ) = W-bound X ;
0 + p `2 <= 2 * r + p `2 ;
x in dom g & not x in g " { 0 } ;
f1 /* ( seq ^\ k ) is divergent_to+infty ;
reconsider u2 = u as VECTOR of RLSp_PFunct X ;
p |-count ( Product Sgm X11 ) = 0 ;
len <* x *> < i + 1 & i + 1 <= len c + 1 ;
assume that I is non empty and { x } (/\) { y } = [[0]] I ;
set ic4 = ( card I + 4 ) .--> goto 0 ;
x in { x , y } & h . x = {} TM ;
consider y being Element of F such that y in B and y <= x9 ;
len S = len the charact of A0 ;
reconsider m = M , i = I , n = N as Element of X ;
A . ( j + 1 ) = ( B . ( j + 1 ) \/ A . j ) ;
set Next = AP:NextBestEdges ( Gn ) , e = the Element of Next ;
rng F c= the carrier of gr { a } ;
IDEA_Q_F ( Key , n , r ) is FuncSequence ;
f . k in rng f & f . ( Euler n ) in rng f ;
h " P /\ [#] T1 = f " P ;
g in dom f2 \ f2 " { 0 } ;
g12X /\ dom f1 = g1 " X ;
consider n being element such that n in NAT and Z = G . n ;
set d1 = real_dist . ( x1 , y1 ) ;
b9 + 1 / 2 < 1 / 2 + 1 / 2 ;
reconsider f1 = f as VECTOR of R_VectorSpace_of_BoundedFunctions ( X , Y ) ;
i <> 0 implies i ^2 mod ( i + 1 ) = 1
j2 in Seg len ( g2 . i2 ) ;
dom ii = dom ia .= a ;
cluster sec | ]. PI / 2 , PI .] -> one-to-one ;
Ball ( u , e ) = Ball ( f . p , e ) ;
reconsider x1 = x0 as Function of S , If ;
reconsider R1 = x , R2 = y as auxiliary Relation of L ;
consider a , b being Subset of A such that x = [ a , b ] ;
( <* 1 *> ^ p ) ^ <* n *> in RT ;
S1 +* S2 = S2 +* S1 ;
exp_R * cos is_differentiable_on Z ;
cluster [. 0 , 1 .] -valued for Function of C , REAL ;
set Czx = 1GateCircStr ( <* z , x *> , f3 ) ;
EL2 . e2 = EL . e2 - T ;
arctan * ln is_differentiable_on Z ;
upper_bound A = PI * 3 / 2 & lower_bound A = 0 ;
F ?- dom f is_transformable_to F ?- cod f ;
reconsider pz = qz as Point of Euclid 2 ;
g . W in [#] Y0 & [#] Y0 c= [#] Y ;
let C be compact non vertical non horizontal Subset of TOP-REAL 2 ;
LSeg ( f ^ g , j ) = LSeg ( f , j ) ;
rng s c= dom f /\ left_open_halfline ( x0 ) ;
assume x in { idseq 2 , Rev idseq 2 } ;
reconsider n2 = n , m2 = m as Element of NAT ;
for y be ExtReal st y in rng seq holds g <= y
for k st P [ k ] holds P [ k + 1 ] ;
m = m1 + m2 .= ( m1 + m2 ) ;
assume for n holds H1 . n = G . n - H . n ;
set BB = f .: the carrier of X1 ;
ex d be Element of L st ( d in D ) & ( x << d ) ;
assume R -Seg ( a ) c= R -Seg ( b ) ;
t in ]. r , s .[ or t = r or t = s ;
z + v2 in W & x = u + ( z + v2 ) ;
x2 ==> y2 iff P [ x2 , y2 ] ;
x1 <> x2 implies |. x1 - x2 .| > 0
assume p2 - p1 , p3 - p1 are_lindependent2 ;
set p = nega ( f ^ <* A *> ) , q = ( nega f ) ^ <* 'not' A *> ;
REAL-NS n ;
( ( n mod ( 2 * k ) ) - k ) = ( n mod k ) ;
dom ( T * ( t succ ) ) = dom ( t succ )
consider x being element such that not ( x in wfp iff x in c ) ;
assume ( F * G ) . ( v . x3 ) = v . x4 ;
assume Terminals D1 c= Terminals D2 ;
reconsider A1 = [. a , b .[ as Subset of R^1 ;
consider y being element such that y in dom F and F . y = x ;
consider s being element such that s in dom o and a = o . s ;
set p = W-min L~ Cage ( C , n ) ;
n1 -' len f + 1 <= len g - 1 + 1 ;
Quadr ( q , O1 ) = [ u , v , a9 , b9 ] ;
set CK1 = ( MCS:CSeq ( G ) ) . ( k + 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 ) ;
set s3 = Comput ( P1 , s1 , k ) , P3 = P1 ;
let P be ( QC-pred_symbol of k , Al ( ) ) , l be QC-variable_list of k , Al ( ) ;
reconsider Ugg = Union GG as Subset-Family of TM ;
consider r such that r > 0 and Ball ( p9 , r ) c= Q9 ;
( h | ( n + 2 ) ) /. ( i + 1 ) = p29 ;
reconsider B = the carrier of X1 as Subset of X2 ;
pj1 = <% - csj1 , 1. L %> ;
attr f is natural-valued means : Def4 : rng f c= NAT ;
consider b being element such that b in dom F & a = F . b ;
x20 < card X0 + card Y0 ;
X c= B1 implies limpoints X c= succ B1
w in cl_Ball ( x , r ) implies dist ( x , w ) <= r
angle ( x , y , z ) = angle ( x - y , 0 , z - y )
1 <= len s implies Op-Shift ( s , 0 ) = s
f . ( k + ( n + 1 ) ) = f . ( k + n + 1 ) .= fkn1 ;
the carrier of (1). G = { 1_ G } ;
( p '&' q ) in HP_TAUT implies ( q '&' p ) in HP_TAUT
- t `1 < ( t `1 ) ^2 ;
US . 1 = US /. 1 .= Wmin ;
f .: the carrier of x = the carrier of x ;
Indices ONE = [: Seg n , Seg n :] ;
for n being Element of NAT holds G . n c= G . ( n + 1 ) ;
V in M -neighbour implies ex x being Element of M st V = { x }
ex f be Element of Fun st f is_a_unity_wrt ADD ;
[ h . 0 , h . 3 ] in the InternalRel of G ;
s +* Initialize ( ( intloc 0 ) .--> 1 ) = s3 ;
|[ w1 , v1 ]| - b <> 0. TOP-REAL 2 ;
reconsider t9 = t as Element of Funcs ( Funcs ( X , INT ) , INT ) ;
C \/ P c= [#] ( GX | ( [#] GX \ A ) ) ;
f " V in PSO X /\ D(alpha,ps) ( X ) ;
x in [#] ( the carrier of FT ) /\ ( A ^delta ) ;
g . x <= h1 . x & h . x <= h1 . x ;
InputVertices S = { xy , yz , zx } ;
for n being Nat st P [ n ] holds P [ n + 1 ] ;
set R = RLine ( M , i , a * Line ( M , i ) ) ;
assume that M1 is line_circulant & M2 is line_circulant and M3 is line_circulant ;
reconsider a = f4 . ( i0 -' 1 ) as Element of K ;
len B2 = Sum Len ( F1 ^ F2 ) ;
len Base_FinSeq ( n , i ) = n ;
dom ( max- ( f + g ) ) = dom ( f + g ) ;
( superior_realsequence seq ) . n = upper_bound Y1 ;
dom ( p1 ^ p2 ) = dom f12 ;
M . [ 1r , y ] = 1r * v1 .= y ;
assume that W is non trivial and W .edges() c= the_Edges_of G2 ;
Ci2 /. i1 = G1 * ( i1 , i2 ) ;
CY |- ( 'not' Ex ( x , p ) ) 'or' ( p . ( x , y ) ) ;
for b st b in rng g holds lower_bound rng f - a <= b
- ( q1 `1 / |. q1 .| ) = 1 ;
LSeg ( c , m ) \/ ml \/ LSeg ( l , k ) c= R ;
consider p being element such that p in south_halfline x and p in L~ f ;
Indices ( X @ ) = [: Seg n , Seg 1 :] ;
cluster ( s => ( q => p ) ) => ( q => ( s => p ) ) -> valid ;
( Im ( Partial_Sums F ) ) . m is_measurable_on E ;
redefine func f .. ( x1 , x2 , x ) -> Element of D ;
consider g being Function such that g = F . t & Q [ t , g ] ;
p in LSeg ( NW-corner Z , NE-corner Z ) ;
set RO = R^1 ( right_open_halfline ( b ) ) , LC = R^1 ( left_closed_halfline ( a ) ) ;
IncAddr ( I , k ) = SubFrom ( da , db ) ;
seq . m <= ( superior_realsequence seq ) . k ;
a + b = ( a ` *' b ` ) ` ;
id ( X /\ Y ) = id ( X ) /\ id ( Y )
for x being element st x in dom h holds h . x = f . x ;
reconsider H = U11 \/ U21 as non empty Subset of U0 ;
u in c /\ ( ( ( d /\ e ) /\ b ) /\ f ) /\ j /\ m ;
consider y being element such that y in Y and P [ y , inf B ] ;
consider A being finite StableSet of R such that card A = stability# R ;
p2 in rng ( f |-- p1 ) \ rng <* p1 *> ;
len s1 - 1 > 1 - 1 & len s2 - 1 > 1 - 1 ;
( NW-corner P ) `2 = N-bound P ;
Ball ( e , r ) c= LeftComp Cage ( C , k + 1 ) ;
( f . a1 ) ` = f . ( a1 ` ) ;
( seq ^\ k ) . n in left_open_halfline ( x0 ) ;
gg . s0 = ( g . s0 ) | ( G . s0 ) ;
the InternalRel of S is_asymmetric_in field the InternalRel of S
deffunc F ( Ordinal , Ordinal ) = phi ( $2 ) ;
( F . s1 ) . a1 = ( F . s2 ) . a1 ;
x9 = ( A ?. o ) . a .= Den ( o , A . a ) ;
Cl ( f " P1 ) c= f " ( Cl P1 ) ;
FinMeetCl the topology of S c= the topology of T ;
attr o is constructor means : Def11 : o <> * & o <> non_op ;
assume that nextcard X = nextcard Y and card X <> card Y ;
stabilization-time s <= 1 + stabilization-time s9 ;
LIN a , a1 , d or b , c // b1 , c1 ;
<e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 ;
then EQ in SS & not EQ in { NOR } ;
set TE = I -TermEval , u = TE . tt , J = ( l , u ) ReassignIn I , LH = I -TruthEval IT , RH = J -TruthEval phii ;
set A1 = GFA0AdderOutput ( ap , bp , cp ) ;
set cindm = [ <* cin , dm *> , and2c ] ;
x * z9 * x " in x * ( z * N ) * x " ;
for x being element st x in dom f holds f . x = g3 . x
right_cell ( f , 1 , G ) c= RightComp f \/ L~ f ;
UA is_an_arc_of W-min C , E-max C ;
set fg = ( C , f ) @ "/\" ( C , g ) @ , R = RealPoset [. 0 , 1 .] , J = C --> R ;
S1 is convergent & S2 is convergent implies S1 - S2 is convergent
f . ( 0 + 1 ) = ( 0 qua Ordinal ) +^ a .= a ;
cluster anti-pcs-like -> reflexive transitive pcs-tol-irreflexive pcs-tol-symmetric pcs-compatible for pcs-Str ;
consider d being element such that R reduces b , d and R reduces c , d ;
not b in dom Start-At ( ( card I + 2 ) , SCMPDS ) ;
( z + a ) + x = z + ( a + y ) .= ( z + a ) + y ;
len Subst ( l , ( A ) a. 0 .--> x ) = len l ;
tt null {} is ( {} \/ rng tt ) -valued FinSequence ;
t = <* F . t *> ^ ( ( C . p ) ^ qq ) ;
set pW = W-min L~ Cage ( C , n ) ;
kk -' ( i + 1 ) = kk - ( i + 1 ) ;
consider u9 being Element of L such that u = ( u9 ) % and u9 in D9 ;
len ( width bG |-> a ) = width bG ;
Fr . x in dom ( ( G * the_arity_of o ) . x ) ;
, cH1 = the carrier of H1 , cH2 = the carrier of H2 , cS = the carrier of S ;
, cH1 = the carrier of H1 , cH2 = the carrier of H2 , cS = the carrier of S ;
Comput ( P , s , 6 ) . intpos m = s . intpos m ;
IC Comput ( Q3 , t , k ) = ( lm + 1 ) ;
dom ( cos * sin ) = REAL ;
cluster <* l *> ^ phi -> ( 1 + Depth phi ) -wff for string of S ;
set bpcp = [ <* bp , cp *> , and2 ] ;
Line ( Segm ( M9 , P , Q ) , x ) = L * Sgm Q ;
n in dom ( ( the Sorts of A ) * ( the_arity_of o ) ) ;
cluster f1 + f2 -> continuous for PartFunc of REAL , the carrier of S ;
consider y be Point of X such that a = y & ||. x - y .|| <= r ;
set x3 = t8 . DataLoc ( s8 . SBP , 2 ) ;
set WHL = while<>0 ( a ( ) , i ( ) , I ( ) ) , pWH = stop WHL , pI = stop I ( ) ;
consider a being Point of D2 such that a in W1 and b = g . a ;
{ A , B , C , D , E } = { A , B } \/ { C , D , E } ;
let A , B , C , D , E , F , J , M be set ;
( |. p2 .| ) ^2 - ( p2 `2 ) ^2 >= 0 ;
( l -' 1 ) + 1 = ( n - 1 ) * lb + ( m - 1 ) + 1 ;
x = v + ( a * w1 + b * w2 ) + c * w3 ;
the TopStruct of L = ConvergenceSpace Scott-Convergence L ;
consider y being element such that y in dom H1 and x = H1 . y ;
fs \ { n } = code Free ( All ( v1 , H ) ) ;
for Y be Subset of X st Y is summable_set holds Y is weakly_summable_set
2 * n in { N : 2 * Sum ( p | N ) = N & N > 0 } ;
for s be FinSequence holds len ( Op-RightShift ( s ) ) = len s
for x st x in Z holds ( #R ( 1 / 2 ) ) * f is_differentiable_in x
rng ( h2 * f2 ) c= the carrier of R^1 ;
j + 1 - len f <= len f + ( len g - 1 ) - len f ;
reconsider R1 = R * I as PartFunc of REAL , REAL-NS n ;
Cs11 . x = s1 . a0 .= Cs21 . x ;
( power F_Complex ) . ( z , n ) = 1 .= x |^ n ;
t value_at ( C , s ) = f . ( the_array_sort_of S ) . t ;
support ( f + g ) c= support ( f ) \/ ( CX /\ support ( g ) ) ;
ex N st N = j1 & 2 * Sum ( rq | N ) > N ;
for y , p st P [ p ] holds P [ All ( y , p ) ]
{ [ x1 , x2 ] : not contradiction } is Subset of [: X1 , X2 :] ;
h = IFEQ ( i , j , h , ( id B ) . i ) .= H . i ;
ex x1 being Element of G st x1 = x & x1 * N c= A ;
set X = Quadr ( q , O1 ) `1_4 , Y = Quadr ( q , O1 ) `2_4 ;
b . n in { g1 : x0 < g1 & g1 < a1 . n } ;
f /* s1 is convergent & f /. x0 = lim ( f /* s1 ) ;
Domains_Lattice Y = Open_Domains_Lattice Y ;
( 'not' a . x '&' b . x ) 'or' ( a . x '&' 'not' b . x ) = FALSE ;
2k1 = len ( q0 ^ r1 ) + len q1 ;
( 1 / a ) (#) ( sec * f1 ) - id Z is_differentiable_on Z ;
set K1 = upper_integral ( lim ( H , AB ) || AB ) ;
assume e in { w1 / w2 : w1 in F & w2 in G } ;
reconsider da9 = dom a9 , dF9 = dom F9 as finite set ;
LSeg ( f :- q , j ) = LSeg ( f , j9 + q .. f ) ;
assume X in { T . ( N2 , K2 ) : h . K2 = N2 } ;
<: f , g :> * f1 = <: f , g :> * f2 ;
dom SN = dom S /\ Seg n .= dom LN ;
x in H |^ a iff ex g st x = g |^ a & g in H
( multint ( n ) ) . ( a , 1 ) = a9 - 0 * n .= a9 ;
D2 . ( j - 1 ) in { r : lower_bound A <= r & r <= D1 . i } ;
ex p being Point of TOP-REAL 2 st p = x & P [ p ] ;
( for c holds f . c <= g . c ) iff ( C , f ) @ <<= ( C , g ) @
dom ( f1 (#) f2 ) /\ X c= dom ( f1 (#) f2 ) ;
1 = ( p * p ) / p .= p * ( p / p ) .= p * 1 ;
len g = len f + len <* x + y *> .= len f + 1 ;
dom Fni1 = dom ( F | [: N1 , SS :] ) ;
dom ( f . t (#) I . t ) = dom ( f . t (#) g . t ) ;
assume a in ( "\/" ( F , ( T |^ the carrier of S ) ) ) .: D ;
assume that g is one-to-one and ( the carrier' of S ) /\ rng g c= dom g ;
( ( x \ y ) \ z ) \ ( ( x \ z ) \ ( y \ z ) ) = 0. X ;
consider f9 such that f * f9 = id b and f9 * f = id a ;
cos | [. 2 * PI * 0 , PI + 2 * PI * 0 .] is decreasing ;
Index ( p , co ) <= len LS - Gik .. LS ;
let t1 , t2 , t3 be Element of TermAlg S , s ;
Inf ( ( Frege curry H ) . h ) <= Inf Sups G ;
P [ f . i0 ] implies F ( f . ( i0 + 1 ) ) < j ;
Q [ [ D . x , 1 ] `1 , F . [ D . x , 1 ] ] ;
consider x being element such that x in dom ( F . s ) and y = F . s . x ;
l . i < r . i & [ l . i , r . i ] is Gap of G . i ;
the Sorts of A2 = ( the carrier of S2 ) --> BOOLEAN ;
consider s be Function such that s is one-to-one and dom s = NAT and rng s = F ;
dist ( b1 , b2 ) <= dist ( b1 , a ) + dist ( a , b2 ) ;
Lower_Seq ( C , n ) /. ( len Lower_Seq ( C , n ) ) = Wmi ;
q <= ( UMP Upper_Arc L~ Cage ( C , 1 ) ) `2 ;
LSeg ( f | i2 , i ) /\ LSeg ( f | i2 , j ) = {} ;
given a being ExtReal such that a <= IT and A = ]. a , IT .] ;
consider a , b being complex number such that z = a & y = b and z + y = a + b ;
set X = { b |^ n where n is Element of NAT : not contradiction } ;
( ( ( ( x * y ) * z ) \ x ) \ z ) \ ( ( x * y ) \ x ) = 0. X ;
set xyz = [ <* xy , yz , zx *> , f4 ] ;
lc /. ( len lc ) = lc . ( len lc ) ;
( q `2 / |. q .| - sn ) / ( 1 - sn ) = 1 ;
( p `2 / |. p .| - sn ) / ( 1 - sn ) < 1 ;
( S-max ( X \/ Y ) ) `2 = S-bound ( X \/ Y ) ;
( sp - sq ) . k = sp . k - sq . k ;
rng ( ( h + c ) ^\ n ) c= dom SVF1 ( 1 , f , u0 )
the carrier of ( X modified_with_respect_to X0 ) = the carrier of X ;
ex p4 st p3 = p4 & |. p4 - |[ a , b ]| .| = r ;
m = |. ar a .| , g = f | ( m -tuples_on AT ) , AF = AtomicFormulasOf S , ch = chi ( X , AF ) ;
( 0 * n ) iter R = Imf ( X , X ) .= 0 iter ( n iter R ) ;
( Partial_Sums ProjMap2 ( FF2 , n ) ) . n is nonnegative ;
f2 = Choice . EvalSet ( V , Kai , len ( H ) ) ;
S1 . b = s1 . b .= s2 . b .= S2 . b ;
p2 in LSeg ( p2 , p1 ) /\ LSeg ( p2 , p00 ) ;
dom ( f . t ) = Seg n & dom ( I . t ) = Seg n ;
assume o = In ( ( the connectives of S ) . 11 , the carrier' of S ) ;
psi = ( l1 , l2 ) -SymbolSubstIn phi , E1 = R#1 ( S ) , E2 = R#2 ( S ) , E5 = R#5 ( S ) ;
pred p is_monic_wrt T means : Def6 : HC ( p , T ) = 1. L ;
Y1 `2 = - 1 & 0. TOP-REAL 2 <> Y1 ;
defpred X [ Nat , set , set ] means P [ $2 , $3 ] ;
consider k be Nat such that for n be Nat st k <= n holds s . n < x0 + g ;
Det 1. ( K , m -' n ) = 1_ K ;
( - b - sqrt ( b ^2 - 4 * a * c ) ) / ( 2 * a ) < 0 ;
Cs2i1 . d = Cs2i . da mod Cs2i . db ;
X1 is everywhere_dense & X2 is everywhere_dense implies X1 meet X2 is everywhere_dense SubSpace of X
deffunc Fb ( Element of E , Element of I ) = $2 * $1 ;
t ^ <* n *> in { t ^ <* i *> : Q [ i , T9 . t ] } ;
( x \ y ) \ x = ( x \ x ) \ y .= y ` .= 0. X ;
for X being non empty set , Y being Subset-Family of X holds Y is Basis of TopStruct (# X , UniCl Y #) ;
pred A , B are_separated means : Def1 : Cl A misses B & A misses Cl B ;
len MR1 = len p & width MR1 = width MR ;
vp v = { x where x is Element of K : 0 < v . x } ;
( ( Sgm RelPrimes ( m ) ) . d ) - ( ( Sgm RelPrimes ( m ) ) . e ) <> 0 ;
lower_bound divset ( D2 , k + k2 ) = D2 . ( k + k2 - 1 ) ;
g . r1 = ( - 2 ) * r1 + 1 & dom h = [. 0 , 1 .] ;
|. a .| * ||. f .|| = 0 * ||. f .|| .= ||. a * f .|| ;
f . x = ( h . x ) `1 & g . x = ( h . x ) `2 ;
ex w st w in dom B1 & <* 1 *> ^ s = <* 1 *> ^ w ;
[ 1 , {} , <* d1 *> ] in { [ 0 , {} , {} ] } \/ S1 \/ S2 ;
IC Exec ( i , s1 ) + n = IC Exec ( i , s2 ) ;
IC Comput ( P , s , 1 ) = ICplusConst ( s , 9 ) .= ( 5 + 9 ) ;
IExec ( WH1 , Q , t ) . intpos me = t . intpos me ;
LSeg ( ( f -: q ) , i ) misses LSeg ( f :- q , j ) ;
for x , y being Element of L st x in C & y in C holds x <= y or y <= x ;
integral ( f `| X , C ) = f . ( upper_bound C ) - f . ( lower_bound C ) ;
for F , G being one-to-one FinSequence st rng F misses rng G holds F ^ G is one-to-one
||. R /. ( L . h ) .|| < e1 * ( ( K + 1 ) * ||. h .|| ) ;
assume a in { q where q is Element of M : dist ( z , q ) <= r } ;
[ 2 , 1 ] .--> [ 2 , 0 , 1 ] , f = id ( [: SegM 3 , { 0 , 1 } :] , { - 1 , 0 , 1 } , 0 ) ;
consider x , y being Subset of X such that [ x , y ] in F and x c= d and not y c= d ;
for y9 , x9 being Element of REAL+ st y9 in Y9 & x9 in X9 holds y9 <=' x9
func index p -> QC-symbol of A equals min NBI p ;
consider t9 being Element of S such that x9 , y9 '||' z9 , t9 & x9 , z9 '||' y9 , t9 ;
dom x1 = Seg len x1 & len x1 = len l1 ;
consider y2 be Real such that x2 = y2 and 0 <= y2 & y2 < 1 / 2 ;
||. ( f | X ) /* s1 .|| = ( ( ||. f .|| ) | X ) /* s1 ;
( the InternalRel of A ) -Seg ( x9 ) /\ Y = {} \/ {} .= {} ;
i + 1 in dom p ;
reconsider h = f | X ( ) as Function of X ( ) , rng ( f | X ( ) ) ;
u1 in the carrier of W1 & u2 in the carrier of W2 ;
defpred P [ Element of L ] means M is_<=_than f . $1 & f . $1 <= $1 ;
Tern ( u , a , v ) = s * x + ( ( - s * x ) + y ) .= b ;
- ( x - y ) = - x + - - y .= - x + y ;
given a being Point of GX such that for x being Point of GX holds a , x are_joined ;
ff2 = [ [ dom ( @ f2 ) , cod ( @ f ) ] , h2 ] ;
for k , n be Nat holds k <> 0 & k < n & n is prime implies k , n are_relative_prime
for x being element holds x in A ^d iff x in ( ( A ` ) ^f ) `
consider u , v being Element of R , a being Element of A such that l /. i = u * a * v ;
1 - ( ( p `1 / |. p .| - cn ) / ( 1 + cn ) ) ^2 > 0 ;
LF . k = LS . ( F . k ) & F . k in dom LS ;
set i1 = ( a , i ) <=0_goto ( card I + 3 ) , i2 = AddTo ( a , i , - n ) , i3 = goto - ( card I + 2 ) ;
B is quantifiable implies CQCSub_the_scope_of ( CQCSub_All ( B , SQ ) ) = B `1
aa "/\" D = { a "/\" d where d is Element of N : d in D } ;
absreal . ( q29 - q19 ) * absreal . b9 >= absreal . b9
( - f ) . ( upper_bound A ) = ( ( - f ) | A ) . ( upper_bound A ) ;
Gik `1 = Ga * ( len Ga , k ) `1 ;
Proj ( i , n ) . Ldiff = <* proj ( i , n ) . Ldiff *> ;
( f1 + f2 ) * reproj ( i , x ) is_differentiable_in proj ( i ) . x ;
for x be Real st cos . x <> 0 holds tan . x = tan x
ex t being SortSymbol of S st t = s & h1 . t . x = h2 . t . x ;
defpred C [ Nat ] means PSI ( $1 ) is Consistent & PSI ( $1 ) is Al2 -Consistent ;
consider y being element such that y in dom pe and qe . i = pe . y ;
reconsider L = product ( { x1 } +* ( indx B , l ) ) as Block of Segre_Product A ;
for c being Element of C ex d being Element of D st T . id c = id d ;
Ins ( f , n , p ) = ( f | n ) ^ <* p *> .= f ^ <* p *> ;
( f * g ) . x = f . ( g . x ) & ( f * h ) . x = f . ( h . x ) ;
p in { 1 / 2 * ( G * ( i + 1 , j ) + G * ( i + 1 , j + 1 ) ) } ;
f9 - cp = f - c | ( n , L ) *' ( f - g ) .= f - c * ( f - g ) ;
consider r be Real such that r in rng ( f | divset ( D , j ) ) and r < m + s ;
f1 . ( |[ r8 `1 , r8 `2 ]| ) in f1 .: W5 ;
eval ( a | ( n , L ) , x ) = coefficient ( a | ( n , L ) ) .= a ;
z = DigB ( tx , xx ) .= DigA ( tx , xx ) ;
set H = { Intersect S where S is Subset-Family of X : S c= G } ;
consider S19 being Element of j -tuples_on D9 , d9 such that S9 = S19 ^ <* d9 *> ;
assume that x1 in dom f and x2 in dom f & f . x1 = f . x2 ;
- 1 <= ( ( q `2 / |. q .| - sn ) ) / ( 1 + sn ) ;
ZeroLC ( V ) is Linear_Combination of A & Sum ( ZeroLC ( V ) ) = 0. V ;
let k1 , k2 , k3 , k4 , k5 be Instruction of SCM+FSA ;
consider j be element such that j in dom a and j in g " { k9 } and x = a . j ;
H1 . x1 c= H1 . x2 or H1 . x2 c= H1 . x1 ;
consider a being Real such that p = ( 1 - a ) * p1 + a * p2 and 0 <= a and a <= 1 ;
assume that a <= c & c <= d & d <= b and [' a , b '] c= dom f & [' a , b '] c= dom g ;
cell ( Gauge ( C , m ) , X-SpanStart ( C , m ) -' 1 , 0 ) is non empty ;
Aq2 in { ( S . i ) `1 where i is Element of NAT : not contradiction } ;
( T * b1 ) . y = L * ( b2 /. Lb ) .= ( F9 * b1 ) . y ;
g . ( s , I ) . x = s . y & g . ( s , I ) . y = |. s . x - s . y .| ;
( log ( 2 , k + k ) ) ^2 >= ( log ( 2 , k + 1 ) ) ^2 ;
p => q in S & not x in still_not-bound_in p implies p => All ( x , q ) in S ;
dom ( the Tran of rtfsm1 ) misses dom ( the Tran of rtfsm2 ) ;
attr f is e.i.-valued means : Def3 : for x being set st x in rng f holds x is ext-integer ;
for X being Subset-Family of D holds f . ( f .: X ) = f . ( union X ) ;
i = len p1 .= len p3 + len <* x *> .= len p3 + 1 ;
l `1_3 = g `1_3 + k `1_3 - e `1_3 ;
CurInstr ( P2 , Comput ( P2 , s2 , l2 ) ) = halt SCM+FSA ;
assume ( for n being Nat holds ||. seq .|| . n <= Rseq . n ) & Rseq is summable ;
sin ( r - s ) = ( sin r ) * ( cos s ) - ( cos r ) * ( sin s ) .= 0 ;
set q = |[ diff ( g1 , t0 ) , diff ( g2 , t0 ) , diff ( g3 , t0 ) ]| ;
consider G being sequence of S such that for n being Element of NAT holds G . n in MeasPart ( F . n ) ;
consider G such that F = G and ex G1 st G1 in SN1 & G = 'X' G1 ;
root-tree [ x , s ] in ( the Sorts of Free ( C , X ) ) . s ;
Z c= dom ( ( #R ( 3 / 2 ) ) * ( f + ( exp_R * f1 ) ) ) ;
for k be Element of NAT holds rseqi . k = ( middle_sum ( ( Im f ) , Si ) ) . k
assume that - 1 < cn and q `2 > 0 and q `1 / |. q .| < cn ;
assume that f is continuous one-to-one and a < b and c < d & f = g & f . a = c & f . b = d ;
consider r being Element of NAT such that sm = Comput ( P1 , s1 , r ) and r <= q ;
LE f /. ( i + 1 ) , f /. j , L~ f , f /. 1 , f /. len f ;
assume that x in the carrier of K and y in the carrier of K and ex_inf_of { x , y } , L ;
assume f +* ( i1 , xi1 ) in proj ( F , i2 ) " Ai2 ;
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 : not contradiction } ;
consider l be Nat such that for m be Nat st l <= m holds ||. s1 . m - x0 .|| < g ;
consider t being VECTOR of product G such that mt = ||. DD . t .|| & ||. t .|| <= 1 ;
branchdeg v = 2 implies v ^ <* 0 *> in dom p & v ^ <* 1 *> in dom p
consider a being Element of the Points of XX , A being Element of the Lines of XX such that not a on A ;
( ( - x ) |^ ( k + 1 ) ) * ( ( ( - x ) |^ ( k + 1 ) ) " ) = 1
for D being set holds ( for i st i in dom p holds p . i in D ) implies p is FinSequence of D
defpred R [ element ] means ex x , y st [ x , y ] = $1 & P [ x , y ] ;
L~ f2 = union { LSeg ( p0 , p10 ) , LSeg ( p10 , p1 ) } ;
i -' len h11 + 2 -' 1 < i -' len h11 + 2 - 1 + 1 ;
for n be Element of NAT st n in dom F holds F . n = |. np . ( n -' 1 ) .|
for r , s1 , s2 holds r in [. s1 , s2 .] iff s1 <= r & r <= s2
assume v in { G where G is Subset of T2 : G in B2 & G c= z1 } ;
let g be Euclidean ExecutionFunction of A , Funcs ( X , INT ) , Funcs ( X , INT ) \ ( b , 0 ) ;
min ( g . [ x , y ] , k . [ y , z ] ) = min ( g , k , x , z ) . y ;
consider q1 be sequence of CNS such that for n holds P [ n , q1 . n ] from FUNCT_2 : sch 3 ( A4 ) ;
consider f being Function such that dom f = NAT & for n being Element of NAT holds f . n = F ( n ) ;
set Z = B \ A , O = A /\ B , f = B --> 0 , g = O --> 1 , IT = chi ( A , B ) ;
consider j be Element of NAT such that x = Base_FinSeq ( n , j ) and 1 <= j & j <= n ;
consider x such that z = x & card ( x . O2 ) in card ( x . O ) & x in L1 ;
( C * Special_Function4 ( k , n2 ) ) . 0 = C . ( ( Special_Function4 ( k , n2 ) ) . 0 ) ;
dom ( X --> rng f ) = X & dom rngs ( X --> f ) = dom ( X --> f ) ;
S-bound L~ SpStSeq C <= b `2 & b `2 <= N-bound L~ SpStSeq C ;
pred x , y are_collinear means : Def1 : x = y or ex l being Block 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 ;
holds x << y iff a << b ;
( 1 / ( 2 * ( m - n ) ) ) (#) ( sin * AffineMap ( m - n , 0 ) ) is_differentiable_on REAL ;
defpred P [ Element of omega ] means ( Partial_Union A1 ) . $1 = A1 . $1 ;
IC Comput ( P , s , 2 ) = succ IC Comput ( P , s , 1 ) .= ( 6 + 1 ) ;
f . x = f . g1 * f . g2 .= f . g1 * 1_ H .= f . g1 ;
( M * Fm ) . n = M . ( Fm . n ) .= M . { ( canFS ( Omega ) ) . n } ;
Carrier ( L1 + L2 ) c= Carrier ( L1 ) \/ Carrier ( L2 ) ;
trap a , b , c , x , o & trap a , b , c , y , o implies x = y
( ( Partial_Product s ) . n ) <= ( ( Partial_Product s ) . n ) * ( s . ( n + 1 ) ) ;
- 1 <= r & r <= 1 implies diff ( arccot , r ) = - 1 / ( 1 + r ^2 )
sp in { p ^ <* n *> where n is Nat : p ^ <* n *> in T1 } ;
|[ x1 , x2 , x3 ]| . 2 - |[ y1 , y2 , y3 ]| . 2 = x2 - y2 ;
for F be Functional_Sequence of X , REAL st ( for m be Nat holds F . m is nonnegative ) holds for m be Nat holds ( Partial_Sums F ) . m is nonnegative
len normsequence ( G , z ) = len ( normsequence ( G , xx ) + normsequence ( G , yy ) ) ;
consider u , v being VECTOR of V such that x = u + v and u in W1 /\ W2 & v in W2 /\ W3 ;
given F be XFinSequence of NAT such that F = x and dom F = n & rng F c= { 0 , 1 } & Sum F = k ;
0 = lambda * mu * nu - q iff 1 = ( lambda / ( 1 - lambda ) ) * ( ( mu * nu ) / ( ( 1 - mu ) * ( 1 - nu ) ) ) ;
consider n be Nat such that for m be Nat st n <= m holds |. ( f # x ) . m - lim ( f # x ) .| < e ;
cluster satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 properly_defined -> Boolean Lattice-like for non empty ShefferOrthoLattStr ;
"/\" ( {} , BS ) = Top BS .= the carrier of S .= [#] S .= "/\" ( {} , InIdsS ) ;
( r / 2 ) ^2 + ( rm / 2 ) ^2 <= ( r / 2 ) ^2 + ( r / 2 ) ^2 ;
for x being element st x in A /\ dom ( ( f `| X ) || A ) holds ( ( f `| X ) || A ) . x >= r2
( 2 * r1 - 1 ) * |[ a , c ]| - ( ( 2 * r1 - 1 ) * |[ b , c ]| ) = 0. TOP-REAL 2 ;
reconsider p = Col ( P , 1 ) , q = a " * ( Base_FinSeq ( K , n , 1 ) ) as FinSequence of K ;
consider x1 , x2 being element such that x1 in wayabove s and x2 in wayabove t and x = [ x1 , x2 ] ;
for n be Nat st 1 <= n & n <= len q1 holds q1 . n = lower_volume ( g , MD1 ) . 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 ] ;
given H1 , H2 being strict Subgroup of G such that x = H1 and y = H2 & H1 is Subgroup of H2 ;
for S , T being non empty Poset , d being Function of T , S st T is complete holds d is sups-preserving iff d is monotone & d is lower_adjoint
[ [** a , 0 **] , b2 ] in [: the carrier of F_Complex , the carrier of V :] ;
reconsider maxFq = max ( len F1 , len ( p . n * ( <% x %> `^ n ) ) ) as Element of NAT ;
I <= width GoB ( Incr ( X_axis ( h ) ) , Incr ( Y_axis ( h ) ) ) ;
f2 /* q = ( f2 /* ( f1 /* s ) ) ^\ k .= ( ( f2 * f1 ) /* s ) ^\ k ;
A1 \/ A2 is linearly-independent & A1 misses A2 implies Lin A1 /\ Lin A2 = (0). V
func A -carrier_of C -> set equals union { A . s where s is Element of R : s in C } ;
dom ( mlt ( Line ( v , i + 1 ) , Col ( mConv ( p , m ) , 1 ) ) ) = dom ( F ^ G ) ;
reduce [ x `1_4 , x `2_4 , x `3_4 , x `4_4 ] to x ;
E |= All ( x1 , All ( x2 , x2 'in' x0 <=> x2 'in' x1 ) => x0 '=' x1 ) ;
F .: ( id X , g ) . x = F . ( id X . x , g . x ) .= F . ( x , g . x ) ;
R . ( h . m ) = F . ( x0 + In ( h . m , REAL ) ) - F . x0 - L . In ( h . m , REAL ) ;
cell ( G , XS -' 1 , YS + ( t + 1 ) ) \ L~ f meets UBD L~ f ;
IC Result ( P2 , s2 ) = IC IExec ( I , P , Initialize s ) .= card I ;
sqrt ( 1 - ( - ( q `1 / |. q .| - cn ) ) ^2 / ( 1 + cn ) ^2 ) > 0 ;
consider x0 be element such that x0 in dom a and x0 in g " { k9 } and y0 = a . x0 ;
dom ( r1 (#) chi ( A . m , C ) ) = dom chi ( A . m , C ) .= C ;
dy . [ y , z ] = [ y , z ] `1 `2 - [ y , z ] `2 `2 ;
for A , B , C being SetSequence of the carrier of TOP-REAL 2 st for i being Nat holds C . i = A . i /\ B . i holds Lim_sup C c= Lim_sup A /\ Lim_sup B
x0 in dom f & f is_continuous_in x0 implies ||. f .|| is_continuous_in x0 & - f is_continuous_in x0
for T being non empty TopStruct , A being Subset of T , p being Point of T holds p in Cl A iff for K being Basis of p , Q being Subset of T st Q in K holds A meets Q
for x being Element of REAL n st x in Line ( x1 , x2 ) holds |. y1 - y2 .| <= |. y1 - x .|
func first_epsilon_greater_than a -> epsilon Ordinal means : Def6 : a in it & for b being epsilon Ordinal st a in b holds it c= b ;
[ a1 , a2 , a3 ] in [: the carrier of A , the carrier of A , the carrier of A :] ;
ex a , b being element st a in the carrier of S1 & b in the carrier of S2 & x = [ a , b ] ;
||. ( vseq . n ) - ( vseq . m ) .|| * ||. x .|| < e / ||. x .|| * ||. x .|| ;
( for Z be set holds Z in { Y where Y is Element of InIdS : F c= Y } implies z in Z ) implies z in x
sup compactbelow [ s , t ] = [ sup proj1 compactbelow [ s , t ] , sup proj2 compactbelow [ s , t ] ] ;
consider i , j being Element of NAT such that i < j and [ y , f . j ] in IR and [ f . i , z ] in IR ;
for D being non empty set , p , q being FinSequence of D st p c= q holds ex p9 being FinSequence of D st p ^ p9 = q
consider e19 be Element of Af ( X ) such that c39 , a39 // a29 , e19 and a29 <> e19 ;
set E = TheEqSymbOf S , p = SubTerms phi , F = S -firstChar , s = F . phi , UV = I -TermEval , V = I -AtomicEval phi , d = U -deltaInterpreter , U2 = 2 -tuples_on U , TT = AllTermsOf S , D = { <* u , u *> where u is Element of U : not contradiction } , n = |. ar s .| ;
( |. q4 .| ) ^2 = ( q4 `1 ) ^2 + ( q4 `2 ) ^2 .= ( |. q .| ) ^2 ;
for T being non empty TopSpace , x , y be Element of InclPoset the topology of T holds x "\/" y = x \/ y & x "/\" y = x /\ y
dom signature U1 = dom the charact of U1 & Args ( o , MSAlg U1 ) = dom O1 ;
dom ( h | X ) = dom h /\ X .= dom abs ( h ) /\ X .= dom ( abs ( h ) | X ) ;
for N1 for K1 being Element of GT1 holds dom ( h . K1 ) = N & rng ( h . K1 ) = K1
( mod ( u , m ) + mod ( v , m ) ) . i = ( mod ( u , m ) . i ) + ( mod ( v , m ) . i ) ;
- q `1 < - 1 or q `2 >= q `1 & q `2 <= - q `1 ;
for r1 , r2 being Real , fr1 , fr2 being Element of F_Real st r1 = fr1 & r2 = fr2 holds r1 * r2 = fr1 * fr2 ;
vseq . m is bounded Function of X , the carrier of Y & xseq . m = modetrans ( ( vseq . m ) , X , Y ) . x ;
a <> b & b <> c & angle ( a , b , c ) = PI implies angle ( b , c , a ) = 0 & angle ( c , a , b ) = 0
consider i , j being Nat , r , s being Real such that p1 = [ i , r ] and p2 = [ j , s ] and i < j & r < s ;
( |. p .| ^2 - 2 * |( p , q )| + |. q .| ^2 ) = ( |. p .| ^2 + |. q .| ^2 - 2 * |( p , q )| ) ;
consider p1 , q1 be Element of X ( ) * such that y = p1 ^ q1 and q1 ^ p1 = pq ;
mult2 ( r1 , r2 , s1 , s2 , Amp ) = s2 / gcd ( r1 , s2 , Amp ) ;
( LMP A ) `2 = lower_bound ( proj2 .: ( A /\ Vertical_Line w ) ) & proj2 .: ( A /\ Vertical_Line w ) is non empty ;
s , kai |= H1 EU H2 iff s |= Evaluate ( H1 , kai ) EU Evaluate ( H2 , kai ) ;
len sb1 + 1 = ( card ( support b1 ) + 1 ) .= card ( support b2 ) .= len sb2 ;
consider z being Element of L1 such that z >= x & z >= y and for z9 being Element of L1 st z9 >= x & z9 >= y holds z9 >= z ;
LSeg ( UMP D , |[ ( W-bound D + E-bound D ) / 2 , N-bound D ]| ) /\ D = { UMP D }
lim ( ( ( f `| N ) / ( g `| N ) ) /* b ) = lim ( ( ( f `| N ) / ( g `| N ) ) , x0 ) ;
P [ i , ( pr1 f ) . i , ( pr2 f ) . i , ( pr1 f ) . ( i + 1 ) , ( pr2 f ) . ( i + 1 ) ] ;
for r be Real st 0 < r ex m be Nat st for k be Nat st m <= k holds ||. ( seq1 . k ) - RNg .|| < r
for X being set , P being a_partition of X , x , a , b being set st x in a & a in P & x in b & b in P holds a = b ;
Z c= dom exp_R /\ ( dom ( exp_R * f ) \ ( exp_R * f ) " { 0 } ) ;
ex j being Nat st j in dom ( l ^ <* x *> ) & j < i & y = ( l ^ <* x *> ) . j
for u , v being VECTOR of V , r being Real st 0 < r & r < 1 & u in M - N & v in M - N holds r * u + ( 1 - r ) * v in M - N
A , Int A , Cl A , Int Cl A , Cl Int A , Cl Int Cl A , Int Cl Int A are_mutually_different ;
- Sum <* v , u , w *> = - ( v + u + w ) .= ( - ( v + u ) ) - w .= ( ( - v ) - u ) - w ;
Exec ( a := b , s ) . IC SCM R = Exec ( a := b , s ) . NAT .= succ IC s ;
consider h being Function such that f . a = h and dom h = I and for x being element st x in I holds h . x in ( Carrier J ) . x ;
for S1 , S2 being non empty reflexive RelStr for D being non empty directed Subset of [: S1 , S2 :] holds proj1 D is directed & proj2 D is directed
card X = 2 iff ex x , y st x in X & y in X & x <> y & for z st z in X holds z = x or z = y
E-max L~ Cage ( C , n ) in rng Rotate ( Cage ( C , n ) , W-min L~ Cage ( C , n ) ) ;
for T , T9 being DecoratedTree , p , q being Element of dom T st not p is_a_prefix_of q holds ( T with-replacement ( p , T9 ) ) . q = T . q
[ i2 + 1 , j2 ] in Indices G & [ i2 , j2 ] in Indices G & f /. k = G * ( i2 + 1 , j2 ) ;
redefine func k lcm n means : Def4 : k divides it & n divides it & for m being Nat st k divides m & n divides m holds it divides m ;
dom ( F " ) = the carrier of X2 & rng ( F " ) = the carrier of X1 & F " is one-to-one ;
consider C being finite Subset of V such that C c= A and card ( C ) = n - m and the VectSpStr of V = Lin ( Bv \/ C ) ;
for T being non empty TopSpace , V being Element of InclPoset the topology of T holds V is prime iff for X , Y being Element of InclPoset the topology of T st X /\ Y c= V holds X c= V or Y c= V
set X = { F ( v1 ) where v1 is Element of B ( ) : P [ v1 ] } , Y = { G ( v2 ) where v2 is Element of B ( ) : P [ v2 ] } ;
angle ( p1 , p3 , p4 ) = 0 .= angle ( p2 , p3 , p2 ) .= angle ( p , p3 , p2 ) ;
- sqrt ( 1 - ( ( q `1 / |. q .| - cn ) / ( 1 - cn ) ) ^2 ) = - sqrt ( 1 - 0 ) .= - 1 ;
ex f being Function of I[01] , TOP-REAL 2 st f is continuous one-to-one & rng f = P & f . 0 = p1 & f . 1 = p3 ;
for u0 being Element of REAL 3 holds f is_hpartial_differentiable`12_in u0 implies SVF1 ( 2 , pdiff1 ( f , 1 ) , u0 ) is_continuous_in proj ( 2 , 3 ) . u0 ;
ex r , s st x = |[ r , s ]| & G * ( len G , 1 ) `1 < r & s < G * ( 1 , 1 ) `2 ;
for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= len G holds G * ( t , width G ) `2 >= N-bound L~ f
for i be set st i in dom G holds r (#) ( f * reproj ( modetrans ( G , i ) , x ) ) = ( r (#) f ) * reproj ( modetrans ( G , i ) , x )
consider c1 , c2 being bag of o1 +^ o2 such that ( decomp c ) /. k = <* c1 , c2 *> and c = c1 + c2 ;
u0 in { |[ r1 , s1 ]| : r1 < G * ( 1 , 1 ) `1 & s1 < G * ( 1 , 1 ) `2 } ;
carr ( X ^ Y ) . k = the carrier of ( X . k2 ) .= CX . k .= ( CX ^ CY ) . k ;
for K being Field , M1 , M2 being Matrix of K st len M1 = len M2 & width M1 = width M2 holds M1 = M1 - ( M2 - M2 )
consider g2 be Real such that 0 < g2 and { y where y is Point of S : ||. y - x0 .|| < g2 } c= N2 ;
assume x < ( - b + sqrt delta ( a , b , c ) ) / ( 2 * a ) or x > ( - b - sqrt delta ( a , b , c ) ) / ( 2 * a ) ;
( G1 '&' G2 ) . i = ( <* 3 *> ^ G1 ) . i & ( H1 '&' H2 ) . i = ( <* 3 *> ^ H1 ) . i ;
for i , j st [ i , j ] in Indices ( M3 + M1 ) holds ( M3 + M1 ) * ( i , j ) < M2 * ( i , j )
for f being FinSequence of NAT , i being Element of NAT st for j being Element of NAT st j in dom f holds i divides f /. j holds i divides Sum f
assume F = { [ a , b ] where a , b is Subset of X : for c being set st c in BB & a c= c holds b c= c } ;
b2 * q2 + b3 * q3 + - a02 * q2 + - a03 * q3 = 0. TOP-REAL n ;
Cl Cl F = { D where D is Subset of T : ex B being Subset of T st D = Cl B & B in Cl F } ;
seq1 is summable & seq2 is summable implies seq1 + seq2 is summable & Sum ( seq1 + seq2 ) = Sum ( seq1 ) + Sum ( seq2 )
dom ( ( Sq_Circ " ) | D ) = ( the carrier of ( TOP-REAL 2 ) ) /\ D .= the carrier of ( ( TOP-REAL 2 ) | D ) ;
oContMaps ( X , Z ) is directed-sups-inheriting full non empty SubRelStr of ( Omega Z ) |^ the carrier of X & oContMaps ( X , Y ) is directed-sups-inheriting full SubRelStr of ( Omega Z ) |^ the carrier of X ;
G * ( 1 , j ) `2 = G * ( i , j ) `2 & G * ( 1 , j ) `1 <= G * ( i , j ) `1 ;
pred m1 c= m2 means : Def3 : for p being set st p in P holds m1 multitude_of p <= m2 multitude_of p ;
consider a being Element of B ( ) such that x = F ( a ) and a in { G ( b ) where b is Element of A ( ) : P [ b ] } ;
struct ( OneStr , multMagma ) multLoopStr (# carrier -> set , multF -> BinOp of the carrier , OneF -> Element of the carrier #) ;
GenFib ( a , b , 1 ) + GenFib ( c , d , 1 ) = b + GenFib ( c , d , 1 ) .= b + d .= GenFib ( a + c , b + d , 1 ) ;
redefine func addint means for i1 , i2 being Element of INT holds it . ( i1 , i2 ) = addreal . ( i1 , i2 ) ;
( 1 - s2 ) * p1 + ( s2 * p2 - s2 * p2 ) = ( 1 - r2 ) * p1 + r2 * p2 - s2 * p2 ;
eval ( ( a | ( n , L ) ) *' p , x ) = eval ( a | ( n , L ) , x ) * eval ( p , x ) .= a * eval ( p , x ) ;
Omega S & for V being open Subset of S st sup D in V holds D meets V ;
assume 1 <= k & k <= len w + 1 implies Tf . ( ( q11 , w ) -admissible . k ) = ( Tf . q11 , w ) -admissible . k ;
2 * a |^ ( n + 1 ) + 2 * b |^ ( n + 1 ) >= a |^ ( n + 1 ) + a |^ n * b + b |^ n * a + b |^ ( n + 1 ) ;
M , v2 |= All ( x. 3 , Ex ( x. 0 , All ( x. 4 , H1 <=> x. 4 '=' x. 0 ) ) ) ;
assume that f is_differentiable_on l and ( for x0 st x0 in l holds 0 < diff ( f , x0 ) ) or for x0 st x0 in l holds diff ( f , x0 ) < 0 ;
for G1 being _Graph , W being Walk of G1 , e being set , G2 being removeEdge of G1 , e st not e in W .edges() holds W is Walk of G2
c02 is not empty iff x2y0 is not empty & x1y1 is not empty or x1y1 is not empty & x0y2 is not empty or x0y2 is not empty & x2y0 is not empty ;
Indices GoB f = [: dom GoB f , Seg width GoB f :] & i1 + 1 in dom GoB f ;
for G1 , G2 , G3 being GroupWithOperators of O holds G1 is StableSubgroup of G2 & G2 is StableSubgroup of G3 implies G1 is StableSubgroup of G3
for f being FinSeq-Location holds UsedIntLoc ( insert-sort f ) = { intloc 0 , intloc 1 , intloc 2 , intloc 3 , intloc 4 , intloc 5 , intloc 6 }
for f1 , f2 be FinSequence of F st f1 ^ f2 is p -element & Q [ f1 ^ f2 ] holds Q [ f2 ^ f1 ]
p `1 / sqrt ( 1 + ( p `1 / p `2 ) ^2 ) = q `1 / sqrt ( 1 + ( q `2 / q `1 ) ^2 ) ;
for x1 , x2 , x3 being Element of REAL n holds |( x1 - x2 , x3 )| = |( x1 , x3 )| - |( x2 , x3 )|
for x st x in dom ( ( F - G ) | A ) & - x in dom ( ( F - G ) | A ) holds ( F - G ) | A . ( - x ) = - ( F - G ) | A . x
for T being non empty TopStruct , P being Subset-Family of T st P c= the topology of T & for x being Point of T ex B being Basis of x st B c= P holds P is Basis of T
( ( a 'or' b ) 'imp' c ) . x = 'not' ( a 'or' b ) . x 'or' ( c ) . x .= 'not' ( ( a ) . x 'or' ( b ) . x ) 'or' ( c ) . x .= TRUE '&' TRUE .= TRUE ;
for e be set st e in AA ex X1 being Subset of XV , Y1 being Subset of Y st e = [: X1 , Y1 :] & X1 is open & Y1 is open
for i be set st i in the carrier of S for f be Function of SA . i , S1 . i st f = H . i holds F . i = f | ( FG . i ) ;
for v , w st for y st x <> y holds w . y = v . y holds Valid ( VERUM ( Al ) , J ) . v = Valid ( VERUM ( Al ) , J ) . w
card D = card D1 + card D1 - card { { i , j } } .= ( c1 + 1 ) + ( c1 + 1 ) - 1 .= 2 * c1 + 1 ;
IC Exec ( i , s ) = ( s +* ( 0 .--> succ ( s . 0 ) ) ) . 0 .= ( 0 .--> succ ( s . 0 ) ) . 0 .= succ ( IC s ) ;
len ( f /^ ( i1 -' 1 ) ) -' 1 + 1 = len ( f /^ ( i1 -' 1 ) ) - 1 + 1 .= len ( f /^ ( i1 -' 1 ) ) ;
for a , b , c being Element of NAT st 1 <= a & 2 <= b holds k < a - 1 or a <= k & k <= a + b - 3 or k = a + b - 2 or a + b - 2 < k or k = a - 1
for f being FinSequence of TOP-REAL 2 , p being Point of TOP-REAL 2 , i being Element of NAT st p in LSeg ( f , i ) holds Index ( p , f ) <= i
lim ( ( ProjMap2 ( PP2 , k + 1 ) ) # x ) = lim ( ( ProjMap2 ( PP2 , k ) ) # x ) + lim ( ( ProjMap1 ( FF2 , k + 1 ) ) # x ) ;
z2 = ( g /^ n1 ) . ( i -' n2 + 1 ) .= g . ( i -' n2 + 1 + n1 ) .= g . ( i -' n2 + n1 + 1 ) ;
[ f . 0 , f . 3 ] in id ( the carrier of G ) \/ ( the InternalRel of G ) or [ f . 0 , f . 3 ] in the InternalRel of CmpG ;
for G being Subset-Family of B st G = { R .:^ X where R is Subset of [: A , B :] : R in FR } holds ( Intersect FR ) .:^ X = Intersect G
CurInstr ( P1 , Comput ( P1 , s1 , m1 + m2 ) ) = CurInstr ( P1 , Comput ( P1 , s2 , m2 ) ) .= halt SCMPDS ;
( not p on P ) & not p on Q & M <> N ;
for T st T is T_4 & T is Lindelof & ex F be Subset-Family of T st F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= 0 holds T is finite-ind & ind T <= 0
for g1 , g2 st g1 in ]. rr - 1 , r .[ & g2 in ]. rr - 1 , r .[ holds |. f . g1 - f . g2 .| <= ( g1 - g2 ) ^2 ;
cosh_C /. ( z1 + z2 ) = ( cosh_C /. z1 ) * ( cosh_C /. z2 ) + ( sinh_C /. z1 ) * ( sinh_C /. z2 )
F . i = F /. i .= 0. R + r2 .= b |^ ( n + 1 ) .= ( ( a , b ) In_Power ( n + 1 ) ) . i ;
ex y being set st ex f being Function st y = f . n ( ) & dom f = NAT & f . 0 = A ( ) & for n holds f . ( n + 1 ) = RecFun ( n , f . n )
func f (#) F -> FinSequence of V means : Def6 : len it = len F & for i being Nat st i in dom it holds it . i = ( F /. i ) * f . ( F /. i ) ;
{ x1 , x2 , x3 , x4 , x5 , x6 , x7 , x8 } = { x1 , x2 } \/ { x3 , x4 , x5 , x6 , x7 , x8 }
for n being Nat , x being set st x = h . n holds h . ( n + 1 ) = o ( x , n ) & x in InputVertices S ( x , n ) & o ( x , n ) in InnerVertices S ( x , n )
ex S1 being Element of QC-Sub-WFF ( Al ( ) ) st Sub_P ( P , ll , e ) = S1 & S1 `1 is Element of CQC-WFF ( Al ( ) ) ;
consider P be FinSequence of Gk such that pk9 = Product P and for i st i in dom P ex trans be Element of Permutations ( k ) st P . i = trans & trans is being_transposition ;
for T1 , T2 being strict non empty TopSpace , P being prebasis of T1 st the carrier of T1 = the carrier of T2 & P is prebasis of T2 holds T1 = T2
f is_hpartial_differentiable`32_in u0 implies r (#) pdiff1 ( f , 3 ) is_partial_differentiable_in u0 , 2 & partdiff ( ( r (#) pdiff1 ( f , 3 ) ) , u0 , 2 ) = r * hpartdiff32 ( f , u0 )
defpred P [ Nat ] means for F , G being FinSequence of ExtREAL , s being Permutation of Seg $1 st len F = $1 & G = F * s & not -infty in rng F holds Sum F = Sum G ;
ex j st 1 <= j & j < width GoB f & ( GoB f ) * ( 1 , j ) `2 <= s & s < ( GoB f ) * ( 1 , j + 1 ) `2 ;
defpred U [ set , set ] means ex FS be FamilySequence of T st $2 = FS & Union FS is open & Union FS is Cover of T & Union FS is_finer_than FB . $1 & FS is sigma_discrete ;
for p6 being Point of TOP-REAL 2 st LE p4 , p6 , P , p1 , p2 & LE p6 , p , P , p1 , p2 holds p6 `1 <= e
for x , H , f holds ( f in St ( H , E ) & for g st for y st g . y <> f . y holds x = y holds g in St ( H , E ) ) iff f in St ( All ( x , H ) , E )
ex p8 being Point of TOP-REAL 2 st x = p8 & p8 `2 / |. p8 .| >= sn & p8 `1 <= 0 & p8 <> 0. TOP-REAL 2 ;
assume for dn being Element of NAT st dn <= max_Data-Loc_in ( nt -tree ( tl , tr ) ) holds s1 . dl. dn = s2 . dl. dn ;
s <> t & s is Point of Tdisk ( x , r ) & s is not Point of Tcircle ( x , r ) implies ex e being Point of Tcircle ( x , r ) st { e } = halfline ( s , t ) /\ Sphere ( x , r )
given r such that 0 < r and for s holds not 0 < s or ex x1 be Point of CNS st x1 in dom f & ||. x1 - x0 .|| < s & not |. f /. x1 - f /. x0 .| < r ;
for x , p holds ( p | x ) | ( p | ( ( x | x ) | ( x | x ) ) ) = ( ( ( x | x ) | ( x | x ) ) | p ) | ( ( ( x | x ) | ( x | x ) ) | p )
x in dom sec & x + h in dom sec implies fD ( sec (#) sec , h ) . x = 4 * sin ( 2 * x + h ) * sin ( h ) / ( cos ( 2 * x + h ) + cos ( h ) ) ^2
i in dom A & len A > 1 implies Solutions_of ( A , B ) c= Solutions_of ( DelLine ( A , i ) , DelLine ( B , i ) )
for i being non zero Element of NAT st i in Seg n holds ( not i divides n or i = n implies h . i = <% 1_ F_Complex %> ) & ( i divides n & i <> n implies h . i = cyclotomic_poly ( i ) )
for a1 , b1 , c1 , a2 , b2 , c2 being Function of Y , BOOLEAN holds ( b1 'imp' b2 ) '&' ( c1 'imp' c2 ) '&' ( a1 'or' b1 'or' c1 ) '&' 'not' ( a2 '&' b2 ) '&' 'not' ( a2 '&' c2 ) '<' ( a2 'imp' a1 )
( for x holds f . x = ( cot (#) sin ) . x ) & x in dom cot & x - h in dom cot implies bD ( f , h ) . x = cos ( x ) - cos ( x - h )
consider RF , IF be Real such that RF = Integral ( M , Re ( F . n ) ) and IF = Integral ( M , Im ( F . n ) ) and Integral ( M , F . n ) = RF + IF * <i> ;
ex k be Element of NAT st k0 = k & 0 < d & for q be Element of product G st q in X & ||. q - x .|| < d holds ||. partdiff ( f , q , k ) - partdiff ( f , x , k ) .|| < r ;
x in { x1 , x2 , x3 , x4 , x5 , x6 , x7 , x8 , x9 } iff x in { x1 , x2 , x3 , x4 } \/ { x5 , x6 , x7 , x8 , x9 } ;
G * ( j , io ) `2 = G * ( 1 , io ) `2 .= G * ( jo , io ) `2 .= p `2 .= G * ( j , i ) `2 ;
f1 * p = p .= ( ( the Arity of S1 ) +* the Arity of S2 ) . o .= ( the Arity of S ) . o .= ( the Arity of S ) . ( g1 . o ) ;
func tree ( T , P , T1 ) -> Tree means : Def1 : q in it iff ( q in T & for p st p in P holds not p is_a_proper_prefix_of q ) or ex p , r st p in P & r in T1 & q = p ^ r ;
F /. ( k + 1 ) = F . ( k + 1 ) .= FPower ( p . ( k + 1 -' 1 ) , k + 1 -' 1 ) .= FPower ( p . k , k + 1 -' 1 ) .= FPower ( p . k , k ) ;
for A , B , C being Matrix of K st len B = len C & width B = width C & len B = width A & len B > 0 & len A > 0 holds A * ( B - C ) = A * B - A * C
seq . ( k + 1 ) = 0c + seq . ( k + 1 ) .= ( Partial_Sums seq ) . k + seq . ( k + 1 ) .= ( Partial_Sums seq ) . ( k + 1 ) ;
assume that x in [: the carrier of CS , the carrier of CS :] and y in [: the carrier of CS , the carrier of CS :] and [ x , y ] in the CONGR of CS ;
defpred P [ Element of NAT ] means for f st len f = $1 holds ( VAL g ) . kon ( f ) = ( VAL g ) . kon ( f | 1 ) '&' ( VAL g ) . kon ( f /^ 1 ) ;
assume 1 <= k & k + 1 <= len f & f is_sequence_on G & [ i , j ] in Indices G & [ i + 1 , j ] in Indices G & f /. k = G * ( i , j ) & f /. ( k + 1 ) = G * ( i + 1 , j ) ;
for sn being Real , q being Point of TOP-REAL 2 st sn < 1 & q `1 > 0 & q `2 / |. q .| >= sn holds for p being Point of TOP-REAL 2 st p = ( sn -FanMorphE ) . q holds p `1 > 0 & p `2 >= 0
for M being non empty MetrSpace , x being Point of TopSpaceMetr ( M ) , x9 being Point of M st x = x9 ex f being sequence of Balls ( x ) st for n being Element of NAT holds f . n = Ball ( x9 , 1 / ( n + 1 ) )
defpred P [ Element of omega ] means f1 is_differentiable_on $1 , Z & f2 is_differentiable_on $1 , Z implies diff ( f1 - f2 , Z ) . $1 = diff ( f1 , Z ) . $1 - diff ( f2 , Z ) . $1 ;
defpred P1 [ Nat , Point of CNS ] means $2 in Y & ||. s1 . $1 - $2 .|| < 1 / ( $1 + 1 ) & not ||. f /. ( s1 . $1 ) - f /. $2 .|| < r ;
( f ^ mid ( g , 2 , len g ) ) . i = mid ( g , 2 , len g ) . ( i -' len f ) .= g . ( i -' len f + 2 - 1 ) .= g . ( i -' len f + 1 ) ;
1 / ( 2 * n0 + 2 ) * ( ( 2 * n0 + 2 ) * Cl ( TB1 ) ) = ( 1 / ( 2 * n0 + 2 ) * ( 2 * n0 + 2 ) ) * Cl ( TB1 ) .= 1 * Cl ( TB1 ) .= Cl ( TB1 ) ;
defpred P [ Nat ] means for G be non empty strict finite irreflexive symmetric RelStr st G is N-free & card the carrier of G = $1 & the carrier of G in FinSETS holds ( the RelStr of G ) in fin_RelStr_sp ;
not f /. 1 in Ball ( u , r ) & 1 <= m & m <= len f - 1 & ( for i st 1 <= i & i <= len f - 1 & LSeg ( f , i ) /\ Ball ( u , r ) <> {} holds m <= i ) implies not f /. m in Ball ( u , r )
defpred P [ Element of NAT ] means Partial_Sums ( Maclaurin ( cos , ]. - r , r .[ , x ) ) . ( 2 * $1 + 1 ) = Partial_Sums ( x P_cos ) . $1 ;
for x being Element of product F holds x is FinSequence of G & dom x = I & dom x = dom ( Carrier F ) & for i be set st i in dom ( Carrier F ) holds x . i in ( Carrier F ) . i
x " |^ ( n + 1 ) = ( x " |^ n ) * x " .= ( x * ( x |^ n ) ) " .= ( ( x |^ 1 ) * ( x |^ n ) ) " .= ( x |^ ( n + 1 ) ) " ;
DataPart Comput ( P +* while>0 ( a , I ) , Initialized s , LifeSpan ( P +* I , Initialized s ) + 3 ) = DataPart Comput ( P +* I , Initialized s , LifeSpan ( P +* I , Initialized s ) ) ;
given r such that 0 < r and ]. x0 , x0 + r .[ c= dom f1 /\ dom f2 /\ dom f and for g st g in ]. x0 , x0 + r .[ holds f1 . g <= f . g & f . g <= f2 . g ;
for X , f1 , f2 st X c= dom f1 /\ dom f2 & f1 | X is continuous & f2 | X is continuous holds ( f1 + f2 ) | X is continuous & ( f1 - f2 ) | X is continuous & ( f1 (#) f2 ) | X is continuous
for L being continuous complete LATTICE st for l being Element of L ex X being Subset of L st l = sup X & for x being Element of L st x in X holds x is co-prime for l being Element of L holds l = "\/" ( ( waybelow l ) /\ PRIME ( L opp ) , L )
Support ep in { Support ( m *' p ) where m is Monomial of n , L , p is Polynomial of n , L : ex i being Element of NAT st i in dom A & A /. i = m *' p } ;
( f1 - f2 ) /. ( lim s1 ) = lim ( f1 /* s1 ) - lim ( f2 /* s1 ) .= lim ( f1 /* s1 - f2 /* s1 ) .= lim ( ( f1 - f2 ) /* s1 ) ;
ex p1 being Element of QC-WFF ( Al ( ) ) st p1 = p9 & for g being Function of QC-WFF ( Al ( ) ) , D ( ) st Pfn [ g , len @ p1 qua Nat ] holds F . p9 = g . p1 ;
( mid ( f , i , len f -' 1 ) ^ <* f /. ( len f ) *> ) /. j = mid ( f , i , len f -' 1 ) /. j .= f /. ( j + i -' 1 ) .= mid ( f , i , len f ) /. j ;
( p ^ q ^ r ) . ( len p + k ) = ( p ^ q ^ r ) . ( len p + len q + n ) .= ( p ^ q ^ r ) . ( len ( p ^ q ) + n ) .= r . n .= ( q ^ r ) . k ;
len mid ( upper_volume ( f , D2 ) , ( indx ( D2 , D1 , j1 ) + 1 ) , indx ( D2 , D1 , j ) ) = indx ( D2 , D1 , j ) -' ( indx ( D2 , D1 , j1 ) + 1 ) + 1 ;
( x * y ) * z = MULT . ( xx * yy , zz ) .= ( xx * yy ) * zz .= xx * ( yy * zz ) .= MULT . ( xx , yy * zz ) .= x * ( y * z ) ;
( v . <* x , y *> - v . <* x0 , y0 *> ) * <i> = ( partdiff ( v , xy0 , 1 ) * ( x - x0 ) + partdiff ( u , xy0 , 1 ) * ( y - y0 ) + proj ( 1 , 1 ) . ( Rv . <* x - x0 , y - y0 *> ) ) * <i> ;
<i> * <i> = [* 0 * 0 - 1 * 1 - 0 * 0 - 0 * 0 , 0 * 1 + 1 * 0 + 0 * 0 - 0 * 0 , 0 * 0 + 0 * 0 + 1 * 0 - 0 * 1 , 0 * 0 + 0 * 0 + 1 * 0 - 0 * 1 *] .= [* - 1 , 0 , 0 , 0 *] ;
Sum ( L (#) F ) = Sum ( L (#) ( F1 ^ F2 ) ) .= Sum ( ( L (#) F1 ) ^ ( L (#) F2 ) ) .= Sum ( L (#) F1 ) + Sum ( L (#) F2 ) .= Sum ( L (#) F1 ) + 0. V .= Sum ( L (#) G ) + 0. V .= Sum ( L ) ;
ex r be Real st for e be Real st 0 < e ex Y0 be finite Subset of X st Y0 is non empty & Y0 c= Y & for Y1 be finite Subset of X st Y0 c= Y1 & Y1 c= Y holds |. r - setopfunc ( Y1 , the carrier of X , REAL , L , addreal ) .| < e
( GoB f ) * ( i , j ) = f /. ( k + 2 ) & ( GoB f ) * ( i , j + 1 ) = f /. ( k + 1 ) or ( GoB f ) * ( i , j ) = f /. ( k + 1 ) & ( GoB f ) * ( i , j + 1 ) = f /. ( k + 2 ) ;
( cos . x ) ^2 = 1 - ( sin . x ) ^2 .= 1 - ( 1 / r ) * ( 1 / r ) .= 1 - 1 / ( r ^2 ) .= ( r ^2 ) / ( r ^2 ) - 1 / ( r ^2 ) .= ( r ^2 - 1 ) / ( r ^2 ) ;
x - ( - b + sqrt delta ( a , b , c ) ) / ( 2 * a ) < 0 & x - ( - b - sqrt delta ( a , b , c ) ) / ( 2 * a ) < 0 or x - ( - b - sqrt delta ( a , b , c ) ) / ( 2 * a ) > 0 & x - ( - b + sqrt delta ( a , b , c ) ) / ( 2 * a ) > 0 ;
for L being non empty Poset , R being auxiliary(i) auxiliary(ii) ( Relation of L ) , C being non empty strict_chain of R , X being Subset of C st ex_inf_of ( uparrow "\/" ( X , L ) ) /\ C , L & ex_sup_of X , L & C is maximal holds "\/" ( X , subrelstr C ) = "/\" ( ( uparrow "\/" ( X , L ) ) /\ C , L ) & ( not "\/" ( X , L ) in C implies "\/" ( X , L ) < "/\" ( ( uparrow "\/" ( X , L ) ) /\ C , L ) )
( Normalized B ) . ( j , i ) = IFEQ ( j , i , id ( the Sorts of OAF . i ) , bind ( B , i , j ) ** id ( the Sorts of OAF . i ) ) & IFEQ ( j , i , id ( the Sorts of OAF . i ) , bind ( B , i , j ) ** id ( the Sorts of OAF . i ) ) = bind ( B , i , j ) ** id ( the Sorts of OAF . i ) ;