:: The Sum and Product of Finite Sequences of Real Numbers
::  by Czes{\l}aw Byli\'nski
::
:: Received May 11, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, NAT_1, FINSEQ_1, VALUED_0, FINSEQ_2, CARD_1, RELAT_1,
      SUBSET_1, XBOOLE_0, FUNCT_1, TARSKI, XREAL_0, ORDINAL4, BINOP_1, BINOP_2,
      ARYTM_1, ARYTM_3, SQUARE_1, FUNCOP_1, REAL_1, FINSEQOP, ZFMISC_1,
      VALUED_1, XXREAL_0, CARD_3, XCMPLX_0, SETWISEO, SETWOP_2, FINSOP_1,
      RVSUM_1, FUNCT_7, ORDINAL1;
 notations TARSKI, SUBSET_1, ZFMISC_1, ORDINAL1, CARD_1, NUMBERS, VALUED_0,
      XBOOLE_0, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, SQUARE_1, RELAT_1,
      FUNCT_1, PARTFUN1, BINOP_2, SETWISEO, FUNCT_2, BINOP_1, FUNCOP_1,
      FINSEQ_1, FINSEQ_2, FINSEQ_4, VALUED_1, NAT_1, FINSOP_1, FINSEQOP,
      SETWOP_2;
 constructors PARTFUN1, BINOP_1, SETWISEO, SQUARE_1, NAT_1, BINOP_2, VALUED_1,
      FINSEQOP, FINSEQ_4, FINSOP_1, SETWOP_2, RELSET_1, XXREAL_1, REAL_1,
      FINSEQ_2;
 registrations XBOOLE_0, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1, NUMBERS,
      XCMPLX_0, XREAL_0, SQUARE_1, NAT_1, BINOP_2, FINSEQ_1, FINSEQ_2,
      VALUED_0, VALUED_1, RELAT_1, FINSEQ_4, CARD_1, INT_1;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;


begin :: Auxiliary theorems

registration
  let n be natural Number;
  cluster n-element natural-valued for FinSequence;
end;

registration
  cluster real-valued for FinSequence;
end;

definition
  let F be real-valued Relation;
  redefine func rng F -> Subset of REAL;
end;

registration
  let D be non empty set;
  let F be Function of REAL,D;
  let F1 be real-valued FinSequence;
  cluster F*F1 -> FinSequence-like;
end;

registration
  let r be Real;
  cluster <*r*> -> real-valued;
end;

registration
  let r1, r2 be Real;
  cluster <*r1, r2*> -> real-valued;
end;

registration
  let r1, r2, r3 be Real;
  cluster <*r1, r2, r3*> -> real-valued;
end;

registration
  let r1, r2, r3, r4 be Real;
  cluster <*r1, r2, r3, r4*> -> real-valued;
end;

registration
  let j be natural Number, r be Real;
  cluster j |-> r -> real-valued;
end;

registration
  let f, g be real-valued FinSequence;
  cluster f ^ g -> real-valued;
end;

reserve s for set,
  i,j for natural Number,
  k for Nat,
  x,x1,x2,x3 for Real,
  r,r1,r2,r3,r4 for Real,
  F,F1,F2,F3 for real-valued FinSequence,
  R,R1,R2 for Element of i-tuples_on REAL;

theorem :: RVSUM_1:1
  0 is_a_unity_wrt addreal;

definition
  redefine func diffreal equals
:: RVSUM_1:def 1
  addreal*(id REAL,compreal);
end;

definition
  func sqrreal -> UnOp of REAL means
:: RVSUM_1:def 2

  for r holds it.r = r^2;
end;

theorem :: RVSUM_1:2
  1 is_a_unity_wrt multreal;

theorem :: RVSUM_1:3
  multreal is_distributive_wrt addreal;

theorem :: RVSUM_1:4
  sqrreal is_distributive_wrt multreal;

definition
  let x be Real;
  func x multreal -> UnOp of REAL equals
:: RVSUM_1:def 3
  multreal[;](x,id REAL);
end;

theorem :: RVSUM_1:5
  (r multreal).r1 = r*r1;

theorem :: RVSUM_1:6
  r multreal is_distributive_wrt addreal;

theorem :: RVSUM_1:7
  compreal is_an_inverseOp_wrt addreal;

theorem :: RVSUM_1:8
  addreal is having_an_inverseOp;

theorem :: RVSUM_1:9
  the_inverseOp_wrt addreal = compreal;

theorem :: RVSUM_1:10
  compreal is_distributive_wrt addreal;

definition
  let F1,F2;
  redefine func F1 + F2 -> FinSequence of REAL equals
:: RVSUM_1:def 4
  addreal.:(F1,F2);
  commutativity;
end;

definition
  let i,R1,R2;
  redefine func R1 + R2 -> Element of i-tuples_on REAL;
end;

theorem :: RVSUM_1:11
  (R1+R2).s = R1.s + R2.s;

theorem :: RVSUM_1:12
  <*>REAL + F = <*>REAL;

theorem :: RVSUM_1:13
  <*r1*> + <*r2*> = <*r1+r2*>;

theorem :: RVSUM_1:14
  (i|->r1) + (i|->r2) = i|->(r1+r2);

theorem :: RVSUM_1:15
  F1 + (F2 + F3) = F1 + F2 + F3;

theorem :: RVSUM_1:16
  R + (i|->(0 qua Real)) = R;

theorem :: RVSUM_1:17
  (-F).s = -F.s;

definition
  let F;
  redefine func -F -> FinSequence of REAL equals
:: RVSUM_1:def 5
  compreal*F;
end;

definition
  let i,R;
  redefine func -R -> Element of i-tuples_on REAL;
end;

theorem :: RVSUM_1:18
  (-F).s = -(F.s);

theorem :: RVSUM_1:19
  -(<*>REAL) = <*>REAL;

theorem :: RVSUM_1:20
  -<*r*> = <*-r*>;

theorem :: RVSUM_1:21
  -(i|->r) = i|->-r;

theorem :: RVSUM_1:22
  R + -R = i|->0;

theorem :: RVSUM_1:23
  R1 + R2 = i|->0 implies R1 = -R2;

theorem :: RVSUM_1:24
  for R1, R2 being complex-valued Function st -R1 = -R2 holds R1 = R2;

theorem :: RVSUM_1:25
  R1 + R = R2 + R implies R1 = R2;

theorem :: RVSUM_1:26
  -(F1 + F2) = -F1 + -F2;

definition
  let F1,F2;
  redefine func F1 - F2 -> FinSequence of REAL equals
:: RVSUM_1:def 6
  diffreal.:(F1,F2);
end;

definition
  let i,R1,R2;
  redefine func R1 - R2 -> Element of i-tuples_on REAL;
end;

theorem :: RVSUM_1:27
  (R1-R2).s = R1.s - R2.s;

theorem :: RVSUM_1:28
  <*>REAL - F = <*>REAL & F - <*>REAL = <*>REAL;

theorem :: RVSUM_1:29
  <*r1*> - <*r2*> = <*r1-r2*>;

theorem :: RVSUM_1:30
  (i|->r1) - (i|->r2) = i|->(r1-r2);

theorem :: RVSUM_1:31
  F1 - F2 = F1 + - F2;

theorem :: RVSUM_1:32
  R - (i|->(0 qua Real)) = R;

theorem :: RVSUM_1:33
  (i|->(0 qua Real)) - R = -R;

theorem :: RVSUM_1:34
  F1 - -F2 = F1 + F2;

theorem :: RVSUM_1:35
  -(F1 - F2) = F2 - F1;

theorem :: RVSUM_1:36
  -(F1 - F2) = -F1 + F2;

theorem :: RVSUM_1:37
  R - R = i|->0;

theorem :: RVSUM_1:38
  R1 - R2 = i|->0 implies R1 = R2;

theorem :: RVSUM_1:39
  F1 - F2 - F3 = F1 - (F2 + F3);

theorem :: RVSUM_1:40
  F1 + (F2 - F3) = F1 + F2 - F3;

theorem :: RVSUM_1:41
  F1 - (F2 - F3) = F1 - F2 + F3;

theorem :: RVSUM_1:42
  R1 = R1 + R - R;

theorem :: RVSUM_1:43
  R1 = R1 - R + R;

notation
  let F; let r be Real;
  synonym r*F for r(#)F;
end;

theorem :: RVSUM_1:44
  (r*F).s = r*(F.s);

definition
  let F; let r be Real;
  redefine func r*F -> FinSequence of REAL equals
:: RVSUM_1:def 7
  (r multreal)*F;
end;

definition
  let i,R,r;
  redefine func r*R -> Element of i-tuples_on REAL;
end;

theorem :: RVSUM_1:45
  (r*F).s = r*(F.s);

theorem :: RVSUM_1:46
  r*(<*>REAL) = <*>REAL;

theorem :: RVSUM_1:47
  r*<*r1*> = <*r*r1*>;

theorem :: RVSUM_1:48
  r1*(i|->r2) = i|->(r1*r2);

theorem :: RVSUM_1:49
  (r1*r2)*F = r1*(r2*F);

theorem :: RVSUM_1:50
  (r1 + r2)*F = r1*F + r2*F;

theorem :: RVSUM_1:51
  r*(F1+F2) = r*F1 + r*F2;

theorem :: RVSUM_1:52
  1*F = F;

theorem :: RVSUM_1:53
  0*R = i|->0;

theorem :: RVSUM_1:54
  (-1)*F = -F;

notation
  let F;
  synonym sqr F for F^2;
end;

definition
  let F;
  redefine func sqr F -> FinSequence of REAL equals
:: RVSUM_1:def 8
  sqrreal*F;
end;

definition
  let i,R;
  redefine func sqr R -> Element of i-tuples_on REAL;
end;

theorem :: RVSUM_1:55
  sqr <*r*> = <*r^2*>;

theorem :: RVSUM_1:56
  sqr(i |-> r) = i |-> r^2;

theorem :: RVSUM_1:57
  sqr -F = sqr F;

theorem :: RVSUM_1:58
  sqr (r*F) = r^2 * sqr F;

notation
  let F1,F2;
  synonym mlt(F1,F2) for F1(#)F2;
end;

definition
  let F1,F2;
  redefine func mlt(F1,F2) -> FinSequence of REAL equals
:: RVSUM_1:def 9
  multreal.:(F1,F2);
  commutativity;
end;

theorem :: RVSUM_1:59
  mlt(F1,F2).s = F1.s * F2.s;

definition
  let i,R1,R2;
  redefine func mlt(R1,R2) -> Element of i-tuples_on REAL;
end;

theorem :: RVSUM_1:60 ::=VALUED_1:5
  mlt(F1,F2).s = F1.s * F2.s;

theorem :: RVSUM_1:61
  mlt(<*>REAL,F) = <*>REAL;

theorem :: RVSUM_1:62
  mlt(<*r1*>,<*r2*>) = <*r1*r2*>;

theorem :: RVSUM_1:63
  mlt(i|->r,R) = r*R;

theorem :: RVSUM_1:64
  mlt(i|->r1,i|->r2) = i|->(r1*r2);

theorem :: RVSUM_1:65
  r*mlt(F1,F2) = mlt(r*F1,F2);

theorem :: RVSUM_1:66 ::=Th92
  r*R = mlt(i|->r,R);

theorem :: RVSUM_1:67
  sqr(F) = mlt(F,F);

theorem :: RVSUM_1:68
  sqr(F1 + F2) = sqr F1 + 2*mlt(F1,F2) + sqr F2;

theorem :: RVSUM_1:69
  sqr(F1 - F2) = sqr F1 - 2*mlt(F1,F2) + sqr F2;

theorem :: RVSUM_1:70
  sqr mlt(F1,F2) = mlt(sqr F1,sqr F2);

:: Finite sum of Finite Sequence of Real Numbers

registration
  cluster -> complex-valued for FinSequence of COMPLEX;
  cluster real-valued complex-valued for FinSequence;
end;

definition
  let F be complex-valued FinSequence;

  func Sum F -> Complex means
:: RVSUM_1:def 10

  ex f being FinSequence of COMPLEX st f = F & it = addcomplex $$ f;
end;

registration
  let F be real-valued FinSequence;
  cluster Sum F -> real;
end;

theorem :: RVSUM_1:71
  for F being FinSequence of REAL holds Sum F = addreal $$ F;

definition
  let F be FinSequence of COMPLEX;
  redefine func Sum F -> Element of COMPLEX equals
:: RVSUM_1:def 11
  addcomplex $$ F;
end;

definition
  let F be FinSequence of REAL;
  redefine func Sum F -> Real equals
:: RVSUM_1:def 12
  addreal $$ F;
end;

theorem :: RVSUM_1:72
  Sum(<*> REAL) = 0;

theorem :: RVSUM_1:73
  Sum <*r*> = r;

theorem :: RVSUM_1:74
  Sum(F^<*r*>) = Sum F + r;

theorem :: RVSUM_1:75
  Sum(F1^F2) = Sum F1 + Sum F2;

theorem :: RVSUM_1:76
  Sum(<*r*>^F) = r + Sum F;

theorem :: RVSUM_1:77
  Sum<*r1,r2*> = r1 + r2;

theorem :: RVSUM_1:78
  Sum<*r1,r2,r3*> = r1 + r2 + r3;

theorem :: RVSUM_1:79
  for R being Element of 0-tuples_on REAL holds Sum R = 0;

theorem :: RVSUM_1:80
  Sum(i |-> r) = i*r;

theorem :: RVSUM_1:81
  Sum(i |-> (0 qua Real)) = 0;

theorem :: RVSUM_1:82
  for R1,R2 being i-element real-valued FinSequence holds
  (for j be Nat st j in Seg i holds R1.j <= R2.j) implies Sum R1 <= Sum R2;

theorem :: RVSUM_1:83
  for R1,R2 being i-element real-valued FinSequence holds
  (for j be Nat st j in Seg i holds R1.j <= R2.j) &
  (ex j be Nat st j in Seg i & R1.j < R2.j) implies Sum R1 < Sum R2;

theorem :: RVSUM_1:84
  (for i be Nat st i in dom F holds 0 <= F.i) implies 0 <= Sum F;

theorem :: RVSUM_1:85
  (for i be Nat st i in dom F holds 0 <= F.i) &
  (ex i be Nat st i in dom F & 0 < F.i) implies 0 < Sum F;

theorem :: RVSUM_1:86
  0 <= Sum sqr F;

theorem :: RVSUM_1:87
  Sum(r*F) = r*(Sum F);

theorem :: RVSUM_1:88
  Sum -F = -(Sum F);

theorem :: RVSUM_1:89
  Sum(R1 + R2) = Sum R1 + Sum R2;

theorem :: RVSUM_1:90
  Sum(R1 - R2) = Sum R1 - Sum R2;

theorem :: RVSUM_1:91
  Sum sqr R = 0 implies R = i |-> 0;

theorem :: RVSUM_1:92
  (Sum mlt(R1,R2))^2 <= (Sum sqr R1)*(Sum sqr R2);

:: The Product of Finite Sequences of Real Numbers

definition
  let F be complex-valued FinSequence;
  func Product F -> Complex means
:: RVSUM_1:def 13

  ex f being FinSequence of COMPLEX st f = F & it = multcomplex $$ f;
end;

registration
  let F be real-valued FinSequence;
  cluster Product F -> real;
end;

theorem :: RVSUM_1:93
  for F being FinSequence of REAL holds Product F = multreal $$ F;

definition
  let F be FinSequence of COMPLEX;
  redefine func Product F -> Element of COMPLEX equals
:: RVSUM_1:def 14
  multcomplex $$ F;
end;

definition
  let F be FinSequence of REAL;
  redefine func Product F -> Real equals
:: RVSUM_1:def 15
  multreal $$ F;
end;

theorem :: RVSUM_1:94
  Product <*>REAL = 1;

registration
  let r be Complex;
  cluster <*r*> -> complex-valued;
end;

registration
  let r1, r2 be Complex;
  cluster <*r1, r2*> -> complex-valued;
end;

registration
  let r1, r2, r3 be Complex;
  cluster <*r1, r2, r3*> -> complex-valued;
end;

registration
  let j be natural Number, c be Complex;
  cluster j |-> c -> complex-valued;
end;

theorem :: RVSUM_1:95
  for r being Complex holds Product <*r*> = r;

registration let c be Complex;
  reduce Product <*c*> to c;
end;

registration
  let f, g be complex-valued FinSequence;
  cluster f ^ g -> complex-valued;
end;

theorem :: RVSUM_1:96
  for F being complex-valued FinSequence, r being Complex holds
    Product (F^<*r*>) = Product F * r;

theorem :: RVSUM_1:97
  for F1, F2 being complex-valued FinSequence holds
  Product (F1^F2) = Product F1 * Product F2;

theorem :: RVSUM_1:98
  Product (<*r*>^F) = r * Product F;

theorem :: RVSUM_1:99
  for r1, r2 being Complex holds Product <*r1,r2*> = r1 * r2;

theorem :: RVSUM_1:100
  for r1, r2, r3 being Complex holds Product <*r1,r2,r3*> = r1 * r2 * r3;

theorem :: RVSUM_1:101
  for R being Element of 0-tuples_on REAL holds Product R = 1;

theorem :: RVSUM_1:102
  Product (i|->1) = 1;

theorem :: RVSUM_1:103
  for F being complex-valued FinSequence holds
  (ex k st k in dom F & F.k = 0) iff Product F = 0;

theorem :: RVSUM_1:104
  Product ((i+j) |->r ) = (Product (i|->r))*(Product (j|->r));

theorem :: RVSUM_1:105
  Product ((i*j) |->r) = Product (j |-> (Product (i|->r)));

theorem :: RVSUM_1:106
  Product (i|->(r1*r2)) = (Product (i|->r1))*(Product (i|->r2));

theorem :: RVSUM_1:107
  Product mlt(R1,R2) = Product R1 * Product R2;

theorem :: RVSUM_1:108
  Product (r*R) = Product (i|->r) * Product R;

theorem :: RVSUM_1:109
  Product sqr R = (Product R)^2;

begin :: Addenda
:: 2006.07.13, A.T.

reserve z,z1,z2 for Element of COMPLEX;

theorem :: RVSUM_1:110
  for F being FinSequence of COMPLEX holds Product F = multcomplex $$ F;

theorem :: RVSUM_1:111
  Product ((i+j) |->z) = (Product (i|->z))*(Product (j|->z));

theorem :: RVSUM_1:112
  Product ((i*j) |->z) = Product (j |-> (Product (i|->z)));

theorem :: RVSUM_1:113
  Product (i|->(z1*z2)) = (Product (i|->z1))*(Product (i|->z2));

begin :: from EUCLID_2 (partially modified), 2009.09.12, A.T.

reserve n for Nat,
  x, y, a for Real,
  p, p1, p2, p3, q, q1, q2 for Element of n-tuples_on REAL;

theorem :: RVSUM_1:114
  for x being real-valued FinSequence holds len (-x)=len x;

theorem :: RVSUM_1:115
  for x1,x2 being real-valued FinSequence st len x1=len x2 holds
  len (x1+x2)=len x1;

theorem :: RVSUM_1:116
  for x1,x2 being real-valued FinSequence st len x1=len x2 holds
  len (x1-x2)=len x1;

theorem :: RVSUM_1:117
  for a being Real, x being real-valued FinSequence
   holds len (a*x)=len x;

theorem :: RVSUM_1:118
  for x,y,z being real-valued FinSequence st len x=len y & len y=len z
  holds mlt(x+y,z) = mlt(x,z)+mlt(y,z);

begin :: Inner Product of Finite Sequences

definition
  let x1,x2 be real-valued FinSequence;
  func |( x1,x2 )| -> Real equals
:: RVSUM_1:def 16
  Sum mlt(x1,x2);
  commutativity;
end;

theorem :: RVSUM_1:119
  for x being real-valued FinSequence holds |(x,x)| >= 0;

theorem :: RVSUM_1:120
  for x,y,z being real-valued FinSequence st len x=len y & len y=len z
  holds |((x+y),z)| = |(x,z)| + |(y,z)|;

theorem :: RVSUM_1:121
  for x,y being real-valued FinSequence,a being Real st len x=
  len y holds |(a*x,y)| = a*|(x,y)|;

theorem :: RVSUM_1:122
  for x1,x2 being real-valued FinSequence st len x1=len x2 holds
  |(-x1, x2)| = -|(x1, x2)|;

theorem :: RVSUM_1:123
  for x1,x2 being real-valued FinSequence st len x1=len x2 holds
  |(-x1, -x2)| = |(x1, x2)|;

theorem :: RVSUM_1:124
  for x1,x2,x3 being real-valued FinSequence st len x1=len x2 & len x2
  =len x3 holds |(x1-x2, x3)| = |(x1, x3)| - |(x2, x3)|;

theorem :: RVSUM_1:125
  for x,y being Real,x1,x2,x3 being real-valued FinSequence st len x1
  =len x2 & len x2=len x3 holds |((x*x1+y*x2), x3)| = x*|(x1,x3)| + y*|(x2,x3)|
;

theorem :: RVSUM_1:126
  for x1,x2,y1,y2 being real-valued FinSequence st len x1=len x2 & len
x2=len y1 & len y1=len y2 holds |(x1+x2, y1+y2)| = |(x1, y1)| + |(x1, y2)| + |(
  x2, y1)| + |(x2, y2)|;

theorem :: RVSUM_1:127
  for x1,x2,y1,y2 being real-valued FinSequence st len x1=len x2 & len
x2=len y1 & len y1=len y2 holds |(x1-x2, y1-y2)| = |(x1, y1)| - |(x1, y2)| - |(
  x2, y1)| + |(x2, y2)|;

theorem :: RVSUM_1:128
  for x,y being real-valued FinSequence st len x=len y holds |(x+y, x+
  y)| = |(x, x)| + 2*|(x, y)| + |(y, y)|;

theorem :: RVSUM_1:129
  for x,y being real-valued FinSequence st len x=len y holds |(x-y, x-
  y)| = |(x, x)| - 2*|(x, y)| + |(y, y)|;

theorem :: RVSUM_1:130
  |(p1 + p2, p3)| = |(p1, p3)| + |(p2, p3)|;

theorem :: RVSUM_1:131
  for x being Real holds |(x*p1, p2)| = x*|(p1, p2)|;

theorem :: RVSUM_1:132
  |(-p1, p2)| = -|(p1, p2)|;

theorem :: RVSUM_1:133
  |(-p1, -p2)| = |(p1, p2)|;

theorem :: RVSUM_1:134
  |(p1-p2, p3)| = |(p1, p3)| - |(p2, p3)|;

theorem :: RVSUM_1:135
  |((x*p1+y*p2), p3)| = x*|(p1,p3)| + y*|(p2,p3)|;

theorem :: RVSUM_1:136
  |(p1+p2, q1+q2)| = |(p1, q1)| + |(p1, q2)| + |(p2, q1)| + |(p2, q2)|;

theorem :: RVSUM_1:137
  |(p1-p2, q1-q2)| = |(p1, q1)| - |(p1, q2)| - |(p2, q1)| + |(p2, q2)|;

theorem :: RVSUM_1:138
  |(p+q, p+q)| = |(p, p)| + 2*|(p, q)| + |(q, q)|;

theorem :: RVSUM_1:139
  |(p-q, p-q)| = |(p, p)| - 2*|(p, q)| + |(q, q)|;

theorem :: RVSUM_1:140
  |(p,q)| <= |(p,p)| + |(q,q)|;

definition
  let p, q be real-valued FinSequence;
  pred p,q are_orthogonal means
:: RVSUM_1:def 17

  |(p,q)| = 0;
  symmetry;
end;

theorem :: RVSUM_1:141
  p, q are_orthogonal implies a*p,q are_orthogonal;

:: 2009.08.15, from TURING_0, A.T.

theorem :: RVSUM_1:142
  Sum<*r1,r2,r3,r4*> = r1 + r2 + r3 + r4;

:: from TOPREAL7, 2011.07.31, A.T.

reserve f,g for real-valued FinSequence;

theorem :: RVSUM_1:143
  len f = len sqr f & dom f = dom sqr f;

theorem :: RVSUM_1:144
  sqr (f^g) = sqr f ^ sqr g;

theorem :: RVSUM_1:145
  for F being real-valued FinSequence holds F is FinSequence of REAL;

theorem :: RVSUM_1:146
 for F being complex-valued FinSequence holds F is FinSequence of COMPLEX;

registration
  let r be natural Number;
  cluster <*r*> -> natural-valued;
end;

registration
  let r1, r2 be natural Number;
  cluster <*r1, r2*> -> natural-valued;
end;

registration
  let r1, r2, r3 be natural Number;
  cluster <*r1, r2, r3*> -> natural-valued;
end;

registration
  let f, g be natural-valued FinSequence;
  cluster f ^ g -> natural-valued;
end;