:: The Sum and Product of Finite Sequences of Real Numbers
:: by Czes{\l}aw Byli\'nski
::
:: Received May 11, 1990
:: Copyright (c) 1990-2026 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;
definitions BINOP_1, FINSEQOP, FINSEQ_1;
equalities FINSEQ_1, SQUARE_1, FINSEQ_2, VALUED_1, FINSEQ_4;
expansions BINOP_1, FINSEQOP, FINSEQ_1;
theorems SQUARE_1, FUNCT_1, FUNCT_2, BINOP_1, FINSEQ_1, FUNCOP_1, FINSEQ_2,
FINSEQOP, SETWOP_2, RELAT_1, FINSOP_1, XREAL_0, ZFMISC_1, XCMPLX_0,
BINOP_2, SETWISEO, XREAL_1, NUMBERS, XBOOLE_1, FINSEQ_3, ORDINAL1,
VALUED_0, VALUED_1, CARD_1, RFUNCT_1, INT_1, TARSKI;
schemes NAT_1, FUNCT_2;
begin :: Auxiliary theorems
registration
let n be natural Number;
cluster n-element natural-valued for FinSequence;
existence
proof
take n|->0;
thus thesis;
end;
end;
registration
cluster real-valued for FinSequence;
existence
proof
the FinSequence of REAL is real-valued;
hence thesis;
end;
end;
definition
let F be real-valued Relation;
redefine func rng F -> Subset of REAL; :: redefines rng (RELAT_1, synonym) → proj2 (XTUPLE_0, definition)
coherence by VALUED_0:def 3;
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;
coherence
proof
consider n1 being Nat such that
A1: dom F1 = Seg n1 by FINSEQ_1:def 2;
take n1;
dom F = REAL & rng F1 c= REAL by FUNCT_2:def 1;
hence thesis by A1,RELAT_1:27;
end;
end;
registration
let r be Real;
cluster <*r*> -> real-valued;
coherence;
end;
registration
let r1, r2 be Real;
cluster <*r1, r2*> -> real-valued;
coherence;
end;
registration
let r1, r2, r3 be Real;
cluster <*r1, r2, r3*> -> real-valued;
coherence;
end;
registration
let r1, r2, r3, r4 be Real;
cluster <*r1, r2, r3, r4*> -> real-valued;
coherence;
end;
registration
let j be natural Number, r be Real;
cluster j |-> r -> real-valued;
coherence;
end;
registration
let f, g be real-valued FinSequence;
cluster f ^ g -> real-valued;
coherence;
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
0 is_a_unity_wrt addreal by BINOP_2:2,SETWISEO:14;
definition
redefine func diffreal equals :: redefines diffreal (BINOP_2, definition)
addreal*(id REAL,compreal);
compatibility
proof
let b be BinOp of REAL;
now
let r1,r2 be Element of REAL;
thus diffreal.(r1,r2) = r1 - r2 by BINOP_2:def 10
.= r1 + - r2
.= addreal.(r1,- r2) by BINOP_2:def 9
.= addreal.(r1,compreal.r2) by BINOP_2:def 7
.= (addreal*(id REAL,compreal)).(r1,r2) by FINSEQOP:82;
end;
hence thesis;
end;
correctness;
end;
definition
func sqrreal -> UnOp of REAL means
:Def2:
for r holds it.r = r^2;
existence
proof
deffunc F(Real) = In($1^2,REAL);
consider G being Function of REAL,REAL such that
A1: for x being Element of REAL holds G.x = F(x) from FUNCT_2:sch 4;
take G;
let r;
r in REAL by XREAL_0:def 1;
then G.r = F(r) by A1;
hence thesis;
end;
uniqueness
proof
let G1,G2 be UnOp of REAL such that
A2: for r holds G1.r = r^2 and
A3: for r holds G2.r = r^2;
now
let x be Element of REAL;
G1.(x) = (x)^2 by A2;
hence G1.x = G2.x by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem
1 is_a_unity_wrt multreal
by BINOP_2:7,SETWISEO:14;
theorem Th3:
multreal is_distributive_wrt addreal
proof
now
let x1,x2,x3 be Element of REAL;
thus multreal.(x1,addreal.(x2,x3)) = multreal.(x1,x2+x3) by BINOP_2:def 9
.= x1*(x2+x3) by BINOP_2:def 11
.= x1*x2+x1*x3
.= addreal.(x1*x2,x1*x3) by BINOP_2:def 9
.= addreal.(multreal.(x1,x2),x1*x3) by BINOP_2:def 11
.= addreal.(multreal.(x1,x2),multreal.(x1,x3)) by BINOP_2:def 11;
thus multreal.(addreal.(x1,x2),x3) = multreal.(x1+x2,x3) by BINOP_2:def 9
.= (x1+x2)*x3 by BINOP_2:def 11
.= x1*x3+x2*x3
.= addreal.(x1*x3,x2*x3) by BINOP_2:def 9
.= addreal.(multreal.(x1,x3),x2*x3) by BINOP_2:def 11
.= addreal.(multreal.(x1,x3),multreal.(x2,x3)) by BINOP_2:def 11;
end;
hence thesis by BINOP_1:11;
end;
theorem
sqrreal is_distributive_wrt multreal
proof
let x1,x2 be Element of REAL;
thus sqrreal.(multreal.(x1,x2)) = sqrreal.(x1*x2) by BINOP_2:def 11
.= (x1*x2)^2 by Def2
.= x1^2*x2^2
.= multreal.(x1^2,x2^2) by BINOP_2:def 11
.= multreal.(sqrreal.x1,x2^2) by Def2
.= multreal.(sqrreal.x1,sqrreal.x2) by Def2;
end;
definition
let x be Real;
func x multreal -> UnOp of REAL equals
multreal[;](x,id REAL);
coherence
proof
reconsider y = x as Element of REAL by XREAL_0:def 1;
multreal[;](y,id REAL) is UnOp of REAL;
hence thesis;
end;
end;
Lm1: (multreal[;](r,id REAL)).r1 = r*r1
proof
reconsider a=r, s=r1 as Element of REAL by XREAL_0:def 1;
thus (multreal[;](r,id REAL)).r1 = multreal.(a,(id REAL).s) by FUNCOP_1:53
.= multreal.(a,s)
.= r*r1 by BINOP_2:def 11;
end;
theorem
(r multreal).r1 = r*r1 by Lm1;
theorem
r multreal is_distributive_wrt addreal
proof
r in REAL by XREAL_0:def 1;
hence thesis by Th3,FINSEQOP:54;
end;
theorem Th7:
compreal is_an_inverseOp_wrt addreal
proof
let x be Element of REAL;
thus addreal.(x,compreal.x) = x+compreal.x by BINOP_2:def 9
.= x+-x by BINOP_2:def 7
.= the_unity_wrt addreal by BINOP_2:2;
thus addreal.(compreal.x,x) = compreal.x+x by BINOP_2:def 9
.= -x+x by BINOP_2:def 7
.= the_unity_wrt addreal by BINOP_2:2;
end;
theorem Th8:
addreal is having_an_inverseOp by Th7;
theorem Th9:
the_inverseOp_wrt addreal = compreal by Th7,Th8,FINSEQOP:def 3;
theorem
compreal is_distributive_wrt addreal by Th8,Th9,FINSEQOP:63;
:: Some Functors on the i-tuples on Real
Lm2: F is FinSequence of REAL
proof
thus rng F c= REAL;
end;
definition
let F1,F2;
redefine func F1 + F2 -> FinSequence of REAL equals :: redefines + (VALUED_1, definition)
addreal.:(F1,F2);
coherence by Lm2;
compatibility
proof
reconsider F3=F1,F4=F2 as FinSequence of REAL by Lm2;
let F be FinSequence of REAL;
dom addreal = [:REAL,REAL:] by FUNCT_2:def 1;
then [:rng F3, rng F4:] c= dom addreal by ZFMISC_1:96;
then
A1: dom(addreal.:(F1,F2)) = dom F1 /\ dom F2 by FUNCOP_1:69;
A2: dom (F1+F2) = dom F1 /\ dom F2 by VALUED_1:def 1;
thus F = F1+F2 implies F = addreal.:(F1,F2)
proof
assume
A3: F = F1+F2;
for z being set st z in dom(addreal.:(F1,F2)) holds F.z = addreal.(
F1.z,F2.z)
proof
let z be set;
assume z in dom(addreal.:(F1,F2));
hence F.z = F1.z + F2.z by A2,A1,A3,VALUED_1:def 1
.= addreal.(F1.z,F2.z) by BINOP_2:def 9;
end;
hence thesis by A2,A1,A3,FUNCOP_1:21;
end;
assume
A4: F = addreal.:(F1,F2);
now
let c be object;
assume c in dom F;
hence F.c = addreal.(F1.c,F2.c) by A4,FUNCOP_1:22
.= F1.c + F2.c by BINOP_2:def 9;
end;
hence thesis by A1,A4,VALUED_1:def 1;
end;
commutativity
proof
let F be FinSequence of REAL;
let F1,F2;
assume
A5: F = addreal.:(F1,F2);
reconsider F1,F2 as FinSequence of REAL by Lm2;
A6: dom addreal = [:REAL,REAL:] by FUNCT_2:def 1;
then
A7: [:rng F2, rng F1:] c= dom addreal by ZFMISC_1:96;
[:rng F1, rng F2:] c= dom addreal by A6,ZFMISC_1:96;
then
A8: dom(addreal.:(F1,F2)) = dom F1 /\ dom F2 by FUNCOP_1:69
.= dom(addreal.:(F2,F1)) by A7,FUNCOP_1:69;
for z being set st z in dom(addreal.:(F2,F1)) holds F.z = addreal.(F2
.z,F1.z)
proof
let z be set;
assume z in dom(addreal.:(F2,F1));
hence F.z = addreal.(F1.z,F2.z) by A5,A8,FUNCOP_1:22
.= F1.z + F2.z by BINOP_2:def 9
.= addreal.(F2.z,F1.z) by BINOP_2:def 9;
end;
hence thesis by A5,A8,FUNCOP_1:21;
end;
end;
definition
let i,R1,R2;
redefine func R1 + R2 -> Element of i-tuples_on REAL; :: redefines + (VALUED_1, definition)
coherence by FINSEQ_2:120;
end;
theorem
(R1+R2).s = R1.s + R2.s
proof
per cases;
suppose
A1: not s in Seg i;
then
A2: not s in dom R2 by FINSEQ_2:124;
A3: not s in dom R1 by A1,FINSEQ_2:124;
not s in dom(R1+R2) by A1,FINSEQ_2:124;
hence (R1+R2).s = (0 qua Element of NAT)+(0 qua Element of NAT) by
FUNCT_1:def 2
.= R1.s + (0 qua Element of NAT) by A3,FUNCT_1:def 2
.= R1.s + R2.s by A2,FUNCT_1:def 2;
end;
suppose
s in Seg i;
then s in dom (R1 + R2) by FINSEQ_2:124;
hence thesis by VALUED_1:def 1;
end;
end;
theorem
<*>REAL + F = <*>REAL
proof
F is FinSequence of REAL by Lm2;
hence thesis by FINSEQ_2:73;
end;
theorem
<*r1*> + <*r2*> = <*r1+r2*>
proof
reconsider s1=r1, s2=r2 as Element of REAL by XREAL_0:def 1;
<*s1*> + <*s2*> = <*addreal.(s1,s2)*> by FINSEQ_2:74
.= <*r1+r2*> by BINOP_2:def 9;
hence thesis;
end;
theorem
(i|->r1) + (i|->r2) = i|->(r1+r2)
proof
reconsider s1=r1, s2=r2 as Element of REAL by XREAL_0:def 1;
(i|->s1) + (i|->s2) = i|->(addreal.(s1,s2)) by FINSEQOP:17
.= i|->(r1+r2) by BINOP_2:def 9;
hence thesis;
end;
theorem
F1 + (F2 + F3) = F1 + F2 + F3 by RFUNCT_1:8;
theorem
R + (i|->(0 qua Real)) = R by BINOP_2:2,FINSEQOP:56;
theorem
(-F).s = -F.s by VALUED_1:8;
definition
let F;
redefine func -F -> FinSequence of REAL equals :: redefines - (VALUED_1, definition)
compreal*F;
coherence by Lm2;
compatibility
proof
let F1 be FinSequence of REAL;
A1: dom(-F) = dom F by VALUED_1:8;
A2: rng F c= REAL & dom compreal = REAL by FUNCT_2:def 1;
then
A3: dom(compreal*F) = dom F by RELAT_1:27;
thus F1 = -F implies F1 = compreal*F
proof
assume
A4: F1 = -F;
now
let c be object;
assume
A5: c in dom F1;
thus F1.c = -(F.c) by A4,VALUED_1:8
.= compreal.(F.c) by BINOP_2:def 7
.= (compreal*F).c by A1,A4,A5,FUNCT_1:13;
end;
hence thesis by A3,A4,FUNCT_1:2,VALUED_1:8;
end;
assume
A6: F1 = compreal*F;
now
let c be object;
assume
A7: c in dom F1;
thus (-F).c = -(F.c) by VALUED_1:8
.= compreal.(F.c) by BINOP_2:def 7
.= (compreal*F).c by A6,A7,FUNCT_1:12;
end;
hence thesis by A1,A2,A6,FUNCT_1:2,RELAT_1:27;
end;
end;
definition
let i,R;
redefine func -R -> Element of i-tuples_on REAL; :: redefines - (VALUED_1, definition)
coherence by FINSEQ_2:113;
end;
theorem
(-F).s = -(F.s) by VALUED_1:8;
theorem
-(<*>REAL) = <*>REAL;
theorem
-<*r*> = <*-r*>
proof
reconsider s=r as Element of REAL by XREAL_0:def 1;
-<*s*> = <*compreal.s*> by FINSEQ_2:35
.= <*-r*> by BINOP_2:def 7;
hence thesis;
end;
theorem Th21:
-(i|->r) = i|->-r
proof
reconsider s=r as Element of REAL by XREAL_0:def 1;
-(i|->s) = i|->(compreal.s) by FINSEQOP:16
.= i|->-r by BINOP_2:def 7;
hence thesis;
end;
theorem
R + -R = i|->0 by Th8,Th9,BINOP_2:2,FINSEQOP:73;
theorem
R1 + R2 = i|->0 implies R1 = -R2 by Th8,Th9,BINOP_2:2,FINSEQOP:74;
theorem
for R1, R2 being complex-valued Function st -R1 = -R2 holds R1 = R2
proof
let R1, R2 be complex-valued Function;
assume -R1 = -R2;
hence R1 = --R2 .= R2;
end;
theorem
R1 + R = R2 + R implies R1 = R2
proof
assume R1 + R = R2 + R;
then R1 + (R + -R)= (R2 + R)+-R by FINSEQOP:28;
then
A1: R1 + (R + -R)= R2 + (R + -R) by FINSEQOP:28;
R + -R = i|->0 by Th8,Th9,BINOP_2:2,FINSEQOP:73;
then R1 = R2 + (i|->(0 qua Real)) by A1,BINOP_2:2,FINSEQOP:56;
hence thesis by BINOP_2:2,FINSEQOP:56;
end;
theorem Th26:
-(F1 + F2) = -F1 + -F2
proof
A1: dom -(F1 + F2) = dom(F1+F2) by VALUED_1:8;
A2: dom(F1+F2) = dom F1 /\ dom F2 by VALUED_1:def 1;
A3: dom (-F1 + -F2) = dom (-F1) /\ dom -F2 by VALUED_1:def 1
.= dom F1 /\ dom -F2 by VALUED_1:8
.= dom F1 /\ dom F2 by VALUED_1:8;
now
let i be Nat;
assume
A4: i in dom -(F1+F2);
thus (-(F1 + F2)).i = -((F1+F2).i) by VALUED_1:8
.= -(F1.i+F2.i) by A1,A4,VALUED_1:def 1
.= -(F1.i)+-(F2.i)
.= -(F1.i) + (-F2).i by VALUED_1:8
.= (-F1).i + (-F2).i by VALUED_1:8
.= (-F1 + -F2).i by A1,A2,A3,A4,VALUED_1:def 1;
end;
hence thesis by A2,A3,FINSEQ_1:13,VALUED_1:8;
end;
definition
let F1,F2;
redefine func F1 - F2 -> FinSequence of REAL equals :: redefines - (VALUED_1, definition)
diffreal.:(F1,F2);
coherence by Lm2;
compatibility
proof
reconsider F3=F1,F4=F2 as FinSequence of REAL by Lm2;
let F be FinSequence of REAL;
A1: dom (F1-F2) = dom F1 /\ dom F2 by VALUED_1:12;
dom diffreal = [:REAL,REAL:] by FUNCT_2:def 1;
then
A2: [:rng F3, rng F4:] c= dom diffreal by ZFMISC_1:96;
then
A3: dom(diffreal.:(F1,F2)) = dom F1 /\ dom F2 by FUNCOP_1:69;
thus F = F1-F2 implies F = diffreal.:(F1,F2)
proof
assume
A4: F = F1-F2;
for z being set st z in dom(diffreal.:(F1,F2)) holds F.z = diffreal.
(F1.z,F2.z)
proof
let z be set;
assume z in dom(diffreal.:(F1,F2));
hence F.z = F1.z - F2.z by A1,A3,A4,VALUED_1:13
.= diffreal.(F1.z,F2.z) by BINOP_2:def 10;
end;
hence thesis by A1,A3,A4,FUNCOP_1:21;
end;
assume
A5: F = diffreal.:(F1,F2);
now
let c be object;
assume c in dom F;
hence F.c = diffreal.(F1.c,F2.c) by A5,FUNCOP_1:22
.= F1.c - F2.c by BINOP_2:def 10;
end;
hence thesis by A1,A2,A5,FUNCOP_1:69,VALUED_1:14;
end;
end;
definition
let i,R1,R2;
redefine func R1 - R2 -> Element of i-tuples_on REAL; :: redefines - (VALUED_1, definition)
coherence by FINSEQ_2:120;
end;
theorem
(R1-R2).s = R1.s - R2.s
proof
per cases;
suppose
A1: not s in Seg i;
then
A2: not s in dom R2 by FINSEQ_2:124;
A3: not s in dom R1 by A1,FINSEQ_2:124;
not s in dom(R1-R2) by A1,FINSEQ_2:124;
hence (R1-R2).s = (0 qua Element of NAT)-(0 qua Element of NAT) by
FUNCT_1:def 2
.= R1.s - (0 qua Element of NAT) by A3,FUNCT_1:def 2
.= R1.s - R2.s by A2,FUNCT_1:def 2;
end;
suppose s in Seg i;
then s in dom (R1 - R2) by FINSEQ_2:124;
hence thesis by VALUED_1:13;
end;
end;
theorem
<*>REAL - F = <*>REAL & F - <*>REAL = <*>REAL
proof
F is FinSequence of REAL by Lm2;
hence thesis by FINSEQ_2:73;
end;
theorem
<*r1*> - <*r2*> = <*r1-r2*>
proof
reconsider s1=r1, s2=r2 as Element of REAL by XREAL_0:def 1;
<*s1*> - <*s2*> = <*diffreal.(s1,s2)*> by FINSEQ_2:74
.= <*r1-r2*> by BINOP_2:def 10;
hence thesis;
end;
theorem
(i|->r1) - (i|->r2) = i|->(r1-r2)
proof
reconsider s1=r1, s2=r2 as Element of REAL by XREAL_0:def 1;
(i|->s1) - (i|->s2) = i|->(diffreal.(s1,s2)) by FINSEQOP:17
.= i|->(r1-r2) by BINOP_2:def 10;
hence thesis;
end;
theorem
F1 - F2 = F1 + - F2;
theorem
R - (i|->(0 qua Real)) = R
proof
thus R - (i|->(0 qua Real)) = R + (i|->(-(0 qua Element of NAT))) by Th21
.= R by BINOP_2:2,FINSEQOP:56;
end;
theorem
(i|->(0 qua Real)) - R = -R by BINOP_2:2,FINSEQOP:56;
theorem
F1 - -F2 = F1 + F2;
theorem
-(F1 - F2) = F2 - F1
proof
thus -(F1 - F2) = -F1 + --F2 by Th26
.= F2 - F1;
end;
theorem
-(F1 - F2) = -F1 + F2
proof
thus -(F1 - F2) = -F1 +--F2 by Th26
.= -F1 + F2;
end;
theorem
R - R = i|->0 by Th8,Th9,BINOP_2:2,FINSEQOP:73;
theorem
R1 - R2 = i|->0 implies R1 = R2
proof
assume R1 - R2 = i|->0;
then R1 = --R2 by Th8,Th9,BINOP_2:2,FINSEQOP:74;
hence thesis;
end;
theorem
F1 - F2 - F3 = F1 - (F2 + F3) by RFUNCT_1:20;
theorem
F1 + (F2 - F3) = F1 + F2 - F3 by RFUNCT_1:23;
theorem
F1 - (F2 - F3) = F1 - F2 + F3 by RFUNCT_1:22;
theorem
R1 = R1 + R - R
proof
thus R1 = R1 + (i|->(0 qua Real)) by BINOP_2:2,FINSEQOP:56
.= R1 + (R - R) by Th8,Th9,BINOP_2:2,FINSEQOP:73
.= R1 + R - R by RFUNCT_1:23;
end;
theorem
R1 = R1 - R + R
proof
thus R1 = R1 + (i|->(0 qua Real)) by BINOP_2:2,FINSEQOP:56
.= R1 + (-R + R) by Th8,Th9,BINOP_2:2,FINSEQOP:73
.= R1 - R + R by FINSEQOP:28;
end;
notation
let F; let r be Real;
synonym r*F for r(#)F;
end;
theorem
(r*F).s = r*(F.s) by VALUED_1:6;
definition
let F; let r be Real;
redefine func r*F -> FinSequence of REAL equals :: redefines * (RVSUM_1, synonym) → (#) (VALUED_1, definition)
(r multreal)*F;
coherence by Lm2;
compatibility
proof
let F1 be FinSequence of REAL;
A1: dom(r*F) = dom F by VALUED_1:def 5;
A2: rng F c= REAL & dom(r multreal) = REAL by FUNCT_2:def 1;
then
A3: dom((r multreal)*F) = dom F by RELAT_1:27;
thus F1 = r*F implies F1 = (r multreal)*F
proof
assume
A4: F1 = r*F;
now
let c be object;
assume
A5: c in dom F1;
hence F1.c = r*(F.c) by A4,VALUED_1:def 5
.= (r multreal).(F.c) by Lm1
.= ((r multreal)*F).c by A1,A4,A5,FUNCT_1:13;
end;
hence thesis by A1,A3,A4,FUNCT_1:2;
end;
assume
A6: F1 = (r multreal)*F;
now
let c be object;
assume
A7: c in dom F1;
thus (r*F).c = r*(F.c) by VALUED_1:6
.= (r multreal).(F.c) by Lm1
.= ((r multreal)*F).c by A6,A7,FUNCT_1:12;
end;
hence thesis by A1,A2,A6,FUNCT_1:2,RELAT_1:27;
end;
end;
definition
let i,R,r;
redefine func r*R -> Element of i-tuples_on REAL; :: redefines * (RVSUM_1, synonym) → (#) (VALUED_1, definition)
coherence by FINSEQ_2:113;
end;
theorem
(r*F).s = r*(F.s) by VALUED_1:6;
theorem
r*(<*>REAL) = <*>REAL;
theorem
r*<*r1*> = <*r*r1*>
proof
reconsider s=r, s1=r1 as Element of REAL by XREAL_0:def 1;
s*<*s1*> = <*(multreal[;](s,id REAL)).s1*> by FINSEQ_2:35
.= <*r*r1*> by Lm1;
hence thesis;
end;
theorem Th48:
r1*(i|->r2) = i|->(r1*r2)
proof
reconsider s1=r1, s2=r2 as Element of REAL by XREAL_0:def 1;
s1*(i|->s2) = i|->((multreal[;](s1,id REAL)).s2) by FINSEQOP:16
.= i|->(r1*r2) by Lm1;
hence thesis;
end;
theorem
(r1*r2)*F = r1*(r2*F) by RFUNCT_1:17;
theorem
(r1 + r2)*F = r1*F + r2*F
proof
A1: dom ((r1 + r2)*F) = dom F by VALUED_1:def 5;
A2: dom (r1*F + r2*F) = dom (r1*F) /\ dom (r2*F) by VALUED_1:def 1;
A3: dom (r1*F) = dom F by VALUED_1:def 5;
A4: dom (r2*F) = dom F by VALUED_1:def 5;
now
let i be Nat;
assume
A5: i in dom ((r1+r2)*F);
thus ((r1+r2)*F).i = (r1+r2)*(F.i) by VALUED_1:6
.= r1*(F.i) + r2*(F.i)
.= r1*(F.i) + (r2*F).i by VALUED_1:6
.= (r1*F).i + (r2*F).i by VALUED_1:6
.= (r1*F+r2*F).i by A1,A2,A3,A4,A5,VALUED_1:def 1;
end;
hence thesis by A1,A2,A3,A4,FINSEQ_1:13;
end;
theorem
r*(F1+F2) = r*F1 + r*F2 by RFUNCT_1:16;
theorem
1*F = F by RFUNCT_1:21;
theorem
0*R = i|->0
proof
A1: rng R c= REAL;
thus 0*R = multreal[;](0,(id REAL)*R) by FUNCOP_1:34
.= multreal[;](0,R) by A1,RELAT_1:53
.= i|->0 by Th3,Th8,BINOP_2:2,FINSEQOP:76;
end;
theorem
(-1)*F = -F;
notation
let F;
synonym sqr F for F^2;
end;
definition
let F;
redefine func sqr F -> FinSequence of REAL equals :: redefines sqr (RVSUM_1, synonym) → ^2 (VALUED_1, definition)
sqrreal*F;
compatibility
proof
let f be FinSequence of REAL;
sqr F = sqrreal*F
proof
dom sqrreal = REAL by FUNCT_2:def 1;
then
A1: rng F c= dom sqrreal;
A2: dom sqr F = dom F by VALUED_1:11
.= dom(sqrreal*F) by A1,RELAT_1:27;
hence len sqr F = len(sqrreal*F) by FINSEQ_3:29;
let k;
assume 1 <= k & k <= len sqr F;
then
A3: k in dom sqr F by FINSEQ_3:25;
thus (sqr F).k = (F.k)^2 by VALUED_1:11
.= sqrreal.(F.k) by Def2
.= (sqrreal*F).k by A2,A3,FUNCT_1:12;
end;
hence thesis;
end;
coherence by Lm2;
end;
definition
let i,R;
redefine func sqr R -> Element of i-tuples_on REAL; :: redefines sqr (RVSUM_1, synonym) → ^2 (VALUED_1, definition)
coherence by FINSEQ_2:113;
end;
theorem
sqr <*r*> = <*r^2*>
proof
reconsider s=r as Element of REAL by XREAL_0:def 1;
sqr <*s*> = <*sqrreal.s*> by FINSEQ_2:35
.= <*r^2*> by Def2;
hence thesis;
end;
theorem
sqr(i |-> r) = i |-> r^2
proof
reconsider s=r as Element of REAL by XREAL_0:def 1;
sqr(i |-> s) = i |-> (sqrreal.s) by FINSEQOP:16
.= i |-> r^2 by Def2;
hence thesis;
end;
theorem Th57:
sqr -F = sqr F
proof
A1: dom sqr -F = dom -F by VALUED_1:11
.= dom F by VALUED_1:8;
A2: dom sqr F = dom F by VALUED_1:11;
now
let j be Nat;
assume j in dom sqr -F;
set r = F.j, r9 = (-F).j;
thus (sqr -F).j = (r9)^2 by VALUED_1:11
.= (-r)^2 by VALUED_1:8
.= r^2
.= (sqr F).j by VALUED_1:11;
end;
hence thesis by A1,A2,FINSEQ_1:13;
end;
theorem Th58:
sqr (r*F) = r^2 * sqr F
proof
A1: dom (r*F) = dom F by VALUED_1:def 5;
A2: dom (r^2 * sqr F) = dom sqr F by VALUED_1:def 5;
A3: dom sqr F = dom F by VALUED_1:11;
now
let i be Nat;
assume i in dom sqr (r*F);
thus (sqr (r*F)).i = ((r*F).i)^2 by VALUED_1:11
.= (r*(F.i))^2 by VALUED_1:6
.= r^2 * (F.i)^2
.= r^2 * (sqr F).i by VALUED_1:11
.= (r^2 * sqr F).i by VALUED_1:6;
end;
hence thesis by A1,A2,A3,FINSEQ_1:13,VALUED_1:11;
end;
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 :: redefines mlt (RVSUM_1, synonym) → (#) (VALUED_1, definition)
multreal.:(F1,F2);
coherence by Lm2;
compatibility
proof
reconsider F3=F1,F4=F2 as FinSequence of REAL by Lm2;
let F be FinSequence of REAL;
dom multreal = [:REAL,REAL:] by FUNCT_2:def 1;
then [:rng F3, rng F4:] c= dom multreal by ZFMISC_1:96;
then
A1: dom(multreal.:(F1,F2)) = dom F1 /\ dom F2 by FUNCOP_1:69;
A2: dom mlt(F1,F2) = dom F1 /\ dom F2 by VALUED_1:def 4;
thus F = mlt(F1,F2) implies F = multreal.:(F1,F2)
proof
assume
A3: F = mlt(F1,F2);
for z being set st z in dom(multreal.:(F1,F2)) holds F.z = multreal.
(F1.z,F2.z)
proof
let z be set;
assume z in dom(multreal.:(F1,F2));
thus F.z = F1.z * F2.z by A3,VALUED_1:5
.= multreal.(F1.z,F2.z) by BINOP_2:def 11;
end;
hence thesis by A2,A1,A3,FUNCOP_1:21;
end;
assume
A4: F = multreal.:(F1,F2);
now
let c be object;
assume c in dom F;
hence F.c = multreal.(F1.c,F2.c) by A4,FUNCOP_1:22
.= F1.c * F2.c by BINOP_2:def 11;
end;
hence thesis by A1,A4,VALUED_1:def 4;
end;
commutativity
proof
let F be FinSequence of REAL;
let F1,F2;
reconsider F3=F1,F4=F2 as FinSequence of REAL by Lm2;
A5: dom multreal = [:REAL,REAL:] by FUNCT_2:def 1;
then
A6: [:rng F4, rng F3:] c= dom multreal by ZFMISC_1:96;
[:rng F3, rng F4:] c= dom multreal by A5,ZFMISC_1:96;
then
A7: dom(multreal.:(F1,F2)) = dom F1 /\ dom F2 by FUNCOP_1:69
.= dom(multreal.:(F2,F1)) by A6,FUNCOP_1:69;
assume
A8: F = multreal.:(F1,F2);
for z being set st z in dom(multreal.:(F2,F1)) holds F.z = multreal.(
F2.z,F1.z)
proof
let z be set such that
A9: z in dom(multreal.:(F2,F1));
set F1z = F1.z, F2z =F2.z;
thus F.z = multreal.(F1.z,F2.z) by A8,A7,A9,FUNCOP_1:22
.= F1z * F2z by BINOP_2:def 11
.= multreal.(F2.z,F1.z) by BINOP_2:def 11;
end;
hence thesis by A8,A7,FUNCOP_1:21;
end;
end;
theorem
mlt(F1,F2).s = F1.s * F2.s by VALUED_1:5;
definition
let i,R1,R2;
redefine func mlt(R1,R2) -> Element of i-tuples_on REAL; :: redefines mlt (RVSUM_1, synonym) → (#) (VALUED_1, definition)
coherence by FINSEQ_2:120;
end;
theorem ::=VALUED_1:5
mlt(F1,F2).s = F1.s * F2.s by VALUED_1:5;
theorem
mlt(<*>REAL,F) = <*>REAL
proof
F is FinSequence of REAL by Lm2;
hence thesis by FINSEQ_2:73;
end;
theorem
mlt(<*r1*>,<*r2*>) = <*r1*r2*>
proof
reconsider s1=r1, s2=r2 as Element of REAL by XREAL_0:def 1;
mlt(<*s1*>,<*s2*>) = <*multreal.(s1,s2)*> by FINSEQ_2:74
.= <*r1*r2*> by BINOP_2:def 11;
hence thesis;
end;
theorem Th63:
mlt(i|->r,R) = r*R
proof
reconsider s=r as Element of REAL by XREAL_0:def 1;
mlt(i|->s,R) = multreal[;](s,R) by FINSEQOP:20
.= r*R by FINSEQOP:22;
hence thesis;
end;
theorem
mlt(i|->r1,i|->r2) = i|->(r1*r2)
proof
reconsider s1=r1, s2=r2 as Element of REAL by XREAL_0:def 1;
mlt(i|->s1,i|->s2) = s1*(i|->s2) by Th63
.= i|->(r1*r2) by Th48;
hence thesis;
end;
theorem
r*mlt(F1,F2) = mlt(r*F1,F2) by RFUNCT_1:12;
theorem ::=Th92
r*R = mlt(i|->r,R) by Th63;
theorem
sqr(F) = mlt(F,F);
theorem Th68:
sqr(F1 + F2) = sqr F1 + 2*mlt(F1,F2) + sqr F2
proof
A1: dom sqr(F1 + F2) = dom (F1+F2) by VALUED_1:11;
A2: dom(F1+F2) = dom F1 /\ dom F2 by VALUED_1:def 1;
A3: dom(sqr F1 + 2*mlt(F1,F2))
= dom(sqr F1) /\ dom (2*mlt(F1,F2)) by VALUED_1:def 1
.= dom F1 /\ dom (2*mlt(F1,F2)) by VALUED_1:11
.= dom F1 /\ dom (mlt(F1,F2)) by VALUED_1:def 5
.= dom F1 /\ (dom F1 /\ dom F2) by VALUED_1:def 4
.= dom F1 /\ dom F1 /\ dom F2 by XBOOLE_1:16
.= dom F1 /\ dom F2;
then A4: dom(sqr F1 + 2*mlt(F1,F2) + sqr F2)
= dom F1 /\ dom F2 /\ dom sqr F2 by VALUED_1:def 1
.= dom F1 /\ dom F2 /\ dom F2 by VALUED_1:11
.= dom F1 /\ (dom F2 /\ dom F2) by XBOOLE_1:16;
now
let j be Nat;
assume
A5: j in dom sqr(F1+F2);
set r1r2 = (F1 + F2).j, r1 = F1.j, r2 = F2.j, r192 = (sqr F1).j,
r292 = (sqr F2).j, r1r2a = mlt(F1,F2).j, 2r1r2 = (2*mlt(F1,F2)).j,
r1922r1r2 = (sqr F1 + 2*mlt(F1,F2)).j;
thus (sqr(F1 + F2)).j = r1r2^2 by VALUED_1:11
.= (r1 + r2)^2 by A1,A5,VALUED_1:def 1
.= r1^2+2*r1*r2+r2^2
.= r192+2*(r1*r2)+r2^2 by VALUED_1:11
.= r192+2*(r1*r2)+r292 by VALUED_1:11
.= r192+2*(r1r2a)+r292 by VALUED_1:5
.= r192+2r1r2+r292 by VALUED_1:6
.= r1922r1r2+r292 by A1,A2,A3,A5,VALUED_1:def 1
.= (sqr F1 + 2*mlt(F1,F2) + sqr F2).j by A1,A2,A4,A5,VALUED_1:def 1;
end;
hence thesis by A2,A4,FINSEQ_1:13,VALUED_1:11;
end;
theorem Th69:
sqr(F1 - F2) = sqr F1 - 2*mlt(F1,F2) + sqr F2
proof
thus sqr(F1 - F2) = sqr F1 + 2*mlt(F1,-F2) + sqr -F2 by Th68
.= sqr F1 + 2*mlt(F1,-F2) + sqr F2 by Th57
.= sqr F1 + 2*((-1)*mlt(F1,F2)) + sqr F2 by RFUNCT_1:12
.= sqr F1 + ((-1)*2)*mlt(F1,F2) + sqr F2 by RFUNCT_1:17
.= sqr F1 - 2*mlt(F1,F2) + sqr F2 by RFUNCT_1:17;
end;
theorem
sqr mlt(F1,F2) = mlt(sqr F1,sqr F2)
proof
A1: dom mlt(F1,F2) = dom F1 /\ dom F2 by VALUED_1:def 4;
A2: dom mlt(sqr F1,sqr F2) = dom sqr F1 /\ dom sqr F2 by VALUED_1:def 4;
A3: dom sqr F1 = dom F1 by VALUED_1:11;
A4: dom sqr F2 = dom F2 by VALUED_1:11;
now
let i be Nat;
assume i in dom sqr mlt(F1,F2);
thus (sqr mlt(F1,F2)).i = (mlt(F1,F2).i)^2 by VALUED_1:11
.= (F1.i*F2.i)^2 by VALUED_1:5
.= (F1.i)^2*(F2.i)^2
.= (sqr F1).i*(F2.i)^2 by VALUED_1:11
.= (sqr F1).i * (sqr F2).i by VALUED_1:11
.= (mlt(sqr F1,sqr F2)).i by VALUED_1:5;
end;
hence thesis by A1,A2,A3,A4,FINSEQ_1:13,VALUED_1:11;
end;
:: Finite sum of Finite Sequence of Real Numbers
registration
cluster -> complex-valued for FinSequence of COMPLEX;
coherence;
cluster real-valued complex-valued for FinSequence;
existence
proof
<*>REAL is real-valued;
hence thesis;
end;
end;
definition
let F be complex-valued FinSequence;
func Sum F -> Complex means
:Def10:
ex f being FinSequence of COMPLEX st f = F & it = addcomplex $$ f;
existence
proof
rng F c= COMPLEX by VALUED_0:def 1;
then reconsider f = F as FinSequence of COMPLEX by FINSEQ_1:def 4;
take addcomplex $$ f;
thus thesis;
end;
uniqueness;
end;
registration
let F be real-valued FinSequence;
cluster Sum F -> real;
coherence
proof
set mc = addcomplex;
consider f being FinSequence of COMPLEX such that
A1: f = F and
A2: Sum F = addcomplex $$ f by Def10;
set g = [#](f,the_unity_wrt mc);
defpred P[Nat] means mc $$ (finSeg $1,[#](f,the_unity_wrt mc)) is real;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: P[k];
reconsider k as Element of NAT by ORDINAL1:def 12;
g.(k+1) is real
proof
per cases;
suppose
k+1 in dom f;
then g.(k+1) = f.(k+1) by SETWOP_2:20;
hence thesis by A1;
end;
suppose
not k+1 in dom f;
hence thesis by BINOP_2:1,SETWOP_2:20;
end;
end;
then reconsider a = g.(k+1), b = mc $$(finSeg k,g) as Real by A4;
not (k + 1) in Seg k by FINSEQ_3:8;
then mc $$ (finSeg k \/ {.In(k+1,NAT).},g)
= mc.(mc $$(finSeg k,g),g.(k+1)) by
SETWOP_2:2
.= b + a by BINOP_2:def 3;
hence thesis by FINSEQ_1:9;
end;
A5: mc $$ f = mc $$ (findom f,[#](f,the_unity_wrt mc)) & ex n being Nat st
dom f = Seg n by FINSEQ_1:def 2,SETWOP_2:def 2;
Seg 0 = {}.NAT;
then
A6: P[0] by BINOP_2:1,SETWISEO:31;
for n being Nat holds P[n] from NAT_1:sch 2(A6,A3);
hence thesis by A2,A5;
end;
end;
theorem Th71:
for F being FinSequence of REAL holds Sum F = addreal $$ F
proof
set g = addreal, h = addcomplex;
let F be FinSequence of REAL;
rng F c= COMPLEX by NUMBERS:11,XBOOLE_1:1;
then reconsider f = F as FinSequence of COMPLEX by FINSEQ_1:def 4;
defpred P[Nat] means g $$ (finSeg $1,[#](F,the_unity_wrt g)) = h $$ (finSeg
$1,[#](f,the_unity_wrt h));
consider n being Nat such that
A1: dom f = Seg n by FINSEQ_1:def 2;
A2: g $$ F = g $$ (finSeg n,[#](F,the_unity_wrt g)) & h $$ f = h $$ (finSeg
n, [#](f,the_unity_wrt h)) by A1,SETWOP_2:def 2;
A3: for k being Nat st P[k] holds P[k+1]
proof
set j = [#](f,the_unity_wrt h);
set i = [#](F,the_unity_wrt g);
let k be Nat;
assume
A4: P[k];
reconsider k as Element of NAT by ORDINAL1:def 12;
A5: i.(k+1) = j.(k+1)
proof
per cases;
suppose
A6: k+1 in dom f;
then j.(k+1) = F.(k+1) by SETWOP_2:20
.= i.(k+1) by A6,SETWOP_2:20;
hence thesis;
end;
suppose
A7: not k+1 in dom f;
then j.(k+1) = the_unity_wrt h by SETWOP_2:20
.= i.(k+1) by A7,BINOP_2:1,2,SETWOP_2:20;
hence thesis;
end;
end;
A8: not (k + 1) in Seg k by FINSEQ_3:8;
g $$ (finSeg (k+1),i) = g $$
(finSeg k \/ {.In(k+1,NAT).},i) by FINSEQ_1:9
.= g.(g $$(finSeg k,i),i.(k+1)) by A8,SETWOP_2:2
.= g $$(finSeg k,i) + (i.(k+1)) by BINOP_2:def 9
.= h.(h $$(finSeg k,j),j.(k+1)) by A4,A5,BINOP_2:def 3
.= h $$ (finSeg k \/ {.In(k+1,NAT).},j) by A8,SETWOP_2:2
.= h $$ (finSeg (k+1),j) by FINSEQ_1:9;
hence thesis;
end;
A9: Seg 0 = {}.NAT;
then g $$ (finSeg 0,[#](F,the_unity_wrt g)) = the_unity_wrt h by BINOP_2:1,2
,SETWISEO:31
.= h $$ (finSeg 0,[#](f,the_unity_wrt h)) by A9,SETWISEO:31;
then
A10: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A10,A3);
then g $$ F = h $$ f by A2;
hence thesis by Def10;
end;
definition
let F be FinSequence of COMPLEX;
redefine func Sum F -> Element of COMPLEX equals :: redefines Sum (RVSUM_1, definition)
addcomplex $$ F;
coherence by XCMPLX_0:def 2;
compatibility by Def10;
end;
definition
let F be FinSequence of REAL;
redefine func Sum F -> Real equals :: redefines Sum (RVSUM_1, definition)
addreal $$ F;
coherence;
compatibility by Th71;
end;
theorem Th72:
Sum(<*> REAL) = 0 by BINOP_2:2,FINSOP_1:10;
theorem
Sum <*r*> = r
proof
reconsider r as Element of REAL by XREAL_0:def 1;
Sum <*r*> = r by FINSOP_1:11;
hence thesis;
end;
theorem Th74:
Sum(F^<*r*>) = Sum F + r
proof
reconsider s=r as Element of REAL by XREAL_0:def 1;
reconsider F1=F as FinSequence of REAL by Lm2;
thus Sum(F^<*r*>) = Sum(F1^<*s*>) .= addreal.(addreal $$ F1,s) by FINSOP_1:4
.= Sum F1 + r by BINOP_2:def 9
.= Sum F + r;
end;
theorem Th75:
Sum(F1^F2) = Sum F1 + Sum F2
proof
reconsider F3=F1,F4=F2 as FinSequence of REAL by Lm2;
thus Sum(F1^F2) = Sum(F3^F4)
.= addreal.(addreal $$ F3,addreal $$ F4) by FINSOP_1:5
.= Sum F3 + Sum F4 by BINOP_2:def 9
.= Sum F1 + Sum F2;
end;
theorem
Sum(<*r*>^F) = r + Sum F
proof
reconsider s=r as Element of REAL by XREAL_0:def 1;
thus Sum(<*r*>^F) = Sum <*s*> + Sum F by Th75
.= r + Sum F by FINSOP_1:11;
end;
theorem Th77:
Sum<*r1,r2*> = r1 + r2
proof
reconsider s1=r1 as Element of REAL by XREAL_0:def 1;
thus Sum<*r1,r2*> = Sum<*s1*> + r2 by Th74
.= r1 + r2 by FINSOP_1:11;
end;
theorem Th78:
Sum<*r1,r2,r3*> = r1 + r2 + r3
proof
thus Sum<*r1,r2,r3*> = Sum<*r1,r2*> + r3 by Th74
.= r1 + r2 + r3 by Th77;
end;
theorem
for R being Element of 0-tuples_on REAL holds Sum R = 0 by Th72;
theorem Th80:
Sum(i |-> r) = i*r
proof
A0: i is Nat by TARSKI:1;
reconsider r as Element of REAL by XREAL_0:def 1;
defpred P[Nat] means Sum($1 |->r) = $1*r;
A1: for i be Nat st P[i] holds P[(i+1)]
proof
let i be Nat such that
A2: Sum(i |-> r) = i*r;
thus Sum((i+1) |-> r) = Sum((i |-> r)^<*r*>) by FINSEQ_2:60
.= i*r + 1*r by A2,Th74
.= (i+1)*r;
end;
A3: P[0] by Th72;
for i be Nat holds P[i] from NAT_1:sch 2(A3,A1);
hence thesis by A0;
end;
theorem Th81:
Sum(i |-> (0 qua Real)) = 0
proof
thus Sum(i |-> (0 qua Real)) = i*(0 qua Element of NAT) by Th80
.= 0;
end;
Lm:
for R1 being i-element real-valued FinSequence holds
R1 is Element of i-tuples_on REAL
proof
let R1 be i-element real-valued FinSequence;
A1: R1 is FinSequence of REAL by Lm2;
len R1 = i by CARD_1:def 7;
hence thesis by A1,FINSEQ_2:92;
end;
theorem Th82:
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
proof
let R1,R2 be i-element real-valued FinSequence;
A0: i is Nat by TARSKI:1;
defpred P[Nat] means for R1,R2 being $1-element real-valued FinSequence st
for j be Nat st j in Seg $1 holds R1.j <= R2.j holds Sum R1 <= Sum R2;
A1: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A2: for R1,R2 being i-element real-valued FinSequence st
for j be Nat st j in Seg i holds R1.j <= R2.j holds Sum R1 <= Sum R2;
set n = i+1;
let R1,R2 be n-element real-valued FinSequence such that
A3: for j be Nat st j in Seg n holds R1.j <= R2.j;
R1 is Element of n-tuples_on REAL by Lm;
then consider R19 being (Element of i-tuples_on REAL),
x1 being Element of REAL such that
A4: R1 = R19^<*x1*> by FINSEQ_2:117;
R2 is Element of n-tuples_on REAL by Lm;
then consider R29 being (Element of i-tuples_on REAL),
x2 being Element of REAL such that
A5: R2 = R29^<*x2*> by FINSEQ_2:117;
for j be Nat st j in Seg i holds R19.j <= R29.j
proof
let j be Nat such that
A6: j in Seg i;
Seg len R29 = dom R29 & len R29 = i by CARD_1:def 7,FINSEQ_1:def 3;
then
A7: R29.j = R2.j by A5,A6,FINSEQ_1:def 7;
Seg len R19 = dom R19 & len R19 = i by CARD_1:def 7,FINSEQ_1:def 3;
then R19.j = R1.j by A4,A6,FINSEQ_1:def 7;
hence thesis by A3,A6,A7,FINSEQ_2:8;
end;
then
A8: Sum R19 <= Sum R29 by A2;
A9: R2.n = x2 by A5,FINSEQ_2:116;
R1.n = x1 by A4,FINSEQ_2:116;
then
A10: x1 <= x2 by A3,A9,FINSEQ_1:4;
A11: Sum R2 = Sum R29 + x2 by A5,Th74;
Sum R1 = Sum R19 + x1 by A4,Th74;
hence thesis by A10,A8,A11,XREAL_1:7;
end;
A12: P[0];
for i be Nat holds P[i] from NAT_1:sch 2(A12,A1);
hence thesis by A0;
end;
theorem Th83:
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
proof
let R1,R2 be i-element real-valued FinSequence;
A0: i is Nat by TARSKI:1;
defpred P[Nat] means for R1,R2 be $1-element real-valued FinSequence st
(for j be Nat st j in Seg $1 holds R1.j <= R2.j) &
(ex j be Nat st j in Seg $1 & R1.j < R2.j) holds Sum
R1 < Sum R2;
now
let i be Nat such that
A1: P[i];
let R1,R2 be (i+1)-element real-valued FinSequence such that
A2: for j be Nat st j in Seg (i+1) holds R1.j <= R2.j;
given j be Nat such that
A3: j in Seg (i+1) and
A4: R1.j < R2.j;
R1 is Element of (i+1)-tuples_on REAL by Lm;
then consider R19 being (Element of i-tuples_on REAL),
x1 being Element of REAL such that
A5: R1 = R19^<*x1*> by FINSEQ_2:117;
R2 is Element of (i+1)-tuples_on REAL by Lm;
then consider R29 being (Element of i-tuples_on REAL),
x2 being Element of REAL such that
A6: R2 = R29^<*x2*> by FINSEQ_2:117;
A7: for j be Nat st j in Seg i holds R19.j <= R29.j
proof
let j be Nat such that
A8: j in Seg i;
Seg len R29 = dom R29 & len R29 = i by CARD_1:def 7,FINSEQ_1:def 3;
then
A9: R29.j = R2.j by A6,A8,FINSEQ_1:def 7;
Seg len R19 = dom R19 & len R19 = i by CARD_1:def 7,FINSEQ_1:def 3;
then R19.j = R1.j by A5,A8,FINSEQ_1:def 7;
hence thesis by A2,A8,A9,FINSEQ_2:8;
end;
A10: R2.(i+1) = x2 by A6,FINSEQ_2:116;
A11: R1.(i+1) = x1 by A5,FINSEQ_2:116;
now
per cases by A3,FINSEQ_2:7;
suppose
A12: j in Seg i;
Seg len R29 = dom R29 & len R29 = i by CARD_1:def 7,FINSEQ_1:def 3;
then
A13: R29.j = R2.j by A6,A12,FINSEQ_1:def 7;
A14: Sum R1 = Sum R19 + x1 & Sum R2 = Sum R29 + x2 by A5,A6,Th74;
A15: x1 <= x2 by A2,A11,A10,FINSEQ_1:4;
Seg len R19 = dom R19 & len R19 = i by CARD_1:def 7,FINSEQ_1:def 3;
then R19.j = R1.j by A5,A12,FINSEQ_1:def 7;
then Sum R19 < Sum R29 by A1,A4,A7,A12,A13;
hence Sum R1 < Sum R2 by A14,A15,XREAL_1:8;
end;
suppose
A16: j = i+1;
A17: Sum R2 = Sum R29 + x2 by A6,Th74;
Sum R19 <= Sum R29 & Sum R1 = Sum R19 + x1 by A5,A7,Th74,Th82;
hence Sum R1 < Sum R2 by A4,A11,A10,A16,A17,XREAL_1:8;
end;
end;
hence Sum R1 < Sum R2;
end;
then
A18: for i be Nat st P[i] holds P[i+1];
A19: P[0];
for i be Nat holds P[i] from NAT_1:sch 2(A19,A18);
hence thesis by A0;
end;
theorem Th84:
(for i be Nat st i in dom F holds 0 <= F.i) implies 0 <= Sum F
proof
reconsider F1 = F as FinSequence of REAL by Lm2;
set i = len F;
set R1 = i|-> In(0,REAL);
reconsider R2 = F1 as Element of i-tuples_on REAL by FINSEQ_2:92;
A1: Seg len F = dom F by FINSEQ_1:def 3;
assume
A2: for i be Nat st i in dom F holds 0 <= F.i;
for j be Nat st j in Seg i holds R1.j <= R2.j
proof let j be Nat;
assume
A3: j in Seg i;
R1.j = In(0,REAL);
hence thesis by A2,A1,A3;
end;
then Sum R1 <= Sum R2 by Th82;
hence thesis by Th81;
end;
theorem Th85:
(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
proof
reconsider F1 = F as FinSequence of REAL by Lm2;
set i = len F, R1 = i|->In(0,REAL);
reconsider R2 = F1 as Element of i-tuples_on REAL by FINSEQ_2:92;
A1: Seg len F = dom F by FINSEQ_1:def 3;
assume
A2: for i be Nat st i in dom F holds 0 <= F.i;
A3: for j be Nat st j in Seg i holds R1.j <= R2.j
proof let j be Nat;
R1.j = In(0,REAL);
hence thesis by A2,A1;
end;
given j be Nat such that
A4: j in dom F and
A5: 0 < F.j;
R1.j = 0;
then Sum R1 < Sum R2 by A1,A3,A4,A5,Th83;
hence thesis by Th81;
end;
theorem Th86:
0 <= Sum sqr F
proof
now
let i be Nat such that i in dom sqr F;
0 <= (F.i)^2 by XREAL_1:63;
hence 0 <= (sqr F).i by VALUED_1:11;
end;
hence thesis by Th84;
end;
theorem Th87:
Sum(r*F) = r*(Sum F)
proof
reconsider F1=F as FinSequence of REAL by Lm2;
reconsider s=r as Element of REAL by XREAL_0:def 1;
set rM = multreal[;](s,id REAL);
thus Sum (r*F) = rM.(addreal $$ F1) by Th3,Th8,SETWOP_2:30
.= r*(Sum F1) by Lm1
.= r*(Sum F);
end;
theorem Th88:
Sum -F = -(Sum F)
proof
reconsider F1=F as FinSequence of REAL by Lm2;
thus Sum -F = compreal.(addreal $$ F1) by Th8,Th9,SETWOP_2:31
.= -(Sum F1) by BINOP_2:def 7
.= -(Sum F);
end;
theorem Th89:
Sum(R1 + R2) = Sum R1 + Sum R2
proof
i is Nat by TARSKI:1;
hence Sum(R1 + R2) = addreal.(addreal$$R1,addreal$$R2) by SETWOP_2:35
.= Sum R1 + Sum R2 by BINOP_2:def 9;
end;
theorem Th90:
Sum(R1 - R2) = Sum R1 - Sum R2
proof
thus Sum(R1 - R2)= Sum R1 + Sum -R2 by Th89
.= Sum R1 +- Sum R2 by Th88
.= Sum R1 - Sum R2;
end;
theorem
Sum sqr R = 0 implies R = i |-> 0
proof
assume
A1: Sum sqr R = 0;
A2: len R = i by CARD_1:def 7;
A3: len(i |-> 0) = i by CARD_1:def 7;
assume R <> i |-> 0;
then consider j be Nat such that
A4: j in dom R and
A5: R.j <> (i |-> 0).j by A2,A3,FINSEQ_2:9;
set x = R.j,x9 = (sqr R).j;
A6: dom R = Seg len R by FINSEQ_1:def 3;
x <> 0 by A5;
then 0 < x^2 by SQUARE_1:12;
then
A7: 0 < x9 by VALUED_1:11;
A8: now
let k such that
k in dom sqr R;
set r = (sqr R).k;
set x = R.k;
0 <= x^2 by XREAL_1:63;
hence 0 <= r by VALUED_1:11;
end;
dom sqr R = Seg len sqr R by FINSEQ_1:def 3;
then j in dom sqr R by A4,A6,FINSEQ_2:33;
hence thesis by A1,A8,A7,Th85;
end;
theorem
(Sum mlt(R1,R2))^2 <= (Sum sqr R1)*(Sum sqr R2)
proof
A0: i is Nat by TARSKI:1;
defpred P[Nat] means for R1,R2 being Element of $1-tuples_on REAL holds (Sum
mlt(R1,R2))^2 <= (Sum sqr R1)*(Sum sqr R2);
A1: for c be Nat st P[c] holds P[c+1]
proof
let c be Nat such that
A2: for R1,R2 being Element of c-tuples_on REAL holds (Sum mlt(R1,R2))
^2 <= (Sum sqr R1)*(Sum sqr R2);
let R1,R2 be Element of (c+1)-tuples_on REAL;
consider R19 being (Element of c-tuples_on REAL),
x1 being Element of REAL such that
A3: R1 = R19^<*x1*> by FINSEQ_2:117;
consider R29 being (Element of c-tuples_on REAL),
x2 being Element of REAL such that
A4: R2 = R29^<*x2*> by FINSEQ_2:117;
A5: for R being Element of c-tuples_on REAL holds
Sum sqr (R^<*r*>) = Sum sqr R + r^2
proof
let R be Element of c-tuples_on REAL;
reconsider s=r as Element of REAL by XREAL_0:def 1;
sqr(R^<*s*>) = (sqrreal*R)^<*sqrreal.s*> by FINSEQOP:8
.= (sqr R)^<*r^2*> by Def2;
hence thesis by Th74;
end;
then
A6: Sum sqr R29 + x2^2 = Sum sqr (R29^<*x2*>)
.= Sum sqr R2 by A4;
(Sum mlt(R19,R29))^2 + (0 qua Element of NAT) <= (Sum sqr R19)*(Sum
sqr R29) by A2;
then
A7: 0 <= (Sum sqr R19)*(Sum sqr R29) - (Sum mlt(R19,R29))^2 by XREAL_1:19;
mlt(R19^<*x1*>,R29^<*x2*>) = (multreal.:(R19,R29))^<*multreal.(x1,x2)
*> by FINSEQOP:10
.= (mlt(R19,R29))^<*x1*x2*> by BINOP_2:def 11;
then
A8: Sum mlt(R19^<*x1*>,R29^<*x2*>) = Sum mlt(R19,R29) + x1*x2 by Th74;
A9: 2*(x1*x2)*Sum mlt(R19,R29) = 2*((x1*x2)*Sum mlt(R19,R29))
.= 2*Sum((x1*x2)*mlt(R19,R29)) by Th87
.= 2*Sum(x1*(x2*mlt(R19,R29))) by RFUNCT_1:17
.= 2*Sum(x1*mlt(R29,x2*R19)) by RFUNCT_1:12
.= 2*Sum(mlt(x1*R29,x2*R19)) by FINSEQOP:26;
A10: -(Sum mlt(R19,R29)+x1*x2)^2 = -(x1*x2)^2+-(2*(x1*x2)*Sum mlt(R19,R29)
+(Sum mlt(R19,R29))^2)
.= -x1^2*x2^2+(-(Sum mlt(R19,R29))^2+ -2*Sum(mlt(x1*R29,x2*R19))) by A9;
A11: 0 <= Sum sqr (x1*R29-x2*R19) by Th86;
A12: (Sum sqr R19 + x1^2)*(Sum sqr R29 + x2^2) = (Sum sqr R19)*(Sum sqr R29
)+(x1^2*(Sum sqr R29)+(Sum sqr R19)*x2^2)+x1^2*x2^2
.= (Sum sqr R19)*(Sum sqr R29)+(Sum(x1^2*sqr R29)+(Sum sqr R19)*x2^2)+
x1^2*x2^2 by Th87
.= (Sum sqr R19)*(Sum sqr R29)+(Sum sqr(x1*R29)+x2^2*(Sum sqr R19))+x1
^2*x2^2 by Th58
.= (Sum sqr R19)*(Sum sqr R29)+(Sum sqr(x1*R29)+Sum (x2^2*sqr R19))+x1
^2*x2^2 by Th87
.= (Sum sqr R19)*(Sum sqr R29)+(Sum sqr(x1*R29)+Sum sqr(x2*R19))+x1^2*
x2^2 by Th58;
A13: Sum sqr(x1*R29)+Sum sqr(x2*R19) + -2*Sum(mlt(x1*R29,x2*R19)) = Sum
sqr(x1*R29)-2*Sum(mlt(x1*R29,x2*R19))+Sum sqr(x2*R19)
.= Sum sqr(x1*R29)-Sum(2*mlt(x1*R29,x2*R19))+Sum sqr(x2*R19) by Th87
.= Sum(sqr(x1*R29)-2*mlt(x1*R29,x2*R19))+Sum sqr(x2*R19) by Th90
.= Sum(sqr (x1*R29)-2*mlt(x1*R29,x2*R19)+sqr(x2*R19)) by Th89;
(Sum sqr R19 + x1^2) = Sum sqr R1 by A3,A5;
then
(Sum sqr R1)*(Sum sqr R2) - (Sum mlt(R1,R2))^2 = (Sum sqr R19 + x1^2)
*(Sum sqr R29 + x2^2) + -(Sum mlt(R19,R29)+x1*x2)^2 by A3,A4,A8,A6
.= (Sum sqr R19)*(Sum sqr R29)+-(Sum mlt(R19,R29))^2 + ((Sum sqr(x1*
R29)+Sum sqr(x2*R19)) +- 2*Sum(mlt(x1*R29,x2*R19))) by A12,A10
.= (Sum sqr R19)*(Sum sqr R29)-(Sum mlt(R19,R29))^2 + Sum sqr (x1*R29-
x2*R19) by A13,Th69;
then (Sum mlt(R1,R2))^2 + (0 qua Element of NAT) <= (Sum sqr R1)*(Sum sqr
R2) by A7,A11,XREAL_1:19;
hence thesis;
end;
A14: P[0];
for i be Nat holds P[i] from NAT_1:sch 2(A14,A1);
hence thesis by A0;
end;
:: The Product of Finite Sequences of Real Numbers
definition
let F be complex-valued FinSequence;
func Product F -> Complex means
:Def13:
ex f being FinSequence of COMPLEX st f = F & it = multcomplex $$ f;
existence
proof
rng F c= COMPLEX by VALUED_0:def 1;
then reconsider f = F as FinSequence of COMPLEX by FINSEQ_1:def 4;
take multcomplex $$ f;
thus thesis;
end;
uniqueness;
end;
registration
let F be real-valued FinSequence;
cluster Product F -> real;
coherence
proof
set mc = multcomplex;
consider f being FinSequence of COMPLEX such that
A1: f = F and
A2: Product F = multcomplex $$ f by Def13;
set g = [#](f,the_unity_wrt mc);
defpred P[Nat] means mc $$ (finSeg $1,[#](f,the_unity_wrt mc)) is real;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: P[k];
reconsider k as Element of NAT by ORDINAL1:def 12;
g.(k+1) is real
proof
per cases;
suppose
k+1 in dom f;
then g.(k+1) = f.(k+1) by SETWOP_2:20;
hence thesis by A1;
end;
suppose
not k+1 in dom f;
hence thesis by BINOP_2:6,SETWOP_2:20;
end;
end;
then reconsider a = g.(k+1), b = mc $$(finSeg k,g) as Real by A4;
not (k + 1) in Seg k by FINSEQ_3:8;
then mc $$ (finSeg k \/ {.In(k+1,NAT).},g)
= mc.(mc $$(finSeg k,g),g.(k+1)) by
SETWOP_2:2
.= b * a by BINOP_2:def 5;
hence thesis by FINSEQ_1:9;
end;
A5: mc $$ f = mc $$ (findom f,[#](f,the_unity_wrt mc)) & ex n being Nat st
dom f = Seg n by FINSEQ_1:def 2,SETWOP_2:def 2;
Seg 0 = {}.NAT;
then
A6: P[0] by BINOP_2:6,SETWISEO:31;
for n being Nat holds P[n] from NAT_1:sch 2(A6,A3);
hence thesis by A2,A5;
end;
end;
theorem Th93:
for F being FinSequence of REAL holds Product F = multreal $$ F
proof
set g = multreal, h = multcomplex;
let F be FinSequence of REAL;
rng F c= COMPLEX by NUMBERS:11,XBOOLE_1:1;
then reconsider f = F as FinSequence of COMPLEX by FINSEQ_1:def 4;
defpred P[Nat] means g $$ (finSeg $1,[#](F,the_unity_wrt g)) = h $$ (finSeg
$1,[#](f,the_unity_wrt h));
consider n being Nat such that
A1: dom f = Seg n by FINSEQ_1:def 2;
A2: g $$ F = g $$ (finSeg n,[#](F,the_unity_wrt g)) & h $$ f = h $$ (finSeg
n, [#](f,the_unity_wrt h)) by A1,SETWOP_2:def 2;
A3: for k being Nat st P[k] holds P[k+1]
proof
set j = [#](f,the_unity_wrt h);
set i = [#](F,the_unity_wrt g);
let k be Nat;
assume
A4: P[k];
A5: i.(k+1) = j.(k+1)
proof
per cases;
suppose
A6: k+1 in dom f;
then j.(k+1) = F.(k+1) by SETWOP_2:20
.= i.(k+1) by A6,SETWOP_2:20;
hence thesis;
end;
suppose
A7: not k+1 in dom f;
then j.(k+1) = the_unity_wrt h by SETWOP_2:20
.= i.(k+1) by A7,BINOP_2:6,7,SETWOP_2:20;
hence thesis;
end;
end;
A8: not (k + 1) in Seg k by FINSEQ_3:8;
reconsider k as Element of NAT by ORDINAL1:def 12;
g $$ (finSeg (k+1),i)
= g $$ (finSeg k \/ {.In(k+1,NAT).},i) by FINSEQ_1:9
.= g.(g $$(finSeg k,i),i.(k+1)) by A8,SETWOP_2:2
.= g $$(finSeg k,i) * (i.(k+1)) by BINOP_2:def 11
.= h.(h $$(finSeg k,j),j.(k+1)) by A4,A5,BINOP_2:def 5
.= h $$ (finSeg k \/ {.In(k+1,NAT).},j) by A8,SETWOP_2:2
.= h $$ (finSeg (k+1),j) by FINSEQ_1:9;
hence thesis;
end;
A9: Seg 0 = {}.NAT;
then g $$ (finSeg 0,[#](F,the_unity_wrt g)) = the_unity_wrt h by BINOP_2:6,7
,SETWISEO:31
.= h $$ (finSeg 0,[#](f,the_unity_wrt h)) by A9,SETWISEO:31;
then
A10: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A10,A3);
then g $$ F = h $$ f by A2;
hence thesis by Def13;
end;
definition
let F be FinSequence of COMPLEX;
redefine func Product F -> Element of COMPLEX equals :: redefines Product (RVSUM_1, definition)
multcomplex $$ F;
coherence by XCMPLX_0:def 2;
compatibility by Def13;
end;
definition
let F be FinSequence of REAL;
redefine func Product F -> Real equals :: redefines Product (RVSUM_1, definition)
multreal $$ F;
coherence;
compatibility by Th93;
end;
Lm3: for F being empty FinSequence holds Product F = 1
proof
Product <*>REAL = 1 by BINOP_2:7,FINSOP_1:10;
hence thesis;
end;
theorem Th94:
Product <*>REAL = 1 by Lm3;
registration
let r be Complex;
cluster <*r*> -> complex-valued;
coherence;
end;
registration
let r1, r2 be Complex;
cluster <*r1, r2*> -> complex-valued;
coherence;
end;
registration
let r1, r2, r3 be Complex;
cluster <*r1, r2, r3*> -> complex-valued;
coherence;
end;
registration
let j be natural Number, c be Complex;
cluster j |-> c -> complex-valued;
coherence;
end;
theorem Th95:
for r being Complex holds Product <*r*> = r
proof
let r be Complex;
reconsider r9 = r as Element of COMPLEX by XCMPLX_0:def 2;
reconsider F = <*r9*> as FinSequence of COMPLEX;
multcomplex $$ F = r by FINSOP_1:11;
hence thesis by Def13;
end;
registration let c be Complex;
reduce Product <*c*> to c;
reducibility by Th95;
end;
registration
let f, g be complex-valued FinSequence;
cluster f ^ g -> complex-valued;
coherence;
end;
theorem Th96:
for F being complex-valued FinSequence, r being Complex holds
Product (F^<*r*>) = Product F * r
proof
let F be complex-valued FinSequence, r be Complex;
reconsider p = r as Element of COMPLEX by XCMPLX_0:def 2;
rng F c= COMPLEX & rng (F^<*p*>) c= COMPLEX by VALUED_0:def 1;
then reconsider Fr = F^<*r*>, Ff = F as FinSequence of COMPLEX
by FINSEQ_1:def 4;
thus Product (F^<*r*>) = multcomplex $$ Fr by Def13
.= multcomplex.(Product Ff,p) by FINSOP_1:4
.= Product F * r by BINOP_2:def 5;
end;
theorem Th97:
for F1, F2 being complex-valued FinSequence holds
Product (F1^F2) = Product F1 * Product F2
proof
let F1, F2 be complex-valued FinSequence;
A1: rng (F1^F2) c= COMPLEX by VALUED_0:def 1;
rng F1 c= COMPLEX & rng F2 c= COMPLEX by VALUED_0:def 1;
then reconsider FF = F1^F2, f1 = F1, f2 = F2 as FinSequence of COMPLEX
by A1,FINSEQ_1:def 4;
thus Product (F1^F2) = multcomplex $$ FF by Def13
.= multcomplex.(Product f1,Product f2) by FINSOP_1:5
.= Product F1 * Product F2 by BINOP_2:def 5;
end;
theorem
Product (<*r*>^F) = r * Product F
proof
thus Product (<*r*>^F) = Product <*r*> * Product F by Th97
.= r * Product F;
end;
theorem Th99:
for r1, r2 being Complex holds Product <*r1,r2*> = r1 * r2
proof
let r1, r2 be Complex;
thus Product <*r1,r2*> = Product <*r1*> * r2 by Th96
.= r1 * r2;
end;
theorem
for r1, r2, r3 being Complex holds Product <*r1,r2,r3*> = r1 * r2 * r3
proof
let r1, r2, r3 be Complex;
thus Product <*r1,r2,r3*> = Product <*r1,r2*> * r3 by Th96
.= r1 * r2 * r3 by Th99;
end;
theorem
for R being Element of 0-tuples_on REAL holds Product R = 1 by Lm3;
theorem
Product (i|->1) = 1
proof
i is Nat by TARSKI:1;
then Product (i |-> the_unity_wrt multreal) = the_unity_wrt multreal
by SETWOP_2:25;
hence thesis by BINOP_2:7;
end;
Lm4: for p being complex-valued FinSequence st len p <> 0 ex q being
complex-valued FinSequence, d being Complex st p = q^<*d*>
proof
let p be complex-valued FinSequence;
assume len p <> 0;
then consider q being FinSequence,d being object such that
A1: p = q^<*d*> by CARD_1:27,FINSEQ_1:46;
for i be Nat st i in dom q holds q.i in COMPLEX
proof
let i be Nat;
assume i in dom q;
then p.i = q.i & i in dom p by A1,FINSEQ_1:def 7,FINSEQ_2:15;
hence thesis by FINSEQ_2:11;
end;
then
A3: q is FinSequence of COMPLEX by FINSEQ_2:12;
len p = len q + 1 by A1,FINSEQ_2:16;
then p.(len p) = d by A1,FINSEQ_1:42;
hence thesis by A1,A3;
end;
theorem
for F being complex-valued FinSequence holds
(ex k st k in dom F & F.k = 0) iff Product F = 0
proof
defpred P[Nat] means for F being complex-valued FinSequence st len F = $1
holds (ex k st k in Seg $1 & F.k = 0) iff Product F = 0;
let F be complex-valued FinSequence;
A1: Seg len F = dom F by FINSEQ_1:def 3;
A2: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A3: for F being complex-valued FinSequence st len F = i holds (ex k
st k in Seg i & F.k = 0) iff Product F = 0;
let F be complex-valued FinSequence;
assume
A4: len F = i+1;
then consider
F9 being complex-valued FinSequence, x being Complex
such that
A5: F = F9^<*x*> by Lm4;
A6: len F = len F9 + 1 by A5,FINSEQ_2:16;
A7: Product F = Product F9 * x by A5,Th96;
thus (ex k st k in Seg (i+1) & F.k = 0) implies Product F = 0
proof
given k such that
A8: k in Seg (i+1) and
A9: F.k = 0;
now
per cases by A8,FINSEQ_2:7;
suppose
A10: k in Seg i;
Seg len F9 = dom F9 by FINSEQ_1:def 3;
then F9.k = F.k by A4,A5,A6,A10,FINSEQ_1:def 7;
then Product F9 = 0 by A3,A4,A6,A9,A10;
hence thesis by A7;
end;
suppose
k = i+1;
then x = 0 by A4,A5,A6,A9,FINSEQ_1:42;
hence thesis by A7;
end;
end;
hence thesis;
end;
assume
A11: Product F = 0;
per cases by A7,A11;
suppose
Product F9 = 0;
then consider k such that
A12: k in Seg i and
A13: F9.k = 0 by A3,A4,A6;
Seg len F9 = dom F9 by FINSEQ_1:def 3;
then F.k = 0 by A4,A5,A6,A12,A13,FINSEQ_1:def 7;
hence thesis by A12,FINSEQ_2:8;
end;
suppose
x = 0;
then F.(i+1) = 0 by A4,A5,A6,FINSEQ_1:42;
hence thesis by FINSEQ_1:4;
end;
end;
A14: P[0] proof let F be complex-valued FinSequence;
assume len F = 0;
then F = <*>COMPLEX;
hence thesis by Th94;
end;
for i be Nat holds P[i] from NAT_1:sch 2(A14,A2);
hence thesis by A1;
end;
theorem
Product ((i+j) |->r ) = (Product (i|->r))*(Product (j|->r))
proof
reconsider i,j as Nat by TARSKI:1;
reconsider s=r as Element of REAL by XREAL_0:def 1;
Product ((i+j) |->s) = multreal.(multreal$$(i|->s),multreal$$(j|->s))
by SETWOP_2:26
.= (Product (i|->s))*(Product (j|->s)) by BINOP_2:def 11;
hence thesis;
end;
theorem
Product ((i*j) |->r) = Product (j |-> (Product (i|->r)))
proof
reconsider r as Element of REAL by XREAL_0:def 1;
reconsider pr = Product (i|->r) as Element of REAL;
i is Nat & j is Nat by TARSKI:1;
then Product ((i*j) |->r) = Product (j |-> pr) by SETWOP_2:27;
hence thesis;
end;
theorem
Product (i|->(r1*r2)) = (Product (i|->r1))*(Product (i|->r2))
proof
reconsider i as Nat by TARSKI:1;
reconsider s1=r1, s2=r2 as Element of REAL by XREAL_0:def 1;
reconsider ss=s1*s2 as Element of REAL;
Product (i|->(ss)) = multreal$$(i|->multreal.(s1,s2)) by BINOP_2:def 11
.= multreal.(multreal$$(i|->s1),multreal$$(i|->s2)) by SETWOP_2:36
.= (Product (i|->s1))*(Product (i|->s2)) by BINOP_2:def 11;
hence thesis;
end;
theorem Th107:
Product mlt(R1,R2) = Product R1 * Product R2
proof
i is Nat by TARSKI:1;
hence Product (mlt(R1,R2)) = multreal.(multreal$$R1,multreal$$R2)
by SETWOP_2:35
.= Product R1 * Product R2 by BINOP_2:def 11;
end;
theorem
Product (r*R) = Product (i|->r) * Product R
proof
reconsider s=r as Element of REAL by XREAL_0:def 1;
thus Product (r*R) = Product mlt(i|->s,R) by Th63
.= Product (i|->r) * Product R by Th107;
end;
theorem
Product sqr R = (Product R)^2 by Th107;
begin :: Addenda
:: 2006.07.13, A.T.
reserve z,z1,z2 for Element of COMPLEX;
theorem
for F being FinSequence of COMPLEX holds Product F = multcomplex $$ F;
theorem
Product ((i+j) |->z) = (Product (i|->z))*(Product (j|->z))
proof
reconsider i,j as Nat by TARSKI:1;
Product ((i+j) |->z) = multcomplex.(multcomplex$$(i|->z),multcomplex$$(j
|->z)) by SETWOP_2:26
.= (Product (i|->z))*(Product (j|->z)) by BINOP_2:def 5;
hence thesis;
end;
theorem
Product ((i*j) |->z) = Product (j |-> (Product (i|->z)))
proof
i is Nat & j is Nat by TARSKI:1;
hence thesis by SETWOP_2:27;
end;
Lm5: for F being complex-valued FinSequence holds F is FinSequence of COMPLEX
proof
let F be complex-valued FinSequence;
thus rng F c= COMPLEX by VALUED_0:def 1;
end;
theorem
Product (i|->(z1*z2)) = (Product (i|->z1))*(Product (i|->z2))
proof
reconsider i as Nat by TARSKI:1;
reconsider zz = i|->(z1*z2) as FinSequence of COMPLEX by Lm5;
Product (i|->(z1*z2)) = Product zz
.= multcomplex$$(i|->multcomplex.(z1,z2)) by BINOP_2:def 5
.= multcomplex.(multcomplex$$(i|->z1),multcomplex$$(i|->z2)) by SETWOP_2:36
.= (Product (i|->z1))*(Product (i|->z2)) by BINOP_2:def 5;
hence thesis;
end;
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 Th114:
for x being real-valued FinSequence holds len (-x)=len x
proof
let x be real-valued FinSequence;
dom (-x)=dom x by VALUED_1:8;
hence thesis by FINSEQ_3:29;
end;
theorem Th115:
for x1,x2 being real-valued FinSequence st len x1=len x2 holds
len (x1+x2)=len x1
proof
let x1,x2 be real-valued FinSequence;
set n=len x1;
A1: x2 is FinSequence of REAL by Lm2;
x1 is FinSequence of REAL by Lm2;
then reconsider z1=x1 as Element of (len x1)-tuples_on REAL by FINSEQ_2:92;
assume len x1=len x2;
then reconsider z2=x2 as Element of n-tuples_on REAL by A1,FINSEQ_2:92;
dom (z1+z2)=Seg n by FINSEQ_2:124;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th116:
for x1,x2 being real-valued FinSequence st len x1=len x2 holds
len (x1-x2)=len x1
proof
let x1,x2 be real-valued FinSequence;
set n=len x1;
A1: x2 is FinSequence of REAL by Lm2;
x1 is FinSequence of REAL by Lm2;
then reconsider z1=x1 as Element of (len x1)-tuples_on REAL by FINSEQ_2:92;
assume len x1=len x2;
then reconsider z2=x2 as Element of n-tuples_on REAL by A1,FINSEQ_2:92;
dom (z1-z2)=Seg n by FINSEQ_2:124;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th117:
for a being Real, x being real-valued FinSequence
holds len (a*x)=len x
proof
let a be Real, x be real-valued FinSequence;
set n=len x;
x is FinSequence of REAL by Lm2;
then reconsider z=x as Element of n-tuples_on REAL by FINSEQ_2:92;
len (a*z)=n by CARD_1:def 7;
hence thesis;
end;
theorem Th118:
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)
proof
let x,y,z be real-valued FinSequence;
A1:x is FinSequence of REAL & y is FinSequence of REAL &
z is FinSequence of REAL by Lm2;
assume len x=len y & len y=len z;
then reconsider x2=x, y2=y, z2=z as Element of (len x)-tuples_on REAL by A1,
FINSEQ_2:92;
A2: dom (mlt(x+y,z))=Seg len(mlt(x2+y2,z2)) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7
.=Seg len (mlt(x2,z2)+mlt(y2,z2)) by CARD_1:def 7
.= dom (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_1:def 3;
A3: dom (mlt(x,z))=Seg len(mlt(x2,z2)) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7
.=Seg len (mlt(x2,z2)+mlt(y2,z2)) by CARD_1:def 7
.= dom (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_1:def 3;
for i being Nat st i in dom (mlt(x+y,z)) holds mlt(x+y,z).i=(mlt(x,z)+
mlt(y,z)).i
proof
let i be Nat;
assume
A4: i in dom mlt(x+y,z);
set a=x.i, b=y.i, d=(x+y).i, e=z.i;
len (x2+y2)=len x by CARD_1:def 7;
then dom (x2+y2)=Seg len x by FINSEQ_1:def 3
.=Seg len(mlt(x2,z2)) by CARD_1:def 7
.=dom (mlt(x,z)) by FINSEQ_1:def 3;
then
A5: d=a+b by A2,A3,A4,VALUED_1:def 1;
thus mlt(x+y,z).i=d*e by VALUED_1:5
.=a*e+b*e by A5
.=mlt(x,z).i +b*e by VALUED_1:5
.=mlt(x,z).i +mlt(y,z).i by VALUED_1:5
.=(mlt(x,z)+mlt(y,z)).i by A2,A4,VALUED_1:def 1;
end;
hence thesis by A2,FINSEQ_1:13;
end;
begin :: Inner Product of Finite Sequences
definition
let x1,x2 be real-valued FinSequence;
func |( x1,x2 )| -> Real equals
Sum mlt(x1,x2);
correctness;
commutativity;
end;
theorem Th119:
for x being real-valued FinSequence holds |(x,x)| >= 0
proof
let x be real-valued FinSequence;
set n=len x;
x is FinSequence of REAL by Lm2;
then reconsider w = x as Element of n-tuples_on REAL by FINSEQ_2:92;
|(x, x)| = Sum sqr(w);
hence thesis by Th86;
end;
theorem Th120:
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)|
proof
let x,y,z be real-valued FinSequence;
A1:x is FinSequence of REAL & y is FinSequence of REAL &
z is FinSequence of REAL by Lm2;
assume
A2: len x=len y & len y=len z;
then reconsider x2=x,y2=y,z2=z as Element of (len x)-tuples_on REAL by A1,
FINSEQ_2:92;
|((x+y),z)|= Sum(mlt(x,z)+mlt(y,z)) by A2,Th118
.= Sum(mlt(x2,z2))+Sum(mlt(y2,z2)) by Th89
.= |(x,z)| + |(y,z)|;
hence thesis;
end;
theorem Th121:
for x,y being real-valued FinSequence,a being Real st len x=
len y holds |(a*x,y)| = a*|(x,y)|
proof
let x,y be real-valued FinSequence,a be Real;
reconsider a2=a as Element of REAL by XREAL_0:def 1;
A1:x is FinSequence of REAL & y is FinSequence of REAL by Lm2;
assume len x=len y;
then reconsider x2=x, y2 = y as Element of (len x)-tuples_on REAL by A1,
FINSEQ_2:92;
|(a*x,y)| =Sum(a2*mlt(x2,y2)) by FINSEQOP:26
.=a*|(x,y)| by Th87;
hence thesis;
end;
theorem Th122:
for x1,x2 being real-valued FinSequence st len x1=len x2 holds
|(-x1, x2)| = -|(x1, x2)|
proof
let x1,x2 be real-valued FinSequence;
assume len x1=len x2;
then |(-x1, x2)| = (-1)*|(x1, x2)| by Th121;
hence thesis;
end;
theorem
for x1,x2 being real-valued FinSequence st len x1=len x2 holds
|(-x1, -x2)| = |(x1, x2)|
proof
let x1,x2 be real-valued FinSequence;
assume
A1: len x1=len x2;
then len (-x2)=len x1 by Th114;
then |(-x1, -x2)| = -|(x1, -x2)| by Th122
.= --|(x1, x2)| by A1,Th122;
hence thesis;
end;
theorem Th124:
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)|
proof
let x1,x2,x3 be real-valued FinSequence;
assume that
A1: len x1=len x2 and
A2: len x2=len x3;
len (-x2)=len x2 by Th114;
then |(x1 - x2, x3)| = |(x1, x3)| + |(-x2, x3)| by A1,A2,Th120
.= |(x1, x3)| + - |(x2, x3)| by A2,Th122;
hence thesis;
end;
theorem
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)|
proof
let x,y be Real,x1,x2,x3 be real-valued FinSequence;
assume that
A1: len x1=len x2 and
A2: len x2=len x3;
len (x*x1)=len x1 & len (y*x2)=len x2 by Th117;
then |(x*x1 + y*x2, x3)| = |(x*x1, x3)| + |(y*x2, x3)| by A1,A2,Th120
.= x*|(x1,x3)| + |(y*x2,x3)| by A1,A2,Th121
.= x*|(x1,x3)| + y*|(x2,x3)| by A2,Th121;
hence thesis;
end;
theorem Th126:
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)|
proof
let x1,x2,y1,y2 be real-valued FinSequence;
assume that
A1: len x1=len x2 and
A2: len x2=len y1 and
A3: len y1=len y2;
|(x1+x2, y2)| = |(x1, y2)| + |(x2, y2)| by A1,A2,A3,Th120;
then
A4: |(x1+x2, y1)| +|(x1+x2, y2)| = (|(x1, y1)|+|(x2, y1)|) + (|(x1, y2)| +
|(x2, y2)|) by A1,A2,Th120;
len (x1+x2)=len x1 by A1,Th115;
hence thesis by A1,A2,A3,A4,Th120;
end;
theorem Th127:
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)|
proof
let x1,x2,y1,y2 be real-valued FinSequence;
assume that
A1: len x1=len x2 and
A2: len x2=len y1 and
A3: len y1=len y2;
|(x1,y1-y2)| = |(x1,y1)| - |(x1,y2)| by A1,A2,A3,Th124;
then
A4: |(x1,y1-y2)| - |(x2,y1-y2)| = (|(x1,y1)|-|(x1,y2)|)-(|(x2,y1)|-|(x2,y2)|
) by A2,A3,Th124;
len (y1 - y2)=len y1 by A3,Th116;
hence thesis by A1,A2,A4,Th124;
end;
theorem
for x,y being real-valued FinSequence st len x=len y holds |(x+y, x+
y)| = |(x, x)| + 2*|(x, y)| + |(y, y)|
proof
let x,y be real-valued FinSequence;
A1: |(x, x)| + |(x, y)| + |(x, y)| = |(x, x)| + 2*|(x, y)|;
assume len x=len y;
hence thesis by A1,Th126;
end;
theorem
for x,y being real-valued FinSequence st len x=len y holds |(x-y, x-
y)| = |(x, x)| - 2*|(x, y)| + |(y, y)|
proof
let x,y be real-valued FinSequence;
assume len x=len y;
then |(x-y, x-y)| = |(x,x)| - |(x,y)| - |(y,x)| + |(y, y)| by Th127
.= |(x,x)| - 2*|(x,y)| + |(y, y)|;
hence thesis;
end;
theorem Th130:
|(p1 + p2, p3)| = |(p1, p3)| + |(p2, p3)|
proof
reconsider f1=p1, f2=p2, f3=p3 as real-valued FinSequence;
len f2=n by CARD_1:def 7;
then len f1=len f2 & len f2=len f3 by CARD_1:def 7;
hence thesis by Th120;
end;
theorem Th131:
for x being Real holds |(x*p1, p2)| = x*|(p1, p2)|
proof
let x be Real;
reconsider f1=p1,f2=p2 as real-valued FinSequence;
len f1=n & len f2=n by CARD_1:def 7;
hence thesis by Th121;
end;
theorem Th132:
|(-p1, p2)| = -|(p1, p2)|
proof
|(-p1, p2)| = |((-1)*p1, p2)| .= (-1)*|(p1, p2)| by Th131;
hence thesis;
end;
theorem
|(-p1, -p2)| = |(p1, p2)|
proof
|(-p1, -p2)| = -|(p1, -p2)| by Th132
.= --|(p1, p2)| by Th132;
hence thesis;
end;
theorem Th134:
|(p1-p2, p3)| = |(p1, p3)| - |(p2, p3)|
proof
|(p1 - p2, p3)| = |(p1, p3)| + |(-p2, p3)| by Th130
.= |(p1, p3)| + - |(p2, p3)| by Th132;
hence thesis;
end;
theorem
|((x*p1+y*p2), p3)| = x*|(p1,p3)| + y*|(p2,p3)|
proof
|(x*p1 + y*p2, p3)| = |(x*p1, p3)| + |(y*p2, p3)| by Th130
.= x*|(p1,p3)| + |(y*p2,p3)| by Th131
.= x*|(p1,p3)| + y*|(p2,p3)| by Th131;
hence thesis;
end;
theorem Th136:
|(p1+p2, q1+q2)| = |(p1, q1)| + |(p1, q2)| + |(p2, q1)| + |(p2, q2)|
proof
A1: |(p1+p2, q1)| = |(p1, q1)| + |(p2, q1)| & |(p1+p2, q2)| = |(p1, q2)| +
|(p2, q2)| by Th130;
|(p1+p2, q1+q2)| = |(p1+p2, q1)| + |(p1+p2, q2)| by Th130
.= |(p1, q1)|+|(p1, q2)|+|(p2, q1)|+|(p2, q2)| by A1;
hence thesis;
end;
theorem Th137:
|(p1-p2, q1-q2)| = |(p1, q1)| - |(p1, q2)| - |(p2, q1)| + |(p2, q2)|
proof
A1: |(p1,q1-q2)| = |(p1,q1)| - |(p1,q2)| & |(p2,q1-q2)| = |(p2,q1)| - |(p2,
q2)| by Th134;
|(p1-p2, q1-q2)| = |(p1, q1-q2)| - |(p2, q1-q2)| by Th134
.= |(p1,q1)|-|(p1,q2)|-|(p2,q1)|+|(p2,q2)| by A1;
hence thesis;
end;
theorem
|(p+q, p+q)| = |(p, p)| + 2*|(p, q)| + |(q, q)|
proof
|(p, p)| + |(p, q)| + |(p, q)| = |(p, p)| + 2*|(p, q)|;
hence thesis by Th136;
end;
theorem Th139:
|(p-q, p-q)| = |(p, p)| - 2*|(p, q)| + |(q, q)|
proof
|(p-q, p-q)| = |(p,p)| - |(p,q)| - |(p,q)| + |(q, q)| by Th137
.= |(p,p)| - 2*|(p,q)| + |(q, q)|;
hence thesis;
end;
theorem
|(p,q)| <= |(p,p)| + |(q,q)|
proof
0 <= |(p,p)| & 0 <= |(q,q)| by Th119;
then
A1: 0/2 <= (|(p,p)| + |(q,q)|)/2;
|(p-q, p-q)| = |(p,p)| - 2*|(p,q)| + |(q,q)| by Th139
.= |(p,p)| + |(q,q)| - 2*|(p,q)|;
then 2*|(p,q)| <= |(p,p)| + |(q,q)| - 0 by Th119,XREAL_1:11;
then (2*|(p,q)|)/2 <= (|(p,p)| + |(q,q)|)/2 by XREAL_1:72;
then (0 qua Element of NAT) + |(p,q)|
<= (|(p,p)| + |(q,q)|)/2 + (|(p,p)| + |(q,q)|)/2 by A1,XREAL_1:7;
hence thesis;
end;
definition
let p, q be real-valued FinSequence;
pred p,q are_orthogonal means
|(p,q)| = 0;
symmetry;
end;
theorem
p, q are_orthogonal implies a*p,q are_orthogonal
proof
assume p, q are_orthogonal;
then |(p,q)|=0;
then a*(|(p,q)|)=0;
then |(a*p,q)|=0 by Th131;
hence thesis;
end;
:: 2009.08.15, from TURING_0, A.T.
theorem
Sum<*r1,r2,r3,r4*> = r1 + r2 + r3 + r4
proof
thus Sum<*r1,r2,r3,r4*> = Sum<*r1,r2,r3*> + r4 by Th74
.= r1 + r2 + r3 + r4 by Th78;
end;
:: from TOPREAL7, 2011.07.31, A.T.
reserve f,g for real-valued FinSequence;
theorem Th143:
len f = len sqr f & dom f = dom sqr f
proof
rng f c= REAL & dom sqrreal = REAL by FUNCT_2:def 1;
hence len f = len (sqrreal*f) by FINSEQ_2:29
.= len sqr f;
hence thesis by FINSEQ_3:29;
end;
theorem
sqr (f^g) = sqr f ^ sqr g
proof
A1: len f = len sqr f by Th143;
A2: len sqr (f^g) = len (f^g) by Th143;
A3: len g = len sqr g & len(f^g) = len f + len g by Th143,FINSEQ_1:22;
A4: for i be Nat st 1 <= i & i <= len sqr (f^g) holds sqr (f^g).i = (sqr f ^
sqr g).i
proof
let i be Nat;
assume that
A5: 1 <= i and
A6: i <= len sqr (f^g);
A7: i in dom (f^g) by A2,A5,A6,FINSEQ_3:25;
per cases;
suppose
A8: i in dom f;
then
A9: i in dom sqr f by Th143;
thus sqr (f^g).i = (sqrreal*(f^g)).i
.= sqrreal.((f^g).i) by A7,FUNCT_1:13
.= sqrreal.(f.i) by A8,FINSEQ_1:def 7
.= (f.i)^2 by Def2
.= (sqr f).i by VALUED_1:11
.= (sqr f ^ sqr g).i by A9,FINSEQ_1:def 7;
end;
suppose
not i in dom f;
then
A10: len f < i by A5,FINSEQ_3:25;
then reconsider j = i - len f as Element of NAT by INT_1:5;
A11: i <= len(f^g) by A6,Th143;
A12: i <= len(sqr f ^ sqr g) by A1,A3,A2,A6,FINSEQ_1:22;
thus sqr (f^g).i = (sqrreal*(f^g)).i
.= sqrreal.((f^g).i) by A7,FUNCT_1:13
.= sqrreal.(g.j) by A10,A11,FINSEQ_1:24
.= (g.j)^2 by Def2
.= (sqr g).j by VALUED_1:11
.= (sqr f ^ sqr g).i by A1,A10,A12,FINSEQ_1:24;
end;
end;
len (sqr (f^g)) = len (sqr f ^ sqr g) by A1,A3,A2,FINSEQ_1:22;
hence thesis by A4;
end;
theorem
for F being real-valued FinSequence holds F is FinSequence of REAL
proof
let F be real-valued FinSequence;
thus rng F c= REAL;
end;
theorem
for F being complex-valued FinSequence holds F is FinSequence of COMPLEX
by Lm5;
registration
let r be natural Number;
cluster <*r*> -> natural-valued;
coherence;
end;
registration
let r1, r2 be natural Number;
cluster <*r1, r2*> -> natural-valued;
coherence;
end;
registration
let r1, r2, r3 be natural Number;
cluster <*r1, r2, r3*> -> natural-valued;
coherence;
end;
registration
let f, g be natural-valued FinSequence;
cluster f ^ g -> natural-valued;
coherence;
end;