The Mizar article:

Trigonometric Functions on Complex Space

by

Takashi Mitsuishi,

Noboru Endou, and

Keiji Ohkubo

Received October 10, 2002

Copyright (c) 2002 Association of Mizar Users

MML identifier: SIN_COS3

[ MML identifier index ]

environ

 vocabulary RELAT_1, FINSEQ_4, ORDINAL2, COMPLEX1, SIN_COS, PREPOWER, SIN_COS2,
      SIN_COS3, FUNCT_1, ARYTM_1, ARYTM_3, XCMPLX_0;
 notation SUBSET_1, NUMBERS, REAL_1, RELAT_1, NAT_1, FINSEQ_4, ARYTM_0,
      COMPLEX1, FUNCT_2, SEQ_1, COMSEQ_3, SIN_COS, SIN_COS2;
 constructors NAT_1, COMSEQ_1, COMSEQ_3, REAL_1, SEQ_1, FINSEQ_4, SIN_COS,
      SIN_COS2, COMPLEX1, MEMBERED, INT_1, ARYTM_0, ARYTM_3, FUNCT_4;
 clusters RELSET_1, COMPLEX1, MEMBERED, ORDINAL2, NUMBERS;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;
 theorems COMPLEX1, REAL_1, SIN_COS, SIN_COS2, COMSEQ_3, FINSEQ_4, FUNCT_2,
      COMPLFLD, HAHNBAN1, XCMPLX_0, XCMPLX_1, ARYTM_0;
 schemes NAT_1, COMPLSP1, FUNCT_2;

begin  :: Definitions of trigonometric functions

 reserve x,y for Element of REAL;
 reserve z,z1,z2 for Element of COMPLEX;
 reserve n for Nat;

definition
 deffunc
  U(Element of COMPLEX) = (exp(<i>*$1)-(exp(-<i> * $1)))/([*2,0*] * <i>);
  func sin_C -> Function of COMPLEX, COMPLEX means :Def1:
  it.z = (exp(<i>*z)-(exp(-<i> * z)))/([*2,0*] * <i>);
  existence
   proof
     thus ex f being Function of COMPLEX, COMPLEX st
       for z holds f.z = U(z) from LambdaD;
   end;
  uniqueness
   proof
    thus for f1,f2 being Function of COMPLEX, COMPLEX st
      (for z holds f1.z = U(z)) &
      (for z holds f2.z = U(z))
       holds f1 = f2 from FuncDefUniq;
   end;
end;

definition
 deffunc U(Element of COMPLEX) = (exp(<i>*$1) + exp(-<i>*$1))/[*2,0*];
  func cos_C -> Function of COMPLEX,COMPLEX means :Def2:
  it.z = (exp(<i>*z) + exp(-<i>*z))/[*2,0*];
  existence
   proof
     thus ex f being Function of COMPLEX, COMPLEX st
       for z holds f.z = U(z) from LambdaD;
   end;
  uniqueness
   proof
    thus for f1,f2 being Function of COMPLEX, COMPLEX st
      (for z holds f1.z = U(z)) &
      (for z holds f2.z = U(z))
       holds f1 = f2 from FuncDefUniq;
   end;
end;

definition
 deffunc U(Element of COMPLEX) = (exp($1) - exp(-$1))/[*2,0*];
  func sinh_C -> Function of COMPLEX,COMPLEX means :Def3:
  it.z = (exp(z) - exp(-z))/[*2,0*];
  existence
   proof
     thus ex f being Function of COMPLEX, COMPLEX st
       for z holds f.z = U(z) from LambdaD;
   end;
  uniqueness
   proof
    thus for f1,f2 being Function of COMPLEX, COMPLEX st
      (for z holds f1.z = U(z)) &
      (for z holds f2.z = U(z))
       holds f1 = f2 from FuncDefUniq;
   end;
end;

definition
 deffunc U(Element of COMPLEX) = (exp($1) + exp(-$1))/[*2,0*];
  func cosh_C -> Function of COMPLEX,COMPLEX means :Def4:
  it.z = (exp(z) + exp(-z))/[*2,0*];
  existence
   proof
     thus ex f being Function of COMPLEX, COMPLEX st
       for z holds f.z = U(z) from LambdaD;
   end;
  uniqueness
   proof
    thus for f1,f2 being Function of COMPLEX, COMPLEX st
      (for z holds f1.z = U(z)) &
      (for z holds f2.z = U(z))
       holds f1 = f2 from FuncDefUniq;
   end;
end;

Lm1: sin_C/.z = (exp(<i>*z)-(exp(-<i> * z)))/([*2,0*] * <i>)
proof
    dom sin_C = COMPLEX by FUNCT_2:def 1;
  then sin_C/.z = sin_C.z by FINSEQ_4:def 4
          .= (exp(<i>*z)-(exp(-<i> * z)))/([*2,0*] * <i>) by Def1;
  hence thesis;
end;

Lm2: cos_C/.z = (exp(<i>*z) + exp(-<i>*z))/[*2,0*]
proof
    dom cos_C = COMPLEX by FUNCT_2:def 1;
  then cos_C/.z = cos_C.z by FINSEQ_4:def 4
          .= (exp(<i>*z) + exp(-<i>*z))/[*2,0*] by Def2;
  hence thesis;
end;

Lm3: sinh_C/.z = (exp(z) - exp(-z))/[*2,0*]
proof
    dom sinh_C = COMPLEX by FUNCT_2:def 1;
  then sinh_C/.z = sinh_C.z by FINSEQ_4:def 4
          .= (exp(z) - exp(-z))/[*2,0*] by Def3;
  hence thesis;
end;

Lm4: cosh_C/.z = (exp(z) + exp(-z))/[*2,0*]
proof
    dom cosh_C = COMPLEX by FUNCT_2:def 1;
  then cosh_C/.z = cosh_C.z by FINSEQ_4:def 4
          .= (exp(z) + exp(-z))/[*2,0*] by Def4;
  hence thesis;
end;

Lm5:
(z1 + z2)*(z1 + z2) = z1*z1 + z2*z2 + z1*z2 + z1*z2
proof
   (z1 + z2)*(z1 + z2) = (z1 + z2)*z1 + (z1 + z2)*z2 by XCMPLX_1:8
 .= z1*z1 + z1*z2 + z2*(z1 + z2) by XCMPLX_1:8
 .= z1*z1 + z1*z2 + (z2*z1 + z2*z2) by XCMPLX_1:8
 .= ((z2*z1 + z2*z2) + z1*z1) + z1*z2 by XCMPLX_1:1
 .= z2*z1 + (z2*z2 + z1*z1) + z1*z2 by XCMPLX_1:1;
 hence thesis;
end;

Lm6:
(z1 - z2)*(z1 - z2) = z1*z1 + z2*z2 - (z1*z2 + z1*z2)
proof
   (z1 -z2)*(z1 - z2) = (z1 + -z2)*(z1 -z2) by XCMPLX_0:def 8
 .= (z1 + -z2)*(z1 + -z2) by XCMPLX_0:def 8
 .= z1*z1 + (-z2)*(-z2) +z1*(-z2) + z1*(-z2) by Lm5
 .= z1*z1 + z2*z2 +z1*(-z2) + z1*(-z2) by XCMPLX_1:177
 .= z1*z1 + z2*z2 + -(z1*z2) + z1*(-z2) by XCMPLX_1:175
 .= z1*z1 + z2*z2 + -(z1*z2) + -(z1*z2) by XCMPLX_1:175
 .= z1*z1 + z2*z2 + (-(z1*z2) + -(z1*z2)) by XCMPLX_1:1
 .= z1*z1 + z2*z2 + -(z1*z2 + z1*z2) by XCMPLX_1:140;
 hence thesis by XCMPLX_0:def 8;
end;

L0: 0c = [*0,0*] by ARYTM_0:def 7;
L1: 1r = [*1,0*] by ARYTM_0:def 7,COMPLEX1:def 7;

Lm7:
[*2,0*]*<i><>0c
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
   <i> <> 0c by ARYTM_0:12,COMPLEX1:def 8,L0;
 hence thesis by A1,XCMPLX_1:6;
end;

Lm8:
for z be Element of COMPLEX holds
exp(z)*exp(-z) = [*1,0*]
proof
 let z be Element of COMPLEX;
   exp(z)*exp(-z) = exp(z + -z) by SIN_COS:24
 .= exp([*0,0*]) by L0,XCMPLX_0:def 6
 .= [*exp(0),0*] by SIN_COS:54;
 hence thesis by SIN_COS:56;
end;

begin  :: Properties of trigonometric functions on complex space

theorem
  for z being Element of COMPLEX holds
(sin_C/.z)*(sin_C/.z) + (cos_C/.z)*(cos_C/.z) = 1r
proof
 let z be Element of COMPLEX;
A1:[*4,0*] <> 0c by ARYTM_0:12,L0;
 set z1 = exp(<i>*z), z2 = exp(-<i>*z);
     (sin_C/.z)*(sin_C/.z) + (cos_C/.z)*(cos_C/.z)
  =(sin_C/.z)*(sin_C/.z) +
   (cos_C/.z)*((exp(<i>*z) + exp(-<i>*z))/[*2,0*]) by Lm2
 .=(sin_C/.z)*(sin_C/.z) + ((z1 + z2)/[*2,0*])*((z1 + z2)/[*2,0*]) by Lm2
 .=(z1 - z2)/([*2,0*]*<i>)*(sin_C/.z) +
   ((z1 + z2)/[*2,0*])*((z1 + z2)/[*2,0*]) by Lm1
 .=((z1 - z2)/([*2,0*]*<i>))*((z1 - z2)/([*2,0*]*<i>)) +
   ((z1 + z2)/[*2,0*])*((z1 + z2)/[*2,0*]) by Lm1
 .=((z1 - z2)*(z1 - z2))/(([*2,0*]*<i>)*([*2,0*]*<i>)) +
   ((z1 + z2)/[*2,0*])*((z1 + z2)/[*2,0*]) by XCMPLX_1:77
 .=((z1 - z2)*(z1 - z2))/([*2,0*]*<i>*([*2,0*]*<i>)) +
   ((z1 + z2)*(z1 + z2))/([*2,0*]*[*2,0*]) by XCMPLX_1:77
 .=((z1 - z2)*(z1 - z2))/(([*2,0*]*<i>)*<i>*[*2,0*]) +
   ((z1 + z2)*(z1 + z2))/([*2,0*]*[*2,0*]) by XCMPLX_1:4
 .=((z1 - z2)*(z1 - z2))/([*2,0*]*(-1r)*[*2,0*]) +
   ((z1 + z2)*(z1 + z2))/([*2,0*]*[*2,0*]) by COMPLEX1:37,XCMPLX_1:4
 .=((z1 - z2)*(z1 - z2))/((-1r)*([*2,0*]*[*2,0*])) +
   ((z1 + z2)*(z1 + z2))/([*2,0*]*[*2,0*]) by XCMPLX_1:4
 .=((z1 - z2)*(z1 - z2))/(-([*2,0*]*[*2,0*])) +
   ((z1 + z2)*(z1 + z2))/([*2,0*]*[*2,0*]) by COMPLEX1:46
 .=((z1 - z2)*(z1 - z2))/(-([*2*2-0*0,2*0+2*0*])) +
   ((z1 + z2)*(z1 + z2))/([*2,0*]*[*2,0*]) by HAHNBAN1:2
 .=((z1 - z2)*(z1 - z2))/(-[*4,0*]) +
   ((z1 + z2)*(z1 + z2))/([*4,0*]) by HAHNBAN1:2
 .=-(((z1 - z2)*(z1 - z2))/[*4,0*]) +
   ((z1 + z2)*(z1 + z2))/[*4,0*] by XCMPLX_1:189
 .=((z1 + z2)*(z1 + z2))/[*4,0*] -
   (((z1 - z2)*(z1 - z2))/[*4,0*])by XCMPLX_0:def 8
 .=((z1 + z2)*(z1 + z2) - (z1 - z2)*(z1 - z2))/[*4,0*]by XCMPLX_1:121
 .=(z1*z1 + z2*z2 + z1*z2 + z1*z2 - (z1 - z2)*(z1 - z2))
   /[*4,0*] by Lm5
 .=(z1*z1 + z2*z2 + z1*z2 + z1*z2 - (z1*z1 + z2*z2 - (z1*z2 + z1*z2)))
    /[*4,0*] by Lm6
 .=(z1*z1 + z2*z2 + (z1*z2 + z1*z2) - (z1*z1 + z2*z2 - (z1*z2 + z1*z2)))
    /[*4,0*] by XCMPLX_1:1
 .=((z1*z2 + z1*z2) + (z1*z1 + z2*z2) - (z1*z1 + z2*z2) + (z1*z2 + z1*z2))
    /[*4,0*] by XCMPLX_1:37
 .=((z1*z2 + z1*z2) + (z1*z2 + z1*z2))/[*4,0*] by XCMPLX_1:26
 .=(([*1,0*] + z1*exp(-(<i>*z))) + (z1*exp(-(<i>*z)) + z1*exp(-(<i>*z))))
   /[*4,0*] by Lm8
 .=(([*1,0*] + [*1,0*]) + (z1*exp(-(<i>*z)) + z1*exp(-(<i>*z))))
   /[*4,0*] by Lm8
 .=(([*1,0*] + [*1,0*]) + (z1*exp(-(<i>*z)) + [*1,0*]))/[*4,0*] by Lm8
 .=(([*1,0*] + [*1,0*]) + ([*1,0*] + [*1,0*]))/[*4,0*] by Lm8
 .=([*1+1,0+0*] + ([*1,0*] + [*1,0*]))/[*4,0*] by COMPLFLD:2
 .=([*2,0*] + [*2,0*])/[*4,0*] by COMPLFLD:2
 .=[*2+2,0+0*]/[*4,0*] by COMPLFLD:2;
 hence thesis by A1,COMPLEX1:86;
end;

theorem Th2:
-sin_C/.z = sin_C/.(-z)
proof
   sin_C/.(-z) = (exp(<i>*(-z)) - exp(-<i>*(-z)))/([*2,0*]*<i>) by Lm1
 .= (exp(<i>*(-z)) - exp((-<i>)*(-z)))/([*2,0*]*<i>) by XCMPLX_1:175
 .= (exp(<i>*(-z)) - exp(<i>*z))/([*2,0*]*<i>) by XCMPLX_1:177
 .= (exp(-<i>*z) - exp(<i>*z))/([*2,0*]*<i>) by XCMPLX_1:175
 .= (-(exp(<i>*z) - exp(-<i>*z)))/([*2,0*]*<i>) by XCMPLX_1:143
 .= -((exp(<i>*z) - exp(-<i>*z))/([*2,0*]*<i>)) by XCMPLX_1:188;
 hence thesis by Lm1;
end;

theorem Th3:
cos_C/.z = cos_C/.(-z)
proof
   cos_C/.(-z) = (exp(<i>*(-z)) + exp(-<i>*(-z)))/[*2,0*] by Lm2
 .=(exp(<i>*(-z)) + exp((-<i>)*(-z)))/[*2,0*] by XCMPLX_1:175
 .=(exp(<i>*(-z)) + exp(<i>*z))/[*2,0*] by XCMPLX_1:177
 .=(exp(-<i>*z) + exp(<i>*z))/[*2,0*] by XCMPLX_1:175;
 hence thesis by Lm2;
end;

theorem Th4:
sin_C/.(z1+z2) = (sin_C/.z1)*(cos_C/.z2) + (cos_C/.z1)*(sin_C/.z2)
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
 set e1 = exp(<i>*z1), e2 = exp(-<i>*z1), e3 = exp(<i>*z2), e4 = exp(-<i>*z2);
     (sin_C/.z1)*(cos_C/.z2) + (cos_C/.z1)*(sin_C/.z2)
  =((exp(<i>*z1) - exp(-<i>*z1))/([*2,0*]*<i>))*(cos_C/.z2) +
   (cos_C/.z1)*(sin_C/.z2) by Lm1
 .=((exp(<i>*z1) - exp(-<i>*z1))/([*2,0*]*<i>))*(cos_C/.z2) +
   (cos_C/.z1)*((exp(<i>*z2) - exp(-<i>*z2))/([*2,0*]*<i>)) by Lm1
 .=((exp(<i>*z1) - exp(-<i>*z1))/([*2,0*]*<i>))*
   ((exp(-<i>*z2) + exp(<i>*z2))/[*2,0*]) +
   (cos_C/.z1)*((exp(<i>*z2) - exp(-<i>*z2))/([*2,0*]*<i>)) by Lm2
 .=((exp(<i>*z1) - exp(-<i>*z1))/([*2,0*]*<i>))*
   ((exp(-<i>*z2) + exp(<i>*z2))/[*2,0*]) +
   ((exp(-<i>*z1) + exp(<i>*z1))/[*2,0*])*
   ((exp(<i>*z2) - exp(-<i>*z2))/([*2,0*]*<i>)) by Lm2
 .=((exp(<i>*z1) - exp(-<i>*z1))*(exp(-<i>*z2) + exp(<i>*z2)))
   /([*2,0*]*<i>*[*2,0*]) + ((exp(-<i>*z1) + exp(<i>*z1))/[*2,0*])*
   ((exp(<i>*z2) - exp(-<i>*z2))/([*2,0*]*<i>)) by XCMPLX_1:77
 .=((exp(<i>*z1) - exp(-<i>*z1))*(exp(-<i>*z2) + exp(<i>*z2)))
   /([*2,0*]*<i>*[*2,0*]) +
   ((exp(-<i>*z1) + exp(<i>*z1))*(exp(<i>*z2) - exp(-<i>*z2)))
   /([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:77
 .=( (exp(<i>*z1) - exp(-<i>*z1))*(exp(-<i>*z2) + exp(<i>*z2)) +
     (exp(-<i>*z1) + exp(<i>*z1))*(exp(<i>*z2) - exp(-<i>*z2)) )
   /([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:63
 .=( (e1-e2)*e4 + (e1-e2)*e3 + (e1+e2)*(e3-e4) )/([*2,0*]*<i>*[*2,0*])
    by XCMPLX_1:8
 .=( e1*e4-e2*e4 + (e1-e2)*e3 + (e1+e2)*(e3-e4) )/([*2,0*]*<i>*[*2,0*])
    by XCMPLX_1:40
 .=( e1*e4-e2*e4 + (e1*e3-e2*e3) + (e1+e2)*(e3-e4) )/([*2,0*]*<i>*[*2,0*])
    by XCMPLX_1:40
 .=( e1*e4-e2*e4 + (e1*e3-e2*e3) + ((e1+e2)*e3-(e1+e2)*e4) )
   /([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:40
 .=( e1*e4-e2*e4 + (e1*e3-e2*e3) + (e1*e3+e2*e3-(e1+e2)*e4) )
   /([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:8
 .=( e1*e4-e2*e4 + (e1*e3-e2*e3) + (e2*e3+e1*e3-(e1*e4+e2*e4)) )
   /([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:8
 .=( e1*e4-e2*e4 + ((e1*e3-e2*e3) + (e2*e3+e1*e3-(e1*e4+e2*e4))) )
   /([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:1
 .=( e1*e4-e2*e4 + ((e1*e3-e2*e3 + (e2*e3+e1*e3))-(e1*e4+e2*e4)) )
   /([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:29
 .=( e1*e4-e2*e4 + ((e1*e3-e2*e3 + e2*e3)+e1*e3-(e1*e4+e2*e4)) )
   /([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:1
 .=(e1*e4-e2*e4 + (e1*e3+e1*e3-(e1*e4+e2*e4)))/([*2,0*]*<i>*[*2,0*])
   by XCMPLX_1:27
 .=( e1*e3+e1*e3-(e1*e4+e2*e4 - (e1*e4-e2*e4)) )
   /([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:37
 .=( e1*e3+e1*e3-(e1*e4+(e2*e4 - (e1*e4-e2*e4))) )
   /([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:29
 .=( e1*e3+e1*e3-(e1*e4+(e2*e4 - e1*e4 + e2*e4)) )
   /([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:37
 .=( e1*e3+e1*e3-((e1*e4+(e2*e4 - e1*e4)) + e2*e4) )
   /([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:1
 .=(e1*e3+e1*e3-((e1*e4+e2*e4 - e1*e4) + e2*e4))/([*2,0*]*<i>*[*2,0*])
   by XCMPLX_1:29
 .=(e1*e3+e1*e3-(e2*e4 + e2*e4))/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:26
 .=([*Re(e1*e3)+Re(e1*e3),Im(e1*e3)+Im(e1*e3)*]-(e2*e4 + e2*e4))
   /([*2,0*]*<i>*[*2,0*]) by COMPLEX1:def 9
 .=([*2*Re(e1*e3),Im(e1*e3)+Im(e1*e3)*]-(e2*e4 + e2*e4))
   /([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:11
 .=([*2*Re(e1*e3),2*Im(e1*e3)*]-(e2*e4 + e2*e4))
   /([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:11
 .=([*Re([*2,0*]*(e1*e3)),2*Im(e1*e3)*]-(e2*e4 + e2*e4))
   /([*2,0*]*<i>*[*2,0*]) by COMSEQ_3:17
 .=([*Re([*2,0*]*(e1*e3)),Im([*2,0*]*(e1*e3))*]-(e2*e4 + e2*e4))
   /([*2,0*]*<i>*[*2,0*]) by COMSEQ_3:17
 .=([*2,0*]*(e1*e3)-(e2*e4 + e2*e4))/([*2,0*]*<i>*[*2,0*]) by COMPLEX1:8
 .=([*2,0*]*(e1*e3)-[*Re(e2*e4)+Re(e2*e4),Im(e2*e4)+Im(e2*e4)*])
   /([*2,0*]*<i>*[*2,0*]) by COMPLEX1:def 9
 .=([*2,0*]*(e1*e3)-[*2*Re(e2*e4),Im(e2*e4)+Im(e2*e4)*])
   /([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:11
 .=([*2,0*]*(e1*e3)-[*2*Re(e2*e4),2*Im(e2*e4)*])
   /([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:11
 .=([*2,0*]*(e1*e3)-[*Re([*2,0*]*(e2*e4)),2*Im(e2*e4)*])
   /([*2,0*]*<i>*[*2,0*]) by COMSEQ_3:17
 .=([*2,0*]*(e1*e3)-[*Re([*2,0*]*(e2*e4)),Im([*2,0*]*(e2*e4))*])
   /([*2,0*]*<i>*[*2,0*]) by COMSEQ_3:17
 .=([*2,0*]*(e1*e3)-[*2,0*]*(e2*e4))/([*2,0*]*<i>*[*2,0*]) by COMPLEX1:8
 .=([*2,0*]*(e1*e3))/([*2,0*]*<i>*[*2,0*])
  -([*2,0*]*(e2*e4))/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:121
 .=(e1*e3)/([*2,0*]*<i>)
  -([*2,0*]*(e2*e4))/([*2,0*]*<i>*[*2,0*]) by A1,XCMPLX_1:92
 .=(e1*e3)/([*2,0*]*<i>)-(e2*e4)/([*2,0*]*<i>) by A1,XCMPLX_1:92
 .=exp(<i>*z1+<i>*z2)/([*2,0*]*<i>)-(e2*e4)/([*2,0*]*<i>) by SIN_COS:24
 .=exp(<i>*(z1+z2))/([*2,0*]*<i>)-(e2*e4)/([*2,0*]*<i>) by XCMPLX_1:8
 .=exp(<i>*(z1+z2))/([*2,0*]*<i>)-exp(-<i>*z1+-<i>*z2)/([*2,0*]*<i>)
   by SIN_COS:24
 .=( exp(<i>*(z1+z2))-exp(-<i>*z1+ -<i>*z2) )/([*2,0*]*<i>) by XCMPLX_1:121
 .=( exp(<i>*(z1+z2))-exp(-(<i>*z1+<i>*z2)) )/([*2,0*]*<i>) by XCMPLX_1:140
 .=( exp(<i>*(z1+z2))-exp(-<i>*(z1+z2)) )/([*2,0*]*<i>) by XCMPLX_1:8;
 hence thesis by Lm1;
end;

theorem
  sin_C/.(z1-z2) = (sin_C/.z1)*(cos_C/.z2) - (cos_C/.z1)*(sin_C/.z2)
proof
   sin_C/.(z1-z2) = sin_C/.(z1 + -z2) by XCMPLX_0:def 8
 .=(sin_C/.z1)*(cos_C/.(-z2)) + (cos_C/.z1)*(sin_C/.(-z2)) by Th4
 .=(sin_C/.z1)*(cos_C/.z2) + (cos_C/.z1)*(sin_C/.(-z2)) by Th3
 .=(sin_C/.z1)*(cos_C/.z2) + (cos_C/.z1)*(-sin_C/.z2) by Th2
 .=(sin_C/.z1)*(cos_C/.z2) + -(cos_C/.z1)*(sin_C/.z2) by XCMPLX_1:175;
 hence thesis by XCMPLX_0:def 8;
end;

theorem Th6:
cos_C/.(z1+z2) = (cos_C/.z1)*(cos_C/.z2) - (sin_C/.z1)*(sin_C/.z2)
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
 set e1 = exp(<i>*z1), e2 = exp(-<i>*z1), e3 = exp(<i>*z2), e4 = exp(-<i>*z2);
     (cos_C/.z1)*(cos_C/.z2) - (sin_C/.z1)*(sin_C/.z2)
  =(cos_C/.z1)*(cos_C/.z2) -
   ((exp(<i>*z1) - exp(-<i>*z1))/([*2,0*]*<i>))*(sin_C/.z2) by Lm1
 .=(cos_C/.z1)*(cos_C/.z2) - ((exp(<i>*z1) - exp(-<i>*z1))/([*2,0*]*<i>))
   *((exp(<i>*z2) - exp(-<i>*z2))/([*2,0*]*<i>)) by Lm1
 .=(cos_C/.z1)*((exp(<i>*z2) + exp(-<i>*z2))/[*2,0*]) -
    ((exp(<i>*z1) - exp(-<i>*z1))/([*2,0*]*<i>))
   *((exp(<i>*z2) - exp(-<i>*z2))/([*2,0*]*<i>)) by Lm2
 .=((e1 + e2)/[*2,0*])*((e3 + e4)/[*2,0*]) -
   ((e1 - e2)/([*2,0*]*<i>))*((e3 - e4)/([*2,0*]*<i>)) by Lm2
 .=((e1 + e2)*(e3 + e4))/([*2,0*]*[*2,0*]) -
   ((e1 - e2)/([*2,0*]*<i>))*((e3 - e4)/([*2,0*]*<i>)) by XCMPLX_1:77
 .=((e1 + e2)*(e3 + e4))/([*2,0*]*[*2,0*]) -
   ((e1 - e2)*(e3 - e4))/([*2,0*]*<i>*([*2,0*]*<i>)) by XCMPLX_1:77
 .=((e1 + e2)*(e3 + e4))/([*2,0*]*[*2,0*]) -
   ((e1 - e2)*(e3 - e4))/(([*2,0*]*<i>*<i>)*[*2,0*]) by XCMPLX_1:4
 .=((e1 + e2)*(e3 + e4))/([*2,0*]*[*2,0*]) -
   ((e1 - e2)*(e3 - e4))/([*2,0*]*(-1r)*[*2,0*]) by COMPLEX1:37,XCMPLX_1:4
 .=((e1 + e2)*(e3 + e4))/([*2,0*]*[*2,0*]) -
   ((e1 - e2)*(e3 - e4))/((-1r)*([*2,0*]*[*2,0*])) by XCMPLX_1:4
 .=((e1 + e2)*(e3 + e4))/([*2,0*]*[*2,0*]) -
   ((e1 - e2)*(e3 - e4))/(-([*2,0*]*[*2,0*])) by COMPLEX1:46
 .=((e1 + e2)*(e3 + e4))/([*2,0*]*[*2,0*]) -
   - ((e1 - e2)*(e3 - e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:189
 .=((e1 + e2)*(e3 + e4))/([*2,0*]*[*2,0*]) +
   ((e1 - e2)*(e3 - e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:151
 .=((e1+e2)*(e3+e4) + (e1-e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:63
 .=((e1+e2)*e3+(e1+e2)*e4 + (e1-e2)*(e3-e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:8
 .=(e1*e3+e2*e3 + (e1+e2)*e4 + (e1-e2)*(e3-e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:8
 .=(e1*e3+e2*e3 + (e1*e4+e2*e4) + (e1-e2)*(e3-e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:8
 .=(e1*e3+e2*e3 + (e1*e4+e2*e4) + ((e1-e2)*e3-(e1-e2)*e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:40
 .=(e1*e3+e2*e3 + (e1*e4+e2*e4) + (e1*e3-e2*e3-(e1-e2)*e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:40
 .=(e1*e3-e2*e3-(e1*e4-e2*e4) + ((e1*e3+e2*e3) + (e1*e4+e2*e4)) )
   /([*2,0*]*[*2,0*]) by XCMPLX_1:40
 .=( (e1*e3+e2*e3)+( e1*e3-e2*e3-(e1*e4-e2*e4) ) + (e1*e4+e2*e4) )
   /([*2,0*]*[*2,0*]) by XCMPLX_1:1
 .=( (e1*e3-e2*e3 + (e2*e3+e1*e3) )-(e1*e4-e2*e4) + (e1*e4+e2*e4) )
   /([*2,0*]*[*2,0*]) by XCMPLX_1:29
 .=( (e1*e3-e2*e3 + e2*e3)+e1*e3 -(e1*e4-e2*e4) + (e1*e4+e2*e4) )
   /([*2,0*]*[*2,0*]) by XCMPLX_1:1
 .=(e1*e3+e1*e3-(e1*e4-e2*e4) + (e1*e4+e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:27
 .=( e1*e3+e1*e3 -(e1*e4-e2*e4 - (e1*e4+e2*e4)) )
   /([*2,0*]*[*2,0*]) by XCMPLX_1:37
 .=( e1*e3+e1*e3 -(e1*e4-e2*e4 - e1*e4-e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:36
 .=( e1*e3+e1*e3 -(-e2*e4+e1*e4- e1*e4-e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_0:
def 8
 .=( e1*e3+e1*e3 -(-e2*e4-e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:26
 .=( e1*e3+e1*e3 -(-e2*e4)+e2*e4)/([*2,0*]*[*2,0*]) by XCMPLX_1:37
 .=( e1*e3+e1*e3 +e2*e4+e2*e4)/([*2,0*]*[*2,0*]) by XCMPLX_1:151
 .=( e1*e3+e1*e3 + (e2*e4+e2*e4) )/([*2,0*]*[*2,0*]) by XCMPLX_1:1
 .=([*Re(e1*e3)+Re(e1*e3),Im(e1*e3)+Im(e1*e3)*]+(e2*e4 + e2*e4))
   /([*2,0*]*[*2,0*]) by COMPLEX1:def 9
 .=([*2*Re(e1*e3),Im(e1*e3)+Im(e1*e3)*]+(e2*e4 + e2*e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:11
 .=([*2*Re(e1*e3),2*Im(e1*e3)*]+(e2*e4 + e2*e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:11
 .=([*Re([*2,0*]*(e1*e3)),2*Im(e1*e3)*]+(e2*e4 + e2*e4))
   /([*2,0*]*[*2,0*]) by COMSEQ_3:17
 .=([*Re([*2,0*]*(e1*e3)),Im([*2,0*]*(e1*e3))*]+(e2*e4 + e2*e4))
   /([*2,0*]*[*2,0*]) by COMSEQ_3:17
 .=([*2,0*]*(e1*e3)+(e2*e4 + e2*e4))/([*2,0*]*[*2,0*]) by COMPLEX1:8
 .=([*2,0*]*(e1*e3)+[*Re(e2*e4)+Re(e2*e4),Im(e2*e4)+Im(e2*e4)*])
   /([*2,0*]*[*2,0*]) by COMPLEX1:def 9
 .=([*2,0*]*(e1*e3)+[*2*Re(e2*e4),Im(e2*e4)+Im(e2*e4)*])
   /([*2,0*]*[*2,0*]) by XCMPLX_1:11
 .=([*2,0*]*(e1*e3)+[*2*Re(e2*e4),2*Im(e2*e4)*])
   /([*2,0*]*[*2,0*]) by XCMPLX_1:11
 .=([*2,0*]*(e1*e3)+[*Re([*2,0*]*(e2*e4)),2*Im(e2*e4)*])
   /([*2,0*]*[*2,0*]) by COMSEQ_3:17
 .=([*2,0*]*(e1*e3)+[*Re([*2,0*]*(e2*e4)),Im([*2,0*]*(e2*e4))*])
   /([*2,0*]*[*2,0*]) by COMSEQ_3:17
 .=([*2,0*]*(e1*e3)+[*2,0*]*(e2*e4))/([*2,0*]*[*2,0*]) by COMPLEX1:8
 .=([*2,0*]*(e1*e3))/([*2,0*]*[*2,0*])
  +([*2,0*]*(e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:63
 .=(e1*e3)/([*2,0*])+([*2,0*]*(e2*e4))/([*2,0*]*[*2,0*]) by A1,XCMPLX_1:92
 .=(e1*e3)/([*2,0*])+(e2*e4)/([*2,0*]) by A1,XCMPLX_1:92
 .=exp(<i>*z1+<i>*z2)/([*2,0*])+(e2*e4)/([*2,0*]) by SIN_COS:24
 .=exp(<i>*(z1+z2))/([*2,0*])+(e2*e4)/([*2,0*]) by XCMPLX_1:8
 .=exp(<i>*(z1+z2))/([*2,0*])+exp(-<i>*z1+-<i>*z2)/([*2,0*]) by SIN_COS:24
 .=( exp(<i>*(z1+z2))+exp(-<i>*z1+ -<i>*z2) )/([*2,0*]) by XCMPLX_1:63
 .=( exp(<i>*(z1+z2))+exp(-(<i>*z1+<i>*z2)) )/([*2,0*]) by XCMPLX_1:140
 .=( exp(<i>*(z1+z2))+exp(-<i>*(z1+z2)) )/([*2,0*]) by XCMPLX_1:8;
 hence thesis by Lm2;
end;

theorem
  cos_C/.(z1-z2) = (cos_C/.z1)*(cos_C/.z2) + (sin_C/.z1)*(sin_C/.z2)
proof
   cos_C/.(z1-z2) = cos_C/.(z1+-z2) by XCMPLX_0:def 8
 .=cos_C/.z1*cos_C/.(-z2) - sin_C/.z1*sin_C/.(-z2) by Th6
 .=cos_C/.z1*cos_C/.z2 - sin_C/.z1*sin_C/.(-z2) by Th3
 .=cos_C/.z1*cos_C/.z2 - sin_C/.z1*(-sin_C/.z2) by Th2
 .=cos_C/.z1*cos_C/.z2 - -sin_C/.z1*sin_C/.z2 by XCMPLX_1:175;
 hence thesis by XCMPLX_1:151;
end;

theorem Th8:
(cosh_C/.z)*(cosh_C/.z) - (sinh_C/.z)*(sinh_C/.z) = 1r
proof
A1:[*4,0*] <> 0c by ARYTM_0:12,L0;
 set e1 = exp(z), e2 = exp(-z);
     (cosh_C/.z)*(cosh_C/.z) - (sinh_C/.z)*(sinh_C/.z)
  =(cosh_C/.z)*(cosh_C/.z) - ((e1-e2)/[*2,0*])*(sinh_C/.z) by Lm3
 .=(cosh_C/.z)*(cosh_C/.z) - ((e1-e2)/[*2,0*])*((e1-e2)/[*2,0*]) by Lm3
 .=(cosh_C/.z)*(cosh_C/.z) - (((e1-e2)*(e1-e2))/([*2,0*]*[*2,0*]))
   by XCMPLX_1:77
 .=((e1+e2)/[*2,0*])*(cosh_C/.z) - (((e1-e2)*(e1-e2))/([*2,0*]*[*2,0*]))
    by Lm4
 .=((e1+e2)/[*2,0*])*((e1+e2)/[*2,0*]) - (((e1-e2)*(e1-e2))/([*2,0*]*[*2,0*]))
    by Lm4
 .=(((e1+e2)*(e1+e2))/([*2,0*]*[*2,0*]))-(((e1-e2)*(e1-e2))/([*2,0*]*[*2,0*]))
    by XCMPLX_1:77
 .=((e1+e2)*(e1+e2)-(e1-e2)*(e1-e2))/([*2,0*]*[*2,0*]) by XCMPLX_1:121
 .=(e1*e1 + e2*e2 + e1*e2 + e1*e2-(e1-e2)*(e1-e2))/([*2,0*]*[*2,0*]) by Lm5
 .=(e1*e1 + e2*e2 + e1*e2 + e1*e2-(e1*e1 + e2*e2 - (e1*e2 + e1*e2)))
   /([*2,0*]*[*2,0*]) by Lm6
 .=(e1*e1 + e2*e2 + (e1*e2 + e1*e2) - (e1*e1 + e2*e2 - (e1*e2 + e1*e2)))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:1
 .=(e1*e1 + e2*e2 + (e1*e2 + e1*e2) - (e1*e1 + e2*e2) + (e1*e2 + e1*e2))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:37
 .=(e1*e2 + e1*e2 + (e1*e2 + e1*e2))/([*2,0*]*[*2,0*]) by XCMPLX_1:26
 .=([*1,0*] + e1*e2 + (e1*e2 + e1*e2))/([*2,0*]*[*2,0*]) by Lm8
 .=([*1,0*] + [*1,0*] + (e1*e2 + e1*e2))/([*2,0*]*[*2,0*]) by Lm8
 .=([*1,0*] + [*1,0*] + ([*1,0*] + e1*e2))/([*2,0*]*[*2,0*]) by Lm8
 .=([*1,0*] + [*1,0*] + ([*1,0*] + [*1,0*]))/([*2,0*]*[*2,0*]) by Lm8
 .=([*1+1,0+0*] + ([*1,0*] + [*1,0*]))/([*2,0*]*[*2,0*]) by COMPLFLD:2
 .=([*2,0*] + [*1+1,0+0*])/([*2,0*]*[*2,0*]) by COMPLFLD:2
 .=[*2+2,0+0*]/([*2,0*]*[*2,0*]) by COMPLFLD:2
 .=[*4,0*]/[*2*2-0*0,2*0+2*0*] by HAHNBAN1:2;
 hence thesis by A1,COMPLEX1:86;
end;

theorem Th9:
-sinh_C/.z = sinh_C/.(-z)
proof
   sinh_C/.(-z) = (exp(-z) - exp(-(-z)))/[*2,0*] by Lm3
 .= (-(exp(z) - exp(-z)))/[*2,0*] by XCMPLX_1:143
 .= -(exp(z) - exp(-z))/[*2,0*] by XCMPLX_1:188;
 hence thesis by Lm3;
end;

theorem Th10:
cosh_C/.z = cosh_C/.(-z)
proof
   cosh_C/.(-z) = (exp(-z) + exp(-(-z)))/[*2,0*] by Lm4
 .= (exp(-z) + exp(z))/[*2,0*];
 hence thesis by Lm4;
end;

theorem Th11:
sinh_C/.(z1+z2) = (sinh_C/.z1)*(cosh_C/.z2) + (cosh_C/.z1)*(sinh_C/.z2)
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
 set e1=exp(z1), e2=exp(-z1), e3=exp(z2), e4=exp(-z2);
     (sinh_C/.z1)*(cosh_C/.z2) + (cosh_C/.z1)*(sinh_C/.z2)
  =((e1-e2)/[*2,0*])*(cosh_C/.z2) + (cosh_C/.z1)*(sinh_C/.z2) by Lm3
 .=((e1-e2)/[*2,0*])*(cosh_C/.z2) + (cosh_C/.z1)*((e3-e4)/[*2,0*]) by Lm3
 .=((e1-e2)/[*2,0*])*(cosh_C/.z2) + ((e1+e2)/[*2,0*])*((e3-e4)/[*2,0*]) by Lm4
 .=((e1-e2)/[*2,0*])*((e3+e4)/[*2,0*]) +
   ((e1+e2)/[*2,0*])*((e3-e4)/[*2,0*]) by Lm4
 .=((e1-e2)*(e3+e4))/([*2,0*]*[*2,0*]) +
   ((e1+e2)/[*2,0*])*((e3-e4)/[*2,0*]) by XCMPLX_1:77
 .=((e1-e2)*(e3+e4))/([*2,0*]*[*2,0*]) +
   ((e1+e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:77
 .=((e1-e2)*(e3+e4)+(e1+e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:63
 .=((e1-e2)*e3+(e1-e2)*e4+(e1+e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:8
 .=(e1*e3-e2*e3+(e1-e2)*e4+(e1+e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:40
 .=(e1*e3-e2*e3+(e1*e4-e2*e4)+(e1+e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:40
 .=(e1*e3-e2*e3+(e1*e4-e2*e4)+((e1+e2)*e3-(e1+e2)*e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:40
 .=(e1*e3-e2*e3+(e1*e4-e2*e4)+(e1*e3+e2*e3-(e1+e2)*e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:8
 .=((e1*e4-e2*e4)+(e1*e3-e2*e3)+(e1*e3+e2*e3-(e1*e4+e2*e4)))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:8
 .=((e1*e4-e2*e4)+(e1*e3-e2*e3)+(e1*e3+e2*e3)-(e1*e4+e2*e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:29
 .=(((e1*e3-e2*e3)+(e1*e3+e2*e3))+(e1*e4-e2*e4)-(e1*e4+e2*e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:1
 .=(e1*e3-e2*e3+e2*e3+e1*e3+(e1*e4-e2*e4)-(e1*e4+e2*e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:1
 .=(e1*e3+e1*e3+(e1*e4-e2*e4)-(e1*e4+e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:27
 .=(e1*e3+e1*e3+(e1*e4-e2*e4-(e1*e4+e2*e4)))/([*2,0*]*[*2,0*]) by XCMPLX_1:29
 .=(e1*e3+e1*e3+(e1*e4-e2*e4-e1*e4-e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:36
 .=(e1*e3+e1*e3+(-e2*e4+e1*e4-e1*e4-e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_0:def 8
 .=(e1*e3+e1*e3+(-e2*e4-e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:26
 .=(e1*e3+e1*e3+(-e2*e4+-e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_0:def 8
 .=(e1*e3+e1*e3+-(e2*e4+e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:140
 .=(e1*e3+e1*e3-(e2*e4+e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_0:def 8
 .=([*Re(e1*e3)+Re(e1*e3),Im(e1*e3)+Im(e1*e3)*]-(e2*e4 + e2*e4))
   /([*2,0*]*[*2,0*]) by COMPLEX1:def 9
 .=([*2*Re(e1*e3),Im(e1*e3)+Im(e1*e3)*]-(e2*e4 + e2*e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:11
 .=([*2*Re(e1*e3),2*Im(e1*e3)*]-(e2*e4 + e2*e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:11
 .=([*Re([*2,0*]*(e1*e3)),2*Im(e1*e3)*]-(e2*e4 + e2*e4))
   /([*2,0*]*[*2,0*]) by COMSEQ_3:17
 .=([*Re([*2,0*]*(e1*e3)),Im([*2,0*]*(e1*e3))*]-(e2*e4 + e2*e4))
   /([*2,0*]*[*2,0*]) by COMSEQ_3:17
 .=([*2,0*]*(e1*e3)-(e2*e4 + e2*e4))/([*2,0*]*[*2,0*]) by COMPLEX1:8
 .=([*2,0*]*(e1*e3)-[*Re(e2*e4)+Re(e2*e4),Im(e2*e4)+Im(e2*e4)*])
   /([*2,0*]*[*2,0*]) by COMPLEX1:def 9
 .=([*2,0*]*(e1*e3)-[*2*Re(e2*e4),Im(e2*e4)+Im(e2*e4)*])
   /([*2,0*]*[*2,0*]) by XCMPLX_1:11
 .=([*2,0*]*(e1*e3)-[*2*Re(e2*e4),2*Im(e2*e4)*])
   /([*2,0*]*[*2,0*]) by XCMPLX_1:11
 .=([*2,0*]*(e1*e3)-[*Re([*2,0*]*(e2*e4)),2*Im(e2*e4)*])
   /([*2,0*]*[*2,0*]) by COMSEQ_3:17
 .=([*2,0*]*(e1*e3)-[*Re([*2,0*]*(e2*e4)),Im([*2,0*]*(e2*e4))*])
   /([*2,0*]*[*2,0*]) by COMSEQ_3:17
 .=([*2,0*]*(e1*e3)-[*2,0*]*(e2*e4))/([*2,0*]*[*2,0*]) by COMPLEX1:8
 .=([*2,0*]*(e1*e3))/([*2,0*]*[*2,0*])
  -([*2,0*]*(e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:121
 .=(e1*e3)/([*2,0*])-([*2,0*]*(e2*e4))/([*2,0*]*[*2,0*]) by A1,XCMPLX_1:92
 .=(e1*e3)/([*2,0*])-(e2*e4)/([*2,0*]) by A1,XCMPLX_1:92
 .=exp(z1+z2)/[*2,0*]-(e2*e4)/([*2,0*]) by SIN_COS:24
 .=exp(z1+z2)/[*2,0*]-exp(-z1+-z2)/[*2,0*] by SIN_COS:24
 .=(exp(z1+z2)-exp(-z1+-z2))/[*2,0*] by XCMPLX_1:121
 .=(exp(z1+z2)-exp(-(z1+z2)))/[*2,0*] by XCMPLX_1:140;
 hence thesis by Lm3;
end;

theorem Th12:
sinh_C/.(z1-z2) = (sinh_C/.z1)*(cosh_C/.z2) - (cosh_C/.z1)*(sinh_C/.z2)
proof
   sinh_C/.(z1-z2) = sinh_C/.(z1+ -z2) by XCMPLX_0:def 8
 .= (sinh_C/.z1)*cosh_C/.(-z2) + (cosh_C/.z1)*sinh_C/.(-z2) by Th11
 .= (sinh_C/.z1)*cosh_C/.z2 + (cosh_C/.z1)*sinh_C/.(-z2) by Th10
 .= (sinh_C/.z1)*cosh_C/.z2 + (cosh_C/.z1)*(-sinh_C/.z2) by Th9
 .= (sinh_C/.z1)*cosh_C/.z2 + -(cosh_C/.z1)*(sinh_C/.z2) by XCMPLX_1:175;
 hence thesis by XCMPLX_0:def 8;
end;

theorem Th13:
cosh_C/.(z1-z2) = (cosh_C/.z1)*(cosh_C/.z2) - (sinh_C/.z1)*(sinh_C/.z2)
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
 set e1=exp(z1), e2=exp(-z1), e3=exp(z2), e4=exp(-z2);
     (cosh_C/.z1)*(cosh_C/.z2) - (sinh_C/.z1)*(sinh_C/.z2)
  =((e1+e2)/[*2,0*])*(cosh_C/.z2) - (sinh_C/.z1)*(sinh_C/.z2) by Lm4
 .=((e1+e2)/[*2,0*])*((e3+e4)/[*2,0*]) - (sinh_C/.z1)*(sinh_C/.z2) by Lm4
 .=((e1+e2)*(e3+e4))/([*2,0*]*[*2,0*]) - (sinh_C/.z1)*(sinh_C/.z2)
   by XCMPLX_1:77
 .=((e1+e2)*(e3+e4))/([*2,0*]*[*2,0*]) - ((e1-e2)/[*2,0*])*(sinh_C/.z2) by Lm3
 .=((e1+e2)*(e3+e4))/([*2,0*]*[*2,0*])-((e1-e2)/[*2,0*])*((e3-e4)/[*2,0*])
   by Lm3
 .=((e1+e2)*(e3+e4))/([*2,0*]*[*2,0*])-((e1-e2)*(e3-e4))/([*2,0*]*[*2,0*])
   by XCMPLX_1:77
 .=((e1+e2)*(e3+e4)-(e1-e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:121
 .=((e1+e2)*e3+(e1+e2)*e4-(e1-e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:8
 .=(e1*e3+e2*e3+(e1+e2)*e4-(e1-e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:8
 .=(e1*e3+e2*e3+(e1*e4+e2*e4)-(e1-e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:8
 .=(e1*e3+e2*e3+(e1*e4+e2*e4)-((e1-e2)*e3-(e1-e2)*e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:40
 .=(e1*e3+e2*e3+(e1*e4+e2*e4)-(e1*e3-e2*e3-(e1-e2)*e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:40
 .=(e1*e4+e2*e4+(e2*e3+e1*e3)-(e1*e3-e2*e3-(e1*e4-e2*e4)))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:40
 .=(e1*e4+e2*e4+(e2*e3+e1*e3)-(e1*e3-e2*e3)+(e1*e4-e2*e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:37
 .=(e1*e4+e2*e4+(e2*e3+e1*e3-(e1*e3-e2*e3))+(e1*e4-e2*e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:29
 .=(e1*e4+e2*e4+(e2*e3+e1*e3-e1*e3+e2*e3)+(e1*e4-e2*e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:37
 .=(e2*e3+e2*e3+(e1*e4+e2*e4)+(e1*e4-e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:26
 .=(e2*e3+e2*e3+(e1*e4+e2*e4+(e1*e4-e2*e4)))/([*2,0*]*[*2,0*]) by XCMPLX_1:1
 .=(e2*e3+e2*e3+(e1*e4+(e2*e4+(e1*e4-e2*e4))))/([*2,0*]*[*2,0*]) by XCMPLX_1:1
 .=(e2*e3+e2*e3+(e1*e4+(e2*e4+e1*e4-e2*e4)))/([*2,0*]*[*2,0*]) by XCMPLX_1:29
 .=(e2*e3+e2*e3+(e1*e4+e1*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:26
 .=([*Re(e2*e3)+Re(e2*e3),Im(e2*e3)+Im(e2*e3)*]+(e1*e4+e1*e4))
   /([*2,0*]*[*2,0*]) by COMPLEX1:def 9
 .=([*2*Re(e2*e3),Im(e2*e3)+Im(e2*e3)*]+(e1*e4+e1*e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:11
 .=([*2*Re(e2*e3),2*Im(e2*e3)*]+(e1*e4+e1*e4))
   /([*2,0*]*[*2,0*]) by XCMPLX_1:11
 .=([*Re([*2,0*]*(e2*e3)),2*Im(e2*e3)*]+(e1*e4+e1*e4))
   /([*2,0*]*[*2,0*]) by COMSEQ_3:17
 .=([*Re([*2,0*]*(e2*e3)),Im([*2,0*]*(e2*e3))*]+(e1*e4+e1*e4))
   /([*2,0*]*[*2,0*]) by COMSEQ_3:17
 .=([*2,0*]*(e2*e3)+(e1*e4+e1*e4))/([*2,0*]*[*2,0*]) by COMPLEX1:8
 .=([*2,0*]*(e2*e3)+[*Re(e1*e4)+Re(e1*e4),Im(e1*e4)+Im(e1*e4)*])
   /([*2,0*]*[*2,0*]) by COMPLEX1:def 9
 .=([*2,0*]*(e2*e3)+[*2*Re(e1*e4),Im(e1*e4)+Im(e1*e4)*])
   /([*2,0*]*[*2,0*]) by XCMPLX_1:11
 .=([*2,0*]*(e2*e3)+[*2*Re(e1*e4),2*Im(e1*e4)*])
   /([*2,0*]*[*2,0*]) by XCMPLX_1:11
 .=([*2,0*]*(e2*e3)+[*Re([*2,0*]*(e1*e4)),2*Im(e1*e4)*])
    /([*2,0*]*[*2,0*]) by COMSEQ_3:17
 .=([*2,0*]*(e2*e3)+[*Re([*2,0*]*(e1*e4)),Im([*2,0*]*(e1*e4))*])
    /([*2,0*]*[*2,0*]) by COMSEQ_3:17
 .=([*2,0*]*(e2*e3)+[*2,0*]*(e1*e4))/([*2,0*]*[*2,0*]) by COMPLEX1:8
 .=([*2,0*]*(e2*e3))/([*2,0*]*[*2,0*])
  +([*2,0*]*(e1*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:63
 .=(e1*e4)/([*2,0*])+([*2,0*]*(e2*e3))/([*2,0*]*[*2,0*]) by A1,XCMPLX_1:92
 .=(e1*e4)/([*2,0*])+(e2*e3)/[*2,0*] by A1,XCMPLX_1:92
 .=exp(z1+-z2)/[*2,0*]+(e2*e3)/[*2,0*] by SIN_COS:24
 .=exp(z1+-z2)/[*2,0*]+exp(-z1+z2)/[*2,0*] by SIN_COS:24
 .=exp(z1-z2)/[*2,0*]+exp(-z1+z2)/[*2,0*] by XCMPLX_0:def 8
 .=(exp(z1-z2)+exp(-z1+z2))/[*2,0*] by XCMPLX_1:63
 .=(exp(z1-z2)+exp(-(z1-z2)))/[*2,0*] by XCMPLX_1:162;
 hence thesis by Lm4;
end;

theorem Th14:
cosh_C/.(z1+z2) = (cosh_C/.z1)*(cosh_C/.z2) + (sinh_C/.z1)*(sinh_C/.z2)
proof
   cosh_C/.(z1+z2) = cosh_C/.(z1- -z2) by XCMPLX_1:151
 .=(cosh_C/.z1)*cosh_C/.(-z2) - (sinh_C/.z1)*sinh_C/.(-z2) by Th13
 .=(cosh_C/.z1)*cosh_C/.(z2) - (sinh_C/.z1)*sinh_C/.(-z2) by Th10
 .=(cosh_C/.z1)*cosh_C/.(z2) - (sinh_C/.z1)*(-sinh_C/.z2) by Th9
 .=(cosh_C/.z1)*cosh_C/.(z2) - -(sinh_C/.z1)*(sinh_C/.z2) by XCMPLX_1:175;
 hence thesis by XCMPLX_1:151;
end;

theorem Th15:
sin_C/.(<i>*z) = <i>*sinh_C/.z
proof
A1: <i> <> 0c by ARYTM_0:12,COMPLEX1:def 8,L0;
   sin_C/.(<i>*z) = (exp(<i>*(<i>*z)) - exp(-<i>*(<i>*z)))/(<i>*[*2,0*]) by Lm1
 .= (exp(<i>*<i>*z) - exp(-<i>*(<i>*z)))/(<i>*[*2,0*]) by XCMPLX_1:4
 .= (exp((-1r)*z) - exp(-(<i>*<i>*z)))/(<i>*[*2,0*]) by COMPLEX1:37,XCMPLX_1:4
 .= (exp(-z) - exp(-(-1r)*z))/(<i>*[*2,0*]) by COMPLEX1:37,46
 .= (exp(-z) - exp(--z))/(<i>*[*2,0*]) by COMPLEX1:46
 .= (<i>*(exp(-z) - exp(z)))/(<i>*(<i>*[*2,0*])) by A1,XCMPLX_1:92
 .= (<i>*(exp(-z) - exp(z)))/((-1r)*[*2,0*]) by COMPLEX1:37,XCMPLX_1:4
 .= (<i>*(exp(-z) - exp(z)))/(-[*2,0*]) by COMPLEX1:46
 .= <i>*((exp(-z) - exp(z))/(-[*2,0*])) by XCMPLX_1:75
 .= <i>*(-(exp(-z) - exp(z))/[*2,0*]) by XCMPLX_1:189
 .= <i>*((-(exp(-z) - exp(z)))/[*2,0*]) by XCMPLX_1:188
 .= <i>*((exp(z) - exp(-z))/[*2,0*]) by XCMPLX_1:143;
 hence thesis by Lm3;
end;

theorem Th16:
cos_C/.(<i>*z) = cosh_C/.z
proof
   cos_C/.(<i>*z) = (exp(<i>*(<i>*z))+exp(-<i>*(<i>*z)))/[*2,0*] by Lm2
 .= (exp(<i>*<i>*z)+exp(-<i>*(<i>*z)))/[*2,0*] by XCMPLX_1:4
 .= (exp((-1r)*z)+exp(-(-1r)*z))/[*2,0*] by COMPLEX1:37,XCMPLX_1:4
 .= (exp(-z)+exp(-(-1r)*z))/[*2,0*] by COMPLEX1:46
 .= (exp(-z)+exp(--z))/[*2,0*] by COMPLEX1:46
 .= (exp(-z)+exp(z))/[*2,0*];
 hence thesis by Lm4;
end;

theorem Th17:
sinh_C/.(<i>*z) = <i>*sin_C/.z
proof
A1: <i> <> 0c by ARYTM_0:12,COMPLEX1:def 8,L0;
   sinh_C/.(<i>*z) = (exp(<i>*z)-exp(-<i>*z))/[*2,0*] by Lm3
 .= (<i>*(exp(<i>*z)-exp(-<i>*z)))/(<i>*[*2,0*]) by A1,XCMPLX_1:92
 .= <i>*((exp(<i>*z)-exp(-<i>*z))/(<i>*[*2,0*])) by XCMPLX_1:75;
 hence thesis by Lm1;
end;

theorem Th18:
cosh_C/.(<i>*z) = cos_C/.z
proof
   cosh_C/.(<i>*z) = (exp(<i>*z) + exp(-<i>*z))/[*2,0*] by Lm4;
 hence thesis by Lm2;
end;

Lm9:
exp([*x,y*])=[*exp(x),0*]*[*cos(y),sin(y)*]
proof
   exp([*x,y*]) = exp([*x+0,0+y*])
 .= exp([*x,0*]+[*0,y*]) by COMPLFLD:2
 .=exp([*x,0*])*exp([*0,y*]) by SIN_COS:24
 .= [*exp(x),0*]*exp([*0,y*]) by SIN_COS:54;
 hence thesis by SIN_COS:28;
end;

theorem Th19:
for x,y being Element of REAL holds
exp([*x,y*]) = [*(exp.x)*(cos.y),(exp.x)*(sin.y)*]
proof
 let x,y be Element of REAL;
   exp([*x,y*])=[*exp(x),0*]*[*cos(y),sin(y)*] by Lm9
 .=[*exp(x)*cos(y)-0*sin(y),exp(x)*sin(y)+cos(y)*0*] by HAHNBAN1:2
 .=[*exp(x)*cos.y,exp(x)*sin(y)*] by SIN_COS:def 23
 .=[*exp.x*cos.y,exp(x)*sin(y)*] by SIN_COS:def 27
 .=[*exp.x*cos.y,exp.x*sin(y)*] by SIN_COS:def 27;
 hence thesis by SIN_COS:def 21;
end;

theorem Th20:
exp(0c) = [*1,0*]
proof
 thus thesis by L0,SIN_COS:54,56;
end;

theorem Th21:
sin_C/.0c = 0c
proof
   sin_C/.0c = (exp(0c)-exp(-<i>*0c))/(<i>*[*2,0*]) by Lm1
 .=0c/(<i>*[*2,0*]) by XCMPLX_1:14;
 hence thesis;
end;

theorem
  sinh_C/.0c = 0c
proof
   sinh_C/.0c = (exp(0c)-exp(-0c))/[*2,0*] by Lm3
 .=0c/[*2,0*] by XCMPLX_1:14;
 hence thesis;
end;

theorem Th23:
cos_C/.0c = [*1,0*]
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
   cos_C/.0c = (exp(0c)+exp(-<i>*0c))/[*2,0*] by Lm2
 .= ([*1+1,0+0*])/[*2,0*] by Th20,COMPLFLD:2
 .= 1r by A1,COMPLEX1:86;
 hence thesis by L1;
end;

theorem
  cosh_C/.0c = [*1,0*]
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
   cosh_C/.0c = ([*1,0*]+[*1,0*])/[*2,0*] by Lm4,Th20,REAL_1:26
 .=[*1+1,0+0*]/[*2,0*] by COMPLFLD:2
 .=1r by A1,COMPLEX1:86;
 hence thesis by L1;
end;

theorem
  exp(z) = cosh_C/.z + sinh_C/.z
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
   cosh_C/.z + sinh_C/.z = (exp(z)+exp(-z))/[*2,0*] + sinh_C/.z by Lm4
 .= (exp(z)+exp(-z))/[*2,0*] + (exp(z)-exp(-z))/[*2,0*] by Lm3
 .= (exp(z)+exp(-z) + (exp(z)-exp(-z)))/[*2,0*] by XCMPLX_1:63
 .= (exp(z)+(exp(-z) + (exp(z)-exp(-z))))/[*2,0*] by XCMPLX_1:1
 .= (exp(z)+(exp(-z) + exp(z)-exp(-z)))/[*2,0*] by XCMPLX_1:29
 .= (exp(z)+exp(z))/[*2,0*] by XCMPLX_1:26
 .=[*Re(exp(z))+Re(exp(z)),Im(exp(z))+Im(exp(z))*]/[*2,0*] by COMPLEX1:def 9
 .=([*2*Re(exp(z)),Im(exp(z))+Im(exp(z))*])/[*2,0*] by XCMPLX_1:11
 .=([*2*Re(exp(z)),2*Im(exp(z))*])/[*2,0*] by XCMPLX_1:11
 .=([*Re([*2,0*]*exp(z)),2*Im(exp(z))*])/[*2,0*] by COMSEQ_3:17
 .=([*Re([*2,0*]*exp(z)),Im([*2,0*]*exp(z))*])/[*2,0*] by COMSEQ_3:17
 .=([*2,0*]*exp(z))/[*2,0*] by COMPLEX1:8
 .=exp(z)*([*2,0*]/[*2,0*]) by XCMPLX_1:75
 .=exp(z)*1r by A1,COMPLEX1:86;
 hence thesis by COMPLEX1:29;
end;

theorem
  exp(-z) = cosh_C/.z - sinh_C/.z
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
   cosh_C/.z - sinh_C/.z = (exp(z)+exp(-z))/[*2,0*] - sinh_C/.z by Lm4
 .= (exp(z)+exp(-z))/[*2,0*] - (exp(z)-exp(-z))/[*2,0*] by Lm3
 .= (exp(-z)+exp(z) - (exp(z)-exp(-z)))/[*2,0*] by XCMPLX_1:121
 .= (exp(-z)+(exp(z) - (exp(z)-exp(-z))))/[*2,0*] by XCMPLX_1:29
 .= (exp(-z)+((exp(z) - exp(z))+exp(-z)))/[*2,0*] by XCMPLX_1:37
 .= (exp(-z)+(exp(-z) + exp(z) - exp(z)))/[*2,0*] by XCMPLX_1:29
 .= (exp(-z)+exp(-z))/[*2,0*] by XCMPLX_1:26
 .=[*Re(exp(-z))+Re(exp(-z)),Im(exp(-z))+Im(exp(-z))*]/[*2,0*]
 by COMPLEX1:def 9
 .=([*2*Re(exp(-z)),Im(exp(-z))+Im(exp(-z))*])/[*2,0*] by XCMPLX_1:11
 .=([*2*Re(exp(-z)),2*Im(exp(-z))*])/[*2,0*] by XCMPLX_1:11
 .=([*Re([*2,0*]*exp(-z)),2*Im(exp(-z))*])/[*2,0*] by COMSEQ_3:17
 .=([*Re([*2,0*]*exp(-z)),Im([*2,0*]*exp(-z))*])/[*2,0*] by COMSEQ_3:17
 .=([*2,0*]*exp(-z))/[*2,0*] by COMPLEX1:8
 .=exp(-z)*([*2,0*]/[*2,0*]) by XCMPLX_1:75
 .=exp(-z)*1r by A1,COMPLEX1:86;
 hence thesis by COMPLEX1:29;
end;

Lm10:
for x being Element of REAL holds
[*0,x*] = [*x,0*]*<i>
proof
 let x be Element of REAL;
   [*x,0*]*<i> = [*x*0-0*1,x*1+0*0*] by COMPLEX1:def 8,HAHNBAN1:2;
 hence thesis;
end;

theorem
  exp(z+[*2*PI,0*]*<i>) = exp(z) &
exp(z+[*0,2*PI*]) = exp(z)
proof
 exp(z+[*2*PI,0*]*<i>) = exp(z)
 proof
    exp(z+[*2*PI,0*]*<i>)
  =exp([*Re z,Im z*]+[*2*PI,0*]*[*0,1*]) by COMPLEX1:8,def 8
  .=exp([*Re z,Im z*]+[*2*PI*0-0*1,2*PI*1+0*0*]) by HAHNBAN1:2
  .=exp([*Re z + 0,Im z + 2*PI*]) by COMPLFLD:2
  .=[*exp.(Re z)*cos.(Im z + 2*PI*1),exp.(Re z)*sin.(Im z + 2*PI)*] by Th19
  .=[*exp.(Re z)*cos.(Im z),exp.(Re z)*sin.(Im z + 2*PI*1)*] by SIN_COS2:11
  .=[*exp.(Re z)*cos.(Im z),exp.(Re z)*sin.(Im z)*] by SIN_COS2:10
  .=exp([*Re z,Im z*]) by Th19;
  hence thesis by COMPLEX1:8;
 end;
 hence thesis by Lm10;
end;

theorem Th28:
exp([*0,2*PI*n*]) = [*1,0*] & exp([*2*PI*n,0*]*<i>) = [*1,0*]
proof
 exp([*0,2*PI*n*]) = [*1,0*]
proof
   exp([*0,2*PI*n*]) = [*cos(0+2*PI*n),sin(0+2*PI*n)*] by SIN_COS:28
 .=[*cos.(0+2*PI*n),sin(0+2*PI*n)*] by SIN_COS:def 23
 .=[*cos.(0+2*PI*n),sin.(0+2*PI*n)*] by SIN_COS:def 21
 .=[*cos.(0+2*PI*n),sin.(0)*] by SIN_COS2:10
 .=[*1,sin.(0)*] by SIN_COS:33,SIN_COS2:11;
 hence thesis by SIN_COS:33;
end;
 hence thesis by Lm10;
end;

theorem Th29:
exp([*0,-2*PI*n*]) = [*1,0*] & exp([*-2*PI*n,0*]*<i>) = [*1,0*]
proof
 exp([*0,-2*PI*n*]) = [*1,0*]
 proof
   exp([*0,-2*PI*n*]) = [*cos(-2*PI*n),sin(-2*PI*n)*] by SIN_COS:28
 .=[*cos(2*PI*n),sin(-2*PI*n)*] by SIN_COS:34
 .=[*cos(0+2*PI*n),-sin(0+2*PI*n)*] by SIN_COS:34
 .=[*cos.(0+2*PI*n),-sin(0+2*PI*n)*] by SIN_COS:def 23
 .=[*cos.(0+2*PI*n),-sin.(0+2*PI*n)*] by SIN_COS:def 21
 .=[*cos.(0+2*PI*n),-sin.(0)*] by SIN_COS2:10
 .=[*1,-sin.(0)*] by SIN_COS:33,SIN_COS2:11;
 hence thesis by SIN_COS:33;
 end;
 hence thesis by Lm10;
end;

theorem
  exp([*0,(2*n+1)*PI*]) = [*-1,0*] & exp([*(2*n+1)*PI,0*]*<i>) = [*-1,0*]
proof
 exp([*0,(2*n+1)*PI*]) = [*-1,0*]
 proof
   exp([*0,(2*n+1)*PI*]) = [*cos((2*n+1)*PI),sin((2*n+1)*PI)*] by SIN_COS:28
 .= [*cos(PI*(2*n)+1*PI),sin((2*n+1)*PI)*] by XCMPLX_1:8
 .= [*cos(PI*(2*n)+1*PI),sin(PI*(2*n)+1*PI)*] by XCMPLX_1:8
 .= [*cos(PI*2*n+PI),sin(PI*(2*n)+1*PI)*] by XCMPLX_1:4
 .= [*cos(PI*2*n+PI),sin(PI*2*n+PI)*] by XCMPLX_1:4
 .= [*cos.(PI*2*n+PI),sin(PI*2*n+PI)*] by SIN_COS:def 23
 .= [*cos.(PI*2*n+PI),sin.(PI*2*n+PI)*] by SIN_COS:def 21
 .= [*cos.(PI),sin.(PI*2*n+PI)*] by SIN_COS2:11
 .= [*-1,sin.(PI)*] by SIN_COS:81,SIN_COS2:10;
 hence thesis by SIN_COS:81;
 end;
 hence thesis by Lm10;
end;

theorem
  exp([*0,-(2*n+1)*PI*]) = [*-1,0*] & exp([*-(2*n+1)*PI,0*]*<i>) = [*-1,0*]
proof
 exp([*0,-(2*n+1)*PI*]) = [*-1,0*]
 proof
   exp([*0,-(2*n+1)*PI*])
  = [*cos(-(2*n+1)*PI),sin(-(2*n+1)*PI)*] by SIN_COS:28
 .= [*cos((2*n+1)*PI),sin(-(2*n+1)*PI)*] by SIN_COS:34
 .= [*cos((2*n+1)*PI),-sin((2*n+1)*PI)*] by SIN_COS:34
 .= [*cos(PI*(2*n)+1*PI),-sin((2*n+1)*PI)*] by XCMPLX_1:8
 .= [*cos(PI*(2*n)+1*PI),-sin(PI*(2*n)+1*PI)*] by XCMPLX_1:8
 .= [*cos(PI*2*n+PI),-sin(PI*(2*n)+1*PI)*] by XCMPLX_1:4
 .= [*cos(PI*2*n+PI),-sin(PI*2*n+PI)*] by XCMPLX_1:4
 .= [*cos.(PI*2*n+PI),-sin(PI*2*n+PI)*] by SIN_COS:def 23
 .= [*cos.(PI*2*n+PI),-sin.(PI*2*n+PI)*] by SIN_COS:def 21
 .= [*cos.(PI),-sin.(PI*2*n+PI)*] by SIN_COS2:11
 .= [*-1,-sin.(PI)*] by SIN_COS:81,SIN_COS2:10;
 hence thesis by SIN_COS:81;
 end;
 hence thesis by Lm10;
end;

theorem
  exp([*0,(2*n + 1/2)*PI*]) = [*0,1*] & exp([*(2*n + 1/2)*PI,0*]*<i>) = [*0,1*]
proof
 exp([*0,(2*n + 1/2)*PI*]) = [*0,1*]
 proof
   exp([*0,(2*n+1/2)*PI*])
  = [*cos((2*n+1/2)*PI),sin((2*n+1/2)*PI)*] by SIN_COS:28
 .= [*cos(PI*(2*n)+1/2*PI),sin((2*n+1/2)*PI)*] by XCMPLX_1:8
 .= [*cos(PI*(2*n)+1/2*PI),sin(PI*(2*n)+1/2*PI)*] by XCMPLX_1:8
 .= [*cos(PI*2*n+1/2*PI),sin(PI*(2*n)+1/2*PI)*] by XCMPLX_1:4
 .= [*cos(PI*2*n+1/2*PI),sin(PI*2*n+1/2*PI)*] by XCMPLX_1:4
 .= [*cos.(PI*2*n+1/2*PI),sin(PI*2*n+1/2*PI)*] by SIN_COS:def 23
 .= [*cos.(PI*2*n+1/2*PI),sin.(PI*2*n+1/2*PI)*] by SIN_COS:def 21
 .= [*cos.(1/2*PI),sin.(PI*2*n+1/2*PI)*] by SIN_COS2:11
 .= [*cos.(1/2*PI),sin.(1/2*PI)*] by SIN_COS2:10
 .= [*cos.((1*PI)/2),sin.(1/2*PI)*] by XCMPLX_1:75
 .= [*0,sin.(PI/2)*] by SIN_COS:81,XCMPLX_1:75;
 hence thesis by SIN_COS:81;
 end;
 hence thesis by Lm10;
end;

theorem
  exp([*0,-(2*n + 1/2)*PI*]) = [*0,-1*] &
exp([*-(2*n + 1/2)*PI,0*]*<i>) = [*0,-1*]
proof
 exp([*0,-(2*n + 1/2)*PI*]) = [*0,-1*]
 proof
    exp([*0,-(2*n+1/2)*PI*])
   = [*cos(-(2*n+1/2)*PI),sin(-(2*n+1/2)*PI)*] by SIN_COS:28
  .= [*cos((2*n+1/2)*PI),sin(-(2*n+1/2)*PI)*] by SIN_COS:34
  .= [*cos((2*n+1/2)*PI),-sin((2*n+1/2)*PI)*] by SIN_COS:34
  .= [*cos(PI*(2*n)+1/2*PI),-sin((2*n+1/2)*PI)*] by XCMPLX_1:8
  .= [*cos(PI*(2*n)+1/2*PI),-sin(PI*(2*n)+1/2*PI)*] by XCMPLX_1:8
  .= [*cos(PI*2*n+1/2*PI),-sin(PI*(2*n)+1/2*PI)*] by XCMPLX_1:4
  .= [*cos(PI*2*n+1/2*PI),-sin(PI*2*n+1/2*PI)*] by XCMPLX_1:4
  .= [*cos.(PI*2*n+1/2*PI),-sin(PI*2*n+1/2*PI)*] by SIN_COS:def 23
  .= [*cos.(PI*2*n+1/2*PI),-sin.(PI*2*n+1/2*PI)*] by SIN_COS:def 21
  .= [*cos.(1/2*PI),-sin.(PI*2*n+1/2*PI)*] by SIN_COS2:11
  .= [*cos.(1/2*PI),-sin.(1/2*PI)*] by SIN_COS2:10
  .= [*cos.((1*PI)/2),-sin.(1/2*PI)*] by XCMPLX_1:75
  .= [*0,-sin.(PI/2)*] by SIN_COS:81,XCMPLX_1:75;
  hence thesis by SIN_COS:81;
 end;
 hence thesis by Lm10;
end;

Lm11:
for a,b being Element of REAL holds
-[*a,b*] = [*-a,-b*]
proof
 let a,b be Element of REAL;
   -[*a,b*] = (-1r)*[*a,b*] by COMPLEX1:46
 .= [*0*0-1*1,0*1+1*0*]*[*a,b*] by COMPLEX1:37,def 8,HAHNBAN1:2
 .= [*(-1)*a-0*b,(-1)*b+0*a*] by HAHNBAN1:2
 .= [*-a,(-1)*b*] by XCMPLX_1:180;
 hence thesis by XCMPLX_1:180;
end;

theorem
  sin_C/.(z + [*2*n*PI,0*]) = sin_C/.z
proof
      sin_C/.(z + [*2*n*PI,0*])
  = (exp(<i>*(z + [*2*n*PI,0*])) - exp(-<i>*(z + [*2*n*PI,0*])))
    /([*2,0*]*<i>) by Lm1
 .= (exp(<i>*z + <i>*[*2*n*PI,0*]) - exp(-<i>*(z + [*2*n*PI,0*])))
    /([*2,0*]*<i>) by XCMPLX_1:8
 .= (exp(<i>*z)*exp(<i>*[*2*n*PI,0*]) - exp(-<i>*(z + [*2*n*PI,0*])))
    /([*2,0*]*<i>) by SIN_COS:24
 .= (exp(<i>*z)*exp(<i>*[*2*PI*n,0*]) - exp(-<i>*(z + [*2*n*PI,0*])))
    /([*2,0*]*<i>) by XCMPLX_1:4
 .= (exp(<i>*z)*[*1,0*] - exp(-<i>*(z + [*2*n*PI,0*])))
    /([*2,0*]*<i>) by Th28
 .= (exp(<i>*z)*[*1,0*] - exp(-(<i>*z + <i>*[*2*n*PI,0*])))
    /([*2,0*]*<i>) by XCMPLX_1:8
 .= (exp(<i>*z)*[*1,0*] - exp(-<i>*z + -<i>*[*2*n*PI,0*]))
    /([*2,0*]*<i>) by XCMPLX_1:140
 .= (exp(<i>*z)*[*1,0*] - exp(-<i>*z) * exp(-<i>*[*2*n*PI,0*]))
    /([*2,0*]*<i>) by SIN_COS:24
 .= (exp(<i>*z)*[*1,0*] - exp(-<i>*z) * exp(-<i>*[*2*PI*n,0*]))
    /([*2,0*]*<i>) by XCMPLX_1:4
 .= (exp(<i>*z)*[*1,0*] - exp(-<i>*z) * exp(<i>*(-[*2*PI*n,0*])))
    /([*2,0*]*<i>) by XCMPLX_1:175
 .= (exp(<i>*z)*[*1,0*] - exp(-<i>*z) * exp(<i>*[*-2*PI*n,-0*]))
    /([*2,0*]*<i>) by Lm11
 .= (exp(<i>*z)*1r - exp(-<i>*z)*1r)/([*2,0*]*<i>) by Th29,L1
 .= (exp(<i>*z)*1r - exp(-<i>*z))/([*2,0*]*<i>) by COMPLEX1:29
 .= (exp(<i>*z) - exp(-<i>*z))/([*2,0*]*<i>) by COMPLEX1:29;
 hence thesis by Lm1;
end;

theorem
  cos_C/.(z + [*2*n*PI,0*]) = cos_C/.z
proof
      cos_C/.(z + [*2*n*PI,0*])
  = (exp(<i>*(z + [*2*n*PI,0*])) + exp(-<i>*(z + [*2*n*PI,0*])))
    /([*2,0*]) by Lm2
 .= (exp(<i>*z + <i>*[*2*n*PI,0*]) + exp(-<i>*(z + [*2*n*PI,0*])))
    /([*2,0*]) by XCMPLX_1:8
 .= (exp(<i>*z)*exp(<i>*[*2*n*PI,0*]) + exp(-<i>*(z + [*2*n*PI,0*])))
    /([*2,0*]) by SIN_COS:24
 .= (exp(<i>*z)*exp(<i>*[*2*PI*n,0*]) + exp(-<i>*(z + [*2*n*PI,0*])))
    /([*2,0*]) by XCMPLX_1:4
 .= (exp(<i>*z)*[*1,0*] + exp(-<i>*(z + [*2*n*PI,0*])))
    /([*2,0*]) by Th28
 .= (exp(<i>*z)*[*1,0*] + exp(-(<i>*z + <i>*[*2*n*PI,0*])))
    /([*2,0*]) by XCMPLX_1:8
 .= (exp(<i>*z)*[*1,0*] + exp(-<i>*z + -<i>*[*2*n*PI,0*]))
    /([*2,0*]) by XCMPLX_1:140
 .= (exp(<i>*z)*[*1,0*] + exp(-<i>*z) * exp(-<i>*[*2*n*PI,0*]))
    /([*2,0*]) by SIN_COS:24
 .= (exp(<i>*z)*[*1,0*] + exp(-<i>*z) * exp(-<i>*[*2*PI*n,0*]))
    /([*2,0*]) by XCMPLX_1:4
 .= (exp(<i>*z)*[*1,0*] + exp(-<i>*z) * exp(<i>*(-[*2*PI*n,0*])))
    /([*2,0*]) by XCMPLX_1:175
 .= (exp(<i>*z)*[*1,0*] + exp(-<i>*z) * exp(<i>*[*-2*PI*n,-0*]))
    /([*2,0*]) by Lm11
 .= (exp(<i>*z)*1r + exp(-<i>*z)*1r)/([*2,0*]) by Th29,L1
 .= (exp(<i>*z)*1r + exp(-<i>*z))/([*2,0*]) by COMPLEX1:29
 .= (exp(<i>*z) + exp(-<i>*z))/([*2,0*]) by COMPLEX1:29;
 hence thesis by Lm2;
end;

theorem Th36:
exp(<i>*z) = cos_C/.z + <i>*sin_C/.z
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
A2:<i> <> 0c by ARYTM_0:12,COMPLEX1:def 8,L0;
      cos_C/.z + <i>*sin_C/.z
  = (exp(<i>*z) + exp(-<i>*z))/([*2,0*]) + <i>*sin_C/.z by Lm2
 .= (exp(<i>*z) + exp(-<i>*z))/[*2,0*]
    + <i>*((exp(<i>*z) - exp(-<i>*z))/([*2,0*]*<i>)) by Lm1
 .= (exp(<i>*z) + exp(-<i>*z))/[*2,0*]
    + (<i>*(exp(<i>*z) - exp(-<i>*z))/([*2,0*]*<i>)) by XCMPLX_1:75
 .= (exp(<i>*z) + exp(-<i>*z))/[*2,0*]
    + (exp(<i>*z) - exp(-<i>*z))/[*2,0*] by A2,XCMPLX_1:92
 .= (exp(<i>*z) + exp(-<i>*z) + (exp(<i>*z) - exp(-<i>*z)))/[*2,0*]
    by XCMPLX_1:63
 .= (exp(<i>*z) + (exp(-<i>*z) +(exp(<i>*z) - exp(-<i>*z))))/[*2,0*]
    by XCMPLX_1:1
 .= (exp(<i>*z) + (exp(-<i>*z) +exp(<i>*z) - exp(-<i>*z)))/[*2,0*]
     by XCMPLX_1:29
 .= (exp(<i>*z) + exp(<i>*z))/[*2,0*] by XCMPLX_1:26
 .= [*Re exp(<i>*z) + Re exp(<i>*z),Im exp(<i>*z) + Im exp(<i>*z)*]/[*2,0*]
    by COMPLEX1:def 9
 .= [*2*Re exp(<i>*z),Im exp(<i>*z) + Im exp(<i>*z)*]/[*2,0*] by XCMPLX_1:11
 .= [*2*Re exp(<i>*z),2*Im exp(<i>*z)*]/[*2,0*] by XCMPLX_1:11
 .= [*Re([*2,0*]*exp(<i>*z)),2*Im exp(<i>*z)*]/[*2,0*] by COMSEQ_3:17
 .= [*Re([*2,0*]*exp(<i>*z)),Im([*2,0*]*exp(<i>*z))*]/[*2,0*] by COMSEQ_3:17
 .= ([*2,0*]*exp(<i>*z))/[*2,0*] by COMPLEX1:8;
 hence thesis by A1,XCMPLX_1:90;
end;

theorem Th37:
exp(-<i>*z) = cos_C/.z - <i>*sin_C/.z
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
A2:<i> <> 0c by ARYTM_0:12,COMPLEX1:def 8,L0;
      cos_C/.z - <i>*sin_C/.z
  = (exp(<i>*z) + exp(-<i>*z))/([*2,0*]) - <i>*sin_C/.z by Lm2
 .= (exp(<i>*z) + exp(-<i>*z))/[*2,0*]
    - <i>*((exp(<i>*z) - exp(-<i>*z))/([*2,0*]*<i>)) by Lm1
 .= (exp(<i>*z) + exp(-<i>*z))/[*2,0*]
    - (<i>*(exp(<i>*z) - exp(-<i>*z))/([*2,0*]*<i>)) by XCMPLX_1:75
 .= (exp(<i>*z) + exp(-<i>*z))/[*2,0*]
    - (exp(<i>*z) - exp(-<i>*z))/[*2,0*] by A2,XCMPLX_1:92
 .= (exp(<i>*z) + exp(-<i>*z) - (exp(<i>*z) - exp(-<i>*z)))/[*2,0*]
    by XCMPLX_1:121
 .= (exp(-<i>*z) + (exp(<i>*z) - (exp(<i>*z) - exp(-<i>*z))))/[*2,0*]
    by XCMPLX_1:29
 .= (exp(-<i>*z) + (exp(<i>*z) - exp(<i>*z) + exp(-<i>*z)))/[*2,0*]
    by XCMPLX_1:37
 .= (exp(-<i>*z) + (exp(-<i>*z) + exp(<i>*z) - exp(<i>*z)))/[*2,0*]
    by XCMPLX_1:29
 .= (exp(-<i>*z) + exp(-<i>*z))/[*2,0*] by XCMPLX_1:26
 .= [*Re exp(-<i>*z) + Re exp(-<i>*z),Im exp(-<i>*z) + Im exp(-<i>*z)*]/[*2,0*]
    by COMPLEX1:def 9
 .= [*2*Re exp(-<i>*z),Im exp(-<i>*z) + Im exp(-<i>*z)*]/[*2,0*]
    by XCMPLX_1:11
 .= [*2*Re exp(-<i>*z),2*Im exp(-<i>*z)*]/[*2,0*]
    by XCMPLX_1:11
 .= [*Re([*2,0*]*exp(-<i>*z)),2*Im exp(-<i>*z)*]/[*2,0*]
    by COMSEQ_3:17
 .= [*Re([*2,0*]*exp(-<i>*z)),Im([*2,0*]*exp(-<i>*z))*]/[*2,0*]
    by COMSEQ_3:17
 .= ([*2,0*]*exp(-<i>*z))/[*2,0*] by COMPLEX1:8;
 hence thesis by A1,XCMPLX_1:90;
end;

Lm12:
for x,y being Element of REAL holds
<i>*[*x,y*] = [*-y,x*]
proof
 let x,y be Element of REAL;
   <i>*[*x,y*] = [*0*x-1*y,0*y+1*x*] by COMPLEX1:def 8,HAHNBAN1:2
 .= [*0-1*y,1*x*];
 hence thesis by XCMPLX_1:150;
end;

theorem Th38:
for x being Element of REAL holds
sin_C/.[*x,0*] = [*sin.x,0*]
proof
 let x be Element of REAL;
A1:[*sin.x,0*]*[*0,2*] = [*sin.x*0-0*2,sin.x*2+0*0*] by HAHNBAN1:2
 .= [*0,2*sin.x*];
A2:[*0,2*] <> 0c
 proof
    [*2,0*]*<i> = [*-0,2*] by Lm12
  .= [*0,2*];
  hence thesis by Lm7;
 end;
   sin_C/.[*x,0*] = (exp(<i>*[*x,0*]) - exp(-<i>*[*x,0*]))/([*2,0*]*<i>) by Lm1
 .= (exp([*-0,x*]) - exp(-<i>*[*x,0*]))/([*2,0*]*<i>) by Lm12
 .= (exp([*0,x*]) - exp(-[*0,x*]))/([*2,0*]*<i>) by Lm12
 .= (exp([*0,x*]) - exp([*-0,-x*]))/([*2,0*]*<i>) by Lm11
 .= (exp([*0,x*]) - exp([*0,-x*]))/[*0,2*] by Lm12
 .= ([*exp.0*cos.x,exp.0*sin.x*] - exp([*0,-x*]))/[*0,2*] by Th19
 .= ([*exp(0)*cos.x,exp.0*sin.x*] - exp([*0,-x*]))/[*0,2*] by SIN_COS:def 27
 .= ([*cos.x,1*sin.x*] - exp([*0,-x*]))/[*0,2*] by SIN_COS:56,def 27
 .= ([*cos.x,1*sin.x*] - [*exp.0*cos.-x,exp.0*sin.-x*])/[*0,2*] by Th19
 .= ([*cos.x,1*sin.x*] - [*exp(0)*cos.-x,exp.0*sin.-x*])/[*0,2*]
    by SIN_COS:def 27
 .= ([*cos.x,sin.x*] - [*cos.-x,1*sin.-x*])/[*0,2*]
    by SIN_COS:56,def 27
 .= ([*cos.x,sin.x*] - [*cos.x,sin.-x*])/[*0,2*]
    by SIN_COS:33
 .= ([*cos.x,sin.x*] - [*cos.x,-sin.x*])/[*0,2*] by SIN_COS:33
 .= ([*cos.x,sin.x*] + - [*cos.x,-sin.x*])/[*0,2*] by XCMPLX_0:def 8
 .= ([*cos.x,sin.x*] + [*-cos.x,--sin.x*])/[*0,2*] by Lm11
 .= [*cos.x+-cos.x,sin.x+sin.x*]/[*0,2*] by COMPLFLD:2
 .= [*cos.x-cos.x,sin.x + sin.x*]/[*0,2*] by XCMPLX_0:def 8
 .= [*0,sin.x + sin.x*]/[*0,2*] by XCMPLX_1:14
 .= ([*sin.x,0*]*[*0,2*])/[*0,2*] by A1,XCMPLX_1:11
 .= [*sin.x,0*] by A2,XCMPLX_1:90;
 hence thesis;
end;

theorem Th39:
for x being Element of REAL holds
cos_C/.[*x,0*] = [*cos.x,0*]
proof
 let x be Element of REAL;
A1:[*2*cos.x,0*] = [*cos.x,0*]*[*2,0*]
 proof
    [*cos.x,0*]*[*2,0*] = [*cos.x*2-0*0,cos.x*0+0*2*] by HAHNBAN1:2
  .=[*2*cos.x,0*];
  hence thesis;
 end;
A2:[*2,0*] <> 0c by ARYTM_0:12,L0;
   cos_C/.[*x,0*] = (exp(<i>*[*x,0*]) + exp(-<i>*[*x,0*]))/[*2,0*] by Lm2
 .= (exp([*-0,x*]) + exp(-<i>*[*x,0*]))/[*2,0*] by Lm12
 .= (exp([*0,x*]) + exp(-[*0,x*]))/[*2,0*] by Lm12
 .= (exp([*0,x*]) + exp([*-0,-x*]))/[*2,0*] by Lm11
 .= ([*exp.0*cos.x,exp.0*sin.x*] + exp([*0,-x*]))/[*2,0*] by Th19
 .= ([*exp(0)*cos.x,exp.0*sin.x*] + exp([*0,-x*]))/[*2,0*] by SIN_COS:def 27
 .= ([*cos.x,1*sin.x*] + exp([*0,-x*]))/[*2,0*] by SIN_COS:56,def 27
 .= ([*cos.x,1*sin.x*] + [*exp.0*cos.-x,exp.0*sin.-x*])/[*2,0*] by Th19
 .= ([*cos.x,1*sin.x*] + [*exp(0)*cos.-x,exp.0*sin.-x*])/[*2,0*]
    by SIN_COS:def 27
 .= ([*cos.x,1*sin.x*] + [*exp(0)*cos.-x,exp(0)*sin.-x*])/[*2,0*]
    by SIN_COS:def 27
 .= ([*cos.x,sin.x*] + [*cos.x,sin.-x*])/[*2,0*] by SIN_COS:33,56
 .= ([*cos.x,sin.x*] + [*cos.x,-sin.x*])/[*2,0*] by SIN_COS:33
 .= [*cos.x+cos.x,sin.x+-sin.x*]/[*2,0*] by COMPLFLD:2
 .= [*cos.x+cos.x,sin.x-sin.x*]/[*2,0*] by XCMPLX_0:def 8
 .= [*cos.x+cos.x,0*]/[*2,0*] by XCMPLX_1:14
 .=([*cos.x,0*]*[*2,0*])/[*2,0*] by A1,XCMPLX_1:11
 .= [*cos.x,0*] by A2,XCMPLX_1:90;
 hence thesis;
end;

theorem Th40:
for x being Element of REAL holds
sinh_C/.[*x,0*] = [*sinh.x,0*]
proof
 let x be Element of REAL;
A1:[*exp.x-exp.(-x),0*] = [*sinh.x,0*]*[*2,0*]
 proof
    [*sinh.x,0*]*[*2,0*] = [*sinh.x*2-0*0,sinh.x*0+0*2*] by HAHNBAN1:2
  .=[*2*((exp.x - exp.(-x))/2),0*] by SIN_COS2:def 1
  .=[*(exp.x - exp.(-x))/(2/2),0*] by XCMPLX_1:82;
  hence thesis;
 end;
A2:[*2,0*] <> 0c by ARYTM_0:12,L0;
   sinh_C/.[*x,0*] = (exp([*x,0*])-exp(-[*x,0*]))/[*2,0*] by Lm3
 .= ([*exp.x*cos.0,exp.x*sin.0*] - exp(-[*x,0*]))/[*2,0*] by Th19
 .= ([*exp.x,0*] - exp([*-x,-0*]))/[*2,0*] by Lm11,SIN_COS:33
 .= ([*exp.x,0*] - [*exp.(-x)*cos.0,exp.(-x)*sin.0*])/[*2,0*] by Th19
 .= ([*exp.x,0*] +- [*exp.(-x),0*])/[*2,0*] by SIN_COS:33,XCMPLX_0:def 8
 .= ([*exp.x,0*] + [*-exp.(-x),-0*])/[*2,0*] by Lm11
 .= ([*exp.x+-exp.(-x),0+0*])/[*2,0*] by COMPLFLD:2
 .= ([*sinh.x,0*]*[*2,0*])/[*2,0*] by A1,XCMPLX_0:def 8;
 hence thesis by A2,XCMPLX_1:90;
end;

theorem Th41:
for x being Element of REAL holds
cosh_C/.[*x,0*] = [*cosh.x,0*]
proof
 let x be Element of REAL;
A1:[*exp.x+exp.(-x),0*] = [*cosh.x,0*]*[*2,0*]
 proof
    [*cosh.x,0*]*[*2,0*] = [*cosh.x*2-0*0,cosh.x*0+0*2*] by HAHNBAN1:2
  .=[*2*((exp.(x) + exp.(-x))/2),0*] by SIN_COS2:def 3
  .=[*(exp.(x) + exp.(-x))/(2/2),0*] by XCMPLX_1:82;
  hence thesis;
 end;
A2:[*2,0*] <> 0c by ARYTM_0:12,L0;
   cosh_C/.[*x,0*] = (exp([*x,0*])+exp(-[*x,0*]))/[*2,0*] by Lm4
 .= ([*exp.x*cos.0,exp.x*sin.0*] + exp(-[*x,0*]))/[*2,0*] by Th19
 .= ([*exp.x,0*] + exp([*-x,-0*]))/[*2,0*] by Lm11,SIN_COS:33
 .= ([*exp.x,0*] + [*exp.(-x)*cos.0,exp.(-x)*sin.0*])/[*2,0*] by Th19
 .= ([*exp.x+exp.(-x),0+0*])/[*2,0*] by COMPLFLD:2,SIN_COS:33
 .= ([*cosh.x,0*]*[*2,0*])/[*2,0*] by A1;
 hence thesis by A2,XCMPLX_1:90;
end;

theorem
  for x,y being Element of REAL holds
[*x,y*] = [*x,0*] + <i>*[*y,0*]
proof
 let x,y being Element of REAL;
   [*x,0*] + <i>*[*y,0*] = [*x,0*] + [*-0,y*] by Lm12
 .= [*x+0,0+y*] by COMPLFLD:2;
 hence thesis;
end;

theorem Th43:
sin_C/.[*x,y*] = [*sin.x*cosh.y,cos.x*sinh.y*]
proof
   sin_C/.[*x,y*] = sin_C/.[*x+0,0+y*]
 .= sin_C/.([*x,0*]+[*0,y*]) by COMPLFLD:2
 .= sin_C/.[*x,0*]*cos_C/.[*0,y*] + cos_C/.[*x,0*]*sin_C/.[*0,y*] by Th4
 .= sin_C/.[*x,0*]*cos_C/.(<i>*[*y,0*]) + cos_C/.[*x,0*]*sin_C/.[*0,y*]
    by Lm10
 .= sin_C/.[*x,0*]*cos_C/.(<i>*[*y,0*]) + cos_C/.[*x,0*]*sin_C/.(<i>*[*y,0*])
     by Lm10
 .= sin_C/.[*x,0*]*cosh_C/.[*y,0*] + cos_C/.[*x,0*]*sin_C/.(<i>*[*y,0*])
     by Th16
 .= sin_C/.[*x,0*]*cosh_C/.[*y,0*] + cos_C/.[*x,0*]*(<i>*sinh_C/.[*y,0*])
     by Th15
 .= [*sin.x,0*]*cosh_C/.[*y,0*] + cos_C/.[*x,0*]*(<i>*sinh_C/.[*y,0*]) by Th38
 .= [*sin.x,0*]*cosh_C/.[*y,0*] + [*cos.x,0*]*(<i>*sinh_C/.[*y,0*]) by Th39
 .= [*sin.x,0*]*cosh_C/.[*y,0*] + [*cos.x,0*]*(<i>*[*sinh.y,0*]) by Th40
 .= [*sin.x,0*]*[*cosh.y,0*] + [*cos.x,0*]*(<i>*[*sinh.y,0*]) by Th41
 .= [*sin.x*cosh.y-0*0,sin.x*0+0*cosh.y*] + [*cos.x,0*]*(<i>*[*sinh.y,0*])
    by HAHNBAN1:2
 .= [*sin.x*cosh.y,0*] + [*cos.x,0*]*[*sinh.y,0*]*<i> by XCMPLX_1:4
 .= [*sin.x*cosh.y,0*] + [*cos.x*sinh.y-0*0,cos.x*0+0*sinh.y*]*<i> by HAHNBAN1:
2
 .= [*sin.x*cosh.y,0*] + [*0,cos.x*sinh.y*] by Lm10
 .= [*sin.x*cosh.y+0,0+cos.x*sinh.y*] by COMPLFLD:2;
 hence thesis;
end;

theorem Th44:
sin_C/.[*x,-y*] = [*sin.x*cosh.y,-cos.x*sinh.y*]
proof
   sin_C/.[*x,-y*] = [*sin.x*cosh.-y,cos.x*sinh.-y*] by Th43
 .= [*sin.x*cosh.y,cos.x*sinh.-y*] by SIN_COS2:19
 .= [*sin.x*cosh.y,cos.x*-sinh.y*] by SIN_COS2:19;
 hence thesis by XCMPLX_1:175;
end;

theorem Th45:
cos_C/.[*x,y*] = [*cos.x*cosh.y,-sin.x*sinh.y*]
proof
   cos_C/.[*x,y*]= cos_C/.[*x+0,0+y*]
 .= cos_C/.([*x,0*]+[*0,y*]) by COMPLFLD:2
 .= cos_C/.[*x,0*]*cos_C/.[*0,y*]-sin_C/.[*x,0*]*sin_C/.[*0,y*] by Th6
 .= cos_C/.[*x,0*]*cos_C/.(<i>*[*y,0*])-sin_C/.[*x,0*]*sin_C/.[*0,y*] by Lm10
 .= cos_C/.[*x,0*]*cos_C/.(<i>*[*y,0*])-sin_C/.[*x,0*]*sin_C/.(<i>*[*y,0*])
    by Lm10
 .= cos_C/.[*x,0*]*cos_C/.(<i>*[*y,0*])-sin_C/.[*x,0*]*(sinh_C/.[*y,0*]*<i>)
     by Th15
 .= cos_C/.[*x,0*]*cosh_C/.[*y,0*]-sin_C/.[*x,0*]*(sinh_C/.[*y,0*]*<i>)
     by Th16
 .= cos_C/.[*x,0*]*cosh_C/.[*y,0*]-[*sin.x,0*]*(sinh_C/.[*y,0*]*<i>) by Th38
 .= [*cos.x,0*]*cosh_C/.[*y,0*]-[*sin.x,0*]*(sinh_C/.[*y,0*]*<i>) by Th39
 .= [*cos.x,0*]*cosh_C/.[*y,0*]-[*sin.x,0*]*([*sinh.y,0*]*<i>) by Th40
 .= [*cos.x,0*]*[*cosh.y,0*]-[*sin.x,0*]*([*sinh.y,0*]*<i>) by Th41
 .= [*cos.x,0*]*[*cosh.y,0*]-[*sin.x,0*]*[*sinh.y,0*]*<i> by XCMPLX_1:4
 .= [*cos.x*cosh.y-0*0,cos.x*0+0*cosh.y*]-[*sin.x,0*]*[*sinh.y,0*]*<i> by
HAHNBAN1:2
 .= [*cos.x*cosh.y,0*]-[*sin.x*sinh.y-0*0,sin.x*0+0*sinh.y-0*]*<i> by HAHNBAN1:
2
 .= [*cos.x*cosh.y,0*]+-[*sin.x*sinh.y,0*]*<i> by XCMPLX_0:def 8
 .= [*cos.x*cosh.y,0*]+-[*-0,sin.x*sinh.y*] by Lm12
 .= [*cos.x*cosh.y,0*]+[*-0,-sin.x*sinh.y*] by Lm11
 .= [*cos.x*cosh.y+-0,0+-sin.x*sinh.y*] by COMPLFLD:2;
 hence thesis;
end;

theorem Th46:
cos_C/.[*x,-y*] = [*cos.x*cosh.y,sin.x*sinh.y*]
proof
   cos_C/.[*x,-y*] = [*cos.x*cosh.-y,-sin.x*sinh.-y*] by Th45
 .= [*cos.x*cosh.y,-sin.x*sinh.-y*] by SIN_COS2:19
 .= [*cos.x*cosh.y,-sin.x*-sinh.y*] by SIN_COS2:19
 .= [*cos.x*cosh.y,--sin.x*sinh.y*] by XCMPLX_1:175;
 hence thesis;
end;

theorem Th47:
sinh_C/.[*x,y*] = [*sinh.x*cos.y,cosh.x*sin.y*]
proof
   sinh_C/.[*x,y*] = sinh_C/.[*--x,y*]
 .= sinh_C/.([*y,-x*]*<i>) by Lm12
 .= <i>*sin_C/.[*y,-x*] by Th17
 .= <i>*[*sin.y*cosh.x,-cos.y*sinh.x*] by Th44
 .= [*--sinh.x*cos.y,cosh.x*sin.y*] by Lm12;
 hence thesis;
end;

theorem Th48:
sinh_C/.[*x,-y*] = [*sinh.x*cos.y,-cosh.x*sin.y*]
proof
   sinh_C/.[*x,-y*] = [*sinh.x*cos.-y,cosh.x*sin.-y*] by Th47
 .= [*sinh.x*cos.y,cosh.x*sin.-y*] by SIN_COS:33
 .= [*sinh.x*cos.y,cosh.x*-sin.y*] by SIN_COS:33;
 hence thesis by XCMPLX_1:175;
end;

theorem Th49:
cosh_C/.[*x,y*] = [*cosh.x*cos.y,sinh.x*sin.y*]
proof
    cosh_C/.[*x,y*] = cosh_C/.[*--x,y*]
 .=cosh_C/.([*y,-x*]*<i>) by Lm12
 .=cos_C/.[*y,-x*] by Th18;
 hence thesis by Th46;
end;

theorem Th50:
cosh_C/.[*x,-y*] = [*cosh.x*cos.y,-sinh.x*sin.y*]
proof
   cosh_C/.[*x,-y*] = [*cosh.x*cos.-y,sinh.x*sin.-y*] by Th49
 .=[*cosh.x*cos.y,sinh.x*sin.-y*] by SIN_COS:33
 .=[*cosh.x*cos.y,sinh.x*-sin.y*] by SIN_COS:33;
 hence thesis by XCMPLX_1:175;
end;

theorem Th51:
for n being Nat, z being Element of COMPLEX holds
(cos_C/.z + <i>*sin_C/.z) #N n = cos_C/.([*n,0*]*z) + <i>*sin_C/.([*n,0*]*z)
proof
 defpred X[Nat] means  for z being Element of COMPLEX holds
 (cos_C/.z + <i>*sin_C/.z) #N ($1)
 = cos_C/.([*$1,0*]*z) + <i>*sin_C/.([*$1,0*]*z);
A1: X[0] by Th21,Th23,L0,L1,COMSEQ_3:11;
A2:for n st X[n] holds X[n+1]
 proof
  let n be Nat such that
A3:for z being Element of COMPLEX holds
  (cos_C/.z + <i>*sin_C/.z) #N n = cos_C/.([*n,0*]*z) + <i>*sin_C/.([*n,0*]*z);
    for z being Element of COMPLEX holds (cos_C/.z + <i>*sin_C/.z) #N (n+1)
  = cos_C/.([*n+1,0*]*z) + <i>*sin_C/.([*n+1,0*]*z)
  proof
   let z being Element of COMPLEX;
   set cn = cos_C/.([*n,0*]*z), sn = sin_C/.([*n,0*]*z),
       c1 = cos_C/.z , s1 = sin_C/.z;
A4:   (cos_C/.z + <i>*sin_C/.z) #N (n+1)
    = (cos_C/.z + <i>*sin_C/.z) GeoSeq.(n+1) by COMSEQ_3:def 2
   .= (cos_C/.z + <i>*sin_C/.z) GeoSeq.n * (cos_C/.z + <i>*sin_C/.z)
     by COMSEQ_3:def 1
   .= (cos_C/.z + <i>*sin_C/.z) #N n * (cos_C/.z + <i>*sin_C/.z)
      by COMSEQ_3:def 2
   .= (cos_C/.([*n,0*]*z) + <i>*sin_C/.([*n,0*]*z)) * (cos_C/.z + <i>*sin_C/.z)
      by A3
   .= (cn + <i>*sn)*c1 + (cn + <i>*sn)*(<i>*s1) by XCMPLX_1:8
   .= cn*c1 + <i>*sn*c1 + (cn + <i>*sn)*(<i>*s1) by XCMPLX_1:8
   .= cn*c1 + <i>*sn*c1 + (cn*(<i>*s1) + <i>*sn*(<i>*s1)) by XCMPLX_1:8
   .= cn*c1 + <i>*sn*c1 + (cn*(<i>*s1) + (<i>*sn*<i>)*s1) by XCMPLX_1:4
   .= cn*c1 + <i>*sn*c1 + (cn*(<i>*s1) + (-1r)*sn*s1) by COMPLEX1:37,XCMPLX_1:4
   .= cn*c1 + <i>*sn*c1 + (cn*(<i>*s1) + (-1r)*(sn*s1)) by XCMPLX_1:4
   .= cn*c1 + <i>*sn*c1 + (cn*(<i>*s1) + -sn*s1) by COMPLEX1:46
   .= cn*c1 + <i>*sn*c1 + (<i>*cn*s1 + -sn*s1) by XCMPLX_1:4;
        cos_C/.([*n+1,0*]*z) + <i>*sin_C/.([*n+1,0*]*z)
   = cos_C/.(([*n,0*] +[*1,0*])*z) + <i>*sin_C/.([*n+1,0+0*]*z) by COMPLFLD:2
   .= cos_C/.(([*n,0*] +[*1,0*])*z) + <i>*sin_C/.(([*n,0*]+[*1,0*])*z) by
COMPLFLD:2
   .= cos_C/.([*n,0*]*z +[*1,0*]*z) + <i>*sin_C/.(([*n,0*]+[*1,0*])*z)
      by XCMPLX_1:8
   .= cos_C/.([*n,0*]*z +[*1,0*]*z) + <i>*sin_C/.([*n,0*]*z+[*1,0*]*z)
      by XCMPLX_1:8
   .= cos_C/.([*n,0*]*z +[*1,0*]*z) +
      <i>*(sin_C/.([*n,0*]*z)*cos_C/.([*1,0*]*z)
      + cos_C/.([*n,0*]*z)*sin_C/.([*1,0*]*z)) by Th4
   .= cos_C/.([*n,0*]*z)*cos_C/.([*1,0*]*z)
      - sin_C/.([*n,0*]*z)*sin_C/.([*1,0*]*z)
      + <i>*(sin_C/.([*n,0*]*z)*cos_C/.([*1,0*]*z)
      + cos_C/.([*n,0*]*z)*sin_C/.([*1,0*]*z)) by Th6
   .= cos_C/.([*n,0*]*z)*cos_C/.z
      - sin_C/.([*n,0*]*z)*sin_C/.(1r*z)
      + <i>*(sin_C/.([*n,0*]*z)*cos_C/.(1r*z)
      + cos_C/.([*n,0*]*z)*sin_C/.(1r*z)) by COMPLEX1:29,L1
   .= cos_C/.([*n,0*]*z)*cos_C/.z
      - sin_C/.([*n,0*]*z)*sin_C/.z
      + <i>*(sin_C/.([*n,0*]*z)*cos_C/.(1r*z)
      + cos_C/.([*n,0*]*z)*sin_C/.(1r*z)) by COMPLEX1:29
   .= cos_C/.([*n,0*]*z)*cos_C/.z
      - sin_C/.([*n,0*]*z)*sin_C/.z
      + <i>*(sin_C/.([*n,0*]*z)*cos_C/.z
      + cos_C/.([*n,0*]*z)*sin_C/.(1r*z)) by COMPLEX1:29
   .= cos_C/.([*n,0*]*z)*cos_C/.z
      - sin_C/.([*n,0*]*z)*sin_C/.z
      + <i>*(sin_C/.([*n,0*]*z)*cos_C/.z
      + cos_C/.([*n,0*]*z)*sin_C/.z) by COMPLEX1:29
   .= cn*c1 - sn*s1 + (<i>*(sn*c1) + <i>*(cn*s1)) by XCMPLX_1:8
   .= cn*c1 +- sn*s1 + (<i>*(sn*c1) + <i>*(cn*s1)) by XCMPLX_0:def 8
   .= cn*c1 +- sn*s1 + (<i>*(sn*c1) + <i>*cn*s1) by XCMPLX_1:4
   .= cn*c1 +- sn*s1 + (<i>*sn*c1 + <i>*cn*s1) by XCMPLX_1:4
   .= cn*c1 +( (<i>*sn*c1 + <i>*cn*s1) + -sn*s1 ) by XCMPLX_1:1
   .= cn*c1 +( <i>*sn*c1 + (<i>*cn*s1 + -sn*s1) ) by XCMPLX_1:1;
   hence thesis by A4,XCMPLX_1:1;
  end;
  hence thesis;
 end;
   for n holds X[n] from Ind(A1,A2);
 hence thesis;
end;

theorem Th52:
for n being Nat, z being Element of COMPLEX holds
(cos_C/.z - <i>*sin_C/.z) #N n = cos_C/.([*n,0*]*z) - <i>*sin_C/.([*n,0*]*z)
proof
 let n be Nat;
 let z be Element of COMPLEX;
     (cos_C/.z - <i>*sin_C/.z) #N n
  =(cos_C/.z + -<i>*sin_C/.z) #N n by XCMPLX_0:def 8
 .=(cos_C/.z + <i>*-sin_C/.z) #N n by XCMPLX_1:175
 .=(cos_C/.z + <i>*sin_C/.-z) #N n by Th2
 .=(cos_C/.-z + <i>*sin_C/.-z) #N n by Th3
 .= cos_C/.([*n,0*]*-z) + <i>*sin_C/.([*n,0*]*-z) by Th51
 .= cos_C/.(-[*n,0*]*z) + <i>*sin_C/.([*n,0*]*-z) by XCMPLX_1:175
 .= cos_C/.(-[*n,0*]*z) + <i>*sin_C/.(-[*n,0*]*z) by XCMPLX_1:175
 .= cos_C/.([*n,0*]*z) + <i>*sin_C/.(-[*n,0*]*z) by Th3
 .= cos_C/.([*n,0*]*z) + <i>*-sin_C/.([*n,0*]*z) by Th2
 .= cos_C/.([*n,0*]*z) + -<i>*sin_C/.([*n,0*]*z) by XCMPLX_1:175;
 hence thesis by XCMPLX_0:def 8;
end;

theorem
  for n being Nat, z being Element of COMPLEX holds
exp(<i>*[*n,0*]*z) = (cos_C/.z + <i>*sin_C/.z) #N n
proof
 let n being Nat;
 let z being Element of COMPLEX;
   exp(<i>*[*n,0*]*z)
 =exp(<i>*([*n,0*]*z)) by XCMPLX_1:4
 .=cos_C/.([*n,0*]*z) + <i>*sin_C/.([*n,0*]*z) by Th36;
 hence thesis by Th51;
end;

theorem
  for n being Nat, z being Element of COMPLEX holds
exp(-<i>*[*n,0*]*z) = (cos_C/.z - <i>*sin_C/.z) #N n
proof
 let n being Nat;
 let z being Element of COMPLEX;
   exp(-<i>*[*n,0*]*z)
 =exp(-<i>*([*n,0*]*z)) by XCMPLX_1:4
 .=cos_C/.([*n,0*]*z) - <i>*sin_C/.([*n,0*]*z) by Th37;
 hence thesis by Th52;
end;

theorem
  for x,y being Element of REAL holds
[*1,-1*]/[*2,0*]*sinh_C/.[*x,y*] + [*1,1*]/[*2,0*]*sinh_C/.[*x,-y*]
= [*sinh.x*cos.y + cosh.x*sin.y,0*]
proof
 let x,y being Element of REAL;
 set shx = sinh.x, cy = cos.y, chx = cosh.x, sy = sin.y;
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
A2:[*2,0*]*[*shx*cy+chx*sy,0*] = [*2*(shx*cy+chx*sy),0*]
 proof
    [*2,0*]*[*shx*cy+chx*sy,0*]
   = [*2*(shx*cy+chx*sy)-0*0,2*0+0*(shx*cy+chx*sy)*] by HAHNBAN1:2;
  hence thesis;
 end;
      [*1,-1*]/[*2,0*]*sinh_C/.[*x,y*] + [*1,1*]/[*2,0*]*sinh_C/.[*x,-y*]
  = [*1,-1*]/[*2,0*]*[*shx*cy,chx*sy*] + [*1,1*]/[*2,0*]*sinh_C/.[*x,-y*]
    by Th47
 .= [*1,-1*]/[*2,0*]*[*shx*cy,chx*sy*] + [*1,1*]/[*2,0*]*[*shx*cy,-chx*sy*]
    by Th48
 .= [*1,-1*]*[*shx*cy,chx*sy*]/[*2,0*] + [*1,1*]/[*2,0*]*[*shx*cy,-chx*sy*]
    by XCMPLX_1:75
 .= [*1,-1*]*[*shx*cy,chx*sy*]/[*2,0*] + [*1,1*]*[*shx*cy,-chx*sy*]/[*2,0*]
    by XCMPLX_1:75
 .= ([*1,-1*]*[*shx*cy,chx*sy*] + [*1,1*]*[*shx*cy,-chx*sy*])/[*2,0*]
    by XCMPLX_1:63
 .= ([*1*(shx*cy)-(-1)*(chx*sy),1*(chx*sy)+(-1)*(shx*cy)*]
    + [*1,1*]*[*shx*cy,-chx*sy*])/[*2,0*] by HAHNBAN1:2
 .= ([*shx*cy-(-1)*(chx*sy),chx*sy+(-1)*(shx*cy)*]
    + [*1*shx*cy-1*(-chx*sy),1*(-chx*sy)+1*shx*cy*])/[*2,0*] by HAHNBAN1:2
 .= ([*shx*cy--chx*sy,chx*sy+(-1)*(shx*cy)*]
    + [*shx*cy-(-chx*sy),(-chx*sy)+shx*cy*])/[*2,0*] by XCMPLX_1:176
 .= ([*shx*cy--chx*sy,chx*sy+-(1*(shx*cy))*]
    + [*shx*cy-(-chx*sy),(-chx*sy)+shx*cy*])/[*2,0*] by XCMPLX_1:175
 .= [*shx*cy--chx*sy+(shx*cy--chx*sy),chx*sy+-shx*cy+(-chx*sy+shx*cy)*]
    /[*2,0*] by COMPLFLD:2
 .= [*shx*cy--chx*sy+(shx*cy--chx*sy),-shx*cy+chx*sy+-chx*sy+shx*cy*]
    /[*2,0*] by XCMPLX_1:1
 .= [*shx*cy--chx*sy+(shx*cy--chx*sy),-shx*cy+(chx*sy+-chx*sy)+shx*cy*]
    /[*2,0*] by XCMPLX_1:1
 .= [*shx*cy--chx*sy+(shx*cy--chx*sy),-shx*cy+(chx*sy-chx*sy)+shx*cy*]
    /[*2,0*] by XCMPLX_0:def 8
 .= [*shx*cy--chx*sy+(shx*cy--chx*sy),-shx*cy+0+shx*cy*]
    /[*2,0*] by XCMPLX_1:14
 .= [*shx*cy--chx*sy+(shx*cy--chx*sy),shx*cy-shx*cy*]
    /[*2,0*] by XCMPLX_0:def 8
 .= [*shx*cy--chx*sy+(shx*cy--chx*sy),0*]
    /[*2,0*] by XCMPLX_1:14
 .= [*shx*cy+--chx*sy+(shx*cy--chx*sy),0*]/[*2,0*] by XCMPLX_0:def 8
 .= [*shx*cy+--chx*sy+(shx*cy+--chx*sy),0*]/[*2,0*] by XCMPLX_0:def 8
 .= [*2,0*]*[*shx*cy+chx*sy,0*]/[*2,0*] by A2,XCMPLX_1:11;
 hence thesis by A1,XCMPLX_1:90;
end;

theorem
  for x,y being Element of REAL holds
[*1,-1*]/[*2,0*]*cosh_C/.[*x,y*] + [*1,1*]/[*2,0*]*cosh_C/.[*x,-y*]
= [*sinh.x*sin.y + cosh.x*cos.y,0*]
proof
 let x,y being Element of REAL;
 set shx = sinh.x, cy = cos.y, chx = cosh.x, sy = sin.y;
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
A2:[*2,0*]*[*shx*sy+chx*cy,0*] = [*2*(shx*sy+chx*cy),0*]
 proof
    [*2,0*]*[*shx*sy+chx*cy,0*]
   = [*2*(shx*sy+chx*cy)-0*0,2*0+0*(shx*sy+chx*cy)*] by HAHNBAN1:2;
  hence thesis;
 end;
   [*1,-1*]/[*2,0*]*cosh_C/.[*x,y*] + [*1,1*]/[*2,0*]*cosh_C/.[*x,-y*]
 = [*1,-1*]/[*2,0*]*[*chx*cy,shx*sy*] + [*1,1*]/[*2,0*]*cosh_C/.[*x,-y*]
   by Th49
 .= [*1,-1*]/[*2,0*]*[*chx*cy,shx*sy*] + [*1,1*]/[*2,0*]*[*chx*cy,-shx*sy*]
    by Th50
 .= [*1,-1*]*[*chx*cy,shx*sy*]/[*2,0*] + [*1,1*]/[*2,0*]*[*chx*cy,-shx*sy*]
    by XCMPLX_1:75
 .= [*1,-1*]*[*chx*cy,shx*sy*]/[*2,0*] + [*1,1*]*[*chx*cy,-shx*sy*]/[*2,0*]
    by XCMPLX_1:75
 .= ([*1,-1*]*[*chx*cy,shx*sy*] + [*1,1*]*[*chx*cy,-shx*sy*])/[*2,0*]
    by XCMPLX_1:63
 .= ([*1*(chx*cy)-(-1)*(shx*sy),1*(shx*sy)+(-1)*(chx*cy)*] +
     [*1,1*]*[*chx*cy,-shx*sy*])/[*2,0*]
    by HAHNBAN1:2
 .= ([*chx*cy-(-1)*(shx*sy),shx*sy+(-1)*(chx*cy)*] +
     [*1*(chx*cy)-1*(-shx*sy),1*(-shx*sy)+1*(chx*cy)*])/[*2,0*] by HAHNBAN1:2
 .= ([*chx*cy--shx*sy,shx*sy+(-1)*(chx*cy)*] +
     [*chx*cy--shx*sy,-shx*sy+chx*cy*])/[*2,0*] by XCMPLX_1:176
 .= ([*chx*cy--shx*sy,shx*sy+-1*(chx*cy)*] +
     [*chx*cy--shx*sy,-shx*sy+chx*cy*])/[*2,0*] by XCMPLX_1:175
 .= [*chx*cy--shx*sy+(chx*cy--shx*sy),shx*sy+-chx*cy+(-shx*sy+chx*cy)*]
    /[*2,0*] by COMPLFLD:2
 .= [*2*(chx*cy--shx*sy),shx*sy+-chx*cy+(-shx*sy+chx*cy)*]
    /[*2,0*] by XCMPLX_1:11
 .= [*2*(chx*cy--shx*sy),-chx*cy+shx*sy+-shx*sy+chx*cy*]
    /[*2,0*] by XCMPLX_1:1
 .= [*2*(chx*cy--shx*sy),-chx*cy+(shx*sy+-shx*sy)+chx*cy*]
    /[*2,0*] by XCMPLX_1:1
 .= [*2*(chx*cy--shx*sy),-chx*cy+(shx*sy-shx*sy)+chx*cy*]
    /[*2,0*] by XCMPLX_0:def 8
 .= [*2*(chx*cy--shx*sy),-chx*cy+0+chx*cy*] /[*2,0*] by XCMPLX_1:14
 .= [*2*(chx*cy--shx*sy),chx*cy-chx*cy*] /[*2,0*] by XCMPLX_0:def 8
 .= [*2*(chx*cy--shx*sy),0*] /[*2,0*] by XCMPLX_1:14
 .= [*2*(chx*cy+--shx*sy),0*] /[*2,0*] by XCMPLX_0:def 8
 .= [*2,0*]*[*shx*sy+chx*cy,0*]/[*2,0*] by A2;
 hence thesis by A1,XCMPLX_1:90;
end;

Lm13:
z + z = [*2,0*]*z
proof
   z + z = [*Re z + Re z,Im z+Im z*] by COMPLEX1:def 9
 .= [*2*(Re z),Im z+Im z*] by XCMPLX_1:11
 .= [*2*(Re z),2*(Im z)*] by XCMPLX_1:11
 .= [*Re ([*2,0*]*z),2*(Im z)*] by COMSEQ_3:17
 .= [*Re ([*2,0*]*z),Im ([*2,0*]*z)*] by COMSEQ_3:17;
 hence thesis by COMPLEX1:8;
end;

theorem
  sinh_C/.z*sinh_C/.z = (cosh_C/.([*2,0*]*z) - [*1,0*])/[*2,0*]
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
 set e1 = exp(z), e2 = exp(-z);
   sinh_C/.z*sinh_C/.z
  = (exp(z) - exp(-z))/[*2,0*]*sinh_C/.z by Lm3
 .= (e1 - e2)/[*2,0*]*((e1 - e2)/[*2,0*]) by Lm3
 .= (e1 - e2)*((e1 - e2)/[*2,0*])/[*2,0*] by XCMPLX_1:75
 .= (e1 - e2)*(e1 - e2)/[*2,0*]/[*2,0*] by XCMPLX_1:75
 .= (e1*e1 + e2*e2 - (e1*e2 + e1*e2))/[*2,0*]/[*2,0*] by Lm6
 .= (e1*e1 + e2*e2 - [*2,0*]*(e1*e2))/[*2,0*]/[*2,0*] by Lm13
 .= (e1*e1 + e2*e2 - [*2,0*]*1r)/[*2,0*]/[*2,0*] by Lm8,L1
 .= (e1*e1 + e2*e2 - [*2,0*])/[*2,0*]/[*2,0*] by COMPLEX1:29
 .= (exp(z+z) + e2*e2 - [*2,0*])/[*2,0*]/[*2,0*] by SIN_COS:24
 .= (exp(z+z) + exp(-z+-z) - [*2,0*])/[*2,0*]/[*2,0*] by SIN_COS:24
 .= (exp([*2,0*]*z) + exp(-z+-z) - [*2,0*])/[*2,0*]/[*2,0*] by Lm13
 .= (exp([*2,0*]*z) + exp([*2,0*]*(-z)) - [*2,0*])/[*2,0*]/[*2,0*] by Lm13
 .= (( exp([*2,0*]*z) + exp([*2,0*]*(-z)) )/[*2,0*] - [*2,0*]/[*2,0*])
    /[*2,0*] by XCMPLX_1:121
 .= (( exp([*2,0*]*z) + exp([*2,0*]*(-z)) )/[*2,0*] - [*1,0*])
     /[*2,0*] by A1,COMPLEX1:86,L1
 .= (( exp([*2,0*]*z) + exp(-[*2,0*]*(z)) )/[*2,0*] - [*1,0*])
      /[*2,0*] by XCMPLX_1:175;
 hence thesis by Lm4;
end;

theorem Th58:
cosh_C/.z*cosh_C/.z = (cosh_C/.([*2,0*]*z) + [*1,0*])/[*2,0*]
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
 set e1 = exp(z), e2 = exp(-z);
   cosh_C/.z*cosh_C/.z
  = (exp(z) + exp(-z))/[*2,0*]*cosh_C/.z by Lm4
 .= (e1 + e2)/[*2,0*]*((e1 + e2)/[*2,0*]) by Lm4
 .= (e1 + e2)*((e1 + e2)/[*2,0*])/[*2,0*] by XCMPLX_1:75
 .= (e1 + e2)*(e1 + e2)/[*2,0*]/[*2,0*] by XCMPLX_1:75
 .= (e1*e1 + e2*e2 + e1*e2 + e1*e2)/[*2,0*]/[*2,0*] by Lm5
 .= (e1*e1 + e2*e2 + (e1*e2 + e1*e2))/[*2,0*]/[*2,0*] by XCMPLX_1:1
 .= (e1*e1 + e2*e2 + [*2,0*]*(e1*e2))/[*2,0*]/[*2,0*] by Lm13
 .= (e1*e1 + e2*e2 + [*2,0*]*1r)/[*2,0*]/[*2,0*] by Lm8,L1
 .= (e1*e1 + e2*e2 + [*2,0*])/[*2,0*]/[*2,0*] by COMPLEX1:29
 .= (exp(z+z) + e2*e2 + [*2,0*])/[*2,0*]/[*2,0*] by SIN_COS:24
 .= (exp(z+z) + exp(-z+-z) + [*2,0*])/[*2,0*]/[*2,0*] by SIN_COS:24
 .= (exp([*2,0*]*z) + exp(-z+-z) + [*2,0*])/[*2,0*]/[*2,0*] by Lm13
 .= (exp([*2,0*]*z) + exp([*2,0*]*(-z)) + [*2,0*])/[*2,0*]/[*2,0*] by Lm13
 .= (( exp([*2,0*]*z) + exp([*2,0*]*(-z)) )/[*2,0*] + [*2,0*]/[*2,0*])
    /[*2,0*] by XCMPLX_1:63
 .= (( exp([*2,0*]*z) + exp([*2,0*]*(-z)) )/[*2,0*] + [*1,0*])
     /[*2,0*] by A1,COMPLEX1:86,L1
 .= (( exp([*2,0*]*z) + exp(-[*2,0*]*(z)) )/[*2,0*] + [*1,0*])
      /[*2,0*] by XCMPLX_1:175;
 hence thesis by Lm4;
end;

theorem Th59:
sinh_C/.([*2,0*]*z) = [*2,0*]*(sinh_C/.z)*(cosh_C/.z) &
cosh_C/.([*2,0*]*z) = [*2,0*]*(cosh_C/.z)*(cosh_C/.z) - [*1,0*]
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
 set e1 = exp(z), e2 = exp(-z);
A2:sinh_C/.([*2,0*]*z) = [*2,0*]*(sinh_C/.z)*(cosh_C/.z)
 proof
    [*2,0*]*(sinh_C/.z)*(cosh_C/.z)
   = [*2,0*]*((sinh_C/.z)*(cosh_C/.z)) by XCMPLX_1:4
  .= [*2,0*]*((sinh_C/.z)*((e1 + e2)/[*2,0*])) by Lm4
  .= [*2,0*]*((e1 - e2)/[*2,0*]*((e1 + e2)/[*2,0*])) by Lm3
  .= [*2,0*]*((e1 - e2)*((e1 + e2)/[*2,0*])/[*2,0*]) by XCMPLX_1:75
  .= [*2,0*]*((e1 - e2)*(e1 + e2)/[*2,0*]/[*2,0*]) by XCMPLX_1:75
  .= [*2,0*]*((e1 - e2)*(e1 + e2)/[*2,0*])/[*2,0*] by XCMPLX_1:75
  .= (e1 - e2)*(e1 + e2)/[*2,0*] by A1,XCMPLX_1:90
  .= ((e1 - e2)*e1 + (e1 - e2)*e2)/[*2,0*] by XCMPLX_1:8
  .= (e1*e1 - e2*e1 + (e1 - e2)*e2)/[*2,0*] by XCMPLX_1:40
  .= (e1*e1 - e2*e1 + (e1*e2 - e2*e2))/[*2,0*] by XCMPLX_1:40
  .= ((e1*e1 - e2*e1 + e1*e2) - e2*e2)/[*2,0*] by XCMPLX_1:29
  .= (e1*e1 - e2*e2)/[*2,0*] by XCMPLX_1:27
  .= (exp(z+z) - e2*e2)/[*2,0*] by SIN_COS:24
  .= (exp(z+z) - exp(-z+-z))/[*2,0*] by SIN_COS:24
  .= (exp([*2,0*]*z) - exp(-z+-z))/[*2,0*] by Lm13
  .= (exp([*2,0*]*z) - exp([*2,0*]*-z))/[*2,0*] by Lm13
  .= (exp([*2,0*]*z) - exp(-[*2,0*]*z))/[*2,0*] by XCMPLX_1:175;
  hence thesis by Lm3;
 end;
   cosh_C/.([*2,0*]*z) = [*2,0*]*(cosh_C/.z)*(cosh_C/.z) - [*1,0*]
 proof
    [*2,0*]*(cosh_C/.z)*(cosh_C/.z) - [*1,0*]
   = [*2,0*]*((cosh_C/.z)*(cosh_C/.z)) - [*1,0*] by XCMPLX_1:4
  .= [*2,0*]*((cosh_C/.([*2,0*]*z) + [*1,0*])/[*2,0*]) - [*1,0*] by Th58
  .= ([*2,0*]*(cosh_C/.([*2,0*]*z) + [*1,0*])/[*2,0*]) - [*1,0*]
     by XCMPLX_1:75
  .= cosh_C/.([*2,0*]*z) + [*1,0*] - [*1,0*] by A1,XCMPLX_1:90;
  hence thesis by XCMPLX_1:26;
 end;
 hence thesis by A2;
end;

theorem Th60:
 (sinh_C/.z1)*(sinh_C/.z1) - (sinh_C/.z2)*(sinh_C/.z2)
=(sinh_C/.(z1+z2))*(sinh_C/.(z1-z2))
&
 (cosh_C/.z1)*(cosh_C/.z1) - (cosh_C/.z2)*(cosh_C/.z2)
=(sinh_C/.(z1+z2))*(sinh_C/.(z1-z2))
&
 (sinh_C/.z1)*(sinh_C/.z1) - (sinh_C/.z2)*(sinh_C/.z2)
=(cosh_C/.z1)*(cosh_C/.z1) - (cosh_C/.z2)*(cosh_C/.z2)
proof
 set s1 = sinh_C/.z1, s2 = sinh_C/.z2, c1 = cosh_C/.z1, c2 = cosh_C/.z2;
A1:(sinh_C/.(z1+z2))*(sinh_C/.(z1-z2))=(s1*s1)*(c2*c2)-(s2*s2)*(c1*c1)
 proof
   (sinh_C/.(z1+z2))*(sinh_C/.(z1-z2))
  =(s1*c2+c1*s2)*(sinh_C/.(z1-z2)) by Th11
 .=(s1*c2+c1*s2)*(s1*c2-c1*s2) by Th12
 .=(s1*c2+c1*s2)*(s1*c2)-(s1*c2+c1*s2)*(c1*s2) by XCMPLX_1:40
 .=s1*c2*(s1*c2)+c1*s2*(s1*c2)-(s1*c2+c1*s2)*(c1*s2) by XCMPLX_1:8
 .=s1*c2*(s1*c2)+c1*s2*(s1*c2)-(s1*c2*(c1*s2)+c1*s2*(c1*s2)) by XCMPLX_1:8
 .=s1*c2*(s1*c2)+c1*s2*(s1*c2)-s1*c2*(c1*s2)-c1*s2*(c1*s2) by XCMPLX_1:36
 .=s1*c2*(s1*c2)-c1*s2*(c1*s2) by XCMPLX_1:26
 .=c2*s1*s1*c2-c1*s2*(c1*s2) by XCMPLX_1:4
 .=(s1*s1)*c2*c2-c1*s2*(c1*s2) by XCMPLX_1:4
 .=(s1*s1)*(c2*c2)-c1*s2*(c1*s2) by XCMPLX_1:4
 .=(s1*s1)*(c2*c2)-s2*c1*c1*s2 by XCMPLX_1:4
 .=(s1*s1)*(c2*c2)-s2*(c1*c1)*s2 by XCMPLX_1:4;
  hence thesis by XCMPLX_1:4;
 end;
A2:(sinh_C/.z1)*(sinh_C/.z1) - (sinh_C/.z2)*(sinh_C/.z2)
 =(sinh_C/.(z1+z2))*(sinh_C/.(z1-z2))
 proof
   (sinh_C/.(z1+z2))*(sinh_C/.(z1-z2))
  =(s1*s1)*(c2*c2)-(s1*s1)*(s2*s2)+(s1*s1)*(s2*s2)-(s2*s2)*(c1*c1)
    by A1,XCMPLX_1:27
  .=(s1*s1)*((c2*c2)-(s2*s2))+(s1*s1)*(s2*s2)-(s2*s2)*(c1*c1) by XCMPLX_1:40
  .=(s1*s1)*1r+(s1*s1)*(s2*s2)-(s2*s2)*(c1*c1) by Th8
  .=(s1*s1)*1r+((s1*s1)*(s2*s2)-(s2*s2)*(c1*c1)) by XCMPLX_1:29
  .=(s1*s1)*1r+(s2*s2)*((s1*s1)-(c1*c1)) by XCMPLX_1:40
  .=(s1*s1)*1r+(s2*s2)*-((c1*c1)-(s1*s1)) by XCMPLX_1:143
  .=(s1*s1)*1r+(s2*s2)*-1r by Th8
  .=(s1*s1)*1r+-(s2*s2) by COMPLEX1:46
  .=(s1*s1)*1r-(s2*s2) by XCMPLX_0:def 8;
  hence thesis by COMPLEX1:29;
 end;
 (cosh_C/.z1)*(cosh_C/.z1) - (cosh_C/.z2)*(cosh_C/.z2)
 =(sinh_C/.(z1+z2))*(sinh_C/.(z1-z2))
 proof
    (sinh_C/.(z1+z2))*(sinh_C/.(z1-z2))
  = (s1*s1)*(c2*c2)-(c1*c1)*(c2*c2)+(c1*c1)*(c2*c2)-(s2*s2)*(c1*c1)
     by A1,XCMPLX_1:27
  .= ((s1*s1)-(c1*c1))*(c2*c2)+(c1*c1)*(c2*c2)-(s2*s2)*(c1*c1) by XCMPLX_1:40
  .= (-((c1*c1)-(s1*s1)))*(c2*c2)+(c1*c1)*(c2*c2)-(s2*s2)*(c1*c1)
      by XCMPLX_1:143
  .= (-1r)*(c2*c2)+(c1*c1)*(c2*c2)-(s2*s2)*(c1*c1) by Th8
  .= (-1r)*(c2*c2)+((c1*c1)*(c2*c2)-(s2*s2)*(c1*c1)) by XCMPLX_1:29
  .= (-1r)*(c2*c2)+(c1*c1)*((c2*c2)-(s2*s2)) by XCMPLX_1:40
  .= (-1r)*(c2*c2)+(c1*c1)*1r by Th8
  .= (-1r)*(c2*c2)+c1*c1 by COMPLEX1:29
  .= -(c2*c2)+c1*c1 by COMPLEX1:46;
  hence thesis by XCMPLX_0:def 8;
 end;
 hence thesis by A2;
end;

theorem Th61:
 (cosh_C/.(z1+z2))*(cosh_C/.(z1-z2))
=(sinh_C/.z1)*(sinh_C/.z1) + (cosh_C/.z2)*(cosh_C/.z2)
&
 (cosh_C/.(z1+z2))*(cosh_C/.(z1-z2))
=(cosh_C/.z1)*(cosh_C/.z1) + (sinh_C/.z2)*(sinh_C/.z2)
&
 (sinh_C/.z1)*(sinh_C/.z1) + (cosh_C/.z2)*(cosh_C/.z2)
=(cosh_C/.z1)*(cosh_C/.z1) + (sinh_C/.z2)*(sinh_C/.z2)
proof
 set s1 = sinh_C/.z1, s2 = sinh_C/.z2, c1 = cosh_C/.z1, c2 = cosh_C/.z2;
A1:(cosh_C/.(z1+z2))*(cosh_C/.(z1-z2))
  = (c1*c2+s1*s2)*(cosh_C/.(z1-z2)) by Th14
 .= (c1*c2+s1*s2)*(c1*c2-s1*s2) by Th13
 .= (c1*c2+s1*s2)*(c1*c2)-(c1*c2+s1*s2)*(s1*s2) by XCMPLX_1:40
 .= c1*c2*(c1*c2)+s1*s2*(c1*c2)-(c1*c2+s1*s2)*(s1*s2) by XCMPLX_1:8
 .= c1*c2*(c1*c2)+(c1*c2)*(s1*s2)-(c1*c2*(s1*s2)+s1*s2*(s1*s2)) by XCMPLX_1:8
 .= c1*c2*(c1*c2)+(c1*c2)*(s1*s2)-c1*c2*(s1*s2)-s1*s2*(s1*s2) by XCMPLX_1:36
 .= c1*c2*(c1*c2)-s1*s2*(s1*s2) by XCMPLX_1:26
 .= c2*c1*c1*c2-s1*s2*(s1*s2) by XCMPLX_1:4
 .= c2*(c1*c1)*c2-s1*s2*(s1*s2) by XCMPLX_1:4
 .= c2*(c1*c1)*c2-s2*s1*s1*s2 by XCMPLX_1:4
 .= c1*c1*c2*c2-(s1*s1)*s2*s2 by XCMPLX_1:4;
A2:(cosh_C/.(z1+z2))*(cosh_C/.(z1-z2))
   =(sinh_C/.z1)*(sinh_C/.z1) + (cosh_C/.z2)*(cosh_C/.z2)
 proof
    (cosh_C/.(z1+z2))*(cosh_C/.(z1-z2))
  = c1*c1*c2*c2 - s1*s1*c2*c2 + s1*s1*c2*c2 -s1*s1*s2*s2 by A1,XCMPLX_1:27
  .= c1*c1*(c2*c2) - s1*s1*c2*c2 + s1*s1*c2*c2 -s1*s1*s2*s2 by XCMPLX_1:4
  .= c1*c1*(c2*c2) - s1*s1*(c2*c2) + s1*s1*c2*c2 -s1*s1*s2*s2 by XCMPLX_1:4
  .= c1*c1*(c2*c2) - s1*s1*(c2*c2) + (s1*s1*c2*c2 -s1*s1*s2*s2) by XCMPLX_1:29
  .= (c1*c1 - s1*s1)*(c2*c2) + (s1*s1*c2*c2 -s1*s1*s2*s2) by XCMPLX_1:40
  .= (c1*c1 - s1*s1)*(c2*c2) + (s1*s1*(c2*c2) -s1*s1*s2*s2) by XCMPLX_1:4
  .= (c1*c1 - s1*s1)*(c2*c2) + (s1*s1*(c2*c2) -s1*s1*(s2*s2)) by XCMPLX_1:4
  .= (c1*c1 - s1*s1)*(c2*c2) + s1*s1*(c2*c2-s2*s2) by XCMPLX_1:40
  .= 1r*(c2*c2) + s1*s1*(c2*c2-s2*s2) by Th8
  .= 1r*(c2*c2) + s1*s1*1r by Th8
  .= (c2*c2) + s1*s1*1r by COMPLEX1:29;
  hence thesis by COMPLEX1:29;
 end;
 (cosh_C/.(z1+z2))*(cosh_C/.(z1-z2))
  =(cosh_C/.z1)*(cosh_C/.z1) + (sinh_C/.z2)*(sinh_C/.z2)
 proof
    (cosh_C/.(z1+z2))*(cosh_C/.(z1-z2))
  = c1*c1*c2*c2 - c1*c1*s2*s2 + c1*c1*s2*s2 -s1*s1*s2*s2 by A1,XCMPLX_1:27
  .= c1*c1*(c2*c2) - c1*c1*s2*s2 + c1*c1*s2*s2 -s1*s1*s2*s2 by XCMPLX_1:4
  .= c1*c1*(c2*c2) - c1*c1*(s2*s2) + c1*c1*s2*s2 -s1*s1*s2*s2 by XCMPLX_1:4
  .= c1*c1*(c2*c2) - c1*c1*(s2*s2) + c1*c1*(s2*s2) -s1*s1*s2*s2 by XCMPLX_1:4
  .= c1*c1*(c2*c2) - c1*c1*(s2*s2) +c1*c1*(s2*s2)-s1*s1*(s2*s2) by XCMPLX_1:4
  .= c1*c1*(c2*c2) - c1*c1*(s2*s2)+(c1*c1*(s2*s2)-s1*s1*(s2*s2)) by XCMPLX_1:29
  .= c1*c1*(c2*c2 - s2*s2)+(c1*c1*(s2*s2)-s1*s1*(s2*s2)) by XCMPLX_1:40
  .= c1*c1*(c2*c2 - s2*s2)+(c1*c1-s1*s1)*(s2*s2) by XCMPLX_1:40
  .= c1*c1*1r+(c1*c1-s1*s1)*(s2*s2) by Th8
  .= c1*c1*1r+1r*(s2*s2) by Th8
  .= c1*c1+1r*(s2*s2) by COMPLEX1:29;
  hence thesis by COMPLEX1:29;
 end;
 hence thesis by A2;
end;

theorem
    sinh_C/.([*2,0*]*z1) + sinh_C/.([*2,0*]*z2)
= [*2,0*]*sinh_C/.(z1+z2)*cosh_C/.(z1-z2)
&
  sinh_C/.([*2,0*]*z1) - sinh_C/.([*2,0*]*z2)
= [*2,0*]*sinh_C/.(z1-z2)*cosh_C/.(z1+z2)
proof
 set c1 = cosh_C/.z1, c2 = cosh_C/.z2, s1=sinh_C/.z1, s2=sinh_C/.z2;
A1:[*2,0*]*sinh_C/.(z1+z2)*cosh_C/.(z1-z2)
  = [*2,0*]*(s1*c2+c1*s2)*cosh_C/.(z1-z2) by Th11
 .= [*2,0*]*(s1*c2+c1*s2)*(c1*c2-s1*s2) by Th13
 .= [*2,0*]*((s1*c2+c1*s2)*(c1*c2-s1*s2)) by XCMPLX_1:4
 .= [*2,0*]*((s1*c2+c1*s2)*(c1*c2)-(s1*c2+c1*s2)*(s1*s2)) by XCMPLX_1:40
 .= [*2,0*]*(s1*c2*(c1*c2)+c1*s2*(c1*c2)-(s1*c2+c1*s2)*(s1*s2)) by XCMPLX_1:8
 .= [*2,0*]*(c1*s2*(c1*c2)+s1*c2*(c1*c2)-(s1*c2*(s1*s2)+c1*s2*(s1*s2)))
    by XCMPLX_1:8
 .= [*2,0*]*(c1*s2*(c1*c2)+s1*c2*(c1*c2)-c1*s2*(s1*s2)-s1*c2*(s1*s2))
    by XCMPLX_1:36
 .= [*2,0*]*((s1*c2*(c1*c2)-c1*s2*(s1*s2))+c1*s2*(c1*c2)-s1*c2*(s1*s2))
    by XCMPLX_1:29
 .= [*2,0*]*(s1*c2*(c1*c2)-c1*s2*(s1*s2)+(c1*s2*(c1*c2)-s1*c2*(s1*s2)))
    by XCMPLX_1:29
 .= [*2,0*]*(s1*c2*c2*c1-c1*s2*(s1*s2)+(c1*s2*(c1*c2)-s1*c2*(s1*s2)))
    by XCMPLX_1:4
 .= [*2,0*]*(c2*c2*s1*c1-c1*s2*(s1*s2)+(c1*s2*(c1*c2)-s1*c2*(s1*s2)))
    by XCMPLX_1:4
 .= [*2,0*]*(c2*c2*s1*c1-c1*s2*s2*s1+(c1*s2*(c1*c2)-s1*c2*(s1*s2)))
    by XCMPLX_1:4
 .= [*2,0*]*(c2*c2*s1*c1-s2*s2*c1*s1+(c1*s2*(c1*c2)-s1*c2*(s1*s2)))
    by XCMPLX_1:4
 .= [*2,0*]*(c2*c2*s1*c1-s2*s2*c1*s1+(s2*c1*c1*c2-s1*c2*(s1*s2)))
    by XCMPLX_1:4
 .= [*2,0*]*(c2*c2*s1*c1-s2*s2*c1*s1+(c1*c1*s2*c2-s1*c2*(s1*s2)))
    by XCMPLX_1:4
 .= [*2,0*]*(c2*c2*s1*c1-s2*s2*c1*s1+(c1*c1*s2*c2-c2*s1*s1*s2))
    by XCMPLX_1:4
 .= [*2,0*]*(c2*c2*s1*c1-s2*s2*c1*s1+(c1*c1*s2*c2-s1*s1*c2*s2))
    by XCMPLX_1:4
 .= [*2,0*]*(c2*c2*(s1*c1)-s2*s2*c1*s1+(c1*c1*s2*c2-s1*s1*c2*s2))
    by XCMPLX_1:4
 .= [*2,0*]*(c2*c2*(s1*c1)-s2*s2*(c1*s1)+(c1*c1*s2*c2-s1*s1*c2*s2))
    by XCMPLX_1:4
 .= [*2,0*]*(c2*c2*(s1*c1)-s2*s2*(c1*s1)+(c1*c1*(s2*c2)-s1*s1*c2*s2))
    by XCMPLX_1:4
 .= [*2,0*]*(c2*c2*(s1*c1)-s2*s2*(c1*s1)+(c1*c1*(s2*c2)-s1*s1*(c2*s2)))
    by XCMPLX_1:4
 .= [*2,0*]*((c2*c2-s2*s2)*(c1*s1)+(c1*c1*(s2*c2)-s1*s1*(c2*s2)))
    by XCMPLX_1:40
 .= [*2,0*]*((c2*c2-s2*s2)*(c1*s1)+(c1*c1-s1*s1)*(c2*s2))
    by XCMPLX_1:40
 .= [*2,0*]*(1r*(c1*s1)+(c1*c1-s1*s1)*(c2*s2)) by Th8
 .= [*2,0*]*(1r*(c1*s1)+1r*(c2*s2)) by Th8
 .= [*2,0*]*(c1*s1+1r*(c2*s2)) by COMPLEX1:29
 .= [*2,0*]*(c1*s1+(c2*s2)) by COMPLEX1:29
 .= [*2,0*]*(c1*s1)+[*2,0*]*(c2*s2) by XCMPLX_1:8
 .= [*2,0*]*s1*c1+[*2,0*]*(c2*s2) by XCMPLX_1:4
 .= [*2,0*]*s1*c1+[*2,0*]*s2*c2 by XCMPLX_1:4
 .= sinh_C/.([*2,0*]*z1) + [*2,0*]*s2*c2 by Th59
 .= sinh_C/.([*2,0*]*z1) + sinh_C/.([*2,0*]*z2) by Th59;
   sinh_C/.([*2,0*]*z1) - sinh_C/.([*2,0*]*z2)
 =[*2,0*]*sinh_C/.(z1-z2)*cosh_C/.(z1+z2)
 proof
       [*2,0*]*sinh_C/.(z1-z2)*cosh_C/.(z1+z2)
   = [*2,0*]*(s1*c2-c1*s2)*cosh_C/.(z1+z2) by Th12
  .= [*2,0*]*(s1*c2-c1*s2)*(c1*c2+s1*s2) by Th14
  .= [*2,0*]*((s1*c2-c1*s2)*(c1*c2+s1*s2)) by XCMPLX_1:4
  .= [*2,0*]*((s1*c2-c1*s2)*(c1*c2)+(s1*c2-c1*s2)*(s1*s2)) by XCMPLX_1:8
  .= [*2,0*]*(s1*c2*(c1*c2)-c1*s2*(c1*c2)+(s1*c2-c1*s2)*(s1*s2)) by XCMPLX_1:40
  .= [*2,0*]*(s1*c2*(c1*c2)-c1*s2*(c1*c2) + (s1*c2*(s1*s2)-c1*s2*(s1*s2)) )
     by XCMPLX_1:40
  .= [*2,0*]*(s1*c2*(c1*c2)-c1*s2*(c1*c2) + s1*c2*(s1*s2)-c1*s2*(s1*s2) )
     by XCMPLX_1:29
  .= [*2,0*]*(s1*c2*(c1*c2)+ -c1*s2*(c1*c2) + s1*c2*(s1*s2)-c1*s2*(s1*s2) )
     by XCMPLX_0:def 8
  .= [*2,0*]*(s1*c2*(c1*c2)+(s1*c2*(s1*s2)+ -c1*s2*(c1*c2)) -c1*s2*(s1*s2) )
     by XCMPLX_1:1
  .= [*2,0*]*(s1*c2*(s1*s2)-c1*s2*(c1*c2) + s1*c2*(c1*c2) -c1*s2*(s1*s2) )
     by XCMPLX_0:def 8
  .= [*2,0*]*(-(c1*s2*(c1*c2)-s1*c2*(s1*s2)) + s1*c2*(c1*c2) -c1*s2*(s1*s2) )
     by XCMPLX_1:143
  .= [*2,0*]*(-(c1*s2*(c1*c2)-s1*c2*(s1*s2)) +( s1*c2*(c1*c2) -c1*s2*(s1*s2)) )
     by XCMPLX_1:29
  .= [*2,0*]*(s1*c2*(c1*c2) -c1*s2*(s1*s2)-(c1*s2*(c1*c2)-s1*c2*(s1*s2)) )
     by XCMPLX_0:def 8
  .= [*2,0*]*(c2*s1*c1*c2 -c1*s2*(s1*s2)-(c1*s2*(c1*c2)-s1*c2*(s1*s2)) )
     by XCMPLX_1:4
  .= [*2,0*]*(s1*c1*c2*c2 -c1*s2*(s1*s2)-(c1*s2*(c1*c2)-s1*c2*(s1*s2)) )
     by XCMPLX_1:4
  .= [*2,0*]*(s1*c1*c2*c2 -s2*c1*s1*s2-(c1*s2*(c1*c2)-s1*c2*(s1*s2)) )
     by XCMPLX_1:4
  .= [*2,0*]*(s1*c1*c2*c2 -c1*s1*s2*s2-(c1*s2*(c1*c2)-s1*c2*(s1*s2)) )
     by XCMPLX_1:4
  .= [*2,0*]*(s1*c1*c2*c2 -c1*s1*s2*s2-(c1*s2*c2*c1-s1*c2*(s1*s2)) )
     by XCMPLX_1:4
  .= [*2,0*]*(s1*c1*c2*c2 -s1*c1*s2*s2-(s2*c2*c1*c1-s1*c2*(s1*s2)) )
     by XCMPLX_1:4
  .= [*2,0*]*(s1*c1*c2*c2 -s1*c1*s2*s2-(s2*c2*c1*c1-s1*c2*s2*s1) )
     by XCMPLX_1:4
  .= [*2,0*]*(s1*c1*c2*c2 -s1*c1*s2*s2-(s2*c2*c1*c1-s2*c2*s1*s1) )
     by XCMPLX_1:4
  .= [*2,0*]*(s1*c1*(c2*c2) -s1*c1*s2*s2-(s2*c2*c1*c1-s2*c2*s1*s1) )
     by XCMPLX_1:4
  .= [*2,0*]*(s1*c1*(c2*c2) -s1*c1*s2*s2-(s2*c2*c1*c1-s2*c2*(s1*s1)) )
     by XCMPLX_1:4
  .= [*2,0*]*(s1*c1*(c2*c2) -s1*c1*s2*s2-(s2*c2*(c1*c1)-s2*c2*(s1*s1)) )
     by XCMPLX_1:4
  .= [*2,0*]*(s1*c1*(c2*c2) -s1*c1*(s2*s2)-(s2*c2*(c1*c1)-s2*c2*(s1*s1)) )
     by XCMPLX_1:4
  .= [*2,0*]*(s1*c1*(c2*c2-s2*s2)-(s2*c2*(c1*c1)-s2*c2*(s1*s1)) )
     by XCMPLX_1:40
  .= [*2,0*]*(s1*c1*(c2*c2-s2*s2)-(s2*c2*(c1*c1-s1*s1))) by XCMPLX_1:40
  .= [*2,0*]*(s1*c1*1r-(s2*c2*(c1*c1-s1*s1))) by Th8
  .= [*2,0*]*(s1*c1*1r-(s2*c2*1r)) by Th8
  .= [*2,0*]*(s1*c1-(s2*c2*1r)) by COMPLEX1:29
  .= [*2,0*]*(s1*c1-(s2*c2)) by COMPLEX1:29
  .= [*2,0*]*(s1*c1)-[*2,0*]*(s2*c2) by XCMPLX_1:40
  .= [*2,0*]*s1*c1-[*2,0*]*(s2*c2) by XCMPLX_1:4
  .= [*2,0*]*s1*c1-[*2,0*]*s2*c2 by XCMPLX_1:4
  .= sinh_C/.([*2,0*]*z1)-[*2,0*]*s2*c2 by Th59;
  hence thesis by Th59;
 end;
 hence thesis by A1;
end;

Lm14:
for z1 holds
(sinh_C/.z1)*(sinh_C/.z1) = (cosh_C/.z1)*(cosh_C/.z1) - [*1,0*]
proof
 let z1;
   (cosh_C/.z1)*(cosh_C/.z1) - [*1,0*] = (cosh_C/.z1)*(cosh_C/.z1)
   - ((cosh_C/.z1)*(cosh_C/.z1) - (sinh_C/.z1)*(sinh_C/.z1))
     by Th8,L1
 .=(cosh_C/.z1)*(cosh_C/.z1)
   - (cosh_C/.z1)*(cosh_C/.z1) + (sinh_C/.z1)*(sinh_C/.z1) by XCMPLX_1:37
 .= (sinh_C/.z1)*(sinh_C/.z1)+
  (cosh_C/.z1)*(cosh_C/.z1) - (cosh_C/.z1)*(cosh_C/.z1) by XCMPLX_1:29;
 hence thesis by XCMPLX_1:26;
end;

theorem
   cosh_C/.([*2,0*]*z1) + cosh_C/.([*2,0*]*z2)
=[*2,0*]*cosh_C/.(z1+z2)*cosh_C/.(z1-z2)
 &
 cosh_C/.([*2,0*]*z1) - cosh_C/.([*2,0*]*z2)
=[*2,0*]*sinh_C/.(z1+z2)*sinh_C/.(z1-z2)
proof
A1:[*2,0*]*cosh_C/.(z1+z2)*cosh_C/.(z1-z2)
  =[*2,0*]*(cosh_C/.(z1+z2)*cosh_C/.(z1-z2 )) by XCMPLX_1:4
 .=[*2,0*]*((sinh_C/.z1)*(sinh_C/.z1) + (cosh_C/.z2)*(cosh_C/.z2)) by Th61
 .=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1) - [*1,0*] + (cosh_C/.z2)*(cosh_C/.z2))
   by Lm14
 .=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1) - [*1,0*])
  +[*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) by XCMPLX_1:8
 .=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) - [*2,0*]*[*1,0*]
  +[*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) by XCMPLX_1:40
 .=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) - ([*1,0*]+[*1,0*])
  +[*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) by Lm13
 .=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) +- ([*1,0*]+[*1,0*])
  +[*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) by XCMPLX_0:def 8
 .=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) +(- [*1,0*]+-[*1,0*])
  +[*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) by XCMPLX_1:140
 .=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) +- [*1,0*]+-[*1,0*]
  +[*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) by XCMPLX_1:1
 .=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) +- [*1,0*]+(-[*1,0*]
  +[*2,0*]*((cosh_C/.z2)*(cosh_C/.z2))) by XCMPLX_1:1
 .=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) +- [*1,0*]+
  ([*2,0*]*((cosh_C/.z2)*(cosh_C/.z2))-[*1,0*]) by XCMPLX_0:def 8
 .=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) - [*1,0*]+
  ([*2,0*]*((cosh_C/.z2)*(cosh_C/.z2))-[*1,0*]) by XCMPLX_0:def 8
  .=[*2,0*]*(cosh_C/.z1)*(cosh_C/.z1) - [*1,0*]+
  ([*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) - [*1,0*]) by XCMPLX_1:4
 .=[*2,0*]*(cosh_C/.z1)*(cosh_C/.z1) - [*1,0*]+
  ([*2,0*]*(cosh_C/.z2)*(cosh_C/.z2) - [*1,0*]) by XCMPLX_1:4
 .=cosh_C/.([*2,0*]*z1)+
  ([*2,0*]*(cosh_C/.z2)*(cosh_C/.z2) - [*1,0*]) by Th59
 .=cosh_C/.([*2,0*]*z1)+cosh_C/.([*2,0*]*z2) by Th59;
   cosh_C/.([*2,0*]*z1)-cosh_C/.([*2,0*]*z2)
 =[*2,0*]*sinh_C/.(z1+z2)*sinh_C/.(z1-z2)
 proof
       [*2,0*]*sinh_C/.(z1+z2)*sinh_C/.(z1-z2)
   = [*2,0*]*(sinh_C/.(z1+z2)*sinh_C/.(z1-z2)) by XCMPLX_1:4
  .= [*2,0*]*((cosh_C/.z1)*(cosh_C/.z1) - (cosh_C/.z2)*(cosh_C/.z2)) by Th60
  .= [*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) - [*2,0*]*((cosh_C/.z2)*(cosh_C/.z2))
     by XCMPLX_1:40
  .= [*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) -[*1,0*]
    +[*1,0*]- [*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) by XCMPLX_1:27
  .= [*2,0*]*(cosh_C/.z1)*(cosh_C/.z1) -[*1,0*]
    +[*1,0*]- [*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) by XCMPLX_1:4
  .= cosh_C/.([*2,0*]*z1)+[*1,0*]- [*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) by Th59
  .= cosh_C/.([*2,0*]*z1)+([*1,0*]- [*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)))
     by XCMPLX_1:29
  .= cosh_C/.([*2,0*]*z1)+-([*2,0*]*((cosh_C/.z2)*(cosh_C/.z2))-[*1,0*])
     by XCMPLX_1:143
  .= cosh_C/.([*2,0*]*z1)+-([*2,0*]*(cosh_C/.z2)*(cosh_C/.z2)-[*1,0*])
     by XCMPLX_1:4
  .= cosh_C/.([*2,0*]*z1)-([*2,0*]*(cosh_C/.z2)*(cosh_C/.z2)-[*1,0*])
     by XCMPLX_0:def 8;
  hence thesis by Th59;
 end;
 hence thesis by A1;
end;