reserve k, k1, n, n1, m, m1 for Element of NAT;
 reserve X, y for set;
 reserve p for Real;
 reserve r for real number;
 reserve a, a1, a2, b, b1, b2, x, x0, z, z0 for Complex;
 reserve s1, s2, s3, seq, seq1 for Complex_Sequence;
 reserve Y for Subset of COMPLEX;
複素空間の部分空間をYと置く
 reserve f, f1, f2 for PartFunc of COMPLEX,COMPLEX;
複素関数の部分関数をf,f1,f2と置く
 reserve Nseq for increasing Seq_of_Nat;
Nseqを増加順序立てられた自然数列と置く
 theorem :: 2
  0 < r implies s1is convergent;
 If 0 < r and for every n holds s1(n) = 1/(n+r) , then s1 is convergent
0 Complex means:: def 7
  ex N being Neighbourhood of z0 st N c= dom f &
  ex L,R st it = L/.1r & for z be Complex
  st z in N holds f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0);
 end;
Let us consider f, z0. Let us assume that f is differentiable in z0. 
The functor f′(z0) yields a Complex number and is defined as follows:
there exists a neighbourhood N of z0 such that N ⊆ domf and there exist L,
R such that f′(z0) = L/.(1r) and for every z such that z ∈ N holds 
f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0).
f,z0と置くとz0点でfは微分可能であると仮定する。
以下より、関数f′(z0)領域は複素数であると定義できる。:
あるz0の近傍Nが存在する。fの定義域の部分空間Nと
存在するL,R においてf′(z0) = L/.(1r)かつ任意のｚにおいてz∈Nはf/.z-f/.z0 = L/.(z-z0)+R/.(z-z0)をもつ。
-------------------------------------------------------------------------------------------------
 definition
  let f;
  attr f is differentiable means:: def 8
  for x st x in dom f holds f is_differentiable_in x;
 end;
Let f. We say that f is differentiable if and only if:
for x such that x in dom f holds f is_differentiable_in x.
fをとる、fは微分可能とする。
任意のxxは定義域を持ち、fはxで微分可能
-------------------------------------------------------------------------------------------------
 definition
  let f,X;
  pred f is_differentiable_on X means:: def 9
  X c= dom f & f|X is differentiable;
 end;
Let us consider f, X. We say that f is differentiable on X if and only if:
X ⊆ domf and for every x such that x ∈ dom f holds f|X is differentiable
あるｆ,Xを考える。f はX上で微分可能ということは、fの定義域の部分空間X かつｄf/dXは微分可能である。
-------------------------------------------------------------------------------------------------
 theorem :: 8
  f is_differentiable_on X implies X is Subset of COMPLEX;
If f is differentiable on X, then X is a subset of COMPLEX
FはX上で微分可能、そのときXは部分複素空間である。
-------------------------------------------------------------------------------------------------
 definition :: complex-membered set
  let X be Subset of COMPLEX;
  attr X is closed means:: def 10
  for s1 be Complex_Sequence
  st rng s1 c= X & s1 is convergent holds lim s1 in X;
 end;
Let X be Subset of COMPLEX. We say that X is closed if and only if:
For every sequence s1 be Complex_Sequence such that rng s1 ⊆ X 
and s1 is convergent holds lim s1 ∈ X.
部分複素空間Xをもってくる.Xは閉である、同値なのは：
任意の列s1は複素列とおいてＸの部分空間である値域s1、かつ、ｓ1が収束することはlim s1 ∈Xを有する。
-------------------------------------------------------------------------------------------------
 definition
  let X be Subset of COMPLEX;
  attr X is open means:: def 11
  X` is closed;
 end;
Let X be a subset of COMPLEX. 
We say that X is open if and only if:  X` is closed.
Xは複素空間部分空間をもってくる。Ｘが開空間というのはX`は閉空間というのと同値である。
-------------------------------------------------------------------------------------------------
 theorem :: 9
  for X being Subset of COMPLEX st X is open
  for z0 be Complex st z0 in X
  ex N being Neighbourhood of z0 st N c= X;
Let X be a subset of COMPLEX. Suppose X is open. 
Let z0 be a Complex. If z0 ∈ X, then there exists a neighbourhood N of z0 such that N ⊆ X.
Ｘを複素部分空間とする。Ｘは開空間と仮定する。
z0は複素空間とする。もし、Xの要素z0、そのとき、存在するz0の近傍Nにおいて、Xの部分空間N
-------------------------------------------------------------------------------------------------
 theorem :: 10
  for X being Subset of COMPLEX st X is open
  for z0 be Complex st z0 in X holds
  ex g be Real st {y where y is Complex : |.y-z0.| < g} c= X;
Let X be a subset of C. Suppose X is open. Let z0 be a complex number.
Suppose z0 ∈ X. Then there exists a real number g such that {y; y ranges
over complex numbers: |y − z0| < g} ⊆ X.
over complex numberではなくin complex numberではないでしょうか？？？.
Xは複素数の部分集合とする。Ｘを開集合と仮定する。
z0は複素数とする。
Ｘの要素z0と仮定する。そのとき存在する実数ｇにおいて、{y|yの値域は複素数：|y − z0| < g} ⊆ X.
-------------------------------------------------------------------------------------------------
 theorem :: 11
  for X being Subset of COMPLEX holds
  ((for z0 be Complex st z0 in X holds ex N be Neighbourhood of z0 st N c= X)
  implies X is open);
Let X be a subset of C. Suppose that for every complex number z0 such
that z0 ∈ X there exists a neighbourhood N of z0 such that N ⊆X. Then  X is open.
Ｘは複素数の部分集合。任意の複素数z0において、z0 ∈ Xz0近傍に存在するＮにおいて、そのときＸは開集合である。
-------------------------------------------------------------------------------------------------
 theorem :: 12
  for X be Subset of COMPLEX holds X is open iff
  for x be Complex st x in X
  ex N be Neighbourhood of x st N c= X;
Let X be a subset of C. Then X is open if and only if for every complex
number x such that x ∈ X there exists a neighbourhood N of x such that N ⊆ X.
Ｘは複素数の部分集合と置く、そのとき、Xは開集合であることは、全ての複素数ｘにおいてx ∈ X、xの近傍に存在するNにおいてN ⊆ Xと同値である。
-------------------------------------------------------------------------------------------------
 theorem :: 13
  for X be Subset of COMPLEX, z0 be Element of COMPLEX, r be Element of REAL st
  X = {y where y is Complex : |.y-z0.| < r} holds X is open;
Let X be a subset of C, z0 be an element of C, and r be an element of R.
If X = {y; y ranges over complex numbers: |y − z0| < r}, then X is open.
Xは複素数の部分集合、z0は複素数の要素、rは実数の要素と置く。
もし、X={y|yの値域は複素数:|y-z0| PartFunc of COMPLEX,COMPLEX means:: def 12
  dom it = X & for x st x in X holds it/.x = diff(f,x);
 end;
Let us consider f, X. 
Let us assume that f is differentiable on X. 
The functor f`|X yielding 
a partial function from COMPLEX to COMPLEX is defined by:
dom f`|X = X  and for every x such that x ∈ X holds f`|X/.x = diff(f,x).
ｆ、ｘを考える。
ｆはＸ上で微分可能と仮定する。
部分関数である関数f`|Xの複素空間から複素空間への意味は
定義域f`|X = Xかつ、任意のxにおいて、x ∈ Xがf`|X/.x = diff(f,x)が成り立つ、と定義される。
-------------------------------------------------------------------------------------------------
 registration let seq be non-zero Complex_Sequence, k be Nat;
  cluster seq ^\k -> non-zero;
一時エリア、０でない複素列seqとする、kは自然数列の集まり、０以外の要素seq^k
 theorem :: 19
  (seq-seq1)^\k = (seq^\k)-(seq1^\k);
-------------------------------------------------------------------------------------------------
 theorem :: 21
  (seq(#)seq1)^\k = (seq^\k)(#)(seq1^\k);
 (seq・seq1)^k = seq^k ・seq^k
-------------------------------------------------------------------------------------------------
 theorem :: CFDIFF_1:22
  for x0 be Complex for N being Neighbourhood of x0 st
  f is_differentiable_in x0 & N c= dom f holds
  for h,c st rng c = {x0} & rng (h+c) c= N holds
  h"(#)(f/*(h+c)-f/*c) is convergent & diff(f,x0) = lim (h"(#)(f/*(h+c)-f/*c));
Let x0 be a complex number and N be a neighbourhood of x0. Suppose f
is differentiable in x0 and N ⊆ dom f. Let given h, c. Suppose rng c = {x0}
and rng(h + c) ⊆ N. Then h" (f • (h + c) − f • c) is convergent and  f0(x0) = lim(h" (f • (h + c) − f • c)).
ｘ0は複素数としＮはx0の近傍。ｆはx0において微分可能、かつ、定義域ｆの部分空間Ｎと仮定する。
h,cを持ってくる。rng c = {x0} かつ rng(h + c) ⊆ N。そのときh" (f • (h + c) − f • c) は収束し、かつ、diff(f,x0) = lim(h" (f • (h + c) − f • c))
-------------------------------------------------------------------------------------------------
 theorem :: CFDIFF_1:23
  for f1,f2,x0 st f1 is_differentiable_in x0 & f2 is_differentiable_in x0
  holds f1+f2 is_differentiable_in x0 &
  diff(f1+f2,x0) = diff(f1,x0)+diff(f2,x0);
Let given f1, f2, x0. Suppose f1 is differentiable in x0 and f2 is differentiable in x0. 
Then f1 + f2 is differentiable in x0 and (f1 + f2)0(x0) = f10(x0) + f20(x0).
f1, f2, x0を持ってくる。f1はx0において微分可能、かつ、f2はx0において微分可能と仮定する。
そのとき、f1+f2はx0において微分可能、かつ、(f1 + f2)0(x0) = f10(x0) + f20(x0).
-------------------------------------------------------------------------------------------------
 theorem :: 26
 for f1,f2,x0 st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
  f1(#)f2 is_differentiable_in x0 &
  diff(f1(#)f2,x0) = (f2/.x0)*diff(f1,x0)+(f1/.x0)*diff(f2,x0);
Let given f1, f2, x0. Suppose f1 is differentiable in x0 and f2 is differentiable in x0. 
Then f1 f2 is differentiable in x0 and (f1 f2)0(x0) = (f2)x0 • f10(x0) + (f1)x0 • f20(x0).
f1, f2, x0を持ってくる。f1はx0において微分可能、かつ、f2はx0において微分可能と仮定する。
そのとき、f1・f2はx0において微分可能、かつ、(f1 f2)0(x0) = (f2)x0 • f10(x0) + (f1)x0 • f20(x0)
-------------------------------------------------------------------------------------------------
 theorem :: 27
  for f,Z st Z c= dom f & f|Z = id Z holds
  f is_differentiable_on Z & for x st x in Z holds (f`|Z)/.x = 1r;
For all f, Z such that Z ⊆ dom f and f | Z = idZ holds f is differentiable 
on Z and for every x such that x 2 Z holds (f0  | Z)x = 1C.
任意のｆ,Ｚにおいて、ｆの定義域Z,かつ、f|Z=id Zより、Ｚ上のfで微分可能であり、かつ、任意のｘにおいて,Zの要素xより(f0  | Z)x = 1Cが成立する。
-------------------------------------------------------------------------------------------------
 theorem :: 30
  for a,f,Z st Z c= dom (a(#)f) & f is_differentiable_on Z holds
  a(#)f is_differentiable_on Z & for x st x in Z holds
  ((a(#)f)`|Z)/.x = a*diff(f,x);
  
Let given a, f, Z. Suppose Z ⊆ dom(a f) and f is differentiable on Z.
Then a f is differentiable on Z and for every x such that x ∈ Z holds  ((a f)0 |Z)x = a • f0(x).
a,f,Zをもってくる。定義域(a f)の部分集合Ｚを仮定し、かつ、ｆはZ上で微分可能である。
そのとき、a・fはZ上で微分可能、かつ、任意の全てのxにおいて、Ｚの要素xより((a f)0 |Z)x = a • f0(x)が成立する。
-------------------------------------------------------------------------------------------------
 theorem :: 32
  Z c= dom f & f|Z is constant implies
  f is_differentiable_on Z & for x st x in Z holds (f`|Z)/.x = 0c;
If Z ⊆ domf and f is a constant on Z, then f is differentiable on Z
and for every x such that x ∈ Z holds (f`|Z)/.x = 0c.
もし、fの定義域Z,かつ,fはZ上で一定、そのとき、ｆはZ上で微分可能、かつ、任意の全てのxにおいてZの要素xにおいて(f`|Z)/.x = 0cが成り立つ。
-------------------------------------------------------------------------------------------------
 theorem :: 33
  Z c= dom f & (for x st x in Z holds f/.x = a*x+b) implies
  f is_differentiable_on Z & for x st x in Z holds (f`|Z)/.x = a;
Suppose Z ⊆ dom f and for every x such that x 2 Z holds fx = a •x+b.
ｆの定義域Ｚ、かつ、z上の任意のｘを仮定すると、fx = a •x+b 
Then f is differentiable on Z and for every x such that x ∈ Z holds (f0|Z)x = a.
そのとき、ｆはZ上で微分可能、かつ任意のxにおいて、整数Ｚの要素xにおいて(f0|Z)x = aが成り立つ
-------------------------------------------------------------------------------------------------
 theorem :: 34
  for x0 be Complex holds
  f is_differentiable_in x0 implies f is_continuous_in x0;
For every complex number x0 such that f is differentiable in x0 holds f is continuous in x0.
任意の複素数x0において、fはx0で微分可能だと成り立つならば、fはx0で連続
-------------------------------------------------------------------------------------------------
 theorem :: 35
  f is_differentiable_on X implies f is_continuous_on X;
If f is differentiable on X, then f is continuous on X.
もし、ｆはX上で微分可能、そのときｆはX上で連続。
-------------------------------------------------------------------------------------------------
 theorem :: 36
  f is_differentiable_on X & Z c= X implies f is_differentiable_on Z;
If f is differentiable on X and Z ⊆ X, then f is differentiable on Z.
もし、fはX上で微分可能、かつZはXの部分空間、そのとき、fはZ上で微分可能。
-------------------------------------------------------------------------------------------------
 theorem :: 37
  seq is convergent implies |.seq.| is convergent;
If seq is convergent, then |.seq.| is convergent.
もし、seq は収束すると、seqの絶対値は収束する。
-------------------------------------------------------------------------------------------------
 theorem :: 38
  f is_differentiable_in x0 implies ex R st R/.0c = 0c & R is_continuous_in 0c;
  
If f is differentiable in x0, then there exists R such that R(0) = 0 and  R is continuous in 0.
もし、fはx0で微分可能、そのとき存在するRにおいてR(0)=0 かつRは0で連続。
-------------------------------------------------------------------------------------------------
 reserve k, k1, n, n1, m, m1 for Element of NAT;
 reserve X, y for set;
 reserve Y for Subset of COMPLEX;
 reserve f, f1, f2 for PartFunc of COMPLEX,COMPLEX;
 reserve r, p for Real;
 reserve a, a1, a2, b, b1, b2, x, x0, y, y0, z, z0 for Complex;
 definition let f be PartFunc of COMPLEX,COMPLEX; 
  func Re f -> PartFunc of COMPLEX,REAL means
 :: CFDIFF_2:def 1
  dom f = dom it &
  for z be Complex st z in dom it holds it.z = Re(f/.z);
 end;
Let f be a partial function from C to C. The functor Re f  yielding a partial function from C to R is defined by:
(Def. 1) dom f = dom Re f   and for every complex number z such that z ∈ dom Re f  holds Re f  (z) = Re (fz).
任意のｆは複素空間から複素空間への部分関数。
関数実部ｆの部分関数の複素空間から実数空間への場は以下によって定義されている：
（定義１）ｆの定義域＝ｆの実数の定義域かつ任意の複素数ｚにおいて、ｚへのｆの実数部の定義域はf  (z)の実部= (fz)の実部に含まれる
-------------------------------------------------------------------------------------------------
 definition let f be PartFunc of COMPLEX,COMPLEX; 
  func Im f -> PartFunc of COMPLEX,REAL means
 :: CFDIFF_2:def 2
  dom f = dom it & for z be Complex st z in dom it holds it.z=Im (f/.z);
 end;
Let f be a partial function from C to C. The functor Im f  yielding a partial function from C to R is defined as follows:
(Def. 2) dom f = dom Im f  and for every complex number z such that z ∈ dom Im f  holds Im f  (z) = Im (fz).
任意のｆは複素関数から複素関数への部分関数。
複素空間から実数空間への部分関数ｆの虚部の場は以下のように定義される：
（定義２）ｆの定義域＝ｆの虚部の定義域かつ任意の複素数ｚにおいて、ｚ∈ｆの虚部の定義域はf  (z)の虚部 = (fz)の虚部に含まれる。
-------------------------------------------------------------------------------------------------
 theorem :: CFDIFF_2:2
  for f be PartFunc of COMPLEX, COMPLEX,
  u,v be PartFunc of REAL 2, REAL,
  z0 be Complex,
  x0, y0 be Real,
  xy0 be Element of REAL 2 st
  (for x, y be Real st x+y*＜i> in dom f holds
  <*x,y*> in dom u & u.<*x,y*> = (Re f).(x+y*＜i＞)) &
  (for x,y be Real st x+y*＜i> in dom f holds
  <*x,y*> in dom v & v.<*x,y*> = (Im f).(x+y*＜i＞)) &
  z0 = x0+y0*＜i＞ & xy0 = <*x0,y0*> & f is_differentiable_in z0 holds
  u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 &
  v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 &
  Re diff(f,z0) = partdiff(u,xy0,1) & Re diff(f,z0) = partdiff(v,xy0,2) &
  Im diff(f,z0) =-partdiff(u,xy0,2) & Im diff(f,z0) = partdiff(v,xy0,1);
Let f be a partial function from C to C, u, v be partial functions from R2 to R, 
z0 be a complex number, x0, y0 be real numbers, 
and x1 be an element of R2. 
任意のｆはＣからＣへの部分関数、u,vはR2からRへの部分関数、z0は複素数、x0,y0は実数、そして、x1はR2の要素である。
Suppose that
以下の仮定をする。
(i) for all real numbers x, y such that x+y • i ∈ dom f holds   ∈ dom u and u  = Re(f)(x + y • i),
(i)任意の実数x,yにおいて、ｆの定義域の要素x+y･iはuの定義域の要素 かつ  u  = 実数部(f)(x + y • i)に含まれる。
(ii) for all real numbers x, y such that x+y • i ∈ dom f holds   ∈ dom v and v  = Im(f)(x + y • i),
(ii)任意の実数x,yにおいて、ｆの定義域の要素x+y･iはvの定義域の要素 かつ  v  = 虚数部(f)(x + y • i)に含まれる。
(iii) z0 = x0 + y0 • i,
(iv) x1 =  , and
かつ
(v) f is differentiable in z0.
ｆはz0で微分可能。
Then
そのとき、
(vi) u is partially differentiable in x1 w.r.t. 1 coordinate and partially differentiable in x1 w.r.t. 2 coordinate,
uは１座標に関して、x1において部分微分可能かつ２座標に関してx１で部分微分可能。
(vii) v is partially differentiable in x1 w.r.t. 1 coordinate and partially differentiable in x1 w.r.t. 2 coordinate,
(viii)   Re(f ′(z0))  =     partdiff(u, x1, 1),
(ix)     Re(f ′(z0))  =     partdiff(v, x1, 2),
(x)      Im(f ′(z0))  = − partdiff(u, x1, 2), and
(xi)     Im(f ′(z0))  =     partdiff(v, x1, 1).
-------------------------------------------------------------------------------------------------
 theorem :: CFDIFF_2:5
  for u be PartFunc of REAL 2, REAL,
  x0, y0 be Real,
  xy0 be Element of REAL 2
  st xy0 = <*x0,y0*> & <>*u is_differentiable_in xy0
  holds
  u is_partial_differentiable_in xy0,1 &
  u is_partial_differentiable_in xy0,2 &
  <* partdiff(u,xy0,1) *> = diff(<>*u,xy0).(<* 1,0 *>) &
  <* partdiff(u,xy0,2) *> = diff(<>*u,xy0).(<* 0,1 *>);
Let u be a partial function from R2 to R, x0, y0 be real numbers, and
x1 be an element of R2. Suppose x1 =   and < u >  is differentiable in x1. 
任意のuはR2からRへの部分関数、x0,y0は実数、かつ、x1はR2の要素。
x1 =   かつ< u >はx1で微分可能であることを仮定する。
Then 
そのとき、
(i) u is partially differentiable in x1 w.r.t. 1 coordinate and partially differentiable  in x1 w.r.t. 2 coordinate,
1座標に関して、uはx1で部分微分可能。かつ、２座標に関してx1で部分微分可能。
(ii)   < partdiff(u, x1, 1) >  = < u′(x1) <1, 0>), and
部分微分、かつ
(iii)  < partdiff(u, x1, 2) >  = < u′(x1) <0, 1>).
-------------------------------------------------------------------------------------------------
 theorem :: CFDIFF_2:6
  for f be PartFunc of COMPLEX, COMPLEX,
  u,v be PartFunc of REAL 2, REAL,
  z0 be Complex,
  x0, y0 be Real,
  xy0 be Element of REAL 2 st
  (for x,y be Real st <*x,y*> in dom v holds x+y*＜i＞ in dom f) &
  (for x,y be Real st x+y*＜i＞ in dom f holds
  <*x,y*> in dom u & u.<*x,y*> = (Re f).(x+y*＜i＞)) &
  (for x,y be Real st x+y*＜i＞ in dom f holds
  <*x,y*> in dom v & v.<*x,y*> = (Im f).(x+y*＜i＞)) &
  z0 = x0+y0*＜i＞ & xy0 = <*x0,y0*> &
  <>*u is_differentiable_in xy0 &
  <>*v is_differentiable_in xy0 &
  partdiff(u,xy0,1) = partdiff(v,xy0,2) &
  partdiff(u,xy0,2) = -partdiff(v,xy0,1)
  holds
  f is_differentiable_in z0 &
  u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 &
  v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 &
  Re diff(f,z0) = partdiff(u,xy0,1) & Re diff(f,z0) = partdiff(v,xy0,2) &
  Im diff(f,z0) =-partdiff(u,xy0,2) & Im diff(f,z0) = partdiff(v,xy0,1);
 Let f be a partial function from C to C,
任意のｆはｃからＣへの部分関数
 u, v be partial functions from R2 to R, 
u, v はR2からRへの部分関数、
 z0 be a complex number, 
z0は複素数、
 x0, y0 be real numbers, and
x0,y0は実数、で、
 x1 be an element of R2. 
x1はR2の要素である。
 Suppose that for all real numbers x, y such that 
   ∈ dom v holds x+y•i ∈ dom f and
  for all real numbers x, y such that x+y•i ∈ dom f holds
   ∈ dom u and u  = Re(f)(x+y • i) and
  for all real numbers x, y such that x+y•i ∈ dom f holds 
   ∈ dom v and v  = Im(f)(x+y•i)
 and z0 = x0 + y0 • i and x1 =   and ＜u> is differentiable in x1
 and    is differentiable in x1 and partdiff(u, x1, 1) = partdiff(v, x1, 2)
 and partdiff(u, x1, 2) = −partdiff(v, x1, 1).
任意(すべて)の実数x,yを仮定すると、定義域vの要素は定義域fの要素x+y•iに含まれる。かつ、任意の実数x,yにおいて、fの定義域の要素x+y•i はuの定義域の要素に含まれる、かつ、 u  = Re(f)(x+y • i) 、かつ、
任意の実数x,yにおいて、fの定義域の要素x+y•i はvの定義域の要素、かつ、v  = Im(f)(x+y•i)、かつ、z0 = x0 + y0 • i 、かつ、 x1 = 、かつ、＜u＞   はx1で微分可能、かつ、 は x1 において微分可能、かつ、 partdiff(u, x1, 1) = partdiff(v, x1, 2)、かつ、partdiff(u, x1, 2) = −partdiff(v, x1, 1).
 Then 
 f is differentiable in z0
 and u is partially differentiable in x1 w.r.t. 1 coordinate and 
 partially differentiable in x1 w.r.t. 2 coordinate and 
 v is partially differentiable in x1 w.r.t. 1 coordinate and 
 partially differentiable in x1 w.r.t. 2 coordinate and 
 Re(f′(z0)) =    partdiff(u, x1, 1) and Re(f′(z0))  = partdiff(v, x1, 2) and
 Im(f′(z0)) = −partdiff(u, x1, 2) and Im(f′(z0))  = partdiff(v, x1, 1).
そのとき、fはz0で微分可能、
かつ、１座標に関してuはx1で部分微分可能、かつ、２座標に関して部分微分可能、
かつ、１座標に関してvはx1で部分微分可能、かつ、２座標に関して部分微分可能、かつ、Re(f′(z0)) =    partdiff(u, x1, 1) かつ Re(f′(z0))  = partdiff(v, x1, 2) and
Im(f′(z0)) = −partdiff(u, x1, 2) かつ Im(f′(z0))  = partdiff(v, x1, 1).
---------------------------------------------------------------------------------------------
---------------------------------------------------------------------------------------------
 omega is the smallest nonempty ordinal number which is a limit.
 It is defined in terms of ordinals.
 We can think about omega as the set on all natural numbers.
 omega is defined in ORDINAL1.
オメガは、制限のある、最も小さい空でない序数です。
それは、序列化した項に関して定められます。
私達は、すべての自然数の集合として、オメガについて考えることができます。
オメガは、ORDINAL1で定められています。
 
 Wikipedia defines Omega:
 Transfinite numbers are cardinal numbers or
 ordinal numbers that are larger than all finite numbers.
 ω (omega) is defined as the lowest transfinite ordinal number.
ウィキペディアは、オメガを定めます：
超限数は、すべての有限数より大きい基数または序数です。
ω（オメガ）は、最も低い超限序数と定義されます。
 Omega is an "extension" to the Natural numbers, to get closure under limit
 operations, not that dissimilar to the integers (positive and negative)
 which are closure of N under subtraction.
オメガは自然数への「拡張」です。そして、極限演算で閉じています。そして、それが引き算において、自然数Nの下で閉じている、整数（正と負の）と異なりません。
 definition
  func omega -> set means
  {} in it & it is limit_ordinal & it is ordinal &
  for A st {} in A & A is limit_ordinal holds it c= A;
 end;
定義
関数 omega 集合の意味することは、
空集合 かつ 極限序数 かつ 序数 かつ
任意のAにおいて、空集合∈A かつ Aは極限序数 は omega⊆A をもつ。
終了
 definition
  let A be set;
  attr A is natural means
  A in omega;
 end;
定義
Aは集合
属性Aは自然数 はＡ∈ omegaを意味する
終了