thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
contradiction ;
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 ;
contradiction ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
contradiction ;
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 ;
contradiction ;
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 ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
contradiction ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
thesis ;
contradiction ;
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 ;
assume not thesis ;
assume not thesis ;
i = 1 ;
assume not thesis ;
x <> b
D c= S
let Y ;
S9 is Cauchy
let p , q ;
let S , V ;
y in N ;
x in T ;
m < n ;
m <= n ;
n > 1 ;
let r ;
t in I ;
n <= 4 ;
M is finite ;
let X ;
Y c= Z ;
A // M ;
let U ;
a in D ;
q in Y ;
let x ;
1 <= l ;
1 <= w ;
let G ;
y in N ;
f = {} ;
let x ;
x in Z ;
let x ;
F is one-to-one ;
e <> b ;
1 <= n ;
f is special ;
S misses C
t <= 1 ;
y divides m ;
P divides M ;
let Z ;
let x ;
y c= x ;
let X ;
let C ;
x _|_ p ;
o is monotone ;
let X ;
A = B ;
1 < i ;
let x ;
let u ;
k <> 0 ;
let p ;
0 < r ;
let n ;
let y ;
f is onto ;
x < 1 ;
G c= F ;
a is_>=_than X ;
T is continuous ;
d <= a ;
p <= r ;
t < s ;
p <= t ;
t < s ;
let r ;
D <= E ;
e > 0 ;
0 < g ;
let D , m , p ;
let S , H , x ;
Y9 in Y ;
0 < g ;
not c in Y ;
not v in L ;
2 in z9 ;
f = g ;
N c= b9 ;
assume i < k ;
assume u = v ;
take D , I ;
B9 = b9 ;
assume e in F ;
assume p > 0 ;
assume x in D ;
let i be element ;
assume F is "onto" ;
assume n <> 0 ;
let x be element ;
set k = z ;
assume o = x ;
assume b < a ;
assume x in A ;
a9 <= b9 ;
assume b in X ;
assume k <> 1 ;
f = Product l ;
assume H <> F ;
assume x in I ;
assume p is prime ;
assume A in D ;
assume 1 in b ;
y is generated_from_squares ;
assume m > 0 ;
assume A c= B ;
X is bounded_below
assume A <> {} ;
assume X <> {} ;
assume F <> {} ;
assume G is open ;
assume f is dilatation ;
assume y in W ;
not y <= x ;
A9 in B9 ;
assume i = 1 ;
let x be element ;
x9 = x99 ;
let X be BCI-algebra ;
S is non empty ;
a in REAL ;
let p be set ;
let A be set ;
let G be _Graph ;
let G be _Graph ;
let a be Complex ;
let x be element ;
let x be element ;
let C be FormalContext ;
let x be element ;
let x be element ;
let x be element ;
n in NAT ;
n in NAT ;
n in NAT ;
not x in T . ( m + n ) ;
, y be Real ;
X c= f . a
let y be element ;
let x be element ;
let i be Nat ;
let x be element ;
n in NAT ;
let a be element ;
m in NAT ;
let u be element ;
i in NAT ;
let g be Function ;
Z c= NAT ;
l <= ma ;
let y be element ;
let r1 , r2 ;
let x be element ;
Integer ;
let X be set ;
let a be element ;
let x be element ;
let x be element ;
let q be element ;
let x be element ;
assume f is being_homeomorphism ;
let z be element ;
a , b // K ;
let n be Nat ;
let k be Nat ;
B9 c= B99 ;
set s = f /" g ;
n >= 0 + 1 ;
k c= k + 1 ;
R1 c= R ;
k + 1 >= k ;
k c= k + 1 ;
let j be Nat ;
o , a // Y ;
R c= Cl G ;
Cl B = B ;
let j be Nat ;
1 <= j + 1 ;
arccot is_differentiable_on Z ;
exp_R is_differentiable_in x ;
j < i0 ;
let j be Nat ;
n <= n + 1 ;
k = i + m ;
assume C meets S ;
n <= n + 1 ;
let n be Nat ;
h1 = {} ;
0 + 1 = 1 ;
o <> b3 ;
f2 is one-to-one ;
support p = {}
assume A12 : x in Z ;
i <= i + 1 ;
r1 <= 1 ;
let n be Nat ;
a "/\" b <= a ;
let n be Nat ;
0 <= r0 ;
let e be Real ;
not r in G . l
c1 = 0 ;
a + a = a ;
<* 0 *> in e ;
t in { t } ;
assume not F is discrete ;
m1 divides m ;
B *^ A <> {} ;
a +^ b <> {} ;
p * p > p ;
let y be ExtReal ;
let a be Int-Location ;
let l be Nat ;
let i be Nat ;
let n , A , r ;
1 <= i2 ;
a "\/" c = c ;
let r be Real ;
let i be Nat ;
let m be Nat ;
x = p2 ;
let i be Nat ;
y < r + 1 ;
rng c c= E
Cl R is boundary ;
let i be Nat ;
registration let R1 , R2 ;
cluster wayabove x -> join-closed ;
X <> { x } ;
x in { x } ;
q , b9 // M ;
A . i c= Y ;
P [ k ] ;
bool x in W ;
X [ 0 ] ;
P [ 0 ] ;
A = A ^i ;
a - s >= s - s ;
G . y <> 0 ;
let X be RealNormSpace ;
let i , j , l , k , a ;
H . 1 = 1 ;
f . y = p ;
let V be RealUnitarySpace ;
assume x in M - M ;
k < s . a ;
not t in { p } ;
let Y be complex-functions-membered set ;
M , L are_isomorphic ;
a <= g . i ;
f . x = b ;
f . x = c ;
assume L is lower-bounded upper-bounded ;
rng f = Y ;
GG c= L ;
assume x in order_type_of Q ;
m in dom P ;
i <= len Q ;
len F = 3 ;
Fixed p = {} ;
z in rng p ;
lim b = 0 ;
len W = 3 ;
k in dom p ;
k <= len p ;
i <= len p ;
1 in dom f ;
b9 = a9 + 1 ;
x9 = a * y9 ;
rng D c= A ;
assume x in K1 ;
1 <= ii ;
1 <= ii ;
poz c= pio ;
1 <= ii ;
1 <= ii ;
LMP C in L ;
1 in dom f ;
let seq ;
set C = a * B ;
x in rng f ;
assume f is_Lipschitzian_on X ;
I = dom A ;
u in dom p ;
assume a < x + 1 ;
seq0 is bounded ;
assume I c= P1 ;
n in dom I ;
let t be State of SCMPDS , Q ;
B c= dom f ;
not b + p _|_ a ;
x in dom g ;
Fn1 is continuous ;
dom g = X ;
len q = m ;
assume A2 is closed ;
cluster R \ S -> real-valued ;
sup D in S ;
x << sup D ;
b1 is_>=_than Z1
assume w = 0. V ;
assume x in A . i ;
g in ComplexBoundedFunctions X ;
then y in dom t ;
then i in dom g ;
assume P [ k ] ;
EMF ( C ) c= f
xj is increasing ;
let e2 be element ;
- b divides b ;
F c= tau F ;
Gseq is non-decreasing ;
Gseq is non-decreasing ;
assume v in H . m ;
assume b in [#] B ;
let S be non void Signature ;
assume P [ n ] ;
union S is affinely-independent finite ;
V is Subspace of V ;
assume P [ k ] ;
rng f c= NAT
assume ex_inf_of X , L ;
y in rng ( f ) ;
let s , I be set ;
b99 c= b19 ;
assume not x in RAT+ ;
A /\ B = { a } ;
assume len f > 0 ;
assume x in dom f ;
b , a // o , c ;
B in BBX ;
cluster product p -> non empty ;
z , x // x , p ;
assume x in rng N ;
cosec is_differentiable_in x ;
assume y in rng S ;
let x , y be element ;
i2 < i1 ;
a * h in a * H ;
p in Y & q in Y ;
cluster sqrt I -> left-ideal ;
q1 in A1 ;
i + 1 <= 2 + 1 ;
A1 c= A2 ;
bn < n ;
assume A c= dom f ;
Re f is_integrable_on M ;
let k , m be element ;
a , a @@ b , b
j + 1 < k + 1 ;
m + 1 <= n1 ;
g is_differentiable_in x0 ;
g is_continuous_in x0 ;
assume O is symmetric & O is transitive ;
let x , y be element ;
let j0 be Nat ;
[ y , x ] in R ;
let x , y be element ;
assume y in conv A ;
x in Int ( V ) ;
let v be VECTOR of V ;
P3 halts_on s ;
d , c // a , b ;
let t , u be set ;
let X be with_non-empty_element set ;
assume k in dom s ;
let r be non negative Real ;
assume x in F | M ;
let Y be Subset of S ;
let X be non empty TopSpace ;
[ a , b ] in R ;
x + w < y + w ;
{ a , b } is_>=_than c ;
let B be Subset of A ;
let S be non empty ManySortedSign ;
let x be Variable of f ;
let b be Element of X ;
R [ x , y ] ;
x ` = x ;
b \ x = 0. X ;
<* d *> in 1 -tuples_on D
P [ k + 1 ] ;
m in dom mn ;
h2 . a = y ;
P [ n + 1 ] ;
cluster G * F -> Contravariant ;
let R be non empty multLoopStr ;
let G be _Graph , v be Vertex of G ;
let j be Element of I ;
a , p // x , p9 ;
assume f | X is bounded_below ;
x in rng co ;
let x be Element of B ;
let t be Element of D ;
assume x in Q .vertices() ;
set q = s ^\ k ;
let t be VECTOR of X ;
let x be Element of A ;
assume y in rng p9 ;
let M be finite-degree Matroid ;
of M ;
let R be with_finite_clique# RelStr ;
let n , k be Nat ;
let P , Q be pcs-Str ;
P = Q /\ [#] S ;
F . r in { 0 } ;
let x be Element of X ;
let x be Element of X ;
let u be VECTOR of V ;
reconsider d = x as FinSeq-Location ;
assume I does not refer a ;
let n , k be Nat ;
let x be Point of T ;
f c= f +* g ;
assume m < vn ;
x <= c2 . x ;
x in COMPLEMENT F ;
cluster S --> T -> reflexive-yielding ;
assume t1 <= t2 ;
let i , j be even Integer ;
assume F1 <> F2 ;
c in Intersect union R ;
dom p1 = c ;
a = 0 or a = 1 ;
assume A1 <> A6 ;
set i1 = i + 1 ;
assume a1 = b1 ;
dom g1 = A ;
i < len M + 1 ;
assume not -infty in rng G ;
N c= dom f1 ;
x in dom sec ;
assume [ x , y ] in R ;
set d = x / y ;
1 <= len g1 ;
len s2 > 1 ;
z in dom f1 ;
1 in dom D2 ;
p `2 = 0 ;
j2 <= width G ;
len pion1 > 1 + 1 ;
set n1 = n + 1 ;
|. qx .| = 1 ;
let s be SortSymbol of S ;
i lcm i = i
X1 c= dom f ;
h . x in h . a ;
let G be IncProjSp ;
cluster m * n -> square ;
let kk be Nat ;
i -' 1 > m ;
R is_transitive_in field R ;
set F = <* u , w *> ;
pIF c= P3 ;
I is_halting_on t , Q ;
assume [ S , x ] is quantifiable ;
i <= len f2 ;
p is FinSequence of X ;
1 + 1 in dom g ;
Sum R2 = n * r ;
cluster f . x -> complex-valued ;
x in dom f1 ;
assume [ X , p ] in C ;
BD c= X3 ;
n2 <= 2M ;
A /\ cP9 c= A9
cluster x -valued -> constant for Function ;
let Q be Subset-Family of S ;
n in dom g2 ;
Subset of R , a be Element of R ;
t9 in dom e2 ;
N . 1 in rng N ;
- z in A \/ B ;
let S be SigmaField of X ;
i . y in rng i ;
REAL c= dom ( f ) ;
f . x in rng f ;
mt <= r / 2 ;
s2 in rset ;
let z , z9 be quaternion number ;
n <= Nseq . m ;
LIN q , p , s ;
f . x = waybelow x /\ B ;
set L = ContMaps ( S , T ) ;
let x be non real positive ExtReal ;
carrier of N , m be Element of M ;
f in union rng F1 ;
doubleLoopStr ;
let i be Element of NAT ;
rng ( F * g ) c= Y
dom f c= dom x ;
n1 < n1 + 1 ;
n1 < n1 + 1 ;
cluster Tarski-Class X -> Tarski ;
[ y2 , 2 ] = z ;
let m be Element of NAT ;
let R be RelStr , S be Subset of R ;
y in rng SN ;
b = sup dom f ;
x in Seg len q ;
reconsider X = D ( ) as set ;
[ a , c ] in E1 ;
assume n in dom h2 ;
w + 1 = ma1 ;
j + 1 <= j + 1 + 1 ;
k2 + 1 <= k1 ;
L , i be Element of NAT ;
Support u = Support p ;
assume X is_CRS_of m ;
assume f = g & p = q ;
n1 <= n1 + 1 ;
let x be Element of REAL ;
assume x in rng s2 ;
x0 < x0 + 1 ;
len Li = W ;
P c= Seg len A ;
dom q = Seg n ;
j <= width ( M @" ) ;
let rf be real-valued FinSubsequence ;
let k be Element of NAT ;
Integral ( M , P ) < +infty ;
let n be Element of NAT ;
let z be element ;
let I be set , X be ManySortedSet of I , i be set ;
n -' 1 = n - 1 ;
len nlist1 = n ;
InitSegm ( Z , c ) c= F
assume x in X or x = X ;
Mid b , x , c ;
let A , B be non empty set ;
set d = dim ( p ) ;
let p be FinSequence of L ;
Seg i = dom q ;
let s be Element of E ^omega ;
let B1 be Basis of x ;
L3 /\ L2 = {} ;
L1 /\ L4 = {} ;
assume downarrow x = downarrow y ;
assume not b , c // b9 , c9 ;
LIN q , c9 , c9 ;
x in rng fX ;
set nj = n + j ;
let DX be non empty set ;
let K be right_zeroed non empty addLoopStr ;
f9 = f & h9 = h ;
R1 - R2 is RestFunc ;
k in NAT & 1 <= k ;
let G be finite Group , a be Element of G ;
x0 in [. a , b .] ;
K1 ` is open ;
assume a , b realize-max-dist-in C ;
let a , b be Element of S ;
reconsider d = x as Vertex of G ;
x in ( s + f ) .: A ;
set a = Integral ( M , f ) ;
cluster necessitive for MP-wff ;
not u in { bg } ;
Carrier ( f ) c= B
reconsider z = x as VECTOR of V ;
cluster the ComplStr of L -> 1 -element ;
r (#) H is_point_conv_on X ;
s . intloc 0 = 1 ;
assume that x in C and y in C ;
let U0 be with_const_op strict Universal_Algebra ;
[ x , Bottom T ] is compact ;
i + 1 + k in dom p ;
F . i is stable Subset of M ;
ry in DEDEKIND_CUT y ;
let x , y be Element of X ;
let A , I be Ideal of X ;
[ y , z ] in OK ;
LastLoc Macro i = 1 ;
rng ( Sgm A ) = A ;
q |-| All ( y , q ) ;
for n holds X [ n ] ;
x in { a } & x in d ;
for n holds P [ n ] ;
set p = |[ x , y , z ]| ;
LIN o9 , a9 , b9 ;
p . 2 = Funcs ( Y , Z ) ;
D0 `2 = {} ;
n + 1 + 1 <= len g ;
a in QC-symbols ( Al ) ;
u in Support ( m *' p ) ;
let x , y be Element of G ;
let L be non empty doubleLoopStr , I be Ideal of L ;
set g = f1 + f2 ;
a <= max ( a , b ) ;
i - 1 < len G + 1 - 1 ;
g . 1 = f . i1 ;
x9 in A2 & y9 in A2 ;
( f /* s ) . k < r ;
set v = VAL g , vf = v . TFALSUM ;
i -' k + 1 <= S ;
cluster associative invertible -> Group-like for non empty multMagma ;
x in support pfexp t ;
assume a in [: cG , cG :] ;
i9 <= len yb2 ;
assume p divides b1 +^ b2 ;
M0 is_<=_than sup M1 ;
assume x in W-most X ;
j in dom znpp ;
let x be Element of D ( ) ;
IC s5 = l1 ;
a = {} or a = { x } ;
set uG = Vertices G ;
seq1 " is non-zero ;
for k holds X [ k ] ;
for n holds X [ n ] ;
F . m in { F . m } ;
hy c= hx ;
]. a , b .[ c= Z ;
X1 , X2 are_weakly_separated ;
a in Cl union ( F \ G ) ;
set x1 = [ 0 , 0 ] ;
k + 1 -' 1 = k ;
cluster natural-valued -> RAT -valued for Relation ;
ex v st C = v + W ;
let GF be non empty ZeroStr ;
assume V is Abelian add-associative right_zeroed right_complementable ;
Xx \/ Y in sigma L ;
reconsider x9 = x as Element of S ;
max ( a , b ) = a ;
sup B is UpperBound of B ;
let L be non empty reflexive antisymmetric RelStr ;
R is_reflexive_in X & R is_transitive_in X ;
E , g |= the_right_argument_of H ;
dom ( G9 /. y ) = a ;
1 / 4 >= - r ;
G . p0 in rng G ;
let x be Element of FT ;
D [ Px , 0 ] ;
z in dom id B ;
y in the carrier of N ;
g in the carrier of H ;
rng fs c= NAT ;
j9 + 1 in dom s1 ;
let A , B be strict Subgroup of G ;
let C be non empty Subset of REAL ;
f . z1 in dom h ;
P . k1 in rng P ;
M = AB +* {} ;
let p be FinSequence of REAL ;
f . n1 in rng f ;
M . ( F . 0 ) in REAL ;
diameter [. a , b .[ = b - a ;
assume V , Q is_dst v ;
let a be Element of opp V ;
let s be Element of PM ;
let PO be non empty OrthoRelStr ;
let p be polyhedron , k be Integer , n be Nat ;
Carrier ( g ) c= B ;
I = halt SCM R ;
consider b being element such that b in B ;
set BK = BCS K ;
l <= Sup ( F . j ) ;
assume x in downarrow [ s , t ] ;
x `2 in uparrow t ;
x in DOM JumpParts T ;
let h9 be Morphism of c , a ;
Y c= Rank the_rank_of Y ;
A2 \/ A4 c= L4 ;
assume LIN o9 , a9 , b9 ;
b , c // d1 , e2 ;
x1 in Y & x2 in Y ;
dom <* y *> = Seg 1 ;
reconsider i = x as Element of NAT ;
reconsider s = F . t as termal Element of S ;
[ x , x9 ] in [: X , X9 :] ;
for n be Nat holds 0 <= x . n
[' a , b '] = [. a , b .] ;
cluster regular_closed -> closed for Subset of T ;
x = h . ( f . z1 ) ;
q1 in P & q2 in P ;
dom M1 = Seg n ;
x = [ x1 , x2 ] ;
let R , Q be ManySortedRelation of A ;
set d = 1 / ( n + 1 ) ;
rng g2 c= dom W ;
P . ( [#] Sigma \ B ) <> 0 ;
a in field R & a = b ;
let M be non empty Affine Subset of V ;
let I be Program of SCM+FSA ;
assume x in rng CL R ;
let b be Element of Closed_Domains_Lattice T ;
dist ( e , z ) - r > r - r ;
u1 + v1 in W2 ;
assume Carrier ( L ) misses rng G ;
let L be lower-bounded with_suprema transitive antisymmetric RelStr ;
assume [ x , y ] in ab ;
dom ( A * e ) = NAT ;
let G be _Graph , a , b be Vertex of G ;
let x be Element of Bool M ;
0 <= Arg a & Arg a < 2 * PI ;
o9 , a19 // o9 , y9 ;
{ v } c= Carrier l ;
let a be free_QC-variable of A , x be bound_QC-variable of A ;
assume x in dom uncurry' f ;
rng F c= Funcs ( X , product f )
assume D2 . k in rng D ;
f " . p1 = 0 ;
set x = the Element of X ;
dom Ser ( G ) = NAT ;
let F be SetSequence of X , n be Element of NAT ;
assume LIN c , a , e1 ;
cluster -> Cardinal-yielding for FinSequence of NAT ;
reconsider d = c as Element of L1 ;
( v2 |-- I ) . X <= 1 ;
assume x in Carrier ( f ) ;
conv @ S c= conv A ;
reconsider B = b as Element of Domains_of T ;
J , v |= P ! ll ;
redefine func J . i -> non empty TopStruct ;
ex_sup_of Y1 \/ Y2 , T ;
W1 well_orders field W1 ;
assume x in the carrier of R ;
dom nf = Seg n ;
sb misses sbs9b ;
assume ( a 'eqv' b ) . z = TRUE ;
assume A1 : X is open & f = X --> d ;
assume [ a , y ] in Trace f ;
CutLastLoc J c= K ;
Im lim ( seq ) = 0 ;
sin . x <> 0 ;
sin is_differentiable_on Z & cos is_differentiable_on Z ;
t6 . n = t3 . n ;
dom ( F /" G ) c= dom F ;
W1 . x = W2 . x ;
y in W .vertices() \/ W .edges() ;
kk <= len vs ;
x * a , y * a are_congruent_mod m ;
proj2 .: S c= proj2 .: P ;
h . p4 = g2 . I ;
Gij = US /. 1 ;
f . rss in rng f ;
i + 1 + 1 - 1 <= len f - 1 ;
rng F = rng FX ;
mode Monoid is well-unital associative non empty multLoopStr ;
[ x , y ] in [: A , { a } :] ;
x1 . o in L2 . o ;
Carrier ( l - m ) c= B ;
not [ y , x ] in id X ;
1 + p .. f <= i + len f ;
seq1 ^\ k1 is bounded_below ;
len Fp = len I ;
let l be Linear_Combination of B \/ { v } ;
let r1 , r2 be complex number ;
Comput ( P , s , n ) = s ;
k <= k + 1 & k + 1 <= len p ;
reconsider c = {} T as Element of L ;
let Y be AntiChain_of_Prefixes of T ;
cluster closure for Function of L , L ;
f . j1 in K . j1 ;
cluster J => y -> total for J -defined Function ;
K c= bool the carrier of T
F . b1 = F . b2 ;
x1 = x or x1 = y ;
a <> {} implies a / a = 1
assume that cf a c= b and b in a ;
s1 . n in rng s1 ;
{ o , b2 } on C2 ;
LIN o9 , b9 , b19 ;
reconsider m = x as Element of Maps V ;
let f be circular non trivial FinSequence of D ;
let FMT be non empty FMT_Space_Str ;
assume that h is being_homeomorphism and y = h . x ;
[ f . 1 , w ] in FSG ;
reconsider pq = x as Subset of m ;
let A , B , C be Element of R ;
cluster strict Regular for non empty OrdTrapSpace ;
rng c9 misses rng ep
z is Element of gr { x } ;
not b in dom ( a .--> p1 ) ;
assume A6 : k >= 2 & P [ k ] ;
Z c= dom cot ;
Component_of Q c= UBD A ;
reconsider E = { i } as finite Subset of I ;
g2 in dom ( f ^ ) ;
f = u implies a (#) f = a * u
for n holds P1 [ prop n ]
{ x . O : x in L } <> {} ;
let s be SortSymbol of S , x be Element of V . s ;
let n be Nat , R be NatRelStr of n , a , b be Nat ;
S = S2 & p = p2 ;
n1 gcd n2 = 1 ;
set om = mult_2 ;
seq . n < |. r1 .| ;
assume that seq is increasing and r < 0 ;
f . ( y1 , x1 ) <= a ;
ex c being Nat st P [ c ] ;
set g = seq_n^ ( 1 ) ;
k = a or k = b or k = c ;
ag , bg are_adjacent ;
assume Y = { 1 } & s = <* 1 *> ;
not x in dom g ;
W4 .first() = W3 . 1 ;
cluster trivial finite Tree-like for Subgraph of G ;
reconsider u9 = u as Element of Bags X ;
A in con_class B iff A , B are_conjugated
x in { [ 2 * n + 3 , k ] } ;
1 >= q `1 / |. q .| ;
f1 is_in_general_position_wrt f2 ;
f `2 <= q `2 ;
h is_in_the_area_of Cage ( C , n ) ;
b `2 <= p `2 ;
let f , g be RMembership_Func of X , Y ;
S * ( k , k ) <> 0. K ( ) ;
x in dom ( max- ( f ) ) ;
p2 in Next ( p1 ) ;
len the_right_argument_of H < len H ;
F [ A , Fn . A ] ;
consider Z such that y in Z and Z in X ;
1 in C implies A c= exp ( C , A )
assume r1 <> 0 or r2 <> 0 ;
rng q1 c= rng C1 ;
A1 , L , A3 are_mutually_different ;
y in rng f & y in { x } ;
f /. ( i + 1 ) in L~ f ;
b in RSub2 ( p , Sub ) ;
S is Sub_atomic implies Pro [ S ]
Cl Int [#] T = [#] T ;
f12 | A2 = f2 ;
0. M in the carrier of W ;
let j be Element of N , v , v9 be Element of M ;
reconsider K9 = union rng K as non empty set ;
X \ V c= Y \ V & Y \ V c= Y \ Z ;
let S , T be RelStr , X be Subset of [: S , T :] ;
consider H1 such that H = 'not' H1 ;
one c= ( numerator t ) *^ denominator r ;
0 * a = 0. R .= a * 0 ;
A |^ ( 2 , 2 ) = A ^^ A
set vn = vs /. n ;
r = 0. ( REAL-NS n ) ;
( f . p4 ) `1 >= 0 ;
len W = len W .reverse() ;
f /* ( s * G ) is divergent_to+infty ;
consider l be Nat such that m = F . l ;
t16 " ;
reconsider Y1 = X1 as SubSpace of X ;
consider w such that w in F and not x in w ;
let a , b , c , d be Real ;
reconsider i9 = i as non zero Element of NAT ;
c . x >= ( id L ) . x ;
( sigma T ) \/ omega T is prebasis of T ;
for x being element st x in X holds x in Y
cluster [ x1 , x2 ] -> pair ;
types a /\ downarrow t is Ideal of T ;
let X be disjoint_with_NAT non empty set ;
rng f = FreeGenSetNSG ( S , X )
let p be Element of B , the bool-sort of S ;
max ( N1 , 2 ) >= N1 ;
0. X <= b |^ ( m * mm ) ;
assume that i in I and R0 . i = R ;
i = j1 & p1 = q1 ;
assume gR in the_RightOptions_of g ;
let A1 , A2 be POINT of S ;
x in h " P /\ [#] T1 ;
1 in Seg 2 & 1 in Seg 3 ;
x in X ;
x in ( the Arrows of B ) . i
cluster ES . n -> the_Edges_of G -defined ;
n1 <= i2 + len g2 ;
i + 1 + 1 = i + ( 1 + 1 ) ;
assume v in the carrier' of G2 ;
y = Re ( y ) + Im ( y ) * <i> ;
Lege ( - 1 , p ) = 1 ;
x2 is_differentiable_on ]. a , b .[ ;
rng MD2 c= rng D2 ;
for p be Real st p in Z holds p >= a
X_axis f = proj1 * f ;
( seq ^\ m ) . k <> 0 ;
s . ( G . ( k + 1 ) ) > x0 ;
Path_matrix ( p , M ) . 2 = d ;
A ++ ( B -- C ) = A ++ B -- C ;
h , gg are_congruent_mod P -Ideal ;
reconsider i1 = i - 1 as Element of NAT ;
let v1 , v2 be VECTOR of V ;
for W being Submodule of V holds W is Submodule of (Omega). V
reconsider ii = i as Element of NAT ;
dom f c= [: C ( ) , D ( ) :] ;
x in ( inferior_setsequence B ) . n ;
len f2a in Seg len f2 ;
pB c= the topology of T ;
]. r , s .] c= [. r , s .] ;
let B1 be prebasis of T1 , B2 be prebasis of T2 ;
G * ( B * A ) = idm o1 ;
assume that are_Prop p , u and are_Prop u , q ;
[ z , z ] in union rng FOAR ;
( 'not' b . x 'or' b . x ) = TRUE ;
deffunc F ( set ) = $1 .. S ;
LIN a1 , a3 , b1 ;
f " Im ( f , x ) = { x } ;
dom w2 = dom r12 ;
assume that 1 <= i and i <= n and j <= n ;
( ( g2 ) . O ) `2 <= 1 ;
p in LSeg ( E . i , F . i ) ;
ID * ( i , j ) = 0. K ;
|. f . ( s . m ) - g .| < g1 ;
qf . x in rng qf ;
LM misses LM ` ;
consider c being element such that [ a , c ] in G ;
assume Name op1 = on ;
q . ( j + 1 ) = q /. ( j + 1 ) ;
rng F c= Funcs ( CA , FS )
P . ( B2 \/ D2 ) <= 0 + 0 ;
f . j in Class ( Q , f . j ) ;
0 <= x & x <= 1 implies x ^2 <= x
p9 - q9 <> 0. TOP-REAL 2 ;
cluster SCMaps ( S , T ) -> non empty ;
let S , T be up-complete non empty Poset , x be Element of [: S , T :] ;
Morph-Map ( F , a , b ) is one-to-one
|. i .| <= - - 2 to_power n ;
the carrier of I[01] = dom P ;
n ! * ( ( n + 1 ) ! ) > 0 * ( n ! ) ;
S c= ( A1 /\ A2 ) /\ A3 ;
a3 , a4 // b3 , b4 ;
dom A <> {} implies dom A <> {} ;
1 + ( 2 * k + 4 ) = 2 * k + 5 ;
x DSJoins X , Y , G2 ;
set v2 = vs /. ( i + 1 ) ;
x = r . n .= rv . n ;
f . s in the carrier of S2 ;
dom g = the carrier of I[01] ;
p in Upper_Arc ( P ) /\ Lower_Arc ( P ) ;
dom d2 = [: A2 , A2 :] ;
0 < p / ( ||. z .|| + 1 ) ;
e . ( m0 + 1 ) <= e . m0 ;
( B (-) X ) \/ ( B (-) Y ) c= B (-) ( X /\ Y )
-infty < Integral ( M , Im ( g | B ) ) ;
cluster O AND F -> filtering for Operation of X ;
let U1 , U2 be non-empty MSAlgebra over S ;
( Proj ( i , n ) * g ) is_differentiable_on X ;
let X be RealNormSpace , x , y , z be Point of X ;
reconsider px = p . x as Subset of V ;
x in the carrier of Lin ( A ) ;
let I , J be parahalting Program of SCM+FSA ;
assume - a is LowerBound of - X ;
Int Cl A c= Cl Int Cl A ;
assume for A being Subset of X holds Cl A = A ;
assume q in Ball ( |[ x , y ]| , r ) ;
p2 `2 <= p `2 ;
Cl ( Q ` ) = [#] TS ;
set S = the carrier of T , L = the carrier of R^1 ;
set IM = im ( f |^ n ) ;
len p -' n = len p - n ;
A is permutation of Swap ( A , x , y ) ;
reconsider ni = n - i as Element of NAT ;
1 <= j + 1 & j + 1 <= len sw ;
let qa , qb be State of M ;
am in the carrier of S1 ;
c1 /. n1 = c1 . n1 ;
let f be FinSequence of TOP-REAL 2 ;
y = ( fvs * SL ) . x ;
consider x be element such that x in Involved A ;
assume r in ( ( dist ( o ) ) .: ( P ) ) ;
set i1 = n_n_w h , i2 = n_n_e h ;
h2 . ( j + 1 ) in rng h2 ;
Line ( Mt , k ) = M . i ;
reconsider m = x / 2 as Element of ExtREAL ;
, U1 , U2 be MSSubAlgebra of U0 ;
set P = Line ( a , d ) , Q = Line ( b , c ) ;
then len p1 < len p2 + 1 ;
let T1 , T2 be correct TopAugmentation of L ;
x <=' y implies DEDEKIND_CUT x c= DEDEKIND_CUT y
set L = n -BinarySequence ( l ) , M = n -BinarySequence ( m ) ;
reconsider i = x1 , j = x2 as Nat ;
rng the_arity_of av c= dom H ;
z1 " = z19 " ;
x0 - r / 2 in L /\ dom f ;
w is wff implies rng w /\ LettersOf S <> {}
set xz = xx ^ <* Z *> ;
len w1 in Seg len w1 ;
( uncurry f ) . ( x , y ) = g . y ;
let a be Element of SubstPoset ( V , { k } ) ;
x . n = |. a . n .| / Ap ;
p `1 <= Gik `1 ;
rng godo c= L~ godo ;
reconsider k = ( i - 1 ) * lb + j as Nat ;
for n be Nat holds F . n is without-infty ;
reconsider xxx = xx as Vector of M ;
dom ( f | X ) = X /\ dom f ;
p , a // p , c & b , a // c , c ;
reconsider x1 = x as Element of m -tuples_on REAL ;
assume i in dom ( a * ( p ^ q ) ) ;
m . bg = p . bg ;
a #Q ( s . m - s . n ) <= 1 ;
S . ( n + k + 1 ) c= S . ( n + k ) ;
assume B1 \/ C1 = B2 \/ C2 ;
X . i = { x1 , x2 } . i ;
r2 in dom ( h1 + h2 ) ;
a - 0. R = a & b - 0. R = b ;
FOR is_closed_on t8 , Q8 ;
set T = DiscrWithInfin ( X , x0 ) ;
Int ( Cl ( Int R ) ) c= Int R ;
consider y be Element of L such that c . y = x ;
rng Fy = { Fy . x } ;
Gk1 .AdjacentSet ( { c } ) c= B \/ S ;
fF is Relation of X * , X ;
set RP = rep_pt ( P ) ;
assume that n + 1 >= 1 and n + 1 <= len M ;
let D be non empty set , f be FinSequence of D , k2 be Element of NAT ;
reconsider pu = u as Element of FTSL1 n ;
g . x in dom f & x in dom g ;
assume that 1 <= n and n + 1 <= len f1 ;
reconsider T = b * N as Element of G ./. N ;
len Pdeb <= len Pdb ;
x " in the carrier of A1 ;
[ i , j ] in Indices AA ;
for m be Nat holds ( Re F ) . m is_simple_func_in S
f . x = a . i .= a1 . k ;
let f be PartFunc of REAL i , REAL ;
rng f = the carrier of Segre_Product A ;
assume s1 = 2 -root ( p |^ 2 - r ) ;
a > 1 & b > 0 implies a #R b > 1
let A , B , C be LINE of IPS ;
reconsider X0 = X , Y0 = Y as RealLinearSpace ;
let a , b be Real , f be PartFunc of REAL , REAL ;
r * ( ( v1 |-- I ) . X ) < r * 1 ;
assume that V is Submodule of X and X is Submodule of V ;
let s be State of SCM , tl , tr be bin-term ;
Q [ ee \/ {. vv .} ] ;
Rotate ( g , W-min L~ z ) = z ;
|. |[ x , v ]| - |[ x , y ]| .| = v - y ;
- f . w = - ( L * w ) ;
z -' y <=' x iff z <=' x + y
( 7 / p1 ) to_power ( 1 / e ) > 0 ;
assume X is BCI-algebra of 0 , 0 , 0 , 0 ;
F . 1 = v1 & F . 2 = v2 ;
( f | X ) . x2 = f . x2 ;
tan . x in dom sec ;
i2 = fs1 /. len fs1 ;
X1 = X2 \/ ( X1 \ X2 ) ;
[. a , b , 1_ G .] = 1_ G ;
let V , W be non empty VectSpStr over F_Complex ;
dom g2 = the carrier of I[01] ;
dom f2 = the carrier of I[01] ;
( proj2 | X ) .: X = proj2 .: X ;
f . ( x , y ) = h1 . ( x9 , y9 ) ;
x0 - r < a1 . n & a1 . n < x0 ;
|. ( f /* s ) . k - GR .| < r ;
len Line ( A , i ) = width ( A ) ;
Sgg opp = ( S . g ) opp ;
reconsider f = v + u as Function of X , the carrier of Y ;
for p being PartState of SCM+FSA holds intloc 0 in dom Initialized p
i1 " ;
arcsin r + arccos r = PI / 2 + 0 ;
for x st x in Z holds f2 is_differentiable_in x ;
reconsider q2 = q / x as Element of REAL ;
0 qua Nat + 1 <= i + j1 ;
assume f in the carrier of ContMaps ( X , Omega Y ) ;
F . a = H / ( x , y ) . a ;
\true T value_at ( C , u ) = TRUE
dist ( ( a * seq ) . n , h ) < r ;
1 in the carrier of Closed-Interval-TSpace ( 0 , 1 ) ;
p2 `1 - x1 > - g ;
|. r1 - p .| = |. a1 .| * |. q - p .| ;
reconsider SEG8E8 = 8 as Element of Seg 8 ;
( A \/ B ) ^b c= ( A ^b ) \/ ( B ^b )
D0W .order() = D0W .size() + 1 ;
i1 = ma + n & i2 = K2 ;
f . a [= f . ( ( f , O1 ) +. a ) ;
f = v & g = u implies f + g = v + u
I . n = Integral ( M , ( F . n ) | E ) ;
chi ( T1 , S ) . s = 1 ;
a = VERUM ( A ) or a = FALSUM ( A ) ;
reconsider k2 = s . b3 as Element of NAT ;
Comput ( P , s , 4 ) . GBP = 0 ;
L~ M1 meets L~ RB2 ;
set h = the continuous Function of X , R ;
set A = { L . ( ksi . n ) : not contradiction } ;
for H st H is atomic holds Pf [ ( H ) ]
set bnt = Sn2 ^\ ix ;
Hom ( a , b ) c= Hom ( a9 , b9 ) ;
1 / ( n + 1 ) < 1 / s " ;
l `1 = [ dom l , cod l ] ;
y +* ( i , y /. i ) in dom g ;
let p be Element of QC-WFF ( Al ( ) ) ;
X /\ X1 c= dom ( f1 - f2 ) ;
p2 in rng ( f :- p1 ) ;
1 <= indx ( D2 , D1 , j1 ) ;
assume x in K2 /\ K3 \/ K4 /\ K5 ;
- 1 <= ( ( f2 ) . O ) `2 ;
Function of I[01] , TOP-REAL 2 ;
k1 -' k2 = k1 - k2 ;
rng seq c= right_open_halfline ( x0 ) ;
g2 in ]. x0 , x0 + r .[ ;
sgn ( p9 , K ) = - 1_ K ;
consider u being Nat such that b = ( p |^ y ) * u ;
ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A
Cl ( union HX ) = union ( clf HX ) ;
len t = len t1 + len t2 ;
vwA = ( v + w ) |-- ( v + Affv ) ;
cv <> DataLoc ( t0 . GBP , 3 ) ;
g . s = sup ( d " { s } ) ;
( . y ) . s = s . ( ( ^ y ) . s ) ;
{ s : s < t } in RAT+ iff t = {}
s ` \ s = s ` \ 0. X ;
defpred P [ Nat ] means B +^ $1 in A ;
( 349 + 1 ) ! = 349 ! * ( 349 + 1 ) ;
UNIVERSE succ A = Tarski-Class UNIVERSE A ;
reconsider y9 = y as Element of ( len y ) -tuples_on COMPLEX ;
consider i2 being Integer such that y0 = p * i2 ;
reconsider p = Y | Seg k as FinSequence of NAT ;
set f = ( S , U ) -TruthEval z , g = ( I , z ) -TruthEval ;
consider Z being set such that lim s in Z and Z in F ;
let f be Function of I[01] , TOP-REAL n ;
not ( SAT M ) . [ n + i , 'not' A ] = 1 ;
ex r be Real st x = r & a <= r & r <= b ;
let R1 , R2 be Element of n -tuples_on REAL ;
reconsider l = ZeroLC ( V ) as Linear_Combination of A ;
|. e .| + |. n .| + |. w .| + |. s .| + a ;
consider y being Element of S such that z <= y and y in X ;
a 'nor' ( b 'or' c ) = 'not' ( a 'or' b 'or' c )
||. xy - gvxy0 .|| < r2 ;
b19 , a19 // b19 , c19 ;
1 <= k2 -' k1
( p `2 / |. p .| - sn ) >= 0 ;
( q `2 / |. q .| - sn ) < 0 ;
E-max C in right_cell ( RC , 1 ) ;
consider e being Element of NAT such that a = 2 * e + 1 ;
Re ( ( lim F ) | D ) = Re ( lim G ) ;
LIN b , a , c or LIN b , c , a ;
p9 , a9 // a9 , b or p9 , a9 // b , a9 ;
g . n = a * ( Sum fa ) .= f . n ;
consider f being Subset of X such that e = f and f is 1 -element ;
F | [: N2 , S :] = CircleMap * Fn ;
q in ( LSeg ( q , v ) \/ LSeg ( v , p ) ) ;
Ball ( m , r0 ) c= Ball ( m , s ) ;
the carrier of (0). V = { 0. V } ;
rng cos = [. - 1 , 1 .]
assume that Re seq is summable and Im seq is summable ;
||. ( vseq . n ) - tv .|| < e ;
set Z = B \ A , O = A /\ B , f = B --> 0 , g = O --> 1 , IT = chi ( A , B ) ;
reconsider t2 = t11 as 0 -termal string of S2 ;
reconsider xseq = seq as sequence of REAL n ;
assume east_halfline E-max C meets L~ go ;
- 1. < ( F . n ) . x - f . x ;
set d1 = real_dist . ( x1 , z1 ) ;
2 |^ 800 -' 1 = 2 |^ 800 - 1 ;
dom vdbrk = Seg len ddbk1 ;
set x1 = - k2 + |. k2 .| + 4 ;
assume for n being Element of X holds 0. <= F . n ;
TT . ( i + 1 ) <= 1 ;
for A being Subset of X holds c . ( c . A ) = c . A
Carrier ( LI + L2 ) c= I2 ;
'not' Ex ( x , p ) => All ( x , 'not' p ) is valid ;
( f | n ) /. ( k + 1 ) = f /. ( k + 1 ) ;
reconsider Z = { [ {} , {} ] } as Element of Normal_forms_on {} ;
then A6 : Z c= dom ( sin * f1 ) ;
|. ( 0. TOP-REAL 2 ) - qz .| < r ;
new_set2 B c= ConsecutiveSet2 ( A , DistEsti ( d ) ) ;
E = dom LExtGp & LExtGp is_measurable_on E ;
exp ( C , A +^ B ) = exp ( C , B ) *^ exp ( C , A )
the carrier of W2 c= the carrier of V ;
I . IC sm = P . IC sm ;
x > 0 implies 1 / x = x to_power ( - 1 )
LSeg ( f ^ g , i ) = LSeg ( f , k ) ;
consider p being Point of T such that C = Class ( R , p ) ;
b , c are_connected & - C , - C are_homotopic ;
assume f = ( id the carrier of OAS ) ;
consider v such that v <> 0. V and f . v = L * v ;
let l be Z_Linear_Combination of {} ( the carrier of V ) ;
reconsider g = f " as Function of U2 , U1 ;
A1 in the Points of G_ ( k , X ) ;
|. - x .| = - ( - x ) .= x ;
set S = MajorityIStr ( x , y , c ) , A = MajorityICirc ( x , y , c ) ;
Lucas n * ( 5 * Lucas n - 2 ) >= 4 * 18 ;
vs1 /. ( k + 1 ) = vs1 . ( k + 1 ) ;
0 mod i = 0 - i * ( 0 qua Nat ) ;
Indices M1 = [: Seg n , Seg n :] ;
Line ( SEGM , j ) = SEGM . j ;
h . ( x1 , y1 ) = [ y1 , x1 ] ;
|. f .| - Re ( |. f .| (#) ( b *' (#) h ) ) is nonnegative ;
x = a1 ^ <* x1 *> ^ b1 ;
Mj is_closed_on IExec ( I , P , s ) , P ;
DataLoc ( t4 . a , 4 ) = intpos ( 0 + 4 ) ;
x + y < - x + y & |. x .| = - x ;
LIN c9 , q , b9 & LIN c9 , q , c9 ;
ff . ( 1 , t ) = f . ( 0 , t ) .= a ;
x + ( y + z ) = x1 + ( y1 + z1 ) ;
ffs . a = ( fffs ) . a
p `1 <= ( E-max C ) `1 ;
set RotEma = Rotate ( Cage ( C , n ) , Ema ) ;
p `1 >= ( E-max C ) `1 ;
consider p such that p = pe and s1 < p /. i ;
|. ( f /* ( s * F ) ) . l - GR .| < r ;
EqSegm ( M , p , q ) = Segm ( M , p , q ) ;
len Line ( N , ( k + 1 + 1 ) ) = width N ;
f1 /* s1 is convergent & f2 /* s1 is convergent ;
f . x1 = x1 & f . y1 = y1 ;
len f <= len f + 1 & len f + 1 <> 0 ;
dom ( Proj ( i , n ) * s ) = REAL m ;
n = k * ( 2 * t ) + ( n mod ( 2 * k ) ) ;
dom B = ( bool the carrier of V ) \ { {} } ;
consider r such that not r _|_ a and not r _|_ x and not r _|_ y ;
reconsider B1 = the carrier of Y1 as Subset of X ;
1 in the carrier of Closed-Interval-TSpace ( 1 / 2 , 1 ) ;
for L being complete Lattice holds ConceptLattice ( Context ( L ) ) , L are_isomorphic
[ gi , gj ] in IR \ IR ~ ;
set S1 = 2GatesCircStr ( x , y , c , 'xor' ) , S2 = MajorityStr ( x , y , c ) ;
assume that f1 is_differentiable_in x0 and f2 is_differentiable_in x0 ;
reconsider y = a ` /\/ FB as Element of L ;
dom s = { 1 , 2 , 3 } & s . 1 = d1 ;
min ( g , 1_minus f ) . c <= h . c ;
set G3 = the removeVertex of G , v ;
reconsider g = f as PartFunc of REAL , REAL-NS n ;
|. ( s1 . m ) #Q p .| < d #Q p ;
for x being element holds x in QClass. u implies x in QClass. t
P = the carrier of ( Euclid n ) | PP ;
assume p10 in LSeg ( p1 , p2 ) /\ L4 ;
( 0. X , x ) to_power ( m * ( k + 1 ) ) = 0. X ;
let C be Category , f be ( Morphism of C ) , g be Element of ( cod f ) Hom ;
2 * a * b + 2 * c * d <= 2 * C1 * C2 ;
let f , g , h be Point of C_NormSpace_of_BoundedFunctions ( X , Y ) ;
set h = hom ( a , g (*) f ) , h2 = hom ( a , g ) , h1 = hom ( a , f ) ;
idseq n | Seg m = idseq m implies m <= n
H * ( g " * a ) in Right_Cosets H ;
x in dom ( cos / sin ) ;
cell ( G , i1 , j2 -' 1 ) misses C ;
LE q2 , p6 , P , p1 , p2 ;
for A being Subset of TOP-REAL n , B being Subset of TOP-REAL n st B is_inside_component_of A holds B c= BDD A
deffunc D ( set , Sequence ) = union rng $2 ;
n + ( - n ) < len pn + ( - n ) ;
a <> 0. K implies the_rank_of M = the_rank_of ( a * M )
consider j such that j in dom b19m and I = len b1m + j ;
consider x1 such that z in x1 and x1 in PB ;
for n ex r being Element of REAL st X [ n , r ]
set Cs2i1 = Comput ( P2 , s2 , i + 1 ) ;
set cv = 3 -rdRWNotIn { a , b , c } ;
conv @ W c= union ( F .: ( E " W ) ) ;
1 in [. - 1 , 1 .] /\ dom arccot ;
r3 <= s0 + r0 / |. v2 - v1 .| ;
dom ( f <##> f4 ) = dom f /\ dom f4 ;
dom ( f (#) G ) = dom ( l (#) F ) /\ Seg k ;
rng ( s ^\ k ) c= dom f1 \ { x0 } ;
reconsider gpp = gp as Point of TOP-REAL n1 ;
( T * ( h . s9 ) ) . x = T . ( h . s9 . x ) ;
I . ( L . ( J . x ) ) = ( I * L ) . ( J . x ) ;
y in dom ( Commute Frege ( A ?. o ) ) ;
for I being non degenerated domRing-like commutative Ring holds the_Field_of_Quotients ( I ) is commutative non empty doubleLoopStr
set s2 = s +* Initialize ( ( intloc 0 ) .--> 1 ) ;
P1 /. IC s1 = P1 . IC s1 ;
lim S1 in the carrier of Closed-Interval-MSpace ( a , b ) ;
v . ( lx . i ) = ( v *' lx ) . i ;
consider n being element such that n in NAT and x = ss1 . n ;
consider x being Element of c such that F1 . x <> F2 . x ;
Choose ( X , 0 , x1 , x2 ) = { Empty } ;
j + 2 * kk + m1 > j + 2 * kk ;
{ s , salpha } on A3 & { s , salpha } on B3 ;
n1 > len crossover ( p2 , p1 , n1 ) ;
mg1 . ( HT ( mg2 , T ) ) = 0. L ;
H1 , H2 are_conjugated implies carr H1 , carr H2 are_conjugated
( N-max L~ ff ) .. ff > 1 ;
]. s , 1 .] = ]. s , 2 .[ /\ [. 0 , 1 .] ;
x1 in [#] ( ( TOP-REAL 2 ) | L~ g ) ;
let f1 , f2 be continuous PartFunc of REAL , the carrier of S ;
DigA ( tz , zz ) is Element of k -SD ;
I P42address = db & I P44const = k2 ;
[: uG , { uG } :] = { [ a , uG ] } ;
for p , w holds ( w | p ) | ( p | ( w | w ) ) = p
consider u2 such that u2 in W2 and x = v + u2 ;
for y st y in rng F holds ex n st y = a |^ n
dom ( ( g * singleton PFuncs ( V , C ) ) | K ) = K ;
ex x be element st x in ( Constants ( U0 ) (\/) A ) . s ;
ex x be element st x in ( OSConstants ( OU0 ) (\/) A ) . s ;
f . x in the carrier of Closed-Interval-TSpace ( - r , r ) ;
( the carrier of ( X1 union X2 ) ) /\ A0 <> {} ;
L1 /\ LSeg ( p10 , p2 ) c= { p00 } ;
( b + ( b - s ) ) / 2 in { r : a < r & r < b } ;
ex_sup_of { x , y } , L & x "\/" y = sup { x , y } ;
for x being element st x in X ex u being element st P [ x , u ]
consider z being Point of GG such that z = y and P [ z ] ;
( the normF of Complex_linfty_Space ) . ( u - v ) <= e ;
len ( w ^ w2 ) + 1 = ( len w + 2 ) + 1 ;
assume q in the carrier of ( TOP-REAL 2 ) | K1 ;
f | EQ ` = g | EQ ` ;
reconsider i1 = x1 , i2 = x2 as Element of NAT ;
( ( a * A ) * B ) @ = ( a * ( A * B ) ) @ ;
assume ex n0 be Element of NAT st iter ( f , n0 ) is contraction ;
Seg len FlattenSeq f2 = dom FlattenSeq f2 ;
( Complement ASeq ) . m c= ( Complement ASeq ) . n ;
f1 . p = pp9 & g1 . pp9 = d ;
FinS ( F , Y ) = FinS ( F , dom ( F | Y ) ) ;
for x , y , z being Element of L holds ( x | y ) | z = z | ( y | x )
|. x .| |^ n / ( n ! ) <= r2 |^ n / ( n ! )
Sum ( Fp ) = Sum ( f ) & dom Fp = dom g ;
assume for x , y being set st x in Y & y in Y holds x /\ y in Y ;
assume W1 is Submodule of W3 & W2 is Submodule of W3 ;
||. tseq . x .|| = lim ||. xseq .|| ;
assume that i in dom D and f | A is bounded_below and g | A is bounded_below ;
( ( p `2 ) - d ) / ( c - d ) <= ( c - d ) / ( c - d ) ;
g | Sphere ( p , r ) = id Sphere ( p , r ) ;
set Nma = N-max L~ Cage ( C , n ) ;
for T being non empty TopSpace holds T is first-countable iff the TopStruct of T is first-countable
width B |-> 0. K = Line ( B , i ) .= B9 . i ;
a <> 0 implies ( A \+\ B ) /// a = ( A /// a ) \+\ ( B /// a )
f is_hpartial_differentiable`13_in u implies pdiff1 ( f , 1 ) is_partial_differentiable_in u , 3
assume that a > 0 and a <> 1 and b > 0 and b <> 1 and c > 0 ;
w1 in Lin { w1 , w2 } & w2 in Lin { w1 , w2 }
p2 /. IC sk2 = p2 . IC sk2 ;
ind ( Tab | b ) = ind b .= ind B ;
[ a , A ] in the Inc of IncProjSp_of ( AS ) ;
m in ( the Arrows of AllRetr C ) . ( o1 , o2 ) ;
B_SUP ( a , CompF ( PA , G ) ) . z = FALSE ;
reconsider phi111 = phi11 , phi222 = phi22 as Element of Phim ;
( len s1 - 1 ) * ( len s2 - 1 ) + 1 > 0 + 1 ;
delta ( D ) * ( f . ( upper_bound A ) - f . ( lower_bound A ) ) < r ;
[ f21 , f22 ] in the carrier' of [: A , B :] ;
the carrier of ( TOP-REAL 2 ) | K1 = K1 ;
consider z being element such that z in dom g2 and p = g2 . z ;
[#] V1 = { 0. V1 } .= the carrier of (0). V1 ;
consider P2 be FinSequence such that rng P2 = M and P2 is one-to-one ;
||. x1 - x0 .|| < s ;
h1 = f ^ ( <* p3 *> ^ <* p *> ) .= h ;
( b , c ) (#) = c .= ( a , c ) (#) ;
reconsider t1 = p1 , t2 = p2 as Term of C , V ;
1 / 2 in the carrier of Closed-Interval-TSpace ( 1 / 2 , 1 ) ;
ex W being Subset of X st p in W & W is open & h .: W c= V ;
( h . p1 ) `2 = C * ( p1 `2 ) + D ;
R . b - a = 2 * a - a - b .= ( 2 - 1 ) * a - b .= a - b ;
consider lambda such that B = ( 1 - lambda ) * C + lambda * A & 0 <= lambda & lambda <= 1 ;
dom g = dom ( ( the Sorts of A ) * ar ) ;
[ P . len1 , P . len2 ] in ==>.-relation ( TS ) ;
s2 = Initialize s , s3 = Initialize s , P2 = P +* pI , P3 = P +* pIF , s4 = Comput ( P3 , s3 , 1 ) , P4 = P3 ;
reconsider M = mid ( z , i2 , i1 ) as S-Sequence_in_R2 ;
y in product ( ( Carrier J ) +* ( V , { 1 } ) ) ;
( 0 , 1 ) (#) = 1 & (#) ( 0 , 1 ) = 0 ;
assume x in the_LeftOptions_of g or x in the_RightOptions_of g ;
consider M being strict MSSubAlgebra of AG such that a = M and T is MSSubAlgebra of M ;
for x st x in Z holds ( exp_R + f ) . x <> 0 ;
len W1 + len W2 + m = 1 + len W3 + m ;
reconsider h1 = vseq . n - tv as Lipschitzian LinearOperator of X , Y ;
( i - j mod len ( p + q ) ) + 1 in dom ( p + q ) ;
assume that s2 is_next_of s1 and F in the LTLold of s2 ;
ALGO_EXGCD ( x , y ) `3_3 = x gcd y ;
for u being element st u in Bags n holds ( p9 + m ) . u = p . u
for B being Subset of uMG st B in E holds A = B or A misses B
ex a being Point of X st a in A & A /\ Cl { y } = { a } ;
set W1 = elementary_tree ( len p + 1 ) , W2 = tree ( p ) \/ W1 , W = W2 with-replacement ( <* len p *> , T ) ;
x in { X where X is Ideal of L opp : not contradiction } ;
the carrier of W1 /\ W2 c= the carrier of W1 ;
in1 ( a , b ) * ( id a ) = in1 ( a , b ) ;
( doms ( X --> f ) ) . x = ( X --> dom f ) . x ;
set x = the Element of LSeg ( g , n ) /\ LSeg ( g , m ) ;
( p => ( q => r ) ) => ( ( p => q ) => ( p => r ) ) in HP_TAUT ;
set pio = LSeg ( G * ( i1 , j ) , G * ( i1 , k ) ) ;
set pio = LSeg ( G * ( i1 , j ) , G * ( i1 , k ) ) ;
- 1 + 1 <= ( i - 2 ) / 2 |^ ( n -' m ) + 1 ;
reproj ( 1 , z0 ) . x in dom ( f1 (#) f2 ) ;
assume that b1 . r = { c1 } and b2 . r = { c2 } ;
ex P st a1 on P & a2 on P & b on P ;
reconsider gf = g9 * f9 , hg = h9 * g9 as strict Element of X ;
consider v1 being Element of T such that Q = ( downarrow v1 ) ` ;
n in { i where i is Nat : i < n0 + 1 } ;
F * ( i , j ) `2 >= F * ( m , k ) `2 ;
assume K1 = { p : p `1 >= ( sn ) * ( |. p .| ) } ;
ConsecutiveSet ( A , succ O1 ) = new_set ConsecutiveSet ( A , O1 ) ;
set IB = I " ;
for i be Nat st 1 < i & i < len z holds z /. i <> z /. 1 ;
X c= [: the carrier of L1 , the carrier of L2 :] ;
consider xa being Element of GF ( p ) such that xa |^ 2 = a ;
reconsider eee = ee , fff = ff as Element of D ;
ex O being set st O in S & C1 c= O & M . O = 0.
consider n being Nat such that for m being Nat st n <= m holds S . m in U1 ;
( f (#) g ) * reproj ( i , x ) is_differentiable_in proj ( i , m ) . x ;
defpred P [ Nat ] means A +^ succ $1 = succ A +^ $1 ;
the_LeftOptions_of - ( - g ) = the_LeftOptions_of g ;
reconsider pw1 = x , pw2 = y as Point of TOP-REAL 2 ;
consider g4 such that g4 = y and x <= g4 and g4 <= x0 ;
for n being Element of NAT ex r being Element of REAL st X [ n , r ]
len ( x2 ^ y2 ) = len x2 + len y2 ;
for x being element st x in X holds x in NatDivisors n0
LSeg ( p01 , p2 ) /\ LSeg ( p1 , p11 ) = {} ;
func FlatCoh X -> set equals CohSp id X ;
len ovlpart ( CR /^ 1 , CR ) <= len CR ;
K is having_valuation & a <> 0. K implies v . ( a |^ i ) = i * v . a
consider o being OperSymbol of S such that t9 . {} = [ o , the carrier of S ] ;
for x st x in X ex y st x c= y & y in X & y is_a_fixpoint_of f
IC Comput ( PP , ss , k ) in dom sIJ ;
q < s & r < s implies not ]. r , s .] c= ]. p , q .]
consider c being Element of Class =_ f such that Y = ( F . c ) `1_3 ;
the ResultSort of S2 = id the carrier' of S2 ;
set xy = [ <* x , y *> , f1 ] , yz = [ <* y , z *> , f2 ] , zx = [ <* z , x *> , f3 ] ;
assume x in dom ( ( exp_R * arccot ) `| Z ) ;
rl in left_cell ( f , i , GoB f ) \ L~ f ;
q `2 >= ( Cage ( C , n ) /. ( i + 1 ) ) `2 ;
set Y = { a "/\" a9 : a9 in X } , b = "\/" ( X , C ) , c = "\/" ( Y , C ) , Z = { b9 : a "/\" b9 [= c } ;
i -' len f <= len f + len f1 -' len f ;
for n ex x st x in N & x in N1 & h . n = x - x0
set si = StepWhile=0 ( a , I , p , s ) . i , psi = p +* while=0 ( a , I ) ;
cp ( k ) . 0 = 1 or cp ( k ) . 0 = - 1
u + Sum ( LLxX ) in ( U \ { u } ) \/ { u + Sum ( LLxX ) } ;
consider xU being set such that x in xU and xU in VV ;
( p ^ ( q | k ) ) . m = ( q | k ) . ( m - len p ) ;
g + h = gg + hh & modetrans ( g + h , X , X ) = g + h ;
L1 is D_Lattice & L2 is D_Lattice iff [: L1 , L2 :] is D_Lattice
x in rng f & y in rng ( f -| x ) implies f -| x -| y = f -| y
assume that 1 < p and 1 / p + 1 / q = 1 and 0 <= a and 0 <= b ;
F* ( f , rho ) = rpoly ( 1 , rho ) *' t + 0_. ( F_Complex ) ;
for X being set , A being Subset of X holds A ` = {} iff A = X
( N-min X ) `1 <= ( NE-corner X ) `1 ;
for c being Element of fixed_QC-variables ( A ) for a being Element of free_QC-variables ( A ) holds c <> a
s1 . GBP = Exec ( i2 , s2 ) . GBP .= 0 ;
for a , b being Real holds |[ a , b ]| in y>=0-plane iff b >= 0
for x , y being Element of X holds x ` \ y = ( x \ y ) ` ;
for X being BCK-algebra of i , j , m , n holds X is BCK-algebra of i , j , j , n
set x1 = |( Re y , Re x )| , x2 = |( Re y , Im x )| , y1 = |( Im y , Re x )| , y2 = |( Im y , Im x )| ;
[ y , x ] in dom ucf & ucf . ( y , x ) = g . y ;
]. lower_bound divset ( D , k ) , upper_bound divset ( D , k ) .[ c= A ;
0 <= delta ( S2 . n ) & |. delta ( S2 . n ) .| < e / 2 ;
( - q `1 ) ^2 <= ( - q `2 ) ^2 ;
set A = 2 / ( b - a ) , B = - ( b + a ) / ( b - a ) , C = 2 / ( d - c ) , D = - ( d + c ) / ( d - c ) ;
for x , y being set st x in RTs & y in RTs holds x , y are_c=-comparable
deffunc Fy ( Nat ) = b . $1 * ( M * G ) . $1 ;
for s being element holds s in SIGMA ( f 'or' g ) iff s in SIGMA ( f ) \/ SIGMA ( g )
for S being non empty non void identifying_close_blocks without_isolated_points TopStruct holds S is strongly_connected implies S is connected
max ( degree ( z `1 ) , degree ( z `2 ) ) >= 0 ;
consider n1 be Nat such that for k holds seq . ( n1 + k ) < r + s ;
Lin ( A /\ B ) is Submodule of Lin ( A ) & Lin ( A /\ B ) is Submodule of Lin ( B ) ;
set ng = nbg '&' ( M . x qua Element of n -tuples_on BOOLEAN ) ;
f " V in PO X & f " V in D(alpha,p) ( X ) ;
rng ( ( a followed_by c ) +* ( 1 , b ) ) c= { a , c , b } ;
consider y9 being WSubgraph of G1 such that y9 = y and dom y9 = WGraphSelectors ;
dom ( f ^ ) /\ left_open_halfline ( x0 ) c= left_open_halfline ( x0 ) ;
Rotation ( i , j , n , r ) is_reverse_of Rotation ( i , j , n , - r ) ;
v ^ ( nc |-> 0 ) in Lin rng ( Bn | c1 ) ;
ex a , k1 , k2 st i = ( a , k1 ) := k2 ;
t . NAT = ( NAT .--> succ i1 ) . NAT .= succ i5 ;
assume that F is being_ball-family and rng p = F and dom p = Seg ( n + 1 ) ;
not LIN b9 , b19 , a9 & not LIN a9 , a19 , c9
( L1 OR L2 ) \& O c= ( L1 \& O ) AND ( L2 \& O )
consider F being ManySortedSet of E such that for d being Element of E holds F . d = F ( d ) ;
consider a , b such that a * ( v - u ) = b * ( y - w ) and 0 < a & 0 < b ;
defpred P [ FinSequence of D ] means |. Sum $1 .| <= Sum |. $1 .| ;
u = pr1 ( x , y , v ) * x + pr2 ( x , y , v ) * y .= v ;
dist ( ( seq . n ) + x , g + x ) <= dist ( ( seq . n ) , g ) + 0 ;
P [ p , index p , {}. bound_QC-variables ( A ) , id bound_QC-variables ( A ) ]
consider X being Subset of CQC-WFF ( Al ) such that X c= Y & X is finite & X is Inconsistent ;
|. b .| * |. eval ( f , z ) .| >= |. b .| * |. eval ( f *' , z ) .| ;
1 < ( S-max L~ Cage ( C , n ) ) .. Cage ( C , n ) ;
l in { l1 where l1 is Real : g <= l1 & l1 <= h } ;
SUM ( ( G . n ) vol ) <= SUM ( ( G0 . n ) vol ) ;
f . y = x .= x * 1_ L .= x * ( power L ) . ( y , 0 ) ;
NIC ( a =0_goto i1 , il ) = { i1 , succ il }
LSeg ( p10 , p2 ) /\ LSeg ( p1 , p11 ) = { p1 } ;
product ( ( Carrier IS ) +* ( i9 , { 1 } ) ) in ZZ ;
Following ( s , n ) | the carrier of S1 = Following ( s1 , n ) ;
W-bound Qa <= q1 `1 & q1 `1 <= E-bound Qa ;
f /. i2 <> f /. ( S_Drop ( ( i1 + len g ) -' 1 , f ) ) ;
M , f / ( x. 3 , a ) / ( x. 4 , a9 ) |= H ;
len ( PR ^ PR1 ) in dom ( PR ^ PR1 ) ;
A |^ mn c= A |^ ( m , n ) & A |^ kl c= A |^ ( k , l ) ;
( REAL n ) \ { q : ( |. q .| ) < a } c= { q1 : ( |. q1 .| ) >= a }
consider n1 be element such that n1 in dom p1 & y1 = p1 . n1 ;
consider X being set such that X in Q and for Z being set st Z in Q & Z <> X holds not X c= Z ;
CurInstr ( P3 , Comput ( P3 , s2 , l ) ) <> halt SCM+FSA ;
for v be VECTOR of l1 holds ||. v .|| = upper_bound rng |. seq_id v .| ;
for phi holds ( phi in X implies not xnot phi in X ) & ( ( not phi in X ) implies xnot phi in X )
rng ( ( Sgm dom fss ) | dom fss1 ) c= dom fss ;
ex c being FinSequence of D ( ) st len c = k ( ) & P [ c ] & a = c ;
the_arity_of compsym ( a , b , c ) = <* homsym ( b , c ) , homsym ( a , b ) *> ;
consider f1 being Function of the carrier of X , REAL such that f1 = |. f .| & f1 is continuous ;
a1 = b1 & a2 = b2 or a1 = b2 & a2 = b1 ;
D2 . indx ( D2 , D1 , n1 + 1 ) = D1 . ( n1 + 1 ) ;
f . ( |[ r ]| ) = |[ r ]| /. 1 .= <* r *> . 1 .= x ;
consider n being Nat such that for m being Nat st n <= m holds CS . n = CS . m ;
consider d being Real such that for a , b being Real st a in X & b in Y holds a <= d & d <= b ;
||. L /. h .|| - K * |. h .| + K * |. h .| <= p0 + K * |. h .| ;
F is commutative & F is associative implies for b being Element of X holds F $$ ( {. b .} , f ) = f . b
p = ( 1 - 0 ) * p0 + 0. TOP-REAL 2 .= 1 * p0 .= p0 ;
consider z1 such that b9 , x3 , z1 is_collinear and o , x1 , z1 is_collinear ;
consider i such that Arg ( ( Rotate ( s ) ) . q ) = s + ( Arg q ) + 2 * PI * i ;
consider g such that g is one-to-one and dom g = card ( f . x ) and rng g = f . x ;
assume that A = P2 \/ Q2 and P2 <> {} and Q2 <> {} and P2 misses Q2 ;
F is associative implies F .: ( F .: ( f , g ) , h ) = F .: ( f , F .: ( g , h ) )
ex x9 be Element of NAT st ( m = x9 & x9 in z & x9 < i or m in { i } ) ;
consider k2 be Nat such that k2 in dom Pk and l in Pk . k2 ;
seq1 = r (#) seq2 iff for n holds seq1 . n = r * seq2 . n
F1 . [ idm a , [ a , a ] ] = [ f * idm a , [ a , b ] ] ;
{ p } "\/" D2 = { p "\/" y where y is Element of L : y in D2 } ;
consider z being element such that z in dom doms F and ( doms F ) . z = y ;
for x , y being element holds x in dom f & y in dom f & f . x = f . y implies x = y ;
v_strip ( G , i ) = { |[ r , s ]| : r <= G * ( 0 + 1 , 1 ) `1 } ;
consider e being element such that e in dom ( T | E1 ) and ( T | E1 ) . e = v ;
( F9 * b1 ) . x = Mx2Tran ( JB , b19m , b29m ) . ( b19m /. j ) ;
- 1. F_Real = mm "**" ( D | n ) .= mm "**" D .= Det M ;
( for x be set st x in dom f /\ dom g holds g . x <= f . x ) implies f - g is nonnegative
len ( f1 . j ) = len ( f2 /. j ) .= len ( f2 . j ) ;
All ( All ( 'not' a , A , G ) , B , G ) '<' Ex ( 'not' All ( a , B , G ) , A , G )
LSeg ( E . k0 , F . k0 ) c= Cl RightComp Cage ( C , k0 + 1 ) ;
x \ ( a |^ m ) = x \ ( ( a |^ k ) * a ) .= ( x \ ( a |^ k ) ) \ a ;
k -th_InputValues InpFs = ( commute InpFs ) . k .= iv ;
for s being State of An holds Following ( s , n ( 0 ) + n ( 2 ) * n ( 1 ) ) is stable ;
for x st x in Z holds f1 . x = a ^2 & ( f1 - f2 ) . x <> 0 ;
support pfexp n \/ support pfexp m c= support max ( pfexp n , pfexp m )
reconsider t = u as Function of [: the carrier of A , the carrier of B :] , the carrier' of C ;
- ( a * sqrt ( 1 + ( b ) ^2 ) ) <= - ( b * sqrt ( 1 + ( a ) ^2 ) ) ;
( succ b1 ) -Veblen a = g . a & b1 -Veblen ( g . a ) = f . ( g . a ) ;
assume that i in dom ( F ^ <* p *> ) and j in dom ( ( F ^ <* p *> ) . i ) ;
{ x1 , x2 , x3 , x4 } = { x1 } \/ { x2 , x3 , x4 }
the Sorts of ( U1 /\ ( U1 "\/"_os U2 ) ) c= the Sorts of U1 ;
( - ( 2 * a ) * ( b / ( 2 * a ) ) + b ) ^2 - delta ( a , b , c ) > 0 ;
consider W00 such that for z being element holds z in W00 iff z in [: N , N :] & P [ z ] ;
assume ( the Arity of S ) . o = <* a *> & ( the ResultSort of S ) . o = r ;
then A4 : Z = dom ( ( ( #Z ( n - 1 ) ) * arccot ) / ( f1 + #Z 2 ) ) ;
middle_sum ( f , Sf ) is convergent & lim ( middle_sum ( f , Sf ) ) = integral ( f ) ;
( 'X' ( alt ( f ) => gnb ) ) => ( xaf => xgnb ) in LTL_axioms ;
len ( M2 * M4 ) = n & width ( M4 ~ * M2 * M4 ) = n ;
X1 union X2 is open SubSpace of X & X1 , X2 are_separated implies X1 is open SubSpace of X
for L being upper-bounded with_suprema antisymmetric RelStr for X being non empty Subset of L holds X "\/" { Top L } = { Top L }
reconsider fb = F3 . b `2 as Function of free_magma ( X , b `2 ) , M ;
consider w being FinSequence of I such that the InitS of M , <* s *> ^ w -leads_to q ;
g . ( a |^ 0 ) = g . ( 1_ G ) .= 1_ H .= ( g . a ) |^ 0 ;
assume for i being Nat st i in dom f ex z being Element of L st f . i = rpoly ( 1 , z ) ;
ex L being Subset of X st Lg = L & for K being Subset of X st K in C holds L /\ K <> {} ;
( the carrier' of C1 ) /\ the carrier' of C2 c= the carrier' of C1 ;
reconsider op = o9 -tree p as Element of TS ( DTConMSA ( the Sorts of A ) ) ;
1 * x1 + 0 * x2 + 0 * x3 = x1 + 0* n .= x1 ;
Ex1 " . 1 = ( Ex1 qua Function ) " . 1 .= 1 / 2 ;
reconsider u112 = the carrier of ( U1 /\ ( U1 "\/" U2 ) ) as non empty Subset of U0 ;
( x "/\" z ) "\/" ( x "/\" y ) "\/" ( z "/\" y ) <= ( x "/\" ( z "\/" y ) ) "\/" ( z "/\" ( x "\/" y ) ) ;
|. f . ( s1 . ( l1 + 1 ) ) - f . ( s1 . l1 ) .| < 1 / ( |. M .| + 1 ) ;
LSeg ( Lower_Seq ( C , n ) /. ii , Lower_Seq ( C , n ) /. ( ii + 1 ) ) is vertical ;
( f | Z ) /. x - ( f | Z ) /. x0 = L /. ( x - x0 ) + R /. ( x - x0 ) ;
( g . c ) * 1 - ( g . c ) * f . c + f . c <= ( h . c ) * ( 1 - f . c ) + f . c ;
( f + g ) | divset ( D , i ) = f | divset ( D , i ) + g | divset ( D , i ) ;
for f st ColVec2Mx f in Solutions_of ( A , ColVec2Mx b ) holds len f = width A
len ( - M4 ) = len M1 & width ( - M4 ) = width M1 ;
for n , i be Nat st i + 1 < n holds [ i , i + 1 ] in the InternalRel of Necklace n
pdiff1 ( f1 , 2 ) is_partial_differentiable_in z0 , 1 & pdiff1 ( f2 , 2 ) is_partial_differentiable_in z0 , 1 ;
a <> 0 & b <> 0 & Arg a = Arg b implies Arg - a = Arg - b
for c be set holds not c in [. a , b .] implies not c in Intersection half_open_sets ( a , b )
assume that V1 is linearly-closed & V2 is linearly-closed and V3 = { v + u : v in V1 & u in V2 } ;
z * x1 + ( 1r - z ) * x2 in M & z * y1 + ( 1r - z ) * y2 in N ;
rng ( ( ( PS qua Function ) " ) * SdX ) = Seg card dfX ;
consider s2 being Rational_Sequence such that s2 is convergent and b = lim s2 and for n holds s2 . n <= b ;
( h2 " ) . n = ( h2 . n ) " & 0 < - 1 / ( h2 . n ) ;
( Partial_Sums abs rseq ) . m = ( abs rseq ) . m .= 0 ;
Comput ( P1 , s1 , 1 ) . b = 0 .= Comput ( P2 , s2 , 1 ) . b ;
- v = ( - 1_ GF ) * v & - w = ( - 1_ GF ) * w ;
sup ( ck .: D ) = sup ( ( inclusion k ) .: ( ck .: D ) ) .= ck . sup D ;
( A |^ ( k , l ) ) ^^ ( A |^.. n ) = ( A |^.. n ) ^^ ( A |^ ( k , l ) )
for R being add-associative non empty addLoopStr , I , J , K being Subset of R holds I + ( J + K ) = ( I + J ) + K
( f . p ) `1 = p `1 / sqrt ( 1 + ( p `2 / p `1 ) ^2 ) ;
for a , b being non zero Nat st a , b are_relative_prime holds ppf ( a * b ) = ppf a + ppf b
consider Al1 being countable QC-alphabet such that r is Element of CQC-WFF ( Al1 ) & Al is Al1 -expanding ;
for X being non empty addLoopStr , M being Subset of X , x , y being Point of X st y in M holds x + y in x + M
{ [ x1 , x2 ] , [ y1 , y2 ] } c= [: { x1 , y1 } , { x2 , y2 } :]
( h . ( f . O ) ) = |[ A * ( ( f . O ) `1 ) + B , C * ( ( f . O ) `2 ) + D ]| ;
Gauge ( C , n ) * ( k , i ) in L~ Upper_Seq ( C , n ) /\ L~ Lower_Seq ( C , n ) ;
redefine pred m , n are_relative_prime means : Def2 : for p being prime Nat holds not ( p divides m & p divides n ) ;
( f * F ) . x1 = f . ( F . x1 ) & ( f * F ) . x2 = f . ( F . x2 ) ;
for L be LATTICE for a , b , c be Element of L holds a \ b <= c & b \ a <= c implies a \+\ b <= c ;
consider b being element such that b in dom ( H / ( x , y ) ) and z = H / ( x , y ) . b ;
assume that x in dom ( F * g ) and y in dom ( F * g ) and ( F * g ) . x = ( F * g ) . y ;
assume not ( ex e being element st e Joins W . 1 , W . 5 , G or e Joins W . 3 , W . 7 , G ) ;
( fdif ( f , h ) . ( 2 * n ) ) . x = ( cdif ( f , h ) . ( 2 * n ) ) . ( x + n * h )
j + 1 = i - len h11 + 2 - 1 + 1 .= i + 1 -' len h11 + 2 -' 1 ;
*' ( /* S ) . f = ( /* S ) . ( opp f ) .= S . ( ( opp f ) opp ) .= S . f ;
consider H such that H is one-to-one and rng H = Carrier ( L2 ) and Sum ( L2 (#) H ) = Sum ( L2 ) ;
R is being_Region & p in R & q in R & p <> q implies ex P st P is_S-P_arc_joining p , q & P c= R
dom <: X --> f :> = meet doms ( X --> f ) .= meet ( X --> dom f ) .= dom f ;
upper_bound ( proj2 .: ( Upper_Arc C /\ Vertical_Line w ) ) <= upper_bound ( proj2 .: ( C /\ Vertical_Line w ) ) ;
for r being Real st 0 < r ex n being Nat st for m being Nat st n <= m holds |. S . m - pp .| < r
i * fx - fe = i * fx - i * yy .= i * ( fx - fy ) ;
consider f being Function such that dom f = bool X and for Y being set st Y in bool X holds f . Y = F ( Y ) ;
consider g1 , g2 be element such that g1 in [#] Y and g2 in union C and g = [ g1 , g2 ] ;
func d |-count n -> Nat means : Def7 : d |^ it divides n & not d |^ ( it + 1 ) divides n ;
fg . [ 0 , t ] = f . [ 0 , t ] .= ( - P ) . ( 2 * x `1 ) .= a ;
t = h . D or t = h . B or t = h . C or t = h . E or t = h . F or t = h . J ;
consider m1 be Nat such that for n st n >= m1 holds dist ( ( seq1 . n ) , ( seq2 . n ) ) < 1 ;
( q `1 / q `2 ) ^2 <= ( q `2 ) ^2 / ( q `2 ) ^2 ;
h0 . ( ( i + 1 ) + 1 ) = h21 . ( ( i + 1 ) + 1 -' len h11 + 2 -' 1 ) ;
consider o being Element of the carrier' of S , x2 being Element of { the carrier of S } such that a = [ o , x2 ] ;
for L being RelStr , a , b being Element of L holds ( a is_<=_than { b } iff a <= b ) & ( a is_>=_than { b } iff b <= a )
||. h1 .|| . n = ||. h1 . n .|| .= |. h . n .| .= ( abs ( h ) ) . n ;
( f - exp_R ) . x = f . x - exp_R . x .= 1 - exp_R . x ;
for F being Function of [: D , D9 :] , E for p being FinSequence of D for q being FinSequence of D9 st r = F .: ( p , q ) holds len r = min ( len p , len q )
( rm1 / 2 ) ^2 + ( rm / 2 ) ^2 <= ( r / 2 ) ^2 + ( r / 2 ) ^2 ;
for i be Nat , M be Matrix of n , K st i in Seg n holds Det M = Sum LaplaceExpL ( M , i )
a <> 0. R implies a " * ( a * v ) = 1. R * v & ( a " * a ) * v = 1. R * v
p . ( j -' 1 ) * ( q *' r ) . ( i + 1 -' j ) = Sum ( p . ( j -' 1 ) * r3 ) ;
deffunc F ( Nat ) = L . 1 + ( ( R /* ( h ^\ n ) ) (#) ( h ^\ n ) " ) . $1 ;
the carrier of H2 ;
Args ( o , FreeMSA X ) = ( ( the Sorts of FreeMSA X ) # * the Arity of S ) . o ;
H1 = ( n + 1 ) -BinarySequence ( |. 2 to_power ( n + 1 ) + h .| ) .= ( n + 1 ) -BinarySequence ( NH ) ;
OO `1_3 = 0 & OO `2_3 = 1 & OO `3_3 = 0 ;
F1 .: ( dom F1 /\ dom F19 ) = Im ( F1 , 1 / 2 ) .= { f /. ( n + 2 ) } ;
b <> 0 & d <> 0 & b <> d & a / b = e / d implies a / b = ( a - e ) / ( b - d )
dom ( ( f +* g ) | D ) = dom ( f +* g ) /\ D .= ( dom f \/ dom g ) /\ D ;
for i being set st i in dom g ex u , v being Element of L , a being Element of B st g /. i = u * a * v ;
g9 * P * g9 " = g99 * ( g9 * P ) * g9 " .= g99 * ( g9 * P * g9 " ) ;
consider i , s1 such that f . i = s1 & ( not emp s1 implies f . ( i + 1 ) <> pop s1 ) ;
hp | ]. a , b .[ = ( g | Z ) | ]. a , b .[ .= g | ]. a , b .[ ;
[ s1 , t1 ] , [ s2 , t2 ] are_connected & [ s2 , t2 ] , [ s3 , t3 ] are_connected ;
H is negative implies ( not H is atomic ) & ( not H is conjunctive ) & ( not H is ExistNext ) & ( not H is ExistGlobal ) & not H is ExistUntill
f1 is total & f2 ^ is total implies ( f1 / f2 ) . c = f1 . c * ( f2 . c ) "
z1 in W2 -Seg ( z2 ) or z1 = z2 & not z1 in W2 -Seg ( z2 ) ;
p = 1 * p .= ( a " * a ) * p .= ( a " ) * ( b * q ) .= ( a " * b ) * q ;
for rseq be Real_Sequence for K be Real st ( for n be Nat holds rseq . n <= K ) holds upper_bound rng rseq <= K
east_halfline E-max C meets ( L~ go \/ L~ pion1 ) or east_halfline E-max C meets L~ co ;
||. f . ( g . ( k + 1 ) ) - f . ( g . k ) .|| <= ||. g . 1 - g . 0 .|| * ( K * ( K to_power k ) ) ;
assume h = ( B .--> B9 ) +* ( C .--> C9 ) +* ( D .--> D9 ) +* ( E .--> E9 ) +* ( A .--> A9 ) ;
|. lower_sum ( ( H . n ) || AB , T ) . k - lower_sum ( H0 , T ) . k .| <= e * ( b - a ) ;
( Fix_inp_ext iv ) . v . e = [ action_at v , the carrier of IIG ] -tree q ;
{ x1 , x1 , x1 , x1 , x1 , x1 , x1 } = { x1 , x1 } .= { x1 } ;
A = [. 0 , 2 * PI .] implies integral ( ( #Z n * cos ) (#) sin , A ) = 0
p9 is Permutation of dom Del ( f1 , i ) & p9 " = ( Sgm Y ) " * ( p " ) * ( Sgm X )
for x , y st x in A & y in A holds |. ( f ^ ) . x - ( f ^ ) . y .| <= 1 * |. f . x - f . y .|
p2 `2 = |. q2 .| * ( ( q2 `2 / |. q2 .| - sn ) / ( 1 - sn ) ) ;
for f be PartFunc of the carrier of CNS , REAL st dom f is compact & f is_continuous_on ( dom f ) holds ( rng f ) is compact
assume not ( for x being Element of Y st x in EqClass ( z , CompF ( B , G ) ) holds ( Ex ( a , A , G ) ) . x = TRUE ) ;
consider Fr2 such that dom Fr2 = n1 and for k be Nat st k in n1 holds Q [ k , Fr2 . k ] ;
ex u , u1 st u <> u1 & u , u1 '//' v , v1 & u , u1 '//' u2 , v2 ;
for G be Group , A , B be non empty Subset of G , N be normal Subgroup of G holds N ~ A * N ~ B = N ~ ( A * B )
for s be Real st s in dom F holds F . s = infty_ext_right_integral ( ( f + g ) (#) ( exp*- s ) , 0 )
width AutMt ( f1 , b1 , b2 ) = len b2 .= width AutMt ( f2 , b1 , b2 ) ;
f | ]. - PI / 2 , PI / 2 .[ = f & dom ( f " ) = ]. - 1 , 1 .[ ;
for n st X is closed_wrt_A1-A7 & a in X & a c= X & y in Funcs ( fs , a ) holds { { [ n , x ] } \/ y : x in a } in X
then A2 : Z = dom ( exp_R (#) arctan ) /\ dom ( exp_R / ( f1 + #Z 2 ) ) ;
func variables_in ( l , V ) -> Subset of V equals { l . k : 1 <= k & k <= len l & l . k in V } ;
for L being non empty TopSpace , N being net of L , M being subnet of N for c being Point of L st c is_a_cluster_point_of M holds c is_a_cluster_point_of N
for s being Element of NAT holds ( seq_id ( v ) + seq_id ( CZeroseq ) ) . s = ( seq_id ( v ) ) . s
z /. 1 = N-min L~ z implies ( N-max L~ z ) .. z < ( S-min L~ z ) .. z
len ( p ^ <* 0 qua Real *> ) = len p + len <* 0 qua Real *> .= len p + 1 ;
assume that Z c= dom ( - ( ln * f ) ) and for x st x in Z holds f . x = a - x & f . x > 0 ;
for R being right_zeroed left_add-cancelable left-distributive non empty doubleLoopStr , I , J being add-closed left-ideal non empty Subset of R holds ( I + J ) *' ( I /\ J ) c= I /\ J
consider f be Function of [: B1 , B2 :] , B12 such that for x be Element of [: B1 , B2 :] holds f . x = F ( x ) ;
dom ( x2 + y2 ) = Seg len x .= Seg len mlt ( x2 , z2 ) .= dom mlt ( x , z ) ;
for S being Contravariant_Functor of C , B , c being Object of C holds S *' . ( id c ) = id ( ( Obj S *' ) . c )
ex a st a = a2 & a in fC1 /\ fC2 & InitSegm ( fC1 , a ) = InitSegm ( fC2 , a ) ;
a in Free ( ( H3 / ( x. 4 , x. k ) ) '&' ( H2 / ( x. 3 , x. k ) ) ) ;
for C1 , C2 being Coherence_Space for f , g being U-stable Function of C1 , C2 st Trace f = Trace g holds f = g
( W-min ( L~ go \/ L~ co ) ) `1 = W-bound ( L~ go \/ L~ co ) ;
u = <* x0 , y0 , z0 *> & f is_hpartial_differentiable`13_in u implies SVF1 ( 3 , pdiff1 ( f , 1 ) , u ) is_differentiable_in z0
( t . {} ) `1 in Vars implies ex x being Element of Vars st x = ( t . {} ) `1 & t = x -term C ;
Valid ( p '&' p , J ) . v = ( Valid ( p , J ) . v ) '&' ( Valid ( p , J ) . v ) .= Valid ( p , J ) . v ;
assume for x , y being Element of S st x <= y for a , b being Element of T ~ st a = f . x & b = f . y holds a >= b ;
func Classes R -> Subset-Family of R means : Def6 : for A being Subset of R holds A in it iff ex a being Element of R st A = Class a ;
defpred P [ Nat ] means ( PRIM:CompSeq ( G ) . $1 ) `1 c= G .reachableFrom ( the Element of the_Vertices_of G ) ;
V2 is_the_direct_sum_of U1 , U2 ;
main-constr ( m term t ) = ( ( m term t ) . {} ) `1 .= [ m , the carrier of C ] `1 .= m ;
d11 = xx ^ d11 .= f . ( yy , d22 ) .= {} ^ d22 .= d22 ;
consider g such that x = g and dom g = dom ff and for x being element st x in dom ff holds g . x in ff . x ;
x + 0c ( len x ) = x + ( len x ) |-> 0c .= addcomplex .: ( x , ( len x ) |-> 0c ) .= x9 ;
k11 -' k21 + 1 in dom ( ( f /^ ( k21 -' 1 ) ) | ( k11 -' k21 + 1 ) ) ;
P1 /\ P2 = { p1 , p2 } ;
reconsider a1 = a , b1 = b , b19 = b9 , p1 = p , p19 = p9 , c1 = c as Element of AFV0 ;
reconsider G1tbF1f = G1 . ( t ! b * F1 . f ) as Morphism of ( G1 * F1 ) . a , ( G1 * F2 ) . b ;
LSeg ( f , i + i1 -' 1 ) = LSeg ( f /. ( i + i1 -' 1 ) , f /. ( i + i1 -' 1 + 1 ) ) ;
integral' ( M , ( P . m ) | dom ( P . n - P . m ) ) <= integral' ( M , ( P . n ) | dom ( P . n - P . m ) ) ;
for x , y being element st [ x , y ] in dom f1 holds f1 . ( x , y ) = f2 . ( x , y ) ;
consider v such that v = y and dist ( u , v ) < min ( r - G * ( i , 1 ) `1 , G * ( i + 1 , 1 ) `1 - r ) ;
for G being Group , H being Subgroup of G , a being Element of H for b being Element of G st a = b for i being Integer holds a |^ i = b |^ i ;
consider B be Function of Seg ( S + L ) , the carrier of V1 such that for x being element st x in Seg ( S + L ) holds P [ x , B . x ] ;
reconsider K1 = { p7 where p7 is Point of TOP-REAL 2 : P [ p7 ] } as Subset of TOP-REAL 2 ;
( N-bound C - S-bound C ) / 2 |^ m <= ( N-bound C - S-bound C ) / 2 |^ ( m9 + 1 ) ;
for x be Element of X , n be Nat st x in E holds ( |. ( Re F ) . n .| ) . x <= P . x & ( |. ( Im F ) . n .| ) . x <= P . x
len @ F = len ( @ p ^ @ q ) + len <* [ 2 , 0 ] *> .= len ( @ p ^ @ q ) + 1 ;
v / ( x. 3 , m1 ) / ( x. 0 , m2 ) / ( x. 4 , m3 ) . ( x. 4 ) = m3 ;
consider r being Element of M such that M , v2 / ( x. 3 , m ) / ( x. 4 , m4 ) |= H2 iff m4 = r ;
func w1 \ w2 -> Element of Union ( G , RK ) equals HKOp ( G , RK ) . ( w1 , w2 ) ;
s2 . b2 = Exec ( n2 , s1 ) . b2 .= s1 . b2 .= s0 . b2 .= s . b2 ;
for n , k be Nat holds 0 <= Partial_Sums ( |. seq .| ) . ( n + k ) - Partial_Sums ( |. seq .| ) . n
set TT = AllTermsOf S , E = TheEqSymbOf S , p = SubTerms phi , F = S -firstChar , r = F . phi , n = |. ar r .| , U = Class R , I = i quotient R , UV = I -TermEval , N1 = n -tuples_on U1 , V = I -AtomicEval phi , uv = i -TermEval , v = i -AtomicEval phi , f = I === . r , G = I . r , g = i . r , d = U -deltaInterpreter ;
Partial_Sums ( seq ) . K + Sum ( seq ^\ ( K + 1 ) ) >= Partial_Sums ( seq ) . K + 0 ;
consider L , R such that for x st x in N holds ( f | Z ) . x - ( f | Z ) . x0 = L . ( x - x0 ) + R . ( x - x0 ) ;
closed_inside_of_rectangle ( a , b , c , d ) = outside_of_rectangle ( a , b , c , d ) `
a * b ^2 + a * c ^2 + b * a ^2 + b * c ^2 + ( c * a ^2 ) + ( c * b ^2 ) >= 6 * a * b * c ;
v / ( x1 , m1 ) / ( x2 , m2 ) / ( x1 , m ) = v / ( x2 , m2 ) / ( x1 , m ) ;
Firing ( Q ^ <* x *> , M0 ) = Firing ( Q , M0 ) +* ( *' { x } --> FALSE ) +* ( { x } *' --> TRUE ) ;
Sum Fr2 = r |^ n1 * ( Sum CatalR ) .= C ( n1 ) .= Cat . n1 .= ( Cat ^\ 1 ) . n ;
( GoB f ) * ( len GoB f , 2 ) `1 = ( GoB f ) * ( len GoB f , 1 ) `1 ;
defpred X [ Element of NAT ] means Partial_Sums ( s ) . $1 = a * ( $1 + 1 ) * $1 / 2 + $1 * b + b ;
the_arity_of g = ( the Arity of S ) . g .= [ ( the Arity of S ) . g , g `2 ] `1 .= g `1 ;
Funcs ( Z , [: X , Y :] ) , [: Funcs ( Z , X ) , Funcs ( Z , Y ) :] are_equipotent & card Funcs ( Z , [: X , Y :] ) = card [: Funcs ( Z , X ) , Funcs ( Z , Y ) :]
for a , b being Element of S , s being Element of NAT st s = n & a = F . n & b = F . ( n + 1 ) holds b = N . ( s + 1 ) \ G . s ;
E , f |= All ( x. 2 , x. 2 'in' x. 0 <=> x. 2 'in' x. 1 ) => x. 0 '=' x. 1 ;
ex R2 being 1-sorted st ( R2 = ( p | ns ) . i ) & ( ( Carrier ( p | ns ) ) . i = the carrier of R2 ) ;
[. a , b + 1 / ( k + 1 ) .[ is Element of Borel_Sets & ( Partial_Intersection half_open_sets ( a , b ) ) . k is Element of Borel_Sets ;
Comput ( P , s , 2 + 1 ) = Exec ( P . 2 , Comput ( P , s , 2 ) ) .= Exec ( a3 := a0 , Comput ( P , s , 2 ) ) ;
( h1 *' ) . k = power ( F_Complex ) . ( - 1_ F_Complex , k ) * ( Sum u ) .= ( ( f *' ) *' ( g *' ) ) . k ;
( f / g ) /. c = ( f /. c ) * ( g /. c ) " .= ( f /. c ) * ( ( g ^ ) /. c ) .= ( f (#) ( g ^ ) ) /. c ;
len CR - len ovlpart ( CR /^ 1 , CR ) = len CR -' len ovlpart ( CR /^ 1 , CR ) ;
dom ( ( r (#) f ) | X ) = dom ( r (#) f ) /\ X .= dom f /\ X .= dom ( f | X ) .= dom ( r (#) ( f | X ) ) ;
defpred P [ Nat ] means for n holds 2 * Lucas ( n + $1 ) = Lucas ( n ) * Lucas ( $1 ) + 5 * Fib ( n ) * Fib ( $1 ) ;
consider f be Function of Segm ( n + 1 ) , Segm ( k + 1 ) such that f = f9 and f is onto "increasing and n < n + 1 implies f " { f . n } = { n } ;
consider chAB be Function of S , BOOLEAN such that chAB = chi ( ( A \/ B ) , S ) & EP . ( A \/ B ) = Prob ( chAB , D ) ;
consider y being Element of Y ( ) such that a = "\/" ( { F ( x , y ) where x is Element of X ( ) : P [ x ] } , L ( ) ) and Q [ y ] ;
assume A1 : A c= Z & Z = dom f & f = exp_R (#) ( sin / cos ) + exp_R / cos ^2 ;
( f /. i ) `2 = ( ( GoB f ) * ( 1 , j2 ) ) `2 .= ( ( GoB f ) * ( I , j2 ) ) `2 ;
dom Shift ( Seq q2 , len Seq q1 ) = { j + len Seq q1 where j is Nat : j in dom Seq q2 } ;
consider G1 , G2 , G3 being Element of V such that G1 <= G2 & G2 <= G3 and g is Morphism of G2 , G3 and f is Morphism of G1 , G2 ;
func - f -> PartFunc of C , V means : Def5 : dom it = dom f & for c st c in dom it holds it /. c = - ( f /. c ) ;
consider phi such that phi is increasing & phi is continuous & for a st phi . a = a & {} <> a for va holds Union L , ( Union L ) ! va |= H iff L . a , va |= H ;
consider i1 , j1 such that [ i1 , j1 ] in Indices GoB f and f /. ( i + 1 ) = ( GoB f ) * ( i1 , j1 ) ;
consider i , n such that n <> 0 and sqrt p = i / n and for i1 being Integer , n1 being Nat st n1 <> 0 & sqrt p = i1 / n1 holds n <= n1 ;
assume that not 0 in Z and Z c= dom ( arccot * ( f ^ ) ) and for x st x in Z holds ( f ^ ) . x > - 1 & ( f ^ ) . x < 1 ;
cell ( G1 , i1 -' 1 , 2 |^ ( m -' AI ) * ( YI -' 2 ) + 2 ) \ L~ f1 c= BDD L~ f1 ;
ex Q1 being open Subset of X st s = Q1 & ex FQ being Subset-Family of [: Y , X :] st FQ c= F & FQ is finite & [: [#] Y , Q1 :] c= union FQ ;
gcd ( mult1 ( r1 , r2 , s1 , s2 , Amp ) , mult2 ( r1 , r2 , s1 , s2 , Amp ) , Amp ) = 1. R ;
Rs = ( Computation ( Computation s2 ) . 1 ) . ( m2 + 1 ) by Th10 .= ( Computation s3 ) . ( m2 + 1 ) .= [ 3 , j1 + m2 , t2 ] ;
CurInstr ( PP , Comput ( PP , ss , m1 + m3 ) ) = CurInstr ( P3 , Comput ( P3 , s3 , m3 ) ) .= halt SCMPDS ;
P1 /\ P2 = { p1 } \/ ( LSeg ( p1 , p11 ) /\ LSeg ( p01 , p2 ) ) \/ ( ( LSeg ( p11 , p2 ) /\ L1 ) \/ { p2 } ) ;
func still_not-bound_in f -> Subset of bound_QC-variables ( Al ) means : Def5 : a in it iff ex i , p st i in dom f & p = f . i & a in still_not-bound_in p ;
for a , b being Element of F_Complex st |. a .| > |. b .| for f being Polynomial of F_Complex st deg ( f ) >= 1 holds f is Hurwitz iff a * f - b * ( f *' ) is Hurwitz
defpred P [ Nat ] means 1 <= $1 & $1 <= len g implies for i , j st [ i , j ] in Indices G & G * ( i , j ) = g . $1 holds j < j0 ;
C1 , C2 are_similar_wrt f , g implies for s1 being State of C1 , s2 being State of C2 st s1 = s2 * f holds s1 is stable iff s2 is stable
( ( ||. f .|| ) | X ) . c = ( ||. f .|| ) . c .= ||. f /. c .|| .= ||. ( f | X ) /. c .|| .= ||. ( f | X ) .|| . c ;
( |. q .| ) ^2 = ( q `1 ) ^2 + ( q `2 ) ^2 & 0 + ( q `1 ) ^2 < ( q `1 ) ^2 + ( q `2 ) ^2 ;
for F be Subset-Family of TM st F is open & not {} in F & for A , B be Subset of TM st A in F & B in F & A <> B holds A misses B holds card F c= iC ;
assume that len F >= 1 and len F = k + 1 and len F = len G and len F = len H and for k st k in dom F holds H . k = g . ( F . k , G . k ) ;
i |^ ( Euler n ) - i |^ s = i |^ ( s + k ) - i |^ s .= i |^ s * i |^ k - i |^ s * 1 .= i |^ s * ( i |^ k - 1 ) ;
consider q being Simple oriented Chain of G such that r = q and q <> {} and FS . ( q . 1 ) = v1 & FT . ( q . ( len q ) ) = v2 and rng q c= rng pq ;
defpred P [ Element of NAT ] means $1 <= ( len I ) - 1 implies ( PartDiffSeq ( g , Z , I ) ) . $1 = ( PartDiffSeq ( f , Z , ( G ^ I ) ) ) . ( len G + $1 ) ;
for A , B being Matrix of n , REAL holds len ( A * B ) = len A & width ( A * B ) = width B & len ( A * B ) = n & width ( A * B ) = n
consider s being FinSequence of the carrier of R such that Sum s = u and for i being Element of NAT st 1 <= i & i <= len s ex a , b being Element of R st s . i = a * b & a in I & b in J ;
func |( x , y )| -> Element of COMPLEX equals |( Re x , Re y )| - <i> * ( |( Re x , Im y )| ) + <i> * ( |( Im x , Re y )| ) + |( Im x , Im y )| ;
consider g0 being FinSequence of FT such that g0 is continuous & rng g0 c= A & g0 . 1 = x1 & g0 . ( len g0 ) = x2 and k0 = len g0 ;
n1 >= len p1 implies crossover ( p1 , p2 , n1 , n2 , n3 , n4 , n5 ) = crossover ( p1 , p2 , n2 , n3 , n4 , n5 )
q `1 * a <= q `1 & - q `1 <= q `1 * a or q `1 * a >= q `1 & q `1 * a <= - q `1 ;
FT . ( pe . len pe ) = FT . ( p . len pe ) .= vs /. ( len pe + 1 ) .= vs . ( len pe + 1 ) ;
consider k1 being Nat such that k1 + k = 1 and a := k = ( <% a := intloc 0 %> ^ ( k1 --> SubFrom ( a , intloc 0 ) ) ^ <% halt SCM+FSA %> ) ;
consider Bo being Subset of B1 , yo1 being Function of Bo , A1 such that Bo is finite and D1 = cylinder0 ( A1 , B1 , Bo , yo1 ) ;
v2 . b2 = ( curry ( F2 , g ) * IdMap B ) . b2 .= curry ( F2 , g ) . ( ( IdMap B ) . b2 ) .= F2 . ( g , id b2 ) ;
dom IExec ( IF , P , Initialize s ) = the carrier of SCMPDS .= dom ( IExec ( I , P , Initialize s ) +* Start-At ( ( card I + 2 ) , SCMPDS ) ) ;
ex dd1 be Real st dd1 > 0 & for h be Real st h <> 0 & |. h .| < dd1 holds |. h .| " * ||. ( R2 * ( L + R1 ) ) /. h .|| < ee ;
LSeg ( G * ( len G , 1 ) + |[ 1 , - 1 ]| , G * ( len G , 1 ) + |[ 1 , 0 ]| ) c= Int cell ( G , len G , 0 ) \/ { G * ( len G , 1 ) + |[ 1 , 0 ]| }
LSeg ( mid ( h , i1 , i2 ) , i ) = LSeg ( h /. ( i + i1 -' 1 ) , h /. ( i + 1 + i1 -' 1 ) ) .= LSeg ( h , i + i1 -' 1 ) ;
A = { q where q is Point of TOP-REAL 2 : LE p1 , q , P , p1 , p2 & LE q , q1 , P , p1 , p2 } ;
( - x ) .|. y = ( - ( 1r *' ) ) * x .|. y .= ( ( - 1r ) *' ) * x .|. y .= x .|. ( ( - 1r ) * y ) .= x .|. ( - y ) ;
0 * sqrt ( 1 + ( p `1 / p `2 ) ^2 ) = p `2 / sqrt ( 1 + ( p `1 / p `2 ) ^2 ) * sqrt ( 1 + ( p `1 / p `2 ) ^2 ) ;
( Ur / Wr ) * ( Wr * ( q - p ) ) = ( Ur / Wr * Wr ) * ( q - p ) .= ( Wr / Wr * Ur ) * ( q - p ) .= Ur * ( q - p ) ;
func Shift ( f , h ) -> PartFunc of REAL , REAL means : Def1 : dom it = - h ++ dom f & for x st x in ( - h ++ dom f ) holds it . x = f . ( x + h ) ;
assume that 1 <= k & k + 1 <= len f and [ i , j ] in Indices G and [ i + 1 , j ] in Indices G & f /. k = G * ( i + 1 , j ) & f /. ( k + 1 ) = G * ( i , j ) ;
not y in variables_in H implies ( x in Free H implies Free ( H / ( x , y ) ) = ( Free H \ { x } ) \/ { y } ) & ( not x in Free H implies Free ( H / ( x , y ) ) = Free H )
defpred P11 [ Element of NAT , Element of NAT , Prime ] means P [ $1 , $2 , $3 ] & $3 |^ ( $3 |-count $2 ) < p |^ ( p |-count $2 ) ;
func sigma_Field ( C ) -> non empty Subset-Family of X means : Def2 : for A being Subset of X holds ( A in it iff for W , Z being Subset of X holds ( W c= A & Z c= X \ A implies C . W + C . Z <= C . ( W \/ Z ) ) ) ;
[#] ( ( dist_min ( P0 ) ) .: ( Q ) ) = ( dist_min ( P0 ) ) .: ( Q ) & lower_bound ( [#] ( ( dist_min ( P0 ) ) .: ( Q ) ) ) = lower_bound ( ( dist_min ( P0 ) ) .: ( Q ) ) ;
rng ( F | the_subsets_of_card ( 2 , S ) ) = {} or rng ( F | the_subsets_of_card ( 2 , S ) ) = { 1 } or rng ( F | the_subsets_of_card ( 2 , S ) ) = { 2 } or rng ( F | the_subsets_of_card ( 2 , S ) ) = { 1 , 2 } ;
( f "" ( rngs f ) ) . i = ( f . i ) " ( ( rngs f ) . i ) .= ( f . i ) " ( rng ( f . i ) ) .= dom ( f . i ) .= ( doms f ) . i ;
consider P1 , P2 being non empty Subset of TOP-REAL 2 such that P1 is_an_arc_of p1 , p2 and P2 is_an_arc_of p1 , p2 and C = P1 \/ P2 and P1 /\ P2 = { p1 , p2 } ;
f . p2 = |[ p2 `1 / sqrt ( 1 + ( p2 `1 / p2 `2 ) ^2 ) , p2 `2 / sqrt ( 1 + ( p2 `1 / p2 `2 ) ^2 ) ]| ;
transl ( a , X ) " . x = ( transl ( a , X ) qua Function ) " . x .= u .= 0. X + u .= ( - a + a ) + u .= - a + x .= transl ( - a , X ) . x ;
for T being non empty normal TopSpace , A , B being closed Subset of T st A <> {} & A misses B holds for G being Rain of A , B , r being Element of DOM , p being Point of T st ( Thunder G ) . p < r holds p in ( Tempest G ) . r
for i st i in dom F & i + 1 in dom F for G1 , G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . ( i + 1 ) holds G2 is strict Subgroup of G1 & [. G1 , (Omega). G .] is strict Subgroup of G2
for x st x in Z holds ( ( ( arctan - arccot ) / exp_R ) `| Z ) . x = ( ( 2 / ( 1 + x ^2 ) ) - arctan . x + arccot . x ) / exp_R . x
pred f is_Rcontinuous_in x0 means : Def2 : x0 in dom f & for a st rng a c= right_open_halfline ( x0 ) /\ dom f & a is convergent & lim a = x0 holds f /* a is convergent & f . x0 = lim ( f /* a ) ;
X1 , X2 are_separated implies ex Y1 , Y2 being non empty SubSpace of X st Y1 , Y2 are_weakly_separated & X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 )
ex N being Neighbourhood of x0 st N c= dom SVF1 ( 1 , f , u ) & ex L , R st for x st x in N holds SVF1 ( 1 , f , u ) . x - SVF1 ( 1 , f , u ) . x0 = L . ( x - x0 ) + R . ( x - x0 ) ;
( p2 `1 ) * sqrt ( 1 + ( p3 `1 ) ^2 ) / sqrt ( 1 + ( p3 `1 ) ^2 ) >= ( p3 `1 ) * sqrt ( 1 + ( p2 `1 ) ^2 ) / sqrt ( 1 + ( p3 `1 ) ^2 ) ;
( ( 1 / t1 (#) ( abs f1 ) ) . x ) to_power m = ( ( 1 / t1 (#) ( abs f1 ) ) to_power m ) . x & ( ( 1 / t2 (#) ( abs g1 ) ) . x ) to_power n = ( ( 1 / t2 (#) ( abs g1 ) ) to_power n ) . x ;
( for x holds f . x = ( cot (#) cos ) . x ) & x in dom cot & x + h in dom cot implies fD ( f , h ) . x = 1 / sin ( x + h ) - sin ( x + h ) - 1 / sin ( x ) + sin ( x )
consider Xx1 being Subset of Y , Yy2 being Subset of X such that t = [: Xx1 , Yy2 :] and ex Y1 being Subset of XV st Y1 = Yy2 /\ [#] ( XV ) & Xx1 is open & Yy2 is open & [: Xx1 , Y1 :] in A ;
card ( S . n ) = card ( { Class ( R_EllCur ( a , b , p ) , [ d , Y , 1 ] ) where Y is Element of GF ( p ) : [ d , Y , 1 ] in EC_SetProjCo ( a , b , p ) } ) .= 1 + Lege_p ( d |^ 3 + a * d + b ) ;
( ( ( E-bound D ) - ( W-bound D ) ) / ( 2 |^ m ) ) * ( i - 2 ) = ( ( E-bound D ) - ( W-bound D ) ) * ( ( i1 - 2 ) / ( 2 |^ n ) ) .= ( ( ( E-bound D ) - ( W-bound D ) ) / ( 2 |^ n ) ) * ( i1 - 2 ) ;