:: Flexary Operations
:: by Karol P\kak
::
:: Received March 26, 2015
:: Copyright (c) 2015-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, ORDINAL1, REAL_1, SUBSET_1, CARD_1, ARYTM_3, TARSKI,
RELAT_1, XXREAL_0, XCMPLX_0, ARYTM_1, XBOOLE_0, FINSET_1, FUNCT_1, NAT_1,
FUNCOP_1, PARTFUN1, FINSEQ_1, VALUED_0, CARD_3, MEMBERED, RFINSEQ2,
AFINSQ_1, NEWTON, PRE_POLY, FOMODEL0, ORDINAL4, ORDINAL2, VALUED_2,
GOBRD13, UPROOTS, FUNCT_6, FUNCT_2, FINSEQ_2, XREAL_0, SETWISEO,
CLASSES1, FUNCT_4, BINOP_1, BINOP_2, FINSOP_1, POWER, NUMERAL1, ALGSTR_0,
MONOID_0, FLEXARY1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0,
XREAL_0, MEMBERED, RELAT_1, FUNCT_1, RELSET_1, MONOID_0, PARTFUN1,
FUNCT_2, BINOP_1, XXREAL_0, NAT_1, CARD_3, FUNCOP_1, SETWISEO, FINSEQ_2,
FINSEQ_1, FINSEQOP, VALUED_0, VALUED_2, SETWOP_2, FINSET_1, RVSUM_1,
CLASSES1, XXREAL_2, PRE_POLY, RFINSEQ2, FUNCT_6, NAT_D, MATRIX_0,
FUNCT_7, FOMODEL2, WSIERP_1, BINOP_2, NEWTON, POWER, FINSOP_1, AFINSQ_1,
AFINSQ_2, NUMERAL1, STRUCT_0, ALGSTR_0;
constructors XXREAL_2, PRE_POLY, ABIAN, RFINSEQ2, CLASSES1, MONOID_0, NAT_D,
VALUED_2, FOMODEL2, RELSET_1, WSIERP_1, SETWISEO, BINOP_2, FINSEQOP,
FINSOP_1, NEWTON, POWER, RECDEF_1, AFINSQ_2, NUMERAL1, JORDAN1H;
registrations ORDINAL1, XREAL_0, FUNCT_1, FINSEQ_1, FINSEQ_2, VALUED_0,
FUNCT_7, PRE_POLY, NAT_1, INT_6, RVSUM_1, XCMPLX_0, MEMBERED, VALUED_2,
FOMODEL0, XBOOLE_0, RELAT_1, FUNCT_2, FUNCOP_1, CARD_1, XXREAL_2,
EUCLID_9, FINSET_1, XXREAL_0, NUMBERS, BINOP_2, INT_1, NEWTON, POWER,
AFINSQ_1, AFINSQ_2;
requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, FUNCT_1, VALUED_0;
equalities FINSEQ_1, FINSEQ_2, XCMPLX_0;
expansions FINSEQ_1, TARSKI, XBOOLE_0, FUNCT_1;
theorems AFINSQ_1, AFINSQ_2, ALGSTR_0, CARD_1, CARD_3, CLASSES1, FINSEQ_1,
FINSEQ_2, FINSEQ_3, FINSEQ_5, FINSEQOP, FINSOP_1, FOMODEL2, FUNCOP_1,
FUNCT_1, FUNCT_2, FUNCT_6, FUNCT_7, GRAPHSP, INTEGRA2, MATRIX_0,
MONOID_0, NAT_1, NAT_D, NEWTON, NUMERAL1, ORDINAL1, PARTFUN1, PEPIN,
PRE_POLY, PREPOWER, RELAT_1, RFINSEQ, RFINSEQ2, RVSUM_1, RVSUM_2, TARSKI,
VALUED_0, VALUED_2, XBOOLE_0, XBOOLE_1, XCMPLX_0, XREAL_0, XREAL_1,
XXREAL_0, XXREAL_2, ZFMISC_1;
schemes CLASSES1, FINSEQ_1, FUNCT_2, NAT_1;
begin :: Auxiliary Facts about Finite Sequences Concatenation
reserve x,y for object,
D,D1,D2 for non empty set,
i,j,k,m,n for Nat,
f,g for FinSequence of D*,
f1 for FinSequence of D1*,
f2 for FinSequence of D2*;
Lm1:
f={} implies D-concatenation "**" f={}
proof
assume A1:f={};
(D-concatenation) is having_a_unity by MONOID_0:67;
then (D-concatenation) "**" f = the_unity_wrt (D-concatenation)
by A1,FINSOP_1:def 1
.= {} by MONOID_0:67;
hence thesis;
end;
theorem Th1:
for F be Function-yielding Function, a be object holds
a in Values F
iff
ex x,y st x in dom F & y in dom (F.x) & a = F.x.y
proof
let F be Function-yielding Function, a be object;
A1:Values F = Union rngs F by MATRIX_0:def 9
.= union rng rngs F by CARD_3:def 4;
A2:dom rngs F = dom F by FUNCT_6:def 3;
thus a in Values F implies ex x,y be object st x in dom F & y in dom (F.x) &
a = F.x.y
proof
assume a in Values F;
then consider y be set such that
A3: a in y & y in rng rngs F by A1,TARSKI:def 4;
consider z be object such that
A4: z in dom rngs F & (rngs F).z = y by A3,FUNCT_1:def 3;
y = rng (F.z) by A2,A4,FUNCT_6:def 3;
then ex x be object st x in dom (F.z) & a=(F.z).x by A3,FUNCT_1:def 3;
hence thesis by A2,A4;
end;
given x,y be object such that
A5: x in dom F & y in dom (F.x) & a = F.x.y;
(rngs F).x = rng (F.x) by A5,FUNCT_6:def 3;
then A6:rng (F.x) in rng rngs F by A5,A2,FUNCT_1:def 3;
a in rng (F.x) by A5,FUNCT_1:def 3;
hence thesis by A6,TARSKI:def 4,A1;
end;
theorem Th2:
for D be set, f,g be FinSequence of D* holds
Values (f^g) =Values f \/ Values g
proof
let D be set, f,g be FinSequence of D*;
set F=f^g;
A1:Values f c= Values F
proof
let a be object;
assume a in Values f;
then consider x,y be object such that
A2:x in dom f & y in dom (f.x) & a = f.x.y by Th1;
reconsider x as Nat by A2;
A3:dom f c= dom F by FINSEQ_1:26;
f.x = F.x by A2,FINSEQ_1:def 7;
hence thesis by A3,A2,Th1;
end;
A4:Values g c= Values F
proof
let a be object;
assume a in Values g;
then consider x,y be object such that
A5: x in dom g & y in dom (g.x) & a = g.x.y by Th1;
reconsider x as Nat by A5;
len f + x in dom F & F.(len f + x)=g.x
by A5,FINSEQ_1:28, FINSEQ_1:def 7;
hence thesis by A5,Th1;
end;
Values F c= Values f \/ Values g
proof
let a be object;
assume a in Values F;
then consider x,y be object such that
A6: x in dom F & y in dom (F.x) & a = F.x.y by Th1;
reconsider x as Nat by A6;
per cases by A6,FINSEQ_1:25;
suppose A7:x in dom f;
then f.x =F.x by FINSEQ_1:def 7;
then a in Values f by Th1,A6,A7;
hence thesis by XBOOLE_0:def 3;
end;
suppose ex k st k in dom g & x=len f+k;
then consider k such that
A8: k in dom g & x =len f+k;
F.x= g.k by A8,FINSEQ_1:def 7;
then a in Values g by Th1,A6,A8;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis by A1,A4,XBOOLE_1:8;
end;
theorem Th3:
D-concatenation "**" (f^g) =
(D-concatenation "**" f) ^ (D-concatenation "**" g)
proof
set DC=D-concatenation;
reconsider df=DC"**"f,dg=DC"**"g as Element of (D*+^) by MONOID_0:def 34;
thus DC "**" (f^g) = DC.(DC"**"f,DC"**"g) by MONOID_0:67,FINSOP_1:5
.= (the multF of D*+^).(DC"**"f,DC"**"g)
by MONOID_0:def 36
.= df*dg by ALGSTR_0:def 18
.= (DC"**"f)^(DC"**"g) by MONOID_0:def 34;
end;
theorem
rng (D-concatenation "**" f) = Values f
proof
set DC=D-concatenation;
defpred P[Nat] means for f be FinSequence of D* st len f=$1 holds
rng (DC "**" f) = Values f;
A1:P[0]
proof
let f be FinSequence of D* such that A2: len f=0;
A3:f={} by A2;
then DC "**" f={} by Lm1;
then A4:rng (DC "**" f)={};
assume rng (DC "**" f) <> Values f;
then consider a be object such that
A5: a in Values f by A4,XBOOLE_0:def 1;
ex x,y be object st x in dom f & y in dom (f.x) & a = f.x.y
by A5,Th1;
hence thesis by A3;
end;
A6:P[i] implies P[i+1]
proof
assume A7:P[i];
set i1=i+1;
let f1 be FinSequence of D* such that A8: len f1=i1;
consider f be FinSequence of D*, d be Element of D* such that
A9:f1=f^<*d*> by FINSEQ_2:19,A8;
len f+1 = len f1 by A9,FINSEQ_2:16;
then A10:rng (DC"**"f) = Values f by A8,A7;
DC "**"f1 = (DC"**"f)^(DC "**"<*d*>) by Th3,A9
.= (DC"**"f)^d by FINSOP_1:11;
then A11:rng (DC "**"f1) = (rng (DC"**"f)) \/ (rng d) by FINSEQ_1:31;
A12:rngs <*d*> = <*rng d*> by FINSEQ_3:132;
rng <*rng d*> = {rng d} by FINSEQ_1:38;
then union rng <*rng d*> =rng d by ZFMISC_1:25;
then Union rngs <*d*> = rng d by CARD_3:def 4,A12;
then Values <*d*> = rng d by MATRIX_0:def 9;
hence thesis by Th2,A9,A10,A11;
end;
A13:P[i] from NAT_1:sch 2(A1,A6);
P[len f] by A13;
hence thesis;
end;
theorem
f1 = f2 implies D1-concatenation "**" f1 = D2-concatenation "**" f2
proof
set CC = D2-concatenation;
set NC = D1-concatenation;
defpred P[Nat] means
for fn be FinSequence of D1*,fc be FinSequence of D2* st $1 = len fn & fn=fc
holds
NC "**" fn = CC "**" fc;
A1:P[0]
proof
let fn be FinSequence of D1*,fc be FinSequence of D2*;
assume 0 = len fn & fn=fc;
then fn={} & fc={};
then NC "**" fn={} & CC "**" fc={} by Lm1;
hence thesis;
end;
A2:P[i] implies P[i+1]
proof
assume A3:P[i];
set i1=i+1;
let fn be FinSequence of D1*,fc be FinSequence of D2*;
assume A4:i1 = len fn & fn=fc;
then consider f1 be FinSequence of D1*, d1 be Element of D1* such that
A5:fn=f1^<*d1*> by FINSEQ_2:19;
consider f2 be FinSequence of D2*, d2 be Element of D2* such that
A6:fc=f2^<*d2*> by FINSEQ_2:19,A4;
A7:len f1+1 = len fn by A5,FINSEQ_2:16;
A8:CC "**"fc = (CC"**"f2)^(CC"**"<*d2*>) by Th3,A6
.= (CC"**"f2)^d2 by FINSOP_1:11;
A9:NC "**"fn = (NC"**"f1)^(NC"**"<*d1*>) by Th3,A5
.= (NC"**"f1)^d1 by FINSOP_1:11;
f1=f2 & d1=d2 by A5,A6,A4,FINSEQ_2:17;
hence thesis by A3,A7,A4,A8,A9;
end;
P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem
i in dom (D-concatenation "**" f)
iff
ex n,k st n+1 in dom f & k in dom (f.(n+1)) &
i = k + len (D-concatenation "**" (f|n))
proof
set DC=D-concatenation;
defpred P[Nat] means
for i for f be FinSequence of D* st len f = $1 holds
i in dom (DC "**" f) iff
ex n,k st n+1 in dom f &
k in dom (f.(n+1)) &
i = k + len (DC "**" (f|n));
A1:P[0]
proof
let i;
let f be FinSequence of D*;
assume len f=0;
then f={};
hence thesis by Lm1;
end;
A2:P[j] implies P[j+1]
proof
assume A3:P[j];
set j1=j+1;
let i;
let f1 be FinSequence of D* such that
A4: len f1 = j1;
consider f be FinSequence of D*, d be Element of D* such that
A5: f1=f^<*d*> by FINSEQ_2:19,A4;
A6: len f+1 = len f1 by A5,FINSEQ_2:16;
A7:DC "**"f1 = (DC"**"f)^(DC"**"<*d*>) by Th3,A5
.= (DC"**"f)^d by FINSOP_1:11;
A8:dom f c= dom f1 by A5,FINSEQ_1:26;
thus i in dom (DC "**" f1) implies
ex n,k st n+1 in dom f1 &
k in dom (f1.(n+1)) &
i = k + len (DC "**" (f1|n))
proof
assume A9:i in dom (DC "**" f1);
per cases by A9,A7,FINSEQ_1:25;
suppose i in dom (DC"**"f);
then consider n,k such that
A10:n+1 in dom f & k in dom (f.(n+1)) &
i = k + len (DC "**" (f|n)) by A6,A4,A3;
take n,k;
thus n+1 in dom f1 & k in dom (f1.(n+1))
by A10,A5,A8,FINSEQ_1:def 7;
1<= n+1 & n+1 <= len f by A10,FINSEQ_3:25;
then n <= len f by NAT_1:13;
hence thesis by FINSEQ_5:22,A5,A10;
end;
suppose ex l be Nat st l in dom d & i=len (DC "**" f) +l;
then consider l be Nat such that
A11:l in dom d & i=l+len (DC "**" f);
take n=len f,l;
1<= n+1 by NAT_1:11;
hence thesis by FINSEQ_1:42,FINSEQ_5:23,A5,A11,A6,FINSEQ_3:25;
end;
end;
given n,k such that A12:n+1 in dom f1 &
k in dom (f1.(n+1)) & i = k + len (DC "**" (f1|n));
per cases by A12,A5,FINSEQ_1:25;
suppose A13: n+1 in dom f;
then 1 <= n+1 & n+1 <= len f by FINSEQ_3:25;
then A14: n < len f by NAT_1:13;
A15: k in dom (f.(n+1)) by A13,A5,FINSEQ_1:def 7,A12;
i = k + len (DC "**" (f|n)) by A12, A14,A5,FINSEQ_5:22;
then A16:i in dom (DC "**" f) by A15,A13,A6,A4,A3;
dom (DC "**" f) c= dom (DC "**" f1) by A7,FINSEQ_1:26;
hence i in dom (DC "**" f1) by A16;
end;
suppose ex j st j in dom <*d*> & n+1 = len f+j;
then consider j such that
A17:j in dom <*d*> & n+1=len f+j;
dom <*d*> = Seg 1 & Seg 1 = {1} by FINSEQ_1:2,38;
then j=1 by A17,TARSKI:def 1;
then f1.(n+1) = d & f1|n = f by A17,FINSEQ_5:23,A5,FINSEQ_1:42;
hence i in dom (DC "**" f1) by A12,FINSEQ_1:28,A7;
end;
end;
P[j] from NAT_1:sch 2(A1,A2);
then P[len f];
hence thesis;
end;
theorem
i in dom (D-concatenation "**" f)
implies
(D-concatenation "**" f).i = (D-concatenation "**" (f^g)).i &
(D-concatenation "**" f).i =
(D-concatenation "**" (g^f)).(i+len (D-concatenation "**" g))
proof
set DC=D-concatenation;
assume A1:i in dom (DC "**" f);
A2: DC "**" (f^g) = (DC"**"f)^(DC"**"g) by Th3;
DC "**" (g^f) = (DC"**"g)^(DC"**"f) by Th3;
hence thesis by A2,A1,FINSEQ_1:def 7;
end;
theorem
k in dom (f.(n+1))
implies
f.(n+1).k = (D-concatenation "**" f).(k + len (D-concatenation "**" (f|n)))
proof
set DC=D-concatenation;
set n1=n+1;
assume A1:k in dom (f.n1);
then f.n1 <>{};
then A2:n1 in dom f by FUNCT_1:def 2;
then n1 <= len f by FINSEQ_3:25;
then A3:f|n1 = (f|n) ^ <*f/.n1*> by FINSEQ_5:82;
A4:f.n1=f/.n1 by A2,PARTFUN1:def 6;
consider q be FinSequence such that
A5: f=(f|n1)^q by FINSEQ_1:80;
reconsider q as FinSequence of D* by A5,FINSEQ_1:36;
A6: DC"**"(f|n1) = (DC"**"(f|n))^(DC"**" <*f/.n1*>) by A3,Th3
.= (DC"**"(f|n))^(f/.n1) by FINSOP_1:11;
then A7:(DC"**"(f|n1)).(k+len (DC"**"(f|n))) = (f.n1).k
by A4,A1,FINSEQ_1:def 7;
A8: k+len (DC"**"(f|n)) in dom (DC"**"(f|n1)) by A6,A4,A1,FINSEQ_1:28;
DC"**"f = (DC"**"(f|n1))^(DC"**"q) by A5,Th3;
hence thesis by A8,FINSEQ_1:def 7,A7;
end;
begin :: Flexary Plus
reserve f for complex-valued Function,
g,h for complex-valued FinSequence;
definition
let k,n;
let f,g be complex-valued Function;
func (f,k) +...+ (g,n) -> complex number means :Def1:
h.(0+1) = f.(0+k) & ... & h.(n-'k+1) = f.(n-'k+k)
implies
it = Sum (h | (n-'k+1)) if f = g & k <= n
otherwise it = 0;
existence
proof
per cases;
suppose f<>g or n <k;
hence thesis;
end;
suppose f=g & n >= k;
deffunc P(Nat) = f.(k+$1-1);
set kn=n-'k+1;
consider p be FinSequence such that
A1: len p = kn & for i st i in dom p holds p.i=P(i) from FINSEQ_1:sch 2;
rng p c= COMPLEX
proof
let y be object;
assume y in rng p;
then consider x be object such that
A2: x in dom p & p.x = y by FUNCT_1:def 3;
reconsider x as Nat by A2;
p.x = f.(k+x-1) by A2,A1;
hence thesis by A2, XCMPLX_0:def 2;
end;
then reconsider p as complex-valued FinSequence by VALUED_0:def 1;
reconsider S=Sum p as complex number by TARSKI:1;
A3:Sum(p|kn) = S by A1,FINSEQ_1:58;
h.(0+1) = f.(0+k) & ... & h.((n-'k)+1) = f.((n-'k)+k)
implies
Sum (p| kn) = Sum (h| kn)
proof
assume A4: h.(0+1) = f.(0+k) & ... & h.((n-'k)+1) = f.((n-'k)+k);
defpred P[Nat] means $1 <= kn implies Sum (h|$1) = Sum (p|$1);
A5:P[0];
A6:for i st P[i] holds P[i+1]
proof
let i;
set i1=i+1;
assume A7:P[i];
assume A8:i1 <= kn;
A9: 1<= i1 by NAT_1:11;
then p|i1 = (p|i) ^ <*p.i1*> by FINSEQ_5:10,A1,A8,FINSEQ_3:25;
then A10: Sum (p|i1) = Sum (p|i) + p.i1 by RVSUM_2:31;
A11: p.i1 = f.(k+i1-1) by A1,A9,A8,FINSEQ_3:25;
i <= n-'k by A8,XREAL_1:6;
then A12: f.(k+i) = h.(1+i) by A4;
per cases;
suppose
i1 <= len h;
then i1 in dom h by NAT_1:11,FINSEQ_3:25;
then h|i1 = (h|i) ^ <*h.i1*> by FINSEQ_5:10;
hence thesis by RVSUM_2:31,A8,NAT_1:13,A7,A10,A11,A12;
end;
suppose A13: i1 > len h;
then not i1 in dom h by FINSEQ_3:25;
then A14:h.i1 = 0 by FUNCT_1:def 2;
h|i = h by A13,NAT_1:13,FINSEQ_1:58;
hence
thesis by A8,NAT_1:13,A7,A10,A11,A12,A13,FINSEQ_1:58,A14;
end;
end;
for i holds P[i] from NAT_1:sch 2(A5,A6);
hence thesis;
end;
hence thesis by A3;
end;
end;
uniqueness
proof
now assume f = g;
let C1,C2 be complex number such that
A15: (h.(0+1) = f.(0+k) & ... & h.(n-'k+1) = f.(n-'k+k))
implies C1 = Sum (h| (n-'k + 1))
and
A16: (h.(0+1) = f.(0+k) & ... & h.(n-'k+1) = f.(n-'k+k))
implies C2 = Sum (h| (n-'k + 1));
deffunc P(Nat) = f.(k+$1-1);
set nk=n-'k+1;
consider p be FinSequence such that
A17: len p = nk & for i st i in dom p holds p.i=P(i) from FINSEQ_1:sch 2;
rng p c= COMPLEX
proof
let y be object;
assume y in rng p;
then consider x be object such that
A18: x in dom p & p.x = y by FUNCT_1:def 3;
reconsider x as Nat by A18;
p.x = f.(k+x-1) by A18,A17;
hence thesis by A18, XCMPLX_0:def 2;
end;
then reconsider p as complex-valued FinSequence by VALUED_0:def 1;
p.(0+1) = f.(0+k) & ... & p.((n-'k)+1) = f.((n-'k)+k)
proof
let i;
assume 0 <= i & i <= n-'k;
then 1<= i+1 & i+1 <= nk by NAT_1:11,XREAL_1:6;
then p.(i+1) = f.(k+(i+1)-1) by A17,FINSEQ_3:25;
hence p.(i+1) = f.(i+k);
end;
then C1 = Sum (p| (n-'k + 1)) & C2 = Sum (p| (n-'k + 1)) by A15,A16;
hence C1=C2;
end;
hence thesis;
end;
correctness;
end;
theorem Th9:
k <= n implies ex h st
(f,k) +...+ (f,n) = Sum h & len h = n-'k+1 &
(h.(0+1) = f.(0+k) & ... & h.(n-'k+1) = f.(n-'k+k))
proof
assume A1: k <= n;
deffunc P(Nat) = f.(k+$1-1);
set nk=n-'k+1;
consider p be FinSequence such that
A2: len p = nk & for i st i in dom p holds p.i=P(i) from FINSEQ_1:sch 2;
rng p c= COMPLEX
proof
let y be object;
assume y in rng p;
then consider x be object such that
A4: x in dom p & p.x = y by FUNCT_1:def 3;
reconsider x as Nat by A4;
p.x = f.(k+x-1) by A4,A2;
hence thesis by A4, XCMPLX_0:def 2;
end;
then reconsider p as complex-valued FinSequence by VALUED_0:def 1;
A5:p.(1+0) = f.(k+0) & ... & p.(1+(n-'k)) = f.(k+(n-'k))
proof
let i;
assume 0 <= i & i <= n-'k;
then 1<= i+1 & i+1 <= nk by NAT_1:11,XREAL_1:6;
then p.(i+1) = f.(k+(i+1)-1) by A2,FINSEQ_3:25;
hence p.(1+i) = f.(k+i);
end;
then (f,k) +...+ (f,n) = Sum (p | (n-'k+1)) by A1,Def1;
then Sum p = (f,k) +...+ (f,n) by FINSEQ_1:58,A2;
hence thesis by A2,A5;
end;
theorem Th10:
(f,k) +...+ (f,n) <> 0 implies
ex i st k <= i & i <=n & i in dom f
proof
assume A1:(f,k) +...+ (f,n) <> 0;
then A2:n >=k by Def1;
then consider h such that
A3:(f,k) +...+ (f,n) = Sum h and
A4:len h = n-'k+1 and
A5:h.(0+1) = f.(0+k) & ... & h.(n-'k+1) = f.(n-'k+k) by Th9;
assume A6:for i st k <= i & i <=n holds not i in dom f;
n-'k +1 >= 1 by NAT_1:11;
then 1 in dom h by A4,FINSEQ_3:25;
then A7: h.1 in rng h by FUNCT_1:def 3;
rng h c= {0}
proof
let y be object;
assume y in rng h;
then consider x be object such that
A8:x in dom h & h.x=y by FUNCT_1:def 3;
reconsider x as Nat by A8;
1<= x & x <= len h by A8,FINSEQ_3:25;
then reconsider x1=x-1 as Nat;
x1+1=x;
then A9:x1<= n-'k by A8,FINSEQ_3:25,A4,XREAL_1:6;
then A10:h.(x1+1)=f.(x1+k) by A5;
n-'k = n- k by A2,XREAL_1:233;
then k <= x1+k & x1+k <= n-'k+k & n-'k+k=n
by A9,XREAL_1:6,NAT_1:11;
then not x1+k in dom f by A6;
then f.(x1+k)=0 by FUNCT_1:def 2;
hence thesis by A10,A8,TARSKI:def 1;
end;
then h = (dom h)--> 0 by A7,ZFMISC_1:33,FUNCOP_1:9;
then h = len h |->0 by FINSEQ_1:def 3;
hence thesis by RVSUM_1:81,A3,A1;
end;
theorem Th11:
(f,k) +...+ (f,k) = f.k
proof
consider h be complex-valued FinSequence such that
A1:(f,k) +...+ (f,k) = Sum h & len h = k-'k+1 &
(h.(0+1) = f.(0+k) & ... & h.(k-'k+1) = f.(k-'k+k)) by Th9;
k-'k+1 = 0+1 by XREAL_1:232;
then h = <*h.1*> by A1,FINSEQ_1:40;
then Sum h = h.1 by RVSUM_2:30;
hence thesis by A1;
end;
theorem Th12:
k <= n+1 implies (f,k) +...+ (f,n+1) = (f,k) +...+ (f,n) + f.(n+1)
proof
set n1=n+1;
assume A1:k <= n1;
per cases by A1,NAT_1:8;
suppose A2: k=n1;
then k > n by NAT_1:13;
then (f,k) +...+ (f,n)=0 & (f,k) +...+ (f,n+1) = f.k by A2, Th11,Def1;
hence thesis by A2;
end;
suppose A3: k <= n;
then consider h be complex-valued FinSequence such that
A4:(f,k) +...+ (f,n) = Sum h & len h = n-'k+1 and
A5:h.(0+1) = f.(0+k) & ... & h.(n-'k+1) = f.(n-'k+k) by Th9;
A6:n1-'k = n-'k+1 by A3,NAT_D:38;
set fn=f.n1;
reconsider fn as Complex;
set h1 = h ^ <*fn*>;
A7:len h1 = n1-'k+1 by A6,A4,FINSEQ_2:16;
h1.(0+1) = f.(0+k) & ... & h1.(n1-'k+1) = f.(n1-'k+k)
proof
let i;
set i1=i+1;
assume A8:0<=i & i <= n1-'k;
per cases by A8,A6,NAT_1:8;
suppose A9:i <= n-'k;
then 1<= i1 & i1 <= len h by NAT_1:11,A4,XREAL_1:6;
then i1 in dom h by FINSEQ_3:25;
then h1.i1 = h.i1 by FINSEQ_1:def 7;
hence thesis by A5,A9;
end;
suppose A10:i = n-'k+1;
n1-'k+k =n1-k+k by NAT_D:37,A3;
hence thesis by A10,A4,FINSEQ_1:42,A6;
end;
end;
then (f,k) +...+ (f,n1) = Sum (h1| (n1-'k+1)) by A1,Def1
.= Sum h1 by A7,FINSEQ_1:58;
hence thesis by A4,RVSUM_2:31;
end;
end;
theorem Th13:
k <= n implies
(f,k) +...+ (f,n) = f.k + (f,k+1) +...+ (f,n)
proof
set k1=k+1;
assume A1:k <=n;
per cases by A1,XXREAL_0:1;
suppose A2:k =n;
then A3:k+1 > n by NAT_1:13;
thus (f,k) +...+ (f,n) = f.k +0 by A2,Th11
.= f.k + (f,k+1) +...+ (f,n) by A3,Def1;
end;
suppose A4: k < n;
then k1 <= n by NAT_1:13;
then consider h be complex-valued FinSequence such that
A5:(f,k1) +...+ (f,n) = Sum h & len h = n-'k1+1 and
A6: h.(0+1) = f.(0+k1) & ... & h.(n-'k1+1) = f.(n-'k1+k1) by Th9;
reconsider fk=f.k as Complex;
set h1 = <*fk*>^h;
A7: n-'k1+1 = n-'k by A4,NAT_D:59;
A8:len <*fk*> = 1 by FINSEQ_1:39;
then len h1 = n-'k+1 by FINSEQ_1:22,A7,A5;
then A9: h1| (n-'k+1) = h1 by FINSEQ_1:58;
h1.(0+1) = f.(0+k) & ... & h1.(n-'k+1) = f.(n-'k+k)
proof
let i;
set i1=i+1;
assume A10: 0 <= i & i <= n-'k;
per cases;
suppose i=0;
hence thesis by FINSEQ_1:41;
end;
suppose A11:i>0;
then reconsider ii=i-1 as Nat;
ii+1 <= n-'k1+1 by A4,NAT_D:59,A10;
then ii <= n-'k1 by XREAL_1:6;
then A12: h.(ii+1) = f.(ii+k1) by A6;
i >= 1 by NAT_1:14,A11;
then i in dom h by A5,A7,A10,FINSEQ_3:25;
hence thesis by A8,FINSEQ_1:def 7,A12;
end;
end;
hence (f,k) +...+ (f,n) = Sum h1 by Def1,A4,A9
.= f.k +(f,k+1) +...+ (f,n) by RVSUM_2:33,A5;
end;
end;
theorem Th14:
k <= m & m <= n implies
(f,k) +...+ (f,m) + (f,m+1) +...+ (f,n) = (f,k) +...+ (f,n)
proof
assume A1: k <= m & m <= n;
defpred P[Nat] means
(f,k) +...+ (f,m) + (f,m+1) +...+ (f,m+$1) =
(f,k) +...+ (f,m+$1);
A2:P[0]
proof
m+1 > m+0 by NAT_1:13;
then (f,m+1) +...+ (f,m+0)=0 by Def1;
hence thesis;
end;
A3: P[i] implies P[i+1]
proof
assume A4:P[i];
A5:m+1 <= m+1+i by NAT_1:11;
m <= m+(i+1) by NAT_1:11;
hence (f,k) +...+ (f,m+(i+1)) = (f,k)+...+(f,m+i)+f.(m+i+1)
by A1,XXREAL_0:2,Th12
.= (f,k) +...+ (f,m) + ((f,m+1) +...+ (f,m+i) + f.(m+i+1)) by A4
.= (f,k) +...+ (f,m) + (f,m+1) +...+ (f,m+(i+1)) by Th12,A5;
end;
A6:P[i] from NAT_1:sch 2(A2,A3);
reconsider nm=n-m as Nat by A1,NAT_1:21;
P[nm] by A6;
hence thesis;
end;
theorem Th15:
k > len h implies (h,k) +...+ (h,n) = 0
proof
assume A1:k >len h;
per cases;
suppose k>n;
hence thesis by Def1;
end;
suppose k <=n;
then consider w be complex-valued FinSequence such that
A2:(h,k) +...+ (h,n) = Sum w & len w = n-'k+1 and
A3:w.(0+1) = h.(0+k) & ... & w.(n-'k+1) = h.(n-'k+k) by Th9;
set nk=n-'k+1,nk0 = nk |-> (0 qua Real);
now let i such that A4: 1<= i & i <= nk;
reconsider i1=i-1 as Nat by A4;
i1+1=i;
then i1 <= n-'k by A4,XREAL_1:6;
then A5:w.(i1+1) = h.(i1+k) by A3;
i1+k > 0+len h by A1,XREAL_1:8;
then not i1+k in dom h by FINSEQ_3:25;
hence w.i=nk0.i by FUNCT_1:def 2,A5;
end;
then w= nk|->0 by CARD_1:def 7,A2;
then Sum w = nk*0 by RVSUM_1:80;
hence thesis by A2;
end;
end;
theorem Th16:
n >= len h implies
(h,k) +...+ (h,n) = (h,k) +...+ (h,len h)
proof
assume A1: n >= len h;
per cases;
suppose k >len h;
then (h,k) +...+ (h,len h) = 0 & (h,k) +...+ (h,n) = 0 by Th15;
hence thesis;
end;
suppose A2: k <= len h;
defpred P[Nat] means (h,k) +...+ (h,len h+$1) = (h,k) +...+ (h,len h);
A3:P[0];
A4:P[i] implies P[i+1]
proof
set i1=i+1;
assume A5:P[i];
len h + i1 > len h +0 by XREAL_1:6;
then A6:not len h+i1 in dom h by FINSEQ_3:25;
A7: len h <= len h+i1 by NAT_1:11;
A8: h.(len h+i1) = 0 by A6,FUNCT_1:def 2;
(h,k) +...+ (h,len h+i+1) = (h,k) +...+ (h,len h+i) + h.(len h+i+1)
by Th12,A7,XXREAL_0:2,A2;
hence thesis by A8,A5;
end;
A9:P[i] from NAT_1:sch 2(A3,A4);
reconsider nl=n-len h as Nat by A1,NAT_1:21;
P[nl] by A9;
hence thesis;
end;
end;
theorem Th17:
(h,0) +...+ (h,k) = (h,1) +...+ (h,k)
proof
not 0 in dom h by FINSEQ_3:25;
then A1:h.0 = 0 by FUNCT_1:def 2;
(h,0) +...+ (h,k) = h.0+(h,0+1) +...+ (h,k) by Th13;
hence thesis by A1;
end;
theorem Th18:
(h,1) +...+ (h,len h) = Sum h
proof
set L=len h;
per cases;
suppose A1:L >=1;
then consider w be complex-valued FinSequence such that
A2:(h,1) +...+ (h,L) = Sum w & len w = L-'1+1 and
A3:w.(0+1) = h.(0+1) & ... & w.(L-'1+1) = h.(L-'1+1) by Th9;
A4:L-'1+1 = L-1+1 by A1,NAT_D:34;
now let i such that A5:1<=i & i <= L;
reconsider i1=i-1 as Nat by A5;
w.(i1+1) =h.(i1+1) by A4,A5,XREAL_1:6,A3;
hence h.i=w.i;
end;
then h=w by A4,A2;
hence thesis by A2;
end;
suppose L <1;
then h=<*>REAL by FINSEQ_1:20;
hence thesis by RVSUM_1:72,Def1;
end;
end;
Lm2: k<=n & n <= len g implies
(g^h,k)+...+(g^h,n) = (g,k) +...+ (g,n)
proof
set gh=g^h;
assume A1:k<=n & n <= len g;
then consider w be complex-valued FinSequence such that
A2:(gh,k) +...+ (gh,n) = Sum w & len w = n-'k+1
and
A3:w.(0+1) = gh.(0+k) & ... & w.(n-'k+1) = gh.(n-'k+k) by Th9;
A4: n-'k+k = n & n-'k = n-k by A1,XREAL_1:235,233;
A5:w| (n-'k+1)=w by A2,FINSEQ_1:58;
w.(0+1) = g.(0+k) & ... & w.(n-'k+1) = g.(n-'k+k)
proof
let i;
assume A6:0<= i & i <= n-'k;
then A7: i+k <= n by A4,XREAL_1:6;
per cases;
suppose A8: i+k=0;
then not i+k in dom g & not i+k in dom gh by FINSEQ_3:25;
then gh.0 = 0 & g.0 = 0 by A8,FUNCT_1:def 2;
hence thesis by A3,A8,A6;
end;
suppose i+k >0;
then A9:i+k >= 1 by NAT_1:14;
i+k <= len g by A1,A7,XXREAL_0:2;
then i+k in dom g by A9,FINSEQ_3:25;
then g.(i+k) = gh.(i+k) by FINSEQ_1:def 7;
hence thesis by A3,A6;
end;
end;
hence thesis by A1,Def1,A5,A2;
end;
Lm3: k<=n & k > len g implies
(g^h,k)+...+(g^h,n) =
(h,k-'len g)+...+(h,n-'len g)
proof
set gh=g^h;
assume A1:k<=n & k > len g;
then consider w be complex-valued FinSequence such that
A2:(gh,k) +...+ (gh,n) = Sum w & len w = n-'k+1
and
A3:w.(0+1) = gh.(0+k) & ... & w.(n-'k+1) = gh.(n-'k+k) by Th9;
A4:n-'k+k = n & n-'k = n-k by A1,XREAL_1:235,233;
A5:w| (n-'k+1)=w by A2,FINSEQ_1:58;
set kL=k-'len g,nL=n-'len g;
A6:kL=k-len g & nL=n-len g by A1,XXREAL_0:2,XREAL_1:233;
A7:kL<= nL by A1,NAT_D:42;
A8:nL-'kL =nL-kL by A1,NAT_D:42,XREAL_1:233;
w.(0+1) = h.(0+kL) & ... & w.(nL-'kL+1) = h.(nL-'kL+kL)
proof
let i;
assume A9: 0<= i & i <= nL-'kL;
then A10:w.(i+1) = gh.(i+k) by A8,A6,A4,A3;
kL<>0 by A1,A6;
then A11:kL+i >= 1+0 by NAT_1:14;
per cases;
suppose kL +i <=len h;
then kL+i in dom h by A11,FINSEQ_3:25;
then h.(kL+i)=gh.(kL+i +len g) by FINSEQ_1:def 7;
then h.(kL+i)=gh.(i+k) by A6;
hence thesis by A9, A8,A6,A4,A3;
end;
suppose A12:kL+i > len h;
then not kL+i in dom h by FINSEQ_3:25;
then A13:h.(i+kL) = 0 by FUNCT_1:def 2;
kL+i+len g > len h+len g by A12,XREAL_1:6;
then i+k >len g+len h & len gh=len g+len h by A6,FINSEQ_1:22;
then not i+k in dom gh by FINSEQ_3:25;
hence thesis by FUNCT_1:def 2,A13,A10;
end;
end;
hence thesis by A8,A6,A4,A5,Def1,A7,A2;
end;
theorem
(g^h,k)+...+(g^h,n) =
(g,k) +...+ (g,n)+ (h,k-'len g)+...+(h,n-'len g)
proof
set gh=g^h;
per cases;
suppose A1:k >n;
then A2:(g^h,k)+...+(g^h,n) = 0 &
(g,k) +...+ (g,n)=0 by Def1;
per cases by XXREAL_0:1;
suppose k-'len g = n-'len g & k-'len g=0;
then A3:(h,k-'len g)+...+(h,n-'len g) = h.0 by Th11;
not 0 in dom h by FINSEQ_3:25;
hence thesis by A3,A2,FUNCT_1:def 2;
end;
suppose A4: k-'len g = n-'len g & k-'len g > 0;
then k-'len g = k- len g & n-'len g = n- len g by XREAL_0:def 2;
hence thesis by A1,A4;
end;
suppose n-'len g < k-'len g;
hence thesis by Def1,A2;
end;
suppose A5:n-'len g > k-'len g;
then n-'len g=n-len g & n-len g >0 & 0 = len g- len g
by XREAL_0:def 2;
then n > len g by XREAL_1:6;
hence thesis by A5,A1,NAT_D:56;
end;
end;
suppose A6: k <= n;
set w =the complex-valued FinSequence;
per cases;
suppose A7:n <= len g;
then k <= len g by A6,XXREAL_0:2;
then n - len g <= 0 & k-len g <= 0 by A7,XREAL_1:47;
then n-'len g =0 & k-'len g =0 by XREAL_0:def 2;
then A8: (h,k-'len g)+...+(h,n-'len g) = h.0 by Th11;
not 0 in dom h by FINSEQ_3:25;
then (h,k-'len g)+...+(h,n-'len g)=0 by FUNCT_1:def 2,A8;
hence thesis by A7,Lm2,A6;
end;
suppose A9: k > len g;
then (g,k) +...+ (g,n) = 0 by Th15;
hence thesis by Lm3,A9,A6;
end;
suppose A10: n > len g & k <= len g;
then A11:(g^h,k)+...+(g^h,len g) = (g,k)+...+(g,len g) by Lm2
.= (g,k)+...+(g,n) by Th16,A10;
k-len g <= len g - len g by A10,XREAL_1:7;
then A12:k-'len g=0 by XREAL_0:def 2;
A13:len g+1-'len g = len g+1-len g by NAT_D:37;
len g+1 > len g & n>= len g+1 by A10,NAT_1:13;
then (g^h,len g+1)+...+(g^h,n) = (h,len g+1-'len g)+...+(h,n-'len g)
by Lm3
.=(h,k-'len g)+...+(h,n-'len g) by A13,Th17,A12;
hence thesis by A10,Th14,A11;
end;
end;
end;
registration
let n,k;
let f be real-valued FinSequence;
cluster (f,k) +...+ (f,n) -> real;
coherence
proof
per cases;
suppose k >n;
hence thesis by Def1;
end;
suppose k <=n;
then consider h such that
A1:(f,k) +...+ (f,n) = Sum h & len h = n-'k+1 and
A2:h.(0+1) = f.(0+k) & ... & h.(n-'k+1) = f.(n-'k+k) by Th9;
rng h c= REAL
proof
let y be object;
assume y in rng h;
then consider x be object such that
A3: x in dom h & h.x=y by FUNCT_1:def 3;
reconsider x as Nat by A3;
1<= x & x <= len h by A3,FINSEQ_3:25;
then reconsider x1=x-1 as Nat;
x1+1 <= n-'k+1 by A3,FINSEQ_3:25,A1;
then x1 <= n-'k by XREAL_1:6;
then h.(x1+1) = f.(x1+k) by A2;
hence thesis by A3,XREAL_0:def 1;
end;
then h is real-valued by VALUED_0:def 3;
hence thesis by A1;
end;
end;
end;
registration
let n,k;
let f be natural-valued FinSequence;
cluster (f,k) +...+ (f,n) -> natural;
coherence
proof
per cases;
suppose k >n;
hence thesis by Def1;
end;
suppose k <=n;
then consider h such that
A1:(f,k) +...+ (f,n) = Sum h & len h = n-'k+1 and
A2:h.(0+1) = f.(0+k) & ... & h.(n-'k+1) = f.(n-'k+k) by Th9;
rng h c= NAT
proof
let y be object;
assume y in rng h;
then consider x be object such that
A3: x in dom h & h.x=y by FUNCT_1:def 3;
reconsider x as Nat by A3;
1<= x & x <= len h by A3,FINSEQ_3:25;
then reconsider x1=x-1 as Nat;
x1+1 <= n-'k+1 by A3,FINSEQ_3:25,A1;
then x1 <= n-'k by XREAL_1:6;
then A4:h.(x1+1) = f.(x1+k) by A2;
per cases;
suppose not x1+k in dom f;
then y=0 by A4,FUNCT_1:def 2,A3;
hence thesis;
end;
suppose x1+k in dom f;
then f.(x1+k) in rng f & rng f c= NAT by FUNCT_1:def 3,VALUED_0:def 6;
hence thesis by A3,A4;
end;
end;
then reconsider H=h as FinSequence of NAT by FINSEQ_1:def 4;
Sum H is Element of NAT;
hence thesis by A1;
end;
end;
end;
definition
let n;
let f be complex-valued Function;
assume A1: dom f /\ NAT is finite;
func (f,n)+... -> complex number means :Def2:
for k st for i st i in dom f holds i <= k holds
it = (f,n) +...+ (f,k);
existence
proof
per cases;
suppose A2:dom f/\NAT={};
take 0;
let k such that for i st i in dom f holds i <= k;
for i st n <= i & i <=k holds not i in dom f
proof
let i;
i in NAT by ORDINAL1:def 12;
hence thesis by A2,XBOOLE_0:def 4;
end;
hence thesis by Th10;
end;
suppose dom f/\NAT is non empty;
then reconsider F=dom f /\NAT as non empty finite Subset of NAT by A1;
reconsider m=max F as Nat by TARSKI:1;
take t=(f,n) +...+ (f,m);
let k such that A3: for i st i in dom f holds i <= k;
m in F by XXREAL_2:def 8;
then reconsider km=k-m as Nat by A3,NAT_1:21;
per cases;
suppose A4: n > m;
(f,n) +...+ (f,k)=0
proof
assume (f,n) +...+ (f,k)<>0;
then consider i such that
A5: n <= i & i <= k & i in dom f by Th10;
i in NAT by ORDINAL1:def 12;
then i in F by A5,XBOOLE_0:def 4;
then i <= m by XXREAL_2:def 8;
hence thesis by A4,XXREAL_0:2,A5;
end;
hence thesis by A4,Def1;
end;
suppose A6:n <= m;
defpred P[Nat] means t=(f,n) +...+ (f,m+$1);
A7:P[0];
A8:P[i] implies P[i+1]
proof
assume A9: P[i];
A10:m< m+i+1 by NAT_1:11,NAT_1:13;
then A11:(f,n) +...+ (f,m+i+1) = (f,n) +...+ (f,m+i) + f.(m+i+1)
by A6,XXREAL_0:2,Th12
.= t+f.(m+i+1) by A9;
not m+i+1 in dom f
proof
assume m+i+1 in dom f;
then m+i+1 in F by XBOOLE_0:def 4;
hence thesis by XXREAL_2:def 8,A10;
end;
then f.(m+i+1)=0 by FUNCT_1:def 2;
hence thesis by A11;
end;
P[i] from NAT_1:sch 2(A7,A8);
then P[km];
hence thesis;
end;
end;
end;
uniqueness
proof
let C1,C2 be complex number such that
A12:for k st for i st i in dom f holds i <= k holds
C1 = (f,n) +...+ (f,k)
and
A13:for k st for i st i in dom f holds i <= k holds
C2 = (f,n) +...+ (f,k);
per cases;
suppose dom f/\NAT is non empty;
then reconsider F=dom f /\NAT as non empty finite Subset of NAT by A1;
reconsider m=max F as Nat by TARSKI:1;
A14: for i st i in dom f holds i <= m
proof
let i;
assume A15:i in dom f;
i in NAT by ORDINAL1:def 12;
then i in F by A15,XBOOLE_0:def 4;
hence thesis by XXREAL_2:def 8;
end;
hence C1 = (f,n) +...+ (f,m) by A12
.= C2 by A14,A13;
end;
suppose A16:dom f/\NAT is empty;
A17: for i st i in dom f holds i <= 1
proof
let i;
assume A18:i in dom f;
i in NAT by ORDINAL1:def 12;
hence thesis by A18,XBOOLE_0:def 4,A16;
end;
hence C1 = (f,n) +...+ (f,1) by A12
.= C2 by A17,A13;
end;
end;
end;
definition
let n,h;
redefine func (h,n)+... -> complex number equals :: redefines +... (FLEXARY1, definition)
(h,n)+...+(h,len h);
coherence;
compatibility
proof
let c be complex number;
A1:dom h/\NAT=dom h by XBOOLE_1:28;
thus c = (h,n)+... implies c =(h,n)+...+(h,len h)
proof
for i st i in dom h holds i <= len h by FINSEQ_3:25;
hence thesis by Def2,A1;
end;
assume A2:c =(h,n)+...+(h,len h);
for k st for i st i in dom h holds i <= k holds
c = (h,n)+...+(h,k)
proof
let k such that A3: for i st i in dom h holds i <= k;
now per cases by NAT_1:14;
suppose len h = 0;
hence len h <= k;
end;
suppose len h >= 1;
then len h in dom h by FINSEQ_3:25;
hence len h <=k by A3;
end;
end;
hence thesis by Th16,A2;
end;
hence thesis by A1,Def2;
end;
end;
registration
let n be Nat;
let h be natural-valued FinSequence;
cluster (h,n)+... -> natural;
coherence;
end;
theorem Th20:
for f be finite complex-valued Function holds
f.n + (f,n+1) +... = (f,n) +...
proof
let f be finite complex-valued Function;
{n} c= NAT by ORDINAL1:def 12;
then reconsider D=(dom f /\NAT)\/{n} as finite non empty Subset of NAT
by XBOOLE_1:8;
reconsider m=max D as Nat by TARSKI:1;
A1:for i st i in dom f holds i <= m
proof
let i;
assume A2:i in dom f;
i in NAT by ORDINAL1:def 12;
then i in dom f /\NAT by A2,XBOOLE_0:def 4;
then i in D by XBOOLE_0:def 3;
hence thesis by XXREAL_2:def 8;
end;
then A3:(f,n+1)+... = (f,n+1)+...+(f,m) by Def2;
A4:(f,n)+... = (f,n)+...+(f,m) by Def2,A1;
n in {n} by TARSKI:def 1;
then n in D by XBOOLE_0:def 3;
then n <=m by XXREAL_2:def 8;
hence thesis by Th13,A3,A4;
end;
theorem Th21:
Sum h = (h,1) +... by Th18;
theorem Th22:
Sum h = h.1 + (h,2) +...
proof
Sum h = (h,1)+... by Th18
.= h.1+(h,1+1)+... by Th20;
hence thesis;
end;
scheme TT{f,g()->complex-valued FinSequence,
a,b()->Nat,
n,k()->non zero Nat}:
(f(),a())+... = (g(),b())+...
provided
A1: for j holds (f(),a()+j*n())+...+(f(),a()+j*n()+(n()-'1)) =
(g(),b()+j*k())+...+(g(),b()+j*k()+(k()-'1))
proof
defpred P[Nat] means
(f(),a())+...+(f(),a()+$1*n()+(n()-'1)) =
(g(),b())+...+(g(),b()+$1*k()+(k()-'1));
A2:P[0] by A1;
A3:P[j] implies P[j+1]
proof
set j1=j+1;
A4: (f(),a())+...+(f(),a()+j*n()+(n()-'1))+
(f(),a()+j1*n())+...+
(f(),a()+j1*n()+(n()-'1))=
(f(),a()) +...+(f(),a()+j1*n()+(n()-'1))
proof
A5: a() <= a()+(j*n()+(n()-'1)) by NAT_1:11;
(n()-'1)+1=n() by NAT_1:14,XREAL_1:235;
then A6:(a()+j*n()+(n()-'1))+1 = a()+j1*n();
a()+j1*n() <= a()+(j1*n()+(n()-'1)) by NAT_1:11,XREAL_1:6;
then a()+j*n()+(n()-'1)<= a()+(j1*n()+(n()-'1)) by A6,NAT_1:13;
hence thesis by Th14,A5,A6;
end;
(g(),b())+...+(g(),b()+j*k()+(k()-'1))+
(g(),b()+j1*k())+...+
(g(),b()+j1*k()+(k()-'1))=
(g(),b()) +...+(g(),b()+j1*k()+(k()-'1))
proof
A7: b() <= b()+(j*k()+(k()-'1)) by NAT_1:11;
(k()-'1)+1=k() by NAT_1:14,XREAL_1:235;
then A8:(b()+j*k()+(k()-'1))+1 = b()+j1*k();
b()+j1*k() <= b()+(j1*k()+(k()-'1)) by NAT_1:11,XREAL_1:6;
then b()+j*k()+(k()-'1)<= b()+(j1*k()+(k()-'1)) by A8,NAT_1:13;
hence thesis by Th14,A7,A8;
end;
hence thesis by A1,A4;
end;
A9: P[j] from NAT_1:sch 2(A2,A3);
per cases;
suppose A10:len f() >= len g();
set l =len f();
l*1 <= l*n() by NAT_1:14,XREAL_1:64;
then l <= l*n()+(a()+(n()-'1)) by XREAL_1:38;
then A11:(f(),a())+...+(f(),a()+l*n()+(n()-'1))
= (f(),a())+... by Th16;
A12:len g()*k()<= l*k() by A10,XREAL_1:64;
len g()*1 <= len g()*k() by NAT_1:14,XREAL_1:64;
then len g() <= l*k() by A12,XXREAL_0:2;
then len g() <= l*k()+(b()+(k()-'1)) by XREAL_1:38;
then (g(),b())+...+(g(),b()+l*k()+(k()-'1)) =
(g(),b())+...+(g(),len g()) = (g(),b())+... by Th16;
hence thesis by A9,A11;
end;
suppose A13:len g() >= len f();
set l =len g();
l*1 <= l*k() by NAT_1:14,XREAL_1:64;
then l <= l*k()+(b()+(k()-'1)) by XREAL_1:38;
then A14: (g(),b())+...+(g(),b()+l*k()+(k()-'1))
= (g(),b())+... by Th16;
A15:len f()*n()<= l*n() by A13,XREAL_1:64;
len f()*1 <= len f()*n() by NAT_1:14,XREAL_1:64;
then len f() <= l*n() by A15,XXREAL_0:2;
then len f() <= l*n()+(a()+(n()-'1)) by XREAL_1:38;
then (f(),a())+...+(f(),a()+l*n()+(n()-'1)) =
(f(),a())+... by Th16;
hence thesis by A9,A14;
end;
end;
begin :: Power Function
definition
let r be Real;
let f be real-valued Function;
func r |^ f -> real-valued Function means :Def4:
dom it = dom f & for x st x in dom f holds it.x = r to_power (f.x);
existence
proof
deffunc P(object) = r to_power (f.$1);
A1: for x st x in dom f holds P(x) in REAL by XREAL_0:def 1;
consider g be Function of dom f,REAL such that
A2:for x st x in dom f holds g.x=P(x) from FUNCT_2:sch 2(A1);
take g;
thus thesis by A2,FUNCT_2:def 1;
end;
uniqueness
proof
let F1,F2 be real-valued Function such that
A3: dom F1 = dom f & for x st x in dom f holds F1.x = r to_power (f.x) and
A4: dom F2 = dom f & for x st x in dom f holds F2.x = r to_power (f.x);
now let x;
assume A5:x in dom f;
hence F1.x = r to_power (f.x) by A3
.= F2.x by A4,A5;
end;
hence thesis by A3,A4;
end;
end;
registration
let n be Nat;
let f be natural-valued Function;
cluster n |^ f -> natural-valued;
coherence
proof
now let x;
assume x in dom (n|^f);
then x in dom f by Def4;
then (n|^f).x = n to_power (f.x) by Def4;
hence (n|^f).x is natural;
end;
hence thesis by VALUED_0:def 12;
end;
end;
registration
let r be Real;
let f be real-valued FinSequence;
cluster r |^ f -> FinSequence-like;
coherence
proof
dom f = Seg len f by FINSEQ_1:def 3;
hence thesis by Def4;
end;
cluster r |^ f -> (len f) -element;
coherence
proof
dom f = dom (r|^f) by Def4;
then len f =len (r|^f) by FINSEQ_3:29;
hence thesis by CARD_1:def 7;
end;
end;
registration
let n be Nat;
let f be one-to-one natural-valued Function;
cluster (2+n) |^ f -> one-to-one;
coherence
proof
set n2=2+n,F=n2|^f;
let x1,x2 be object such that
A1: x1 in dom F & x2 in dom F & F.x1=F.x2;
A2: dom F=dom f by Def4;
then A3:F.x1 = n2 to_power (f.x1) & F.x2 = n2 to_power (f.x2) by A1,Def4;
n+1+1 > 0+1 by XREAL_1:8;
then f.x1=f.x2 by A1,A3,PEPIN:30;
hence thesis by A1,A2,FUNCT_1:def 4;
end;
end;
theorem Th23:
for r,s be Real holds
r |^ <*s*> = <* r to_power s *>
proof
let r,s be Real;
A1: len <*s*> =1 by FINSEQ_1:39;
dom <*s*> = Seg 1 & Seg 1 = {1} by FINSEQ_1:2,38;
then 1 in dom <*s*> & <*s*>.1=s;
then (r |^ <*s*>).1 = r to_power s by Def4;
hence thesis by A1,CARD_1:def 7,FINSEQ_1:40;
end;
theorem Th24:
for r be Real,
f,g be real-valued FinSequence holds
r |^ (f^g) = (r |^ f) ^ (r |^ g)
proof
let r be Real,f,g be real-valued FinSequence;
set fg=f^g,rf=r|^f,rg=r|^g;
A1:len fg=len f+len g & len (rf^rg) = len rf + len rg by FINSEQ_1:22;
A2:len rf = len f & len rg = len g & len (r|^fg) = len fg by CARD_1:def 7;
then A3:dom f = dom rf & dom g = dom rg by FINSEQ_3:29;
for i st 1<= i & i <= len fg holds (r|^fg).i = (rf^rg).i
proof
let i;
assume 1<= i & i <= len fg;
then A4:i in dom fg by FINSEQ_3:25;
then A5: (r|^fg).i = r to_power (fg.i) by Def4;
per cases by A4,FINSEQ_1:25;
suppose A6: i in dom f;
then fg.i=f.i & (rf^rg).i = rf.i by A3,FINSEQ_1:def 7;
hence thesis by A6,Def4,A5;
end;
suppose ex j st j in dom g & i=len f+j;
then consider j such that
A7:j in dom g & i = len f+j;
fg.i = g.j & (rf^rg).i = rg.j by A3,A7,A2,FINSEQ_1:def 7;
hence thesis by A7,Def4,A5;
end;
end;
hence thesis by A1,A2;
end;
theorem
for f be real-valued Function, g be Function holds
(2|^f) * g = 2|^(f * g)
proof
let f be real-valued Function, g be Function;
set 2f=2|^f,fg=f*g;
A1:dom 2f=dom f & dom (2|^fg)= dom fg by Def4;
A2:dom (2f*g) c= dom (2|^fg)
proof
let x;
assume x in dom (2f*g);
then x in dom g & g.x in dom 2f by FUNCT_1:11;
hence thesis by A1,FUNCT_1:11;
end;
dom (2|^fg) c= dom (2f*g)
proof
let x;
assume x in dom (2|^fg);
then x in dom g & g.x in dom f by A1,FUNCT_1:11;
hence thesis by A1,FUNCT_1:11;
end;
then A3:dom (2|^fg) = dom (2f*g) by A2;
for x st x in dom (2|^fg) holds (2f*g).x = (2|^fg).x
proof
let x;
assume A4: x in dom (2|^fg);
then x in dom g & g.x in dom f by A1,FUNCT_1:11;
then
(2f*g).x = 2f.(g.x) & 2f.(g.x) = 2 to_power (f.(g.x)) & f.(g.x) = fg.x
by Def4,FUNCT_1:13;
hence thesis by A4,A1,Def4;
end;
hence thesis by A3;
end;
Lm5:for f1,f2 be natural-valued FinSequence st len f1 = i+1 & f1|i=f2 holds
Sum (n|^f1) = Sum (n|^ f2) + (n |^ (f1.(i+1)))
proof
let f1,f2 be natural-valued FinSequence such that A1:
len f1 = i+1 & f1|i=f2;
set i1=i+1;
f1 = (f1|i)^ <*f1.i1*> by A1,FINSEQ_3:55;
then n|^f1 = (n|^ f2) ^ (n|^<*f1.i1*>) by Th24,A1
.= (n|^ f2) ^ <*n to_power (f1.i1)*> by Th23;
hence thesis by RVSUM_1:74;
end;
theorem Th26:
for f be increasing natural-valued FinSequence st n > 1 holds
(n|^f).1 + (n|^f,2) +... < 2 * n |^ (f.len f)
proof
defpred P[Nat] means
for f be increasing natural-valued FinSequence st n >1 & f.len f <= $1 &
f <> {}
holds
Sum (n|^f) < 2 * n |^ (f.len f);
A1:for f be natural-valued FinSequence st n>1 & len f = 1 holds
Sum (n|^f) < 2 * n |^ (f.len f)
proof
let f be natural-valued FinSequence;
assume A2:n>1 & len f =1;
then A3:1 in dom f by FINSEQ_3:25;
n to_power (f.1)>0 by A2,NEWTON:83;
then 1*(n to_power (f.1)) < 2* (n to_power (f.1)) by XREAL_1:68;
then A4:(n|^f).1 < 2 * n |^ (f.len f) by A3,Def4,A2;
n|^f = <* (n|^f).1 *> by CARD_1:def 7,A2,FINSEQ_1:40;
hence thesis by RVSUM_1:73,A4;
end;
A5:P[0]
proof
let f be increasing natural-valued FinSequence such that
A6:n >1 & f.len f <= 0 & f <>{};
len f <=1
proof
assume A7:len f >1;
then 1 in dom f & len f in dom f by FINSEQ_3:25;
then f.1 < 0 by A7,VALUED_0:def 13,A6;
hence thesis;
end;
then len f =1 by NAT_1:25, A6;
hence thesis by A6,A1;
end;
A8:P[i] implies P[i+1]
proof
assume A9:P[i];
set i1=i+1;
let f be increasing natural-valued FinSequence such that
A10:n >1 & f.len f <= i1 & f <>{};
per cases by A10,NAT_1:8;
suppose f.len f <=i;
hence thesis by A10,A9;
end;
suppose f.len f = i1;
per cases by A10,NAT_1:25;
suppose len f =1;
hence thesis by A10,A1;
end;
suppose A11:len f >1;
then reconsider l1=len f-1 as Nat;
reconsider f1=f|l1 as natural-valued FinSequence;
l1+1>1 by A11;
then A12: l1 >= 1 & l1+1 > l1 by NAT_1:13;
then A13:l1 in dom f & len f in dom f by A11,FINSEQ_3:25;
then f.l1 < f.len f by A12,VALUED_0:def 13;
then f.l1 < i1 by A10,XXREAL_0:2;
then A14: f.l1 <= i by NAT_1:13;
len f = l1+1;
then A15:Sum (n|^f) = Sum (n|^ f1) + (n |^ (f.len f)) by Lm5;
A16:len f1 = l1 by A12,FINSEQ_1:59;
A17:f1<>{} by A12,FINSEQ_1:59;
l1 in Seg l1 by A12;
then A18:f.l1 = f1.l1 by FUNCT_1:49;
A19: Sum (n|^f1) < 2 * n|^(f.l1) by A17,A18,A16,A10,A9,A14;
1+f.l1 <= f.len f by A13,A12,VALUED_0:def 13,NAT_1:13;
then A20: n |^ (1+f.l1) <= n |^ (f.len f) by PREPOWER:93,A10;
n>= 1+ 1 by A10,NAT_1:13;
then A21: 2* (n |^ (f.l1)) <= n*(n |^(f.l1)) by XREAL_1:64;
n |^ (1+f.l1) = n* (n |^(f.l1)) by NEWTON:6;
then Sum (n|^f1) < n |^(1+f.l1) by XXREAL_0:2,A19,A21;
then Sum (n|^f1) < n |^(f.len f) by XXREAL_0:2,A20;
then Sum (n|^f) < (n |^(f.len f))+(n |^(f.len f)) by A15,XREAL_1:8;
hence thesis;
end;
end;
end;
A22:P[i] from NAT_1:sch 2(A5,A8);
let f be increasing natural-valued FinSequence such that A23: n > 1;
A24:Sum (n|^f) = (n|^f).1+(n|^f,2)+... by Th22;
per cases;
suppose f={};
then A25:Sum (n|^f)=0 by RVSUM_1:72;
n |^ (f.len f) >0 by A23,NEWTON:83;
hence thesis by A24,A25;
end;
suppose f<>{};
hence thesis by A22,A23,A24;
end;
end;
Lm6:for f1,f2 be increasing natural-valued FinSequence st
n > 1 & Sum (n|^f1) > 0 & Sum (n|^f1) = Sum (n|^f2)
holds f1.len f1 <= f2.len f2
proof
let f1,f2 be increasing natural-valued FinSequence such that
A1: n > 1 & Sum (n|^f1) >0 & Sum (n|^f1) = Sum (n|^f2);
A2:(n|^f1,1)+... = Sum (n|^f1) & Sum (n|^f2) = (n|^f2).1 + (n|^f2,2)+... &
(n|^f2,1)+... = Sum (n|^f2) by Th21,Th22;
set l1=len f1;
set l2=len f2;
A3: f1 <>{} by A1,RVSUM_1:72;
assume f1.l1 > f2.l2;
then f1.l1 >= 1+f2.l2 by NAT_1:13;
then A4: n|^ (f1.l1) >= n|^ (1+f2.l2) by PREPOWER:93,A1;
A5:Sum (n|^f1) < 2* n |^ (f2.l2) by A1,Th26,A2;
reconsider L1=l1-1 as Nat by A3;
reconsider F1=f1|L1 as natural-valued FinSequence;
A6:(n|^F1,1)+... = Sum (n|^F1) by Th21;
L1+1 = l1;
then Sum (n|^f1) = Sum (n|^ F1) + (n |^ (f1.l1)) by Lm5;
then Sum (n|^f1) >= 0+(n |^ (f1.l1)) by A6,XREAL_1:6;
then A7: n |^ (f1.l1) < 2* n |^ (f2.l2) by A5,XXREAL_0:2;
n>= 1+ 1 by A1,NAT_1:13;
then 2* (n |^ (f2.l2)) <= n*(n |^ (f2.l2)) by XREAL_1:64;
then 2* (n |^ (f2.l2)) <= n |^ (1+ f2.l2) by NEWTON:6;
hence thesis by A7,XXREAL_0:2,A4;
end;
theorem Th27:
for f1,f2 be increasing natural-valued FinSequence st
n > 1 & (n|^f1).1 + (n|^f1,2) +... = (n|^f2).1 + (n|^f2,2) +...
holds f1 = f2
proof
A1:for f be natural-valued FinSequence st
n > 1 & Sum (n|^f) <= 0 holds f={}
proof
let f be natural-valued FinSequence such that
A2:n > 1 & Sum (n|^f) <= 0;
assume f<>{};
then consider x such that
A3: x in dom f by XBOOLE_0:def 1;
reconsider x as Nat by A3;
A4:for i st i in dom (n|^f) holds 0 <= (n|^f).i;
dom (n|^f) =dom f by Def4;
then A5: 0 >= (n|^f).x by A4,A2,RVSUM_1:85,A3;
n to_power (f.x) > 0 by A2, NEWTON:83;
hence thesis by A5,A3,Def4;
end;
defpred P[Nat] means
for f1,f2 be increasing natural-valued FinSequence st
n > 1 & Sum (n|^f1) <= $1 & Sum (n|^f1) = Sum (n|^f2)
holds f1 = f2;
A6:P[0]
proof
let f1,f2 be increasing natural-valued FinSequence such that
A7:n > 1 & Sum (n|^f1) <= 0 &
Sum (n|^f1) = Sum (n|^f2);
f1 ={} by A7,A1;
hence thesis by A7,A1;
end;
A8:P[i] implies P[i+1]
proof
assume A9:P[i];
set i1=i+1;
let f1,f2 be increasing natural-valued FinSequence such that
A10:n > 1 & Sum (n|^f1) <= i+1 &
Sum (n|^f1) = Sum (n|^f2);
per cases by A10,NAT_1:8;
suppose Sum (n|^f1) <= i;
hence thesis by A10,A9;
end;
suppose A12:Sum (n|^f1) = i1;
set l1=len f1;
set l2=len f2;
A13: f1 <>{} by A12,RVSUM_1:72;
A14: f2 <>{} by A10,A12,RVSUM_1:72;
A15:f1.l1 <= f2.l2 by Lm6,A10,A12;
A16: f1.l1 >= f2.l2 by Lm6,A10,A12;
then A17: f1.l1 = f2.l2 by A15,XXREAL_0:1;
reconsider L1=l1-1,L2=l2-1 as Nat by A14, A13;
reconsider F1=f1|L1,F2=f2|L2 as increasing natural-valued FinSequence;
A18:n |^ (f2.l2) = n |^ (f1.l1) by A16,A15,XXREAL_0:1;
A19:l1=L1+1 & l2=L2+1;
then A20: Sum (n|^f1) = Sum (n|^ F1) + (n |^ (f1.l1)) &
Sum (n|^f2) = Sum (n|^ F2) + (n |^ (f2.l2)) by Lm5;
n |^ (f1.l1) >0 by PREPOWER:6,A10;
then Sum (n|^ F1)+0 < Sum (n|^f1) by A20,XREAL_1:8;
then A22: Sum (n|^ F1) <= i by A12,NAT_1:13;
f1=F1^<*f1.l1*> & f2=F2^<*f2.l2*> by A19,FINSEQ_3:55;
hence thesis by A17,A22,A10, A20,A18,A9;
end;
end;
A23:P[i] from NAT_1:sch 2(A6,A8);
let f1,f2 be increasing natural-valued FinSequence;
A24:(n|^f1).1+(n|^f1,2)+... = Sum (n|^f1) by Th22;
(n|^f2).1+(n|^f2,2)+... = Sum (n|^f2) by Th22;
hence thesis by A23,A24;
end;
theorem Th28:
for f be natural-valued Function st n>1 holds
Coim(n|^f,n|^k) = Coim(f,k)
proof
let f be natural-valued Function such that A1:n>1;
thus Coim(n|^f,n|^k) c= Coim(f,k)
proof
let x be object;
assume x in Coim(n|^f,n|^k);
then x in (n|^f)"{n|^k} by RELAT_1:def 17;
then x in dom (n|^f) & (n|^f).x in {n|^k} by FUNCT_1:def 7;
then A2:x in dom f & (n|^f).x =n|^k by TARSKI:def 1,Def4;
then (n|^f).x = n to_power (f.x) by Def4
.=n |^ (f.x);
then k=f.x by A2,A1,PEPIN:30;
then f.x in {k} by TARSKI:def 1;
then x in f"{k} by A2,FUNCT_1:def 7;
hence thesis by RELAT_1:def 17;
end;
let x be object;
assume x in Coim(f,k);
then x in f"{k} by RELAT_1:def 17;
then A3:x in dom f & f.x in {k} by FUNCT_1:def 7;
then A4:f.x=k & x in dom (n|^f) by TARSKI:def 1,Def4;
then (n|^f).x = n to_power k by Def4,A3
.= n|^k;
then (n|^f).x in {n|^k} by TARSKI:def 1;
then x in (n|^f)"{n|^k} by FUNCT_1:def 7,A4;
hence thesis by RELAT_1:def 17;
end;
theorem Th29:
for f1,f2 be natural-valued Function st n>1 holds
f1,f2 are_fiberwise_equipotent
iff
n|^f1,n|^f2 are_fiberwise_equipotent
proof
let f1,f2 be natural-valued Function such that
A1:n>1;
set n1=n|^f1,n2=n|^f2;
thus f1,f2 are_fiberwise_equipotent implies n|^f1,n|^f2
are_fiberwise_equipotent
proof
assume A2:f1,f2 are_fiberwise_equipotent;
for x be object holds card Coim(n1,x) = card Coim(n2,x)
proof
let x be object;
A3:Coim(n1,x)= n1"{x} & Coim(n2,x)= n2"{x} by RELAT_1:def 17;
A4:dom n1 = dom f1 & dom n2=dom f2 by Def4;
per cases;
suppose not x in rng n1 & not x in rng n2;
then n1"{x}={} & n2"{x}={} by FUNCT_1:72;
hence thesis by A3;
end;
suppose A5:x in rng n1 & not x in rng n2;
then consider y be object such that
A6: y in dom n1 & n1.y=x by FUNCT_1:def 3;
A7: x = n to_power (f1.y) by A6,A4,Def4;
f1.y in rng f1 by A6,A4,FUNCT_1:def 3;
then f1"{f1.y}<>{} by FUNCT_1:72;
then A8:Coim(f1,f1.y)<>{} by RELAT_1:def 17;
card Coim(f1,f1.y) = card Coim(f2,f1.y) by A2,CLASSES1:def 10;
then Coim(f2,f1.y)<>{} by A8;
then f2"{f1.y}<>{} by RELAT_1:def 17;
then f1.y in rng f2 by FUNCT_1:72;
then consider z be object such that
A9:z in dom f2 & f2.z = f1.y by FUNCT_1:def 3;
A10:z in dom n2 by A9, Def4;
n2.z = x by A9,Def4,A7;
hence thesis by A10,FUNCT_1:def 3,A5;
end;
suppose A11:x in rng n2 & not x in rng n1;
then consider y be object such that
A12: y in dom n2 & n2.y=x by FUNCT_1:def 3;
A13: x = n to_power (f2.y) by A12,A4,Def4;
f2.y in rng f2 by A12,A4,FUNCT_1:def 3;
then f2"{f2.y}<>{} by FUNCT_1:72;
then A14:Coim(f2,f2.y)<>{} by RELAT_1:def 17;
card Coim(f2,f2.y) = card Coim(f1,f2.y) by A2,CLASSES1:def 10;
then Coim(f1,f2.y)<>{} by A14;
then f1"{f2.y}<>{} by RELAT_1:def 17;
then f2.y in rng f1 by FUNCT_1:72;
then consider z be object such that
A15: z in dom f1 & f1.z = f2.y by FUNCT_1:def 3;
A16:z in dom n1 by A15,Def4;
n1.z = x by A15,Def4,A13;
hence thesis by A16,FUNCT_1:def 3,A11;
end;
suppose A17:x in rng n1 & x in rng n2;
then consider y1 be object such that
A18: y1 in dom n1 & n1.y1=x by FUNCT_1:def 3;
A19: x = n to_power (f1.y1) by A18,A4,Def4;
consider y2 be object such that
A20: y2 in dom n2 & n2.y2=x by A17,FUNCT_1:def 3;
A21: x = n to_power (f2.y2) by A20,A4,Def4;
then A22: f2.y2 = f1.y1 by A19,A1,PEPIN:30;
A23:Coim(f2,f2.y2) = Coim(n2,x) by A1,Th28, A21;
Coim(f1,f1.y1) = Coim(n1,x) by A1,Th28,A19;
hence thesis by A22,A2,CLASSES1:def 10,A23;
end;
end;
hence thesis by CLASSES1:def 10;
end;
assume A24:n|^f1,n|^f2 are_fiberwise_equipotent;
for x be object holds card Coim(f1,x) = card Coim(f2,x)
proof
let x be object;
A25: Coim(f1,x) = f1"{x} & Coim(f2,x) = f2"{x} by RELAT_1:def 17;
A26:dom n1 = dom f1 & dom n2=dom f2 by Def4;
per cases;
suppose not x in rng f1 & not x in rng f2;
then f1"{x}={} & f2"{x}={} by FUNCT_1:72;
hence thesis by A25;
end;
suppose A27:x in rng f1 & not x in rng f2;
then consider y be object such that
A28:y in dom f1 & f1.y=x by FUNCT_1:def 3;
n1.y in rng n1 by A26,A28,FUNCT_1:def 3;
then n1"{n1.y}<>{} by FUNCT_1:72;
then A29:Coim(n1,n1.y)<>{} by RELAT_1:def 17;
card Coim(n1,n1.y) = card Coim(n2,n1.y) by A24,CLASSES1:def 10;
then Coim(n2,n1.y)<>{} by A29;
then n2"{n1.y}<>{} by RELAT_1:def 17;
then n1.y in rng n2 by FUNCT_1:72;
then consider z be object such that
A30: z in dom n2 & n2.z = n1.y by FUNCT_1:def 3;
n2.z = n to_power (f2.z) & n1.y = n to_power (f1.y)
by A28,A30,A26,Def4;
then f2.z = f1.y by A30,A1,PEPIN:30;
hence thesis by A30,A26,A28,FUNCT_1:def 3,A27;
end;
suppose A31:x in rng f2 & not x in rng f1;
then consider y be object such that
A32:y in dom f2 & f2.y=x by FUNCT_1:def 3;
n2.y in rng n2 by A26,A32,FUNCT_1:def 3;
then n2"{n2.y}<>{} by FUNCT_1:72;
then A33:Coim(n2,n2.y)<>{} by RELAT_1:def 17;
card Coim(n2,n2.y) = card Coim(n1,n2.y) by A24,CLASSES1:def 10;
then Coim(n1,n2.y)<>{} by A33;
then n1"{n2.y}<>{} by RELAT_1:def 17;
then n2.y in rng n1 by FUNCT_1:72;
then consider z be object such that
A34: z in dom n1 & n1.z = n2.y by FUNCT_1:def 3;
n1.z = n to_power (f1.z) & n2.y = n to_power (f2.y) by A32,A34,A26,Def4;
then f1.z = f2.y by A34,A1,PEPIN:30;
hence thesis by A34,A26,A32,FUNCT_1:def 3,A31;
end;
suppose A35:x in rng f1 & x in rng f2;
then consider y1 be object such that
A36: y1 in dom f1 & f1.y1=x by FUNCT_1:def 3;
A37: n1.y1 = n to_power (f1.y1) by A36,Def4;
consider y2 be object such that
A38: y2 in dom f2 & f2.y2=x by A35,FUNCT_1:def 3;
A39: n2.y2 = n to_power (f2.y2) by A38,Def4;
then A40:card Coim(n2,n2.y2) = card Coim(n1,n1.y1)
by A37,A38,A36,A24,CLASSES1:def 10;
Coim(f2,f2.y2) = Coim(n2,n2.y2) by A1,Th28,A39;
hence thesis by A1,Th28,A37,A40,A36,A38;
end;
end;
hence thesis by CLASSES1:def 10;
end;
theorem
for f1,f2 be one-to-one natural-valued FinSequence st
n > 1 & (n|^f1).1 + (n|^f1,2)+... = (n|^f2).1 + (n|^f2,2)+...
holds rng f1 = rng f2
proof
let f1,f2 be one-to-one natural-valued FinSequence such that
A1: n > 1 & (n|^f1).1+(n|^f1,2)+... = (n|^f2).1+(n|^f2,2)+...;
A2:rng f1 c= NAT & rng f2 c= NAT by VALUED_0:def 6;
then reconsider F1=f1,F2=f2 as FinSequence of REAL by FINSEQ_1:def 4;
set s1=sort_a F1,s2=sort_a F2;
A3:F1,s1 are_fiberwise_equipotent & F2,s2 are_fiberwise_equipotent
by RFINSEQ2:def 6;
A4:rng s1=rng f1 by RFINSEQ2: def 6,CLASSES1:75;
then A5:s1 is natural-valued by A2,VALUED_0:def 6;
n|^F1,n|^s1 are_fiberwise_equipotent by A3,A1,A5,Th29;
then A8: Sum (n|^F1) = Sum(n|^s1) by RFINSEQ:9;
A9:rng s2=rng f2 by RFINSEQ2:def 6,CLASSES1:75;
then A10:s2 is natural-valued by A2,VALUED_0:def 6;
A12:s2 is natural-valued by A9,A2,VALUED_0:def 6;
n|^F2,n|^s2 are_fiberwise_equipotent by A10,A3,A1,Th29;
then A14: Sum (n|^F2) = Sum(n|^s2) by RFINSEQ:9;
A15:for e1,e2 be ExtReal st e1 in dom s1 & e2 in dom s1 & e1 < e2 holds
s1.e1 < s1.e2
proof
let e1,e2 be ExtReal;
assume A16:e1 in dom s1 & e2 in dom s1 & e1 < e2;
then A17:s1.e1 <=s1.e2 by INTEGRA2:2;
assume A18: s1.e1 >= s1.e2;
consider H be Function such that
A19:dom H = dom s1 & rng H = dom F1 & H is one-to-one & s1 = F1 *H
by A3,CLASSES1:77;
s1 is one-to-one by A19;
hence thesis by A18,A17,XXREAL_0:1,A16;
end;
for e1,e2 be ExtReal st e1 in dom s2 & e2 in dom s2 & e1 < e2 holds
s2.e1 < s2.e2
proof
let e1,e2 be ExtReal;
assume A20:e1 in dom s2 & e2 in dom s2 & e1 < e2;
then A21:s2.e1 <=s2.e2 by INTEGRA2:2;
assume A22: s2.e1 >= s2.e2;
consider H be Function such that
A23:dom H = dom s2 & rng H = dom F2 & H is one-to-one & s2 = F2 *H
by A3,CLASSES1:77;
s2 is one-to-one by A23;
hence thesis by A22,A21,XXREAL_0:1,A20;
end;
then A24:s2 is increasing by VALUED_0:def 13;
A25:Sum (n|^s1) = (n|^s1).1+(n|^s1,2)+... by Th22;
Sum (n|^f1) = (n|^f1).1+(n|^f1,2)+... by Th22;
then Sum (n|^s1) = Sum (n|^s2) by Th22,A1,A8,A14;
then
(n|^s1).1+(n|^s1,2)+... = (n|^s2).1+(n|^s2,2)+... &
s1 is increasing natural-valued
by A15,VALUED_0:def 13,A25,Th22,A4,A2,VALUED_0:def 6;
hence thesis by A1,A12,A24,Th27,A9,A4;
end;
theorem
ex f be increasing natural-valued FinSequence st
n = (2|^f).1 + (2|^f,2) +...
proof
set D=digits(n,2);
consider d be XFinSequence of NAT such that
A1: (dom d = dom D & for i being Nat st i in dom d holds d.i = (D.i)*(2|^i))
& value(D,2) = Sum d by NUMERAL1:def 1;
defpred P[Nat] means $1 <= len d implies
ex f be increasing natural-valued FinSequence st
(len f=0 or f.len f < $1) & Sum (2|^f) = Sum (d| $1);
A2:P[0 qua Nat]
proof
assume 0<=len d;
reconsider f=<*>NAT as increasing natural-valued FinSequence;
take f;
Sum (2|^f)=0 by RVSUM_1:72;
hence thesis;
end;
A3:P[i] implies P[i+1]
proof
assume A4:P[i];
set i1=i+1;
assume A5:i1 <= len d;
then consider f be increasing natural-valued FinSequence such that
A6:(len f = 0 or f.len f < i) & Sum (2|^f) = Sum (d|i)
by NAT_1:13,A4;
A7: i in dom d by A5,NAT_1:13,AFINSQ_1:86;
then A8:Sum (d|i1) = Sum (d|i) + d.i & d.i = (D.i)*(2|^i)
by A1,AFINSQ_2:65;
A9:D.i = 0 or D.i =1
proof
per cases;
suppose n=0;
then A10:D=<%0%> by NUMERAL1:def 2;
then dom D=1 & 1 =Segm 1 by AFINSQ_1:def 4,ORDINAL1:def 17;
then i < 1 by A5,NAT_1:13,A1;
then i = 0 by NAT_1:25;
thus thesis by A10;
end;
suppose n<>0;
then 0<= D.i & D.i < 2 by A7,A1,NUMERAL1:def 2;
hence thesis by NAT_1:23;
end;
end;
per cases by A9;
suppose A11:D.i=0;
take f;
thus thesis by A11,A8,A6,NAT_1:13;
end;
suppose A12:D.i =1;
set fi = f^<*i*>;
A13: len fi = len f +1 by FINSEQ_2:16;
for e1,e2 be ExtReal st e1 in dom fi & e2 in dom fi & e1 < e2 holds
fi.e1 < fi.e2
proof
let e1,e2 be ExtReal such that
A14: e1 in dom fi & e2 in dom fi & e1 < e2;
A15:1<= e1 & 1 <= e2 & e1 <= len f+1 & e2 <= len f+1
by A14,A13,FINSEQ_3:25;
per cases;
suppose e1 <= len f & e2 <= len f;
then e1 in dom f & e2 in dom f by A15,A14,FINSEQ_3:25;
then f.e1 < f.e2 & f.e1 = fi.e1 & f.e2 = fi.e2
by A14,VALUED_0:def 13,FINSEQ_1:def 7;
hence thesis;
end;
suppose A16:e1 <= len f & e2 > len f;
then e2 >= len f+1 by A14,NAT_1:13;
then e2 = len f+1 by A15,XXREAL_0:1;
then A17:fi.e2 = i by FINSEQ_1:42;
A18:e1=len f or e1 < len f by A16,XXREAL_0:1;
len f >= 1 by A16,A15,XXREAL_0:2;
then A19:f.len f < i & len f in dom f & e1 in dom f
by A14,A15,A16,A6,FINSEQ_3:25;
then f.e1 <= f.len f by A18,VALUED_0:def 13;
then f.e1 < i by A16,A14,FINSEQ_3:25,XXREAL_0:2, A6;
hence thesis by A19,FINSEQ_1:def 7,A17;
end;
suppose e1 > len f & e2 <= len f;
hence thesis by A14,XXREAL_0:2;
end;
suppose e1 > len f & e2 > len f;
then e1 >= len f+1 & e2 >= len f+1 by A14,NAT_1:13;
hence thesis by A15,A14,XXREAL_0:1;
end;
end;
then reconsider fi as increasing natural-valued FinSequence
by VALUED_0:def 13;
take fi;
fi.len fi = i & i < i1 by A13,NAT_1:13,FINSEQ_1:42;
hence len fi=0 or fi.len fi < i+1;
dom f = Seg len f by FINSEQ_1:def 3;
then fi|len f = f by FINSEQ_1:21;
then Sum (2|^fi) = Sum (2|^f) + (2|^fi.(len f+1)) by FINSEQ_2:16,Lm5;
hence thesis by FINSEQ_1:42,A12,A8,A6;
end;
end;
P[i] from NAT_1:sch 2(A2,A3);
then consider f be increasing natural-valued FinSequence such that
len f=0 or f.len f < len d and
A20:Sum (2|^f) = Sum (d| len d);
A21:Sum (2|^f) = (2|^f).1 + (2|^f,2)+... by Th22;
Sum d = n by A1,NUMERAL1:5;
hence thesis by A20,A21;
end;
begin :: Value-based Function (Re)Organization
definition
let o be Function-yielding Function;
let x,y be object;
func o_(x,y) -> set
equals o.x.y;
coherence;
end;
definition
let F be Function-yielding Function;
attr F is double-one-to-one means :Def6:
for x1,x2,y1,y2 be object st
x1 in dom F & y1 in dom (F.x1) &
x2 in dom F & y2 in dom (F.x2) & F_(x1,y1)=F_(x2,y2)
holds x1=x2 & y1=y2;
end;
registration
let D be set;
cluster empty -> double-one-to-one for FinSequence of D*;
coherence;
end;
registration
cluster double-one-to-one for Function-yielding Function;
existence
proof
take the empty FinSequence of (the set)*;
thus thesis;
end;
let D be set;
cluster double-one-to-one for FinSequence of D*;
existence
proof
take the empty FinSequence of D*;
thus thesis;
end;
end;
registration
let F be double-one-to-one Function-yielding Function;
let x be object;
cluster F.x -> one-to-one;
coherence
proof
per cases;
suppose A1:x in dom F;
let x1,x2 be object;
assume A2:x1 in dom (F.x) & x2 in dom (F.x) & (F.x).x1=(F.x).x2;
then F_(x,x1) = F_(x,x2);
hence thesis by A2,A1,Def6;
end;
suppose not x in dom F;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let F be one-to-one Function;
cluster <*F*> -> double-one-to-one;
coherence
proof
set FF=<*F*>;
let x1,x2,y1,y2 be object such that
A1:x1 in dom FF & y1 in dom (FF.x1) &
x2 in dom FF & y2 in dom (FF.x2) & FF_(x1,y1)=FF_(x2,y2);
dom FF=Seg 1 & Seg 1 = {1} by FINSEQ_1:2,38;
then x1 = 1 & x2 = 1 & FF.1=F by A1,TARSKI:def 1;
hence thesis by A1,FUNCT_1:def 4;
end;
end;
theorem
for f be Function-yielding Function holds
f is double-one-to-one iff
(for x holds f.x is one-to-one)
&
for x,y st x<>y holds rng (f.x) misses rng (f.y)
proof
let f be Function-yielding Function;
thus f is double-one-to-one implies
(for x holds f.x is one-to-one)&
for x,y st x<>y holds rng (f.x) misses rng (f.y)
proof
assume A1:f is double-one-to-one;
hence for x holds f.x is one-to-one;
let x,y;
assume A2:x<>y;
assume rng (f.x) meets rng (f.y);
then consider z be object such that
A3: z in rng (f.x) & z in rng (f.y) by XBOOLE_0:3;
consider w1 be object such that
A4:w1 in dom (f.x) & (f.x).w1 = z by A3,FUNCT_1:def 3;
consider w2 be object such that
A5:w2 in dom (f.y) & (f.y).w2 = z by A3,FUNCT_1:def 3;
A6:f_(x,w1)=f_(y,w2) by A4,A5;
A7:x in dom f
proof
assume not x in dom f;
then f.x={} by FUNCT_1:def 2;
hence thesis by A4;
end;
y in dom f
proof
assume not y in dom f;
then f.y={} by FUNCT_1:def 2;
hence thesis by A5;
end;
hence thesis by A4,A5,A1,A6,A7,A2;
end;
assume that A8:for x holds f.x is one-to-one
and
A9:for x,y st x<>y holds rng (f.x) misses rng (f.y);
let x1,x2,y1,y2 be object such that
A10: x1 in dom f & y1 in dom (f.x1) &
x2 in dom f & y2 in dom (f.x2) & f_(x1,y1)=f_(x2,y2);
A11:f.x1.y1 in rng (f.x1) by A10,FUNCT_1:def 3;
f.x2.y2 in rng (f.x2) by A10,FUNCT_1:def 3;
then x1=x2 & f.x1.y1=f.x2.y2 & f.x1 is one-to-one
by A11,A10,XBOOLE_0:3,A8,A9;
hence thesis by A10;
end;
theorem Th33:
for D be set
for f1,f2 be double-one-to-one FinSequence of D* st
Values f1 misses Values f2
holds
f1^f2 is double-one-to-one
proof
let D be set;
let f1,f2 be double-one-to-one FinSequence of D* such that
A1:Values f1 misses Values f2;
set F=f1^f2;
let x1,x2,y1,y2 be object such that
A2:x1 in dom F & y1 in dom (F.x1) &
x2 in dom F & y2 in dom (F.x2) & F_(x1,y1)=F_(x2,y2);
reconsider x1,x2 as Nat by A2;
per cases;
suppose A3:x1 in dom f1 & x2 in dom f1;
then A4:F.x1 = f1.x1 & F.x2 = f1.x2 by FINSEQ_1:def 7;
then f1_(x1,y1)=f1_(x2,y2) by A2;
hence thesis by A2,A3,Def6,A4;
end;
suppose A5:x1 in dom f1 & not x2 in dom f1;
then consider n such that
A6:n in dom f2 & x2= len f1+n by A2,FINSEQ_1:25;
F.x2=f2.n & F.x1=f1.x1 by A5,A6,FINSEQ_1:def 7;
then F.x2.y2 in Values f2 & F.x2.y2 in Values f1 by A2,A5,A6,Th1;
hence thesis by A1,XBOOLE_0:3;
end;
suppose A7:not x1 in dom f1 & x2 in dom f1;
then consider n such that
A8:n in dom f2 & x1= len f1+n by A2,FINSEQ_1:25;
F.x1=f2.n & F.x2=f1.x2 by A7,A8,FINSEQ_1:def 7;
then F.x2.y2 in Values f1 & F.x2.y2 in Values f2
by A2,A7,A8,Th1;
hence thesis by A1,XBOOLE_0:3;
end;
suppose A9:not x1 in dom f1 & not x2 in dom f1;
then consider n such that
A10:n in dom f2 & x1= len f1+n by A2,FINSEQ_1:25;
consider k such that
A11:k in dom f2 & x2= len f1+k by A2,A9,FINSEQ_1:25;
A12:F.x1 = f2.n & F.x2 = f2.k by A10,A11,FINSEQ_1:def 7;
then f2_(n,y1)=f2_(k,y2) by A2;
hence thesis by A2,A10,A11,Def6,A12;
end;
end;
definition
let D be finite set;
mode DoubleReorganization of D -> double-one-to-one FinSequence of D*
means :Def7:
Values it = D;
existence
proof
set F=canFS D;
F is Element of D* by FINSEQ_1:def 11;
then {F} c= D* & rng <*F*> = {F} by ZFMISC_1:31,FINSEQ_1:38;
then reconsider FF=<*F*> as double-one-to-one FinSequence of D*
by FINSEQ_1:def 4;
A1:rngs FF = <*rng F*> by FINSEQ_3:132;
rng <*rng F*> = {rng F} by FINSEQ_1:38;
then union rng <*rng F*> =rng F by ZFMISC_1:25;
then Union rngs FF = rng F by CARD_3:def 4,A1;
then Values FF = rng F by MATRIX_0:def 9;
hence thesis by FUNCT_2:def 3;
end;
end;
theorem Th34:
{} is DoubleReorganization of {} & <* {} *> is DoubleReorganization of {}
proof
{} = <*> ({}*);
then reconsider D={} as double-one-to-one FinSequence of {}*;
rngs D = {} --> D by FUNCT_6:23;
then Union rngs D={} by FUNCT_6:26;
then Values D = {} by MATRIX_0:def 9;
hence {} is DoubleReorganization of {} by Def7;
rng {} = {};
then reconsider F={} as FinSequence of {} by FINSEQ_1:def 4;
{F} c= {}* & rng <*F*> = {F} by FINSEQ_1:38;
then reconsider FF=<*F*> as double-one-to-one FinSequence of {}*
by FINSEQ_1:def 4;
A1: rngs FF = <*rng F*> by FINSEQ_3:132;
rng <*rng F*> = {rng F} by FINSEQ_1:38;
then union rng <*rng F*> =rng F by ZFMISC_1:25;
then Union rngs FF = rng F by CARD_3:def 4,A1;
then Values FF ={} by MATRIX_0:def 9;
hence thesis by Def7;
end;
theorem Th35:
for D be finite set, F be one-to-one onto FinSequence of D holds
<*F*> is DoubleReorganization of D
proof
let D be finite set,
F be one-to-one onto FinSequence of D;
F is Element of D* by FINSEQ_1:def 11;
then {F} c= D* & rng <*F*> = {F} by ZFMISC_1:31,FINSEQ_1:38;
then reconsider FF=<*F*> as double-one-to-one FinSequence of D*
by FINSEQ_1:def 4;
A1:rngs FF = <*rng F*> by FINSEQ_3:132;
rng <*rng F*> = {rng F} by FINSEQ_1:38;
then union rng <*rng F*> =rng F by ZFMISC_1:25;
then Union rngs FF = rng F by CARD_3:def 4,A1;
then Values FF = rng F by MATRIX_0:def 9;
hence thesis by FUNCT_2:def 3,Def7;
end;
theorem Th36:
for D1,D2 be finite set st D1 misses D2
for o1 be DoubleReorganization of D1,
o2 be DoubleReorganization of D2 holds
o1^o2 is DoubleReorganization of D1\/D2
proof
let D1,D2 be finite set such that A1:D1 misses D2;
let o1 be DoubleReorganization of D1,
o2 be DoubleReorganization of D2;
set D=D1\/D2;
rng o1 c= D*
proof
let x be object;
assume x in rng o1;
then reconsider x as FinSequence of D1 by FINSEQ_1:def 11;
rng x c= D1 & D1 c= D by XBOOLE_1:7;
then rng x c= D;
then x is FinSequence of D by FINSEQ_1:def 4;
hence thesis by FINSEQ_1:def 11;
end;
then reconsider O1=o1 as FinSequence of D* by FINSEQ_1:def 4;
rng o2 c= D*
proof
let x be object;
assume x in rng o2;
then reconsider x as FinSequence of D2 by FINSEQ_1:def 11;
rng x c= D2 & D2 c= D by XBOOLE_1:7;
then rng x c= D;
then x is FinSequence of D by FINSEQ_1:def 4;
hence thesis by FINSEQ_1:def 11;
end;
then reconsider O2=o2 as FinSequence of D* by FINSEQ_1:def 4;
A2:Values o1 =D1 & Values o2 =D2 by Def7;
then A3:O1^O2 is double-one-to-one by A1,Th33;
Values(O1^O2)=D1\/D2 by A2,Th2;
hence thesis by A3,Def7;
end;
theorem Th37:
for D be finite set,
o be DoubleReorganization of D,
F be one-to-one FinSequence st
i in dom o & rng F /\ D c= rng (o.i)
holds
o+*(i,F) is DoubleReorganization of rng F \/ (D\rng (o.i))
proof
let D be finite set,
o be DoubleReorganization of D,
F be one-to-one FinSequence such that
A1: i in dom o & rng F /\ D c= rng (o.i);
set rF=rng F,oi=o.i,roi=rng oi,oF=o+*(i,F);
A2:dom oF=dom o by FUNCT_7:30;
A3:oF.i=F by A1,FUNCT_7:31;
A4:Values o=D by Def7;
rng oF c= (rF\/(D\roi))*
proof
let y be object;
assume y in rng oF;
then consider x be object such that
A5: x in dom oF & oF.x=y by FUNCT_1:def 3;
per cases;
suppose x=i;
then A6:y=F by A5,A1,FUNCT_7:31;
F is FinSequence of rF \/ (D\roi) by XBOOLE_1:7,FINSEQ_1:def 4;
hence thesis by A6,FINSEQ_1:def 11;
end;
suppose A7:x<>i;
then A8:oF.x = o.x by FUNCT_7:32;
o.x in rng o by A2,A5,FUNCT_1:def 3;
then reconsider ox=o.x as FinSequence of D by FINSEQ_1:def 11;
rng ox misses roi
proof
assume rng ox meets roi;
then consider z be object such that
A9: z in rng ox & z in roi by XBOOLE_0:3;
consider a be object such that
A10: a in dom ox & ox.a = z by A9,FUNCT_1:def 3;
consider b be object such that
A11: b in dom oi & oi.b = z by A9,FUNCT_1:def 3;
o_(x,a) = o_(i,b) by A10,A11;
hence thesis by A10,A11,A5,A2,A1,Def6,A7;
end;
then A12: rng ox c= D\roi by XBOOLE_1:86;
D\roi c= rF\/(D\roi) by XBOOLE_1:7;
then rng ox c= rF\/(D\roi) by A12;
then ox is FinSequence of rF\/(D\roi) by FINSEQ_1:def 4;
hence thesis by A8,A5,FINSEQ_1:def 11;
end;
end;
then reconsider oF as FinSequence of (rF\/(D\roi))* by FINSEQ_1:def 4;
A13:oF is double-one-to-one
proof
let x1,x2,y1,y2 be object such that
A14:x1 in dom oF & y1 in dom (oF.x1) &
x2 in dom oF & y2 in dom (oF.x2) & oF_(x1,y1)=oF_(x2,y2);
per cases;
suppose x1 = i & x2=i;
hence thesis by A3,A14,FUNCT_1:def 4;
end;
suppose A15: x1 = i & x2<>i;
then A16: oF.x1.y1 in rF by A3,A14,FUNCT_1:def 3;
A17: oF.x2 = o.x2 by A15,FUNCT_7:32;
then o.x2.y2 in D by A14,A2,Th1,A4;
then o.x2.y2 in D/\rF by A14,A17,A16,XBOOLE_0:def 4;
then consider y3 be object such that
A18:y3 in dom oi & oi.y3 = o.x2.y2 by A1,FUNCT_1:def 3;
o_(x2,y2)=o_(i,y3) by A18;
hence thesis by Def6,A2,A18,A14,A17,A15;
end;
suppose A19: x1 <> i & x2=i;
then A20: oF.x2.y2 in rF by A3,A14,FUNCT_1:def 3;
A21: oF.x1 = o.x1 by A19,FUNCT_7:32;
then o.x1.y1 in D by A14,A2,Th1,A4;
then o.x1.y1 in D/\rF by A14,A21,A20,XBOOLE_0:def 4;
then consider y3 be object such that
A22:y3 in dom oi & oi.y3 = o.x1.y1 by A1,FUNCT_1:def 3;
o_(x1,y1) = o_(i,y3) by A22;
hence thesis by Def6,A2,A22,A14,A21,A19;
end;
suppose x1 <> i & x2<>i;
then A23:o.x1 = oF.x1 & o.x2=oF.x2 by FUNCT_7:32;
then o_(x1,y1)=o_(x2,y2) by A14;
hence thesis by A23,A14,A2,Def6;
end;
end;
A24: Values oF c= rF\/(D\roi)
proof
let z be object;
assume z in Values oF;
then consider x,y be object such that
A25:x in dom oF & y in dom (oF.x) & z = oF.x.y by Th1;
per cases;
suppose x=i;
then oF.x = F by A1,FUNCT_7:31;
then z in rF by A25,FUNCT_1:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose A26:x<>i;
then A27:oF.x = o.x by FUNCT_7:32;
then A28:z in D by A4,A2,A25,Th1;
not z in roi
proof
assume z in roi;
then consider a be object such that
A29:a in dom oi & oi.a = z by FUNCT_1:def 3;
o_(i,a)=o_(x,y) by A26,FUNCT_7:32,A25,A29;
hence thesis by A27,A25,A29,A1,A2,Def6,A26;
end;
then z in D\roi by A28,XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
end;
A30: D\roi c= Values oF
proof
let d be object;
assume A31:d in D\roi;
then A32:d in D & not d in roi by XBOOLE_0:def 5;
consider x,y be object such that
A33:x in dom o & y in dom (o.x) & d = o.x.y by A31,Th1,A4;
x<>i by A33,FUNCT_1:def 3,A32;
then o.x = oF.x by FUNCT_7:32;
hence thesis by Th1,A2,A33;
end;
rF c= Values oF
proof
let d be object;
assume d in rF;
then ex x be object st x in dom F & F.x = d by FUNCT_1:def 3;
hence thesis by A1,A2,A3,Th1;
end;
then Values oF = rF\/(D\roi) by A30,XBOOLE_1:8,A24;
hence thesis by A13,Def7;
end;
registration
let D be finite set;
let n be non zero Nat;
cluster n-element for DoubleReorganization of D;
existence
proof
defpred P[Nat] means $1>0 implies
ex o be DoubleReorganization of D st o is $1-element;
A1:P[0];
A2:P[i] implies P[i+1]
proof
assume A3:P[i];
assume i+1>0;
per cases;
suppose A4:i=0;
set F=canFS D;
<*F*> is DoubleReorganization of D by Th35;
hence thesis by A4;
end;
suppose i>0;
then consider o be DoubleReorganization of D such that
A5:o is i-element by A3;
reconsider e = <* {} *> as DoubleReorganization of {} by Th34;
D misses {};
then o^e is DoubleReorganization of D\/{} by Th36;
hence thesis by A5;
end;
end;
P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
end;
registration
let D be finite natural-membered set;
let o be DoubleReorganization of D;
let x be object;
cluster o.x -> natural-valued;
coherence
proof
set ox=o.x;
per cases;
suppose A1: x in dom o;
rng ox c= NAT
proof
let y be object;
assume y in rng ox;
then consider z be object such that
A2:z in dom ox & ox.z=y by FUNCT_1:def 3;
y in Values o by A1,A2,Th1;
then y in D by Def7;
hence thesis by ORDINAL1:def 12;
end;
hence thesis by VALUED_0:def 6;
end;
suppose not x in dom o;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
theorem Th38:
for F be non empty FinSequence,
G be finite Function st rng G c= rng F
ex o be len F-element DoubleReorganization of dom G st
for n holds
(F.n = G.o_(n,1) &...& F.n = G.o_(n,len (o.n)) )
proof
let F be non empty FinSequence,
G be finite Function such that A1: rng G c= rng F;
set D=dom G;
set d = the one-to-one onto FinSequence of D;
A2:rng d = D by FUNCT_2:def 3;
then A3: card dom d = card D by CARD_1:70;
A4:dom d = Seg len d by FINSEQ_1:def 3;
A5:card D=len d & card G = card D by CARD_1:62,A3;
defpred P[Nat] means
$1 <= card G implies
ex o be len F-element DoubleReorganization of d.:(Seg $1) st
for k holds
(F.k = G.(o_(k,1)) &...& F.k = G.(o_(k,len (o.k))));
A6: P[0]
proof
assume 0 <= card G;
take o= the len F-element DoubleReorganization of d.:(Seg 0);
let i,j;
thus thesis;
end;
A7:P[i] implies P[i+1]
proof
set i1=i+1,di1=d.i1;
assume A8:P[i];
assume A9: i1 <= card G;
then consider o be len F-element DoubleReorganization of d.:(Seg i)
such that
A10: for j holds
( F.j = G.(o_(j,1)) &...& F.j = G.(o_(j,len (o.j)))) by NAT_1:13,A8;
A11: len o =len F by CARD_1:def 7;
then A12: dom o = dom F by FINSEQ_3:29;
A13: Values o = d.:(Seg i) by Def7;
A14: i1 in dom d by NAT_1:11,A5,A9,FINSEQ_3:25;
then di1 in D by A2,FUNCT_1:def 3;
then G.di1 in rng G by FUNCT_1:def 3;
then consider x be object such that
A15: x in dom F & F.x = G.di1 by A1,FUNCT_1:def 3;
reconsider x as Nat by A15;
set ox=o.x,I1=<*di1*>,oxI=ox^I1;
A16: i < i1 by NAT_1:13;
not di1 in rng ox
proof
assume d.i1 in rng ox;
then consider y be object such that
A17:y in dom ox & d.i1=ox.y by FUNCT_1:def 3;
d.i1 in d.:(Seg i) by Th1,A15,A12,A13,A17;
then consider z be object such that
A18:z in dom d & z in Seg i & d.z = d.i1 by FUNCT_1:def 6;
i1 in Seg i by A14,FUNCT_1:def 4,A18;
hence thesis by FINSEQ_1:1,A16;
end;
then A19: oxI is one-to-one by GRAPHSP:1;
A20: x in dom o by A15, A11,FINSEQ_3:29;
ox in rng o by A15,A12,FUNCT_1:def 3;
then A21: ox is FinSequence of d.:Seg i by FINSEQ_1:def 11;
then A22: rng ox c= d.:Seg i by FINSEQ_1:def 4;
A23:rng ox /\d.:Seg i = rng ox by A21,FINSEQ_1:def 4,XBOOLE_1:28;
not i1 in Seg i by A16,FINSEQ_1:1;
then {i1} misses Seg i by ZFMISC_1:52,45;
then A24:d.:{i1} /\d.:Seg i=d.:{} by FUNCT_1:62;
then A25:d.:{i1} misses d.:Seg i;
Im(d,i1)={di1} by A14,FUNCT_1:59;
then A26:d.:{i1}={di1} by RELAT_1:def 16;
A27: rng I1 = {di1} by FINSEQ_1:39;
then rng oxI = rng ox \/ {di1} by FINSEQ_1:31;
then A28: rng oxI /\(d.:Seg i) =rng ox \/ {}
by A23,XBOOLE_1:23,A24,A26;
A29: Seg i \/{i1} = Seg i1 by FINSEQ_1:9;
then A30:d.:(Seg i) \/ d.:{i1} = d.:Seg i1 by RELAT_1:120;
d.:Seg i c= d.:Seg i1 by XBOOLE_1:7,A29,RELAT_1:123;
then A31: rng ox c= d.:Seg i1 by A22;
set O= o +*(x,oxI);
rng oxI \/ ((d.: Seg i) \rng ox) =
rng ox \/ {di1} \/ ((d.: Seg i) \rng ox) by A27,FINSEQ_1:31
.= rng ox \/ ({di1} \/ (d.:Seg i \rng ox)) by XBOOLE_1:4
.= rng ox \/ (({di1} \/ d.:Seg i) \rng ox)
by A22,A25,A26,XBOOLE_1:63,XBOOLE_1:87
.= rng ox \/ ({di1} \/ d.:Seg i) by XBOOLE_1:39
.=d.:Seg i1 by A26,A31,XBOOLE_1:12,A30;
then reconsider O as len F-element DoubleReorganization of (d.:Seg i1)
by A19,A20,Th37,A28;
take O;
let k;
set Ok=O.k;
A32: dom I1 = Seg 1 & Seg 1= {1} & I1.1 = di1 by FINSEQ_1:38,2;
thus F.k = G.(O_(k,1)) &...& F.k = G.(O_(k,len Ok))
proof
let j;
assume A33:1 <= j & j <= len Ok;
A34:F.k = G.(o_(k,1)) &...& F.k = G.(o_(k,len (o.k))) by A10;
per cases;
suppose A35: k<>x;
then Ok=o.k by FUNCT_7:32;
then F.k = G.(o_(k,j)) by A33,A34;
hence thesis by A35,FUNCT_7:32;
end;
suppose A36:k=x;
then A37: Ok = oxI by A15,A12,FUNCT_7:31;
per cases;
suppose A38: j in dom ox;
then A39:oxI.j = ox.j & j <= len ox by FINSEQ_1:def 7,FINSEQ_3:25;
o_(k,j) = oxI.j by A36,A38,FINSEQ_1:def 7
.= Ok.j by A36,A15,A12,FUNCT_7:31;
hence thesis by A39,A36,A34,A33;
end;
suppose not j in dom ox;
then consider n such that
A40:n in dom I1 & j=len ox + n by A37,A33,FINSEQ_3:25,FINSEQ_1:25;
n=1 by A32,A40,TARSKI:def 1;
then F.k = G.(oxI.j) by A40,A32,FINSEQ_1:def 7,A15,A36
.= G.(Ok.j) by A36,A15,A12,FUNCT_7:31;
hence thesis;
end;
end;
end;
end;
A41:d.:Seg card D = D by A2,RELAT_1:113,A5,A4;
P[i] from NAT_1:sch 2(A6,A7);
then ex o be len F-element DoubleReorganization of dom G
st
for k holds
(F.k = G.(o_(k,1)) &...& F.k = G.(o_(k,len (o.k)))) by A41,A5;
hence thesis;
end;
theorem
for F be non empty FinSequence,
G be FinSequence st rng G c= rng F
ex o be len F-element DoubleReorganization of dom G st
for n holds o.n is increasing &
(F.n = G.o_(n,1) &...& F.n = G.o_(n,len (o.n)) )
proof
let F be non empty FinSequence,
G be FinSequence such that A1: rng G c= rng F;
defpred P[Nat] means
$1 <= len G implies
ex o be len F-element DoubleReorganization of Seg $1 st
for k holds o.k is increasing &
(F.k = G.(o_(k,1)) &...& F.k = G.(o_(k,len (o.k))));
A2: P[0]
proof
assume 0 <= len G;
take o= the len F-element DoubleReorganization of Seg 0;
let i;
thus o.i is increasing;
let j;
thus thesis;
end;
A3:P[i] implies P[i+1]
proof
set i1=i+1;
assume A4:P[i];
assume A5: i1 <= len G;
then consider o be len F-element DoubleReorganization of Seg i such that
A6: for j holds o.j is increasing &
( F.j = G.(o_(j,1)) &...& F.j = G.(o_(j,len (o.j)))) by NAT_1:13,A4;
A7: len o =len F by CARD_1:def 7;
then A8: dom o = dom F by FINSEQ_3:29;
A9: Values o = Seg i by Def7;
i1 in dom G by NAT_1:11,A5,FINSEQ_3:25;
then G.i1 in rng G by FUNCT_1:def 3;
then consider x be object such that
A10: x in dom F & F.x = G.i1 by A1,FUNCT_1:def 3;
reconsider x as Nat by A10;
set ox=o.x,I1=<*i1*>,oxI=ox^I1;
A11: i < i1 by NAT_1:13;
not i1 in rng ox
proof
assume i1 in rng ox;
then consider y be object such that
A12:y in dom ox & i1=ox.y by FUNCT_1:def 3;
i1 in Seg i by Th1,A10,A8,A9,A12;
hence thesis by FINSEQ_1:1,A11;
end;
then A13: oxI is one-to-one by GRAPHSP:1;
A14: x in dom o by A10, A7,FINSEQ_3:29;
ox in rng o by A10,A8,FUNCT_1:def 3;
then A15: ox is FinSequence of Seg i by FINSEQ_1:def 11;
then A16: rng ox c= Seg i by FINSEQ_1:def 4;
A17:rng ox /\Seg i = rng ox by A15,FINSEQ_1:def 4,XBOOLE_1:28;
not i1 in Seg i by A11,FINSEQ_1:1;
then A18:{i1} misses Seg i by ZFMISC_1:52,45;
A19: rng I1 = {i1} by FINSEQ_1:39;
then rng oxI = rng ox \/ {i1} by FINSEQ_1:31;
then A20: rng oxI /\Seg i =rng ox \/ {} by A17, A18,XBOOLE_1:23;
A21: Seg i \/{i1} = Seg i1 by FINSEQ_1:9;
Seg i c= {i1} \/ Seg i by XBOOLE_1:7;
then A22: rng ox c= {i1} \/ Seg i by A16;
set O= o +*(x,oxI);
rng oxI \/ ( Seg i \rng ox) =
rng ox \/ {i1} \/ ( Seg i \rng ox) by A19,FINSEQ_1:31
.= rng ox \/ ({i1} \/ (Seg i \rng ox)) by XBOOLE_1:4
.= rng ox \/ (({i1} \/ Seg i) \rng ox) by A16,A18,XBOOLE_1:63,XBOOLE_1:87
.= rng ox \/ ({i1} \/ Seg i) by XBOOLE_1:39
.= {i1} \/ Seg i by A22,XBOOLE_1:12;
then reconsider O as len F-element DoubleReorganization of Seg i1
by A13,A14,Th37,A20,A21;
take O;
let k;
set Ok=O.k;
A23: dom I1 = Seg 1 & Seg 1= {1} & I1.1 = i1 by FINSEQ_1:38,2;
thus Ok is increasing
proof
per cases;
suppose k<>x;
then Ok=o.k by FUNCT_7:32;
hence thesis by A6;
end;
suppose k=x;
then A24:Ok= oxI by A10,A8,FUNCT_7:31;
let e1,e2 be ExtReal;
assume A25: e1 in dom Ok & e2 in dom Ok & e1 < e2;
per cases;
suppose A26:e1 in dom ox & e2 in dom ox;
then Ok.e1 = ox.e1 & Ok.e2 = ox.e2 & ox is increasing
by A6,A24,FINSEQ_1:def 7;
hence Ok.e1 < Ok.e2 by A25,A26,VALUED_0:def 13;
end;
suppose not e1 in dom ox & e2 in dom ox;
then e2 <= len ox & 1 <= e1 & (1 > e1 or e1 > len ox)
by A25,FINSEQ_3:25;
hence thesis by XXREAL_0:2,A25;
end;
suppose A27: e1 in dom ox & not e2 in dom ox;
then consider n such that
A28:n in dom I1 & e2=len ox + n by A24,A25,FINSEQ_1:25;
n=1 by A23,A28,TARSKI:def 1;
then A29:oxI.e2 = i1 by A28,FINSEQ_1:def 7,A23;
A30: ox.e1= oxI.e1 by A27,FINSEQ_1:def 7;
ox.e1 in Seg i by A10,A8,Th1,A9,A27;
then ox.e1 <= i by FINSEQ_1:1;
hence thesis by A29,A30, NAT_1:13,A24;
end;
suppose A31: not e1 in dom ox & not e2 in dom ox;
then consider n such that
A32:n in dom I1 & e1=len ox + n by A24,A25,FINSEQ_1:25;
consider k such that
A33:k in dom I1 & e2=len ox + k by A24,A31,A25,FINSEQ_1:25;
n=1 & k=1 by A33,A23,A32,TARSKI:def 1;
hence thesis by A32,A33,A25;
end;
end;
end;
thus F.k = G.(O_(k,1)) &...& F.k = G.(O_(k,len Ok))
proof
let j;
assume A34:1 <= j & j <= len Ok;
A35:F.k = G.(o_(k,1)) &...& F.k = G.(o_(k,len (o.k))) by A6;
per cases;
suppose A36:k<>x;
then Ok=o.k by FUNCT_7:32;
then F.k = G.(o_(k,j)) by A34,A35;
hence thesis by A36,FUNCT_7:32;
end;
suppose A37:k=x;
then A38: Ok = oxI by A10,A8,FUNCT_7:31;
per cases;
suppose A39: j in dom ox;
then A40:oxI.j = ox.j & j <= len ox by FINSEQ_1:def 7,FINSEQ_3:25;
o_(k,j) = oxI.j by A37,A39,FINSEQ_1:def 7
.= Ok.j by A37,A14,FUNCT_7:31;
hence thesis by A40,A37,A35,A34;
end;
suppose not j in dom ox;
then consider n such that
A41:n in dom I1 & j=len ox + n by A38,A34,FINSEQ_3:25,FINSEQ_1:25;
n=1 by A23,A41,TARSKI:def 1;
then F.k = G.(oxI.j) by A41,A23,FINSEQ_1:def 7,A10,A37
.= G.(Ok.j) by A37,A14,FUNCT_7:31;
hence thesis;
end;
end;
end;
end;
A42: dom G=Seg len G by FINSEQ_1:def 3;
P[i] from NAT_1:sch 2(A2,A3);
then ex o be len F-element DoubleReorganization of dom G
st for k holds o.k is increasing &
(F.k = G.(o_(k,1)) &...& F.k = G.(o_(k,len (o.k)))) by A42;
hence thesis;
end;
registration
let f be finite Function;
let o be DoubleReorganization of dom f;
let x be object;
cluster f*(o.x) -> FinSequence-like;
coherence
proof
reconsider X=x as set by TARSKI:1;
per cases;
suppose x in dom o;
then o.x in rng o by FUNCT_1:def 3;
then reconsider ox=o.X as FinSequence of dom f by FINSEQ_1:def 11;
A1: rng ox c= dom f;
dom ox=Seg len ox by FINSEQ_1:def 3;
hence thesis by A1,RELAT_1:27;
end;
suppose not x in dom o;
then o.x={} by FUNCT_1:def 2;
hence thesis;
end;
end;
end;
registration
cluster complex-functions-valued FinSequence-yielding for FinSequence;
existence
proof
take T=the empty Function;
thus thesis;
end;
end;
notation
let f be Function-yielding Function, g be Function;
synonym g*.f for ^^^ g, f __;
end;
registration
let f be Function-yielding Function,g be Function;
cluster g*.f -> Function-yielding;
coherence
proof
now let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in dom (g*.f);
then x in dom f by FOMODEL2:def 6;
then (g*.f).x = g*(f.xx) by FOMODEL2:def 6;
hence (g*.f).x is Function;
end;
hence thesis by FUNCOP_1:def 6;
end;
end;
registration
let g be Function;
let f be (dom g)*-valued FinSequence;
cluster g*.f -> FinSequence-yielding;
coherence
proof
set gf=g*.f;
now let x be object;
reconsider X=x as set by TARSKI:1;
A1:dom gf=dom f by FOMODEL2:def 6;
assume A2:x in dom gf;
then A3: gf.x = g*(f.X) by A1,FOMODEL2:def 6;
f.x in rng f by A2,A1,FUNCT_1:def 3;
then reconsider fx=f.X as FinSequence of dom g by FINSEQ_1:def 11;
A4: rng fx c= dom g;
dom fx=Seg len fx by FINSEQ_1:def 3;
hence gf.x is FinSequence by FINSEQ_1:def 2,A3,A4,RELAT_1:27;
end;
hence thesis by PRE_POLY:def 3;
end;
let x be object;
cluster g*.f.x -> len (f.x) -element;
coherence
proof
set gf=g*.f;
reconsider X=x as set by TARSKI:1;
A5:dom gf=dom f by FOMODEL2:def 6;
per cases;
suppose A6:x in dom gf;
then A7: gf.x = g*(f.X) by A5,FOMODEL2:def 6;
f.x in rng f by A6,A5,FUNCT_1:def 3;
then reconsider fx=f.X as FinSequence of dom g by FINSEQ_1:def 11;
rng fx c= dom g;
then dom (gf.x) = dom fx by RELAT_1:27,A7;
then len (gf.X)=len fx by FINSEQ_3:29;
hence thesis by CARD_1:def 7;
end;
suppose not x in dom gf;
then gf.x = {} & f.x={} by A5,FUNCT_1:def 2;
hence thesis;
end;
end;
end;
registration
let f be Function-yielding FinSequence,g be Function;
cluster g*.f -> FinSequence-like;
coherence
proof
dom (g*.f) = dom f & dom f= Seg len f by FOMODEL2:def 6,FINSEQ_1:def 3;
hence thesis;
end;
cluster g*.f -> len f -element;
coherence
proof
dom (g*.f) = dom f & dom f= Seg len f by FOMODEL2:def 6,FINSEQ_1:def 3;
then len (g*.f) = len f by FINSEQ_3:29;
hence thesis by CARD_1:def 7;
end;
end;
registration
let f be Function-yielding Function, g be complex-valued Function;
cluster g*.f -> complex-functions-valued;
coherence
proof
set gf=g*.f;
now
let x be object;
A1:dom gf=dom f by FOMODEL2:def 6;
reconsider X=x as set by TARSKI:1;
assume x in dom gf;
then gf.x= g*(f.X) by A1,FOMODEL2:def 6;
hence gf.x is complex-valued Function;
end;
hence thesis by VALUED_2:def 26;
end;
end;
registration
let f be Function-yielding Function, g be natural-valued Function;
cluster g*.f -> natural-functions-valued;
coherence
proof
set gf=g*.f;
now
let x be object;
A1:dom gf=dom f by FOMODEL2:def 6;
reconsider X=x as set by TARSKI:1;
assume x in dom gf;
then gf.x= g*(f.X) by A1,FOMODEL2:def 6;
hence gf.x is natural-valued Function;
end;
hence thesis by VALUED_2:def 31;
end;
end;
theorem
for f be Function-yielding Function, g be Function
holds Values(g*.f) =g.:Values f
proof
let f be Function-yielding Function, g be Function;
set gf=g*.f;
A1: dom gf = dom f by FOMODEL2:def 6;
thus Values gf c= g.:Values f
proof
let a be object;
assume a in Values gf;
then consider x,y be object such that
A2:x in dom gf & y in dom (gf.x) & a = gf.x.y by Th1;
gf.x = g*(f.x) by A1,FOMODEL2:def 6,A2;
then A3:gf.x.y = g.(f.x.y) & y in dom (f.x) & f.x.y in dom g
by A2,FUNCT_1:11,12;
then f.x.y in Values f by A1,A2,Th1;
hence thesis by A3,A2,FUNCT_1:def 6;
end;
let a be object;
assume a in g.:Values f;
then consider b be object such that
A4:b in dom g & b in Values f & g.b = a by FUNCT_1:def 6;
consider x,y be object such that
A5:x in dom f & y in dom (f.x) & b = f.x.y by A4,Th1;
A6: g.(f.x.y) = (g*(f.x)).y & y in dom (g*(f.x))
by A4,A5,FUNCT_1:11,13;
g*(f.x) = gf.x & x in dom gf by A5,FOMODEL2:def 6;
hence thesis by Th1,A4,A5,A6;
end;
theorem Th41:
for f be Function-yielding Function, g be Function holds
(g*.f).x = g*(f.x)
proof
let f be Function-yielding Function, g be Function;
per cases;
suppose x in dom f;
hence thesis by FOMODEL2:def 6;
end;
suppose not x in dom f;
then not x in dom (g*.f) & f.x={} by FOMODEL2:def 6,FUNCT_1:def 2;
then (g*.f).x={} & g*(f.x)={} by FUNCT_1:def 2;
hence thesis;
end;
end;
theorem Th42:
for f be Function-yielding Function,g be FinSequence, x,y be object
holds (g*.f)_(x,y) = g.f_(x,y)
proof
let f be Function-yielding Function,g be FinSequence,x,y be object;
A1:(g*.f).x = g*(f.x) by Th41;
per cases by A1,FUNCT_1:11;
suppose y in dom ((g*.f).x);
hence thesis by A1,FUNCT_1:12;
end;
suppose not y in dom (f.x);
then not y in dom ((g*.f).x) & f.x.y = {} by A1,FUNCT_1:11,def 2;
then not f.x.y in dom g & (g*.f).x .y = {} by FINSEQ_3:25,FUNCT_1:def 2;
hence thesis by FUNCT_1:def 2;
end;
suppose not (f.x.y) in dom g;
then not y in dom ((g*.f).x) & g.(f.x .y) = {} by A1,FUNCT_1:11,def 2;
hence thesis by FUNCT_1:def 2;
end;
end;
definition
let f be complex-functions-valued FinSequence-yielding Function;
func Sum f -> complex-valued Function means :Def8:
dom it = dom f & for x be set holds it.x = Sum (f.x);
existence
proof
defpred P[object,object] means for x be set st x=$1 holds $2=Sum (f.x);
A1:for e be object st e in dom f ex u be object st P[e,u]
proof
let e be object;
assume e in dom f;
then reconsider E=e as set;
take s=Sum (f.E);
thus thesis;
end;
consider s be Function such that
A2:dom s = dom f &
for e be object st e in dom f holds P[e,s.e] from CLASSES1:sch 1(A1);
rng s c= COMPLEX
proof
let y be object;
assume y in rng s;
then consider x be object such that
A3:x in dom s & s.x=y by FUNCT_1:def 3;
reconsider x as set by TARSKI:1;
s.x=Sum (f.x) by A3,A2;
hence thesis by A3,XCMPLX_0:def 2;
end;
then reconsider s as complex-valued Function by VALUED_0:def 1;
take s;
thus dom s=dom f by A2;
let x be set;
per cases;
suppose x in dom f;
hence thesis by A2;
end;
suppose A4: not x in dom f;
then Sum (f.x) = 0 by RVSUM_2:29,FUNCT_1:def 2;
hence thesis by A4,A2,FUNCT_1:def 2;
end;
end;
uniqueness
proof
let C1,C2 be complex-valued Function such that
A5: dom C1 = dom f & for x be set holds C1.x = Sum (f.x) and
A6:dom C2 = dom f & for x be set holds C2.x = Sum (f.x);
now let x be object;
reconsider X=x as set by TARSKI:1;
thus C1.x = Sum (f.X) by A5
.= C2.x by A6;
end;
hence thesis by A5,A6;
end;
end;
registration
let f be complex-functions-valued FinSequence-yielding FinSequence;
cluster Sum f -> FinSequence-like;
coherence
proof
dom f = Seg len f by FINSEQ_1:def 3;
hence thesis by Def8;
end;
cluster Sum f -> (len f) -element;
coherence
proof
dom Sum f = dom f by Def8;
then len Sum f = len f by FINSEQ_3:29;
hence thesis by CARD_1:def 7;
end;
end;
registration
let f be natural-functions-valued FinSequence-yielding Function;
cluster Sum f -> natural-valued;
coherence
proof
now let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in dom Sum f;
A1:(Sum f).x= Sum (f.xx) by Def8;
rng (f.xx) c= NAT by VALUED_0:def 6;
then reconsider fx=f.x as FinSequence of NAT by FINSEQ_1:def 4;
Sum fx is Nat;
hence (Sum f).x is natural by A1;
end;
hence thesis by VALUED_0:def 12;
end;
end;
registration
let f,g be complex-functions-valued FinSequence;
cluster f^g -> complex-functions-valued;
coherence
proof
A1: rng (f^g) = (rng f)\/rng g by FINSEQ_1:31;
now let x be object;
assume x in rng (f^g);
then x in rng f or x in rng g by A1,XBOOLE_0:def 3;
hence x is complex-valued Function;
end;
hence thesis by VALUED_2:def 2,VALUED_2:def 20;
end;
end;
registration
let f,g be ext-real-valued FinSequence;
cluster f^g -> ext-real-valued;
coherence;
end;
registration
let f be complex-functions-valued Function;
let X be set;
cluster f|X -> complex-functions-valued;
coherence
proof
A1: dom (f|X) c= dom f by RELAT_1:60;
now let x be object;
assume x in dom (f|X);
then x in dom f & (f|X).x= f.x by FUNCT_1:47,A1;
hence (f|X).x is complex-valued Function;
end;
hence thesis by VALUED_2:def 26;
end;
end;
registration
let f be FinSequence-yielding Function;
let X be set;
cluster f|X -> FinSequence-yielding;
coherence
proof
A1: dom (f|X) c= dom f by RELAT_1:60;
now let x be object;
assume x in dom (f|X);
then x in dom f & (f|X).x= f.x by FUNCT_1:47,A1;
hence (f|X).x is FinSequence;
end;
hence thesis by PRE_POLY:def 3;
end;
end;
registration
let F be complex-valued Function;
cluster <*F*> -> complex-functions-valued;
coherence
proof
now let x be object;
A1:dom <*F*> = Seg 1 & Seg 1 = {1} by FINSEQ_1:2,38;
assume x in dom <*F*>;
then x = 1 by A1,TARSKI:def 1;
hence <*F*>.x is complex-valued Function;
end;
hence thesis by VALUED_2:def 26;
end;
end;
theorem Th43:
for f,g be FinSequence st f^g is FinSequence-yielding
holds f is FinSequence-yielding & g is FinSequence-yielding
proof
let f,g be FinSequence such that A1: f^g is FinSequence-yielding;
A2:now let x be object;
A3:dom f c= dom (f^g) by FINSEQ_1:26;
assume x in dom f;
then f.x = (f^g).x & x in dom (f^g) by A3,FINSEQ_1:def 7;
hence f.x is FinSequence by A1;
end;
now let x be object;
assume A4:x in dom g;
then reconsider xx=x as Nat;
g.x = (f^g).(xx+len f) by A4,FINSEQ_1:def 7;
hence g.x is FinSequence by A1;
end;
hence thesis by A2,PRE_POLY:def 3;
end;
theorem Th44:
for f,g be FinSequence st f^g is complex-functions-valued holds
f is complex-functions-valued
& g is complex-functions-valued
proof
let f,g be FinSequence such that A1:f^g is complex-functions-valued;
A2:now let x be object;
A3:dom f c= dom (f^g) by FINSEQ_1:26;
assume x in dom f;
then f.x = (f^g).x & x in dom (f^g) by A3,FINSEQ_1:def 7;
hence f.x is complex-valued Function by A1;
end;
now let x be object;
assume A4:x in dom g;
then reconsider xx=x as Nat;
g.x = (f^g).(xx+len f) by A4,FINSEQ_1:def 7;
hence g.x is complex-valued Function by A1;
end;
hence thesis by A2,VALUED_2:def 26;
end;
theorem Th45:
for f be complex-valued FinSequence holds
Sum <*f*> = <*Sum f*>
proof
let f be complex-valued FinSequence;
A1:len <*f*> = 1 & dom <*f*>= dom Sum <*f*> & dom <*f*> = Seg 1
by Def8,FINSEQ_1:39,38;
A2:(Sum <*f*>).1 = Sum (<*f*>.1) by Def8;
thus thesis by A1,FINSEQ_3:29,A2,FINSEQ_1:40;
end;
theorem Th46:
for f,g be complex-functions-valued FinSequence-yielding FinSequence holds
Sum (f^g) = (Sum f) ^ (Sum g)
proof
let f,g be complex-functions-valued FinSequence-yielding FinSequence;
A1:len (Sum f)=len f & len (Sum g)=len g & len (Sum (f^g))=len (f^g)
by CARD_1:def 7;
A2:len (f^g)=len f+len g & len ((Sum f) ^ (Sum g))= len f + len g
by CARD_1:def 7,FINSEQ_1:22;
A3:dom f= dom Sum f & dom g= dom Sum g by Def8;
for i st 1<= i & i <= len f+len g holds (Sum (f^g)).i = ((Sum f) ^ (Sum g)).i
proof
let i such that A4: 1<= i & i <= len f+len g;
A5:(Sum (f^g)).i = Sum ((f^g).i) & (Sum f).i= Sum (f.i) by Def8;
A6:i in dom (f^g) by A4,A2,FINSEQ_3:25;
per cases by A6,FINSEQ_1:25;
suppose i in dom f;
then (f^g).i = f.i & (Sum f^Sum g).i = (Sum f).i by A3,FINSEQ_1:def 7;
hence thesis by A5;
end;
suppose ex j st j in dom g & i=len f+j;
then consider j such that
A7:j in dom g & i=len f+j;
(f^g).i = g.j & (Sum f^Sum g).i = (Sum g).j by A7,A3,A1,FINSEQ_1:def 7;
hence thesis by A5,Def8;
end;
end;
hence thesis by A1,A2;
end;
theorem
for f be complex-valued FinSequence,
o be DoubleReorganization of dom f holds
Sum f = Sum Sum (f*.o)
proof
defpred P[Nat] means
for f be complex-valued FinSequence,
o be DoubleReorganization of dom f st len f=$1 holds
Sum f = Sum Sum (f*.o);
A1:P[0]
proof
let f be complex-valued FinSequence,
o be DoubleReorganization of dom f such that A2: len f=0;
set fo=f*.o, S=Sum fo;
A3:dom S= Seg len S by FINSEQ_1:def 3;
x in dom S implies S.x=0
proof
reconsider xx=x as set by TARSKI:1;
assume x in dom S;
A4: S.xx = Sum (fo.x) by Def8;
dom (fo.x) ={}
proof
assume dom (fo.x) <>{};
then consider y be object such that
A5: y in dom (fo.x) by XBOOLE_0:def 1;
len (fo.x) = len (o.x) by CARD_1:def 7;
then A6: dom (fo.x) = dom (o.x) by FINSEQ_3:29;
f={} by A2;
hence thesis by A6,A5;
end;
then fo.x=<*>REAL;
hence thesis by RVSUM_1:72,A4;
end;
then A7: S= (len S) |-> 0 by A3;
f=<*>REAL by A2;
hence thesis by RVSUM_1:72,A7,RVSUM_1:81;
end;
A8: P[i] implies P[i+1]
proof
assume A9:P[i];
set i1=i+1;
let f be complex-valued FinSequence,
o be DoubleReorganization of dom f such that A10:len f=i1;
set fo=f*.o;
A11: 1 <= i1 by NAT_1:11;
then A12:i1 in dom f by A10,FINSEQ_3:25;
Values o = dom f by Def7;
then consider x,y be object such that
A13:x in dom o & y in dom (o.x) & o.x.y=i1 by A11,A10,FINSEQ_3:25,Th1;
reconsider x,y as Nat by A13;
set ox=o.x,rox=rng ox;
A14:ox in rng o by A13,FUNCT_1:def 3;
then A15: rox c= dom f by RELAT_1:def 19;
set C=canFS (rox\{i1});
A16:i1 in rox by A13,FUNCT_1:def 3;
A17:rng C=rox\{i1} by FUNCT_2:def 3;
A18: (rox\{i1}) \/ {i1} = rox by ZFMISC_1:116,A16;
A19:rng <*i1*>= {i1} by FINSEQ_1:38;
then A20: rng (C^<*i1*>) = rox by A18,A17,FINSEQ_1:31;
C^<*i1*> is one-to-one by XBOOLE_1:79,FINSEQ_3:91,A17,A19;
then consider P be Permutation of dom ox such that
A21: C^<*i1*> = ox*P by A20,RFINSEQ:26,RFINSEQ:4;
A22:rng C c= rox by A17;
A23:rng C c= dom f\{i1} by A17,A14,RELAT_1:def 19,XBOOLE_1:33;
A24: rng C \/ (dom f \{i1}) = dom f \{i1} by
A17,A15,XBOOLE_1:33,XBOOLE_1:12;
A25:rng C c= dom f by A15,A17;
A26:rng C \/ (dom f \rox) = rng C \/ (dom f \(rng C\/{i1}))
by A17,ZFMISC_1:116,A16
.= rng C \/ ((dom f \(rng C)) /\ (dom f \{i1}) ) by XBOOLE_1:53
.= (rng C \/ (dom f \(rng C))) /\ ( rng C \/ (dom f \{i1})) by XBOOLE_1:24
.= dom f /\ (dom f \{i1}) by A25,XBOOLE_1:45,A24
.= dom f\{i1} by XBOOLE_1:28;
dom f=Seg i1 by A10,FINSEQ_1:def 3;
then A27: dom f\{i1} = Seg i by FINSEQ_1:10;
set fi=f|i;
A28: len fi = i by NAT_1:11,A10,FINSEQ_1:59;
rng C /\ dom f c= rox by A22;
then reconsider oC=o+*(x,C) as DoubleReorganization of dom fi
by A27,A13,Th37,A26;
set FO=fi*.oC;
A29:dom oC=dom o by FUNCT_7:30;
then A30:len oC=len o by FINSEQ_3:29;
A31: len FO = len oC by CARD_1:def 7;
set FOx=FO|x;
consider H be FinSequence such that
A32: FO = FOx^H by FINSEQ_1:80;
A33: 1<= x & x <= len o by A13,FINSEQ_3:25;
then A34:len FOx = x by FINSEQ_1:59,A30,A31;
then A35:dom FOx = Seg x by FINSEQ_1:def 3;
A36: x in Seg x by A33;
reconsider x1=x-1 as Nat by A33;
len FOx = x1+1 by A33,FINSEQ_1:59,A30,A31;
then A37: FOx = (FOx|x1) ^ <*FOx.x*> by FINSEQ_3:55;
A38:x1 <=x1+1 by NAT_1:11;
then A39:FOx|x1=FO|x1 by FINSEQ_1:82;
reconsider H as complex-functions-valued FinSequence-yielding FinSequence
by A32,Th43,Th44;
reconsider FF=<*FO.x*>,FOx1=FO|x1 as
complex-functions-valued FinSequence-yielding FinSequence;
Sum (FOx1^FF) = Sum FOx1^ Sum FF by Th46;
then A40:Sum Sum (FOx1^FF) = Sum Sum FOx1 + Sum Sum FF by RVSUM_2:32;
FO = FOx1^FF^H by A39,A37,A35,A36,FUNCT_1:47,A32;
then A41:Sum FO = Sum (FOx1^FF) ^ Sum H by Th46;
A42: Sum FF = <*Sum (FO.x)*> by Th45;
A43: len fo = len o by CARD_1:def 7;
set fox=fo|x;
consider h be FinSequence such that
A44: fo = fox^h by FINSEQ_1:80;
A45:len fox = x by A33,FINSEQ_1:59,A43;
then A46:dom fox = Seg x by FINSEQ_1:def 3;
len fox = x1+1 by A33,FINSEQ_1:59,A43;
then A47: fox = (fox|x1) ^ <*fox.x*> by FINSEQ_3:55;
A48:fox|x1=fo|x1 by A38,FINSEQ_1:82;
reconsider h as complex-functions-valued FinSequence-yielding FinSequence
by A44,Th43,Th44;
reconsider ff=<*fo.x*>,fox1=fo|x1 as
complex-functions-valued FinSequence-yielding FinSequence;
Sum (fox1^ff) = Sum fox1^ Sum ff by Th46;
then A49:Sum Sum (fox1^ff) = Sum Sum fox1 + Sum Sum ff by RVSUM_2:32;
fo = fox1^ff^h by A44,A47,A48,A46,A36,FUNCT_1:47;
then A50:Sum fo = Sum (fox1^ff) ^ Sum h by Th46;
A51: Sum ff= <*Sum (fo.x)*> by Th45;
A52:len fox1 = x1 & len FOx1 = x1 by A38,A45,A34,A48,A39,FINSEQ_1:59;
for i st 1<= i & i <= x1 holds fox1.i = FOx1.i
proof
let j;
assume A53: 1<= j & j <= x1;
then A54:j < x by A38,NAT_1:13;
then A55: j <= len o by A33,XXREAL_0:2;
then A56: j in dom o by A53,FINSEQ_3:25;
A57: fo.j = f*(o.j) & FO.j = fi*(oC.j)
by A55,A53,FINSEQ_3:25,A29,FOMODEL2:def 6;
j in Seg x1 by A53;
then A58:fox1.j = fo.j & FOx1.j = FO.j by FUNCT_1:49;
o.j in rng o & rng o c= (dom f)* by A56,FUNCT_1:def 3;
then A59: o.j is FinSequence of dom f by FINSEQ_1:def 11;
not i1 in rng (o.j)
proof
assume i1 in rng (o.j);
then consider w be object such that
A60: w in dom (o.j) & o.j.w = i1 by FUNCT_1:def 3;
o_(j,w) = o_(x,y) by A60,A13;
hence thesis by A60,A56,A13,Def6,A54;
end;
then A61: rng (o.j) c= Seg i by A27,A59,FINSEQ_1:def 4,ZFMISC_1:34;
(f|Seg i)*(o.j) = (f*id Seg i)*(o.j) by RELAT_1:65
.= f*((id Seg i)*(o.j)) by RELAT_1:36
.= f*(o.j) by A61,RELAT_1:53;
hence thesis by A57,A54,FUNCT_7:32,A58;
end;
then A62: fox1 = FOx1 by A52;
A63:len FO = len FOx + len H by A32,FINSEQ_1:22;
then A64:len FOx + len H = len fox + len h
by A44,FINSEQ_1:22,A43,A31,A30;
for i st 1<= i & i <= len H holds H.i = h.i
proof
let j;
set jx=j+x;
assume A65: 1<= j & j <= len H;
then j in dom H & j in dom h by A64,A34,A45,FINSEQ_3:25;
then A66:H.j = FO.jx & h.j = fo.jx by A34,A45,A32,A44,FINSEQ_1:def 7;
j<>0 by A65;
then A67: jx<>x;
j <= jx by NAT_1:11;
then jx >= 1 by A65,XXREAL_0:2;
then A68: jx in dom o by A65,A63,A34,A31,A29,XREAL_1:6,FINSEQ_3:25;
then A69: fo.jx = f*(o.jx) & FO.jx = fi*(oC.jx) by A29,FOMODEL2:def 6;
o.jx in rng o & rng o c= (dom f)* by A68,FUNCT_1:def 3;
then A70: o.jx is FinSequence of dom f by FINSEQ_1:def 11;
not i1 in rng (o.jx)
proof
assume i1 in rng (o.jx);
then consider w be object such that
A71: w in dom (o.jx) & o.jx.w = i1 by FUNCT_1:def 3;
o_(jx,w) = o_(x,y) by A71,A13;
then jx=x & y = w by A71,A68,A13,Def6;
then j=0;
hence thesis by A65;
end;
then A72: rng (o.jx) c= Seg i by A27,A70,FINSEQ_1:def 4,ZFMISC_1:34;
(f|Seg i)*(o.jx) = (f*id Seg i)*(o.jx) by RELAT_1:65
.= f*((id Seg i)*(o.jx)) by RELAT_1:36
.= f*(o.jx) by A72,RELAT_1:53;
hence thesis by A69,A67,FUNCT_7:32,A66;
end;
then A73: H = h by A64,A34,A45;
A74: fo.x= f*ox & FO.x = fi*(oC.x) by A13,A29,FOMODEL2:def 6;
A75: dom (f*ox) = dom ox by A15,RELAT_1:27;
rng (f*ox) c= COMPLEX;
then reconsider g=f*ox as FinSequence of COMPLEX by FINSEQ_1:def 4;
reconsider PP=P as Permutation of dom g by A75;
A76:dom ox = Seg len ox by FINSEQ_1:def 3;
rng P = dom ox by FUNCT_2:def 3;
then
A77:dom (ox*P) = dom P & rng (ox*P) = rng ox & dom (g*P) = dom P &
rng (g*P) = rng g by A75,RELAT_1:27,28;
then g*PP is FinSequence by A76,FUNCT_2:52,FINSEQ_1:def 2;
then reconsider G=g*PP as FinSequence of COMPLEX by FINSEQ_1:def 4,A77;
A78: Sum g = addcomplex $$ g by RVSUM_1:def 11
.=addcomplex "**" G by FINSOP_1:7
.=Sum G by RVSUM_1:def 11;
reconsider F=f as Function of dom f,rng f by FUNCT_2:1;
reconsider I1=i1 as Element of dom f by A11,A10,FINSEQ_3:25;
reconsider C1=C as FinSequence of dom f by A25,FINSEQ_1:def 4;
A79:dom f is non empty & rng f is non empty by A12, RELAT_1:42;
G = f*(ox*P) by RELAT_1:36;
then A80: G = (F*C1) ^ <*f.i1*> by A21,A79,A12,FINSEQOP:8;
fi*C = (f*id Seg i)*C by RELAT_1:65
.= f*((id Seg i)*C) by RELAT_1:36
.=f*C by A23,A27,RELAT_1:53;
then FO.x = f*C by A74, A13,FUNCT_7:31;
then A81: Sum (fo.x) = Sum (FO.x) + f.i1 by A80,RVSUM_2:31,A78,A74;
A82:Sum fi = Sum Sum FO by A9,A28
.= Sum Sum FOx1 + Sum Sum FF + Sum Sum H by A41,A40,RVSUM_2:32
.= Sum Sum fox1 + Sum (FO.x) + Sum Sum h by A62,A73,A42,RVSUM_2:30;
A83: Sum Sum fo = Sum Sum fox1 + Sum Sum ff + Sum Sum h by
A49,A50,RVSUM_2:32
.= Sum Sum fox1 + Sum (fo.x) + Sum Sum h by A51,RVSUM_2:30
.= Sum Sum fox1 + Sum (FO.x) + Sum Sum h+f.i1 by A81;
f= fi ^ <*f.i1*> by FINSEQ_3:55,A10;
hence thesis by RVSUM_2:31,A83,A82;
end;
A84:P[i] from NAT_1:sch 2(A1,A8);
let f be complex-valued FinSequence,o be DoubleReorganization of dom f;
P[len f] by A84;
hence thesis;
end;
registration
cluster NAT* -> natural-functions-membered;
coherence
proof
for x be object st x in NAT* holds x is natural-valued Function;
hence thesis by VALUED_2:def 7;
end;
cluster COMPLEX* -> complex-functions-membered;
coherence
proof
for x be object st x in COMPLEX* holds x is complex-valued Function;
hence thesis by VALUED_2:def 2;
end;
end;
theorem
for f be FinSequence of COMPLEX* holds
Sum (COMPLEX-concatenation "**" f) = Sum Sum f
proof
set CC = COMPLEX-concatenation;
defpred P[Nat] means
for f be FinSequence of COMPLEX* st len f=$1 holds
Sum (CC "**" f) = Sum Sum f;
A1:CC is having_a_unity & the_unity_wrt CC={} by MONOID_0:67;
A2:P[0]
proof
let f be FinSequence of COMPLEX*;
assume A3:len f=0;
then Sum f={};
hence thesis by A1,A3,FINSOP_1:def 1;
end;
A4:P[i] implies P[i+1]
proof
assume A5:P[i];
set i1=i+1;
let f be FinSequence of COMPLEX*;
assume A6:len f=i1;
then consider q be FinSequence of COMPLEX*, d be Element of COMPLEX*
such that
A7:f=q^<*d*> by FINSEQ_2:19;
len q+1 = len f by A7,FINSEQ_2:16;
then A8:Sum Sum q = Sum (CC"**"q) by A6,A5;
Sum f = (Sum q)^(Sum <*d*>) by A7,Th46
.= (Sum q)^(<*Sum d*>) by Th45;
then A9: Sum Sum f = (Sum Sum q) + Sum d by RVSUM_2:31;
CC "**"f = (CC"**"q)^(CC"**"<*d*>) by Th3,A7
.= (CC"**"q)^ d by FINSOP_1:11;
hence thesis by RVSUM_2:32,A8,A9;
end;
P[i] from NAT_1:sch 2(A2,A4);
hence thesis;
end;
definition
let f be finite Function;
mode valued_reorganization of f -> DoubleReorganization of dom f means
:Def9:
(for n ex x st
x = f.it_(n,1) & ... & x = f.it_(n,len (it.n))) &
for n1,n2,i1,i2 be Nat st
i1 in dom (it.n1) & i2 in dom (it.n2) &
f.it_(n1,i1) = f.it_(n2,i2)
holds n1 = n2;
existence
proof
per cases;
suppose A1:f={};
take o = the DoubleReorganization of dom f;
thus for n ex x st
x = f.o_(n,1) & ... & x = f.o_(n,len (o.n))
proof
let n;
take x={};
thus thesis by A1;
end;
let n1,n2,i1,i2 be Nat;
thus thesis by A1;
end;
suppose f<>{};
then reconsider F=rng f as non empty finite set;
set c = the one-to-one onto FinSequence of F;
A2:rng c = F by FUNCT_2:def 3;
then reconsider C=c as non empty FinSequence;
consider o be (len C)-element DoubleReorganization of dom f such that
A3:for n holds c.n = f.o_(n,1) &...& c.n = f.o_(n,len (o.n)) by Th38,A2;
take o;
thus for n ex x st x = f.o_(n,1) & ... & x = f.o_(n,len (o.n))
proof
let n;
take x=c.n;
let i;
assume A4:1<= i & i <= len (o.n);
c.n = f.o_(n,1) &...& c.n = f.o_(n,len (o.n)) by A3;
hence thesis by A4;
end;
let n1,n2,i1,i2 be Nat such that
A5:i1 in dom (o.n1) & i2 in dom (o.n2) &
f.o_(n1,i1) = f.o_(n2,i2);
A6: c.n1 = f.o_(n1,1) &...& c.n1 = f.o_(n1,len (o.n1)) by A3;
A7: c.n2 = f.o_(n2,1) &...& c.n2 = f.o_(n2,len (o.n2)) by A3;
1<= i1 & i1 <= len (o.n1) by A5,FINSEQ_3:25;
then A8:c.n1 = f.o_(n1,i1) by A6;
A9: 1<= i2 & i2 <= len (o.n2) by A5,FINSEQ_3:25;
len o = len C by CARD_1:def 7;
then A10: dom o = dom c by FINSEQ_3:29;
A11:n1 in dom o
proof
assume not n1 in dom o;
then o.n1={} by FUNCT_1:def 2;
hence thesis by A5;
end;
n2 in dom o
proof
assume not n2 in dom o;
then o.n2={} by FUNCT_1:def 2;
hence thesis by A5;
end;
hence n1 = n2 by FUNCT_1:def 4,A9,A7,A5,A8,A11,A10;
end;
end;
end;
theorem
for f be finite Function
for o be valued_reorganization of f holds
rng (f*.o.n) = {} or (rng (f*.o.n) = {f.o_(n,1)} & 1 in dom (o.n))
proof
let f be finite Function;
let o be valued_reorganization of f;
assume rng (f*.o.n) <> {};
then consider y such that
A1:y in rng (f*.o.n) by XBOOLE_0:def 1;
consider x such that
A2:x in dom (f*.o.n) & (f*.o.n).x = y by A1,FUNCT_1:def 3;
reconsider x as Nat by A2;
A3:dom (f*.o) = dom o by FOMODEL2:def 6;
n in dom (f*.o)
proof
assume not n in dom (f*.o);
then (f*.o).n={} by FUNCT_1:def 2;
hence thesis by A1;
end;
then (f*.o.n) = f*(o.n) by A3, FOMODEL2:def 6;
then A4: (f*(o.n)).x = f.(o.n.x) & x in dom (o.n) by A2,FUNCT_1:11,12;
consider w be object such that
A5:w = f.o_(n,1) & ... & w = f.o_(n,len (o.n)) by Def9;
1<= x & x <= len (o.n) by A4,FINSEQ_3:25;
then A6:w = f.o_(n,x) & 1<= len (o.n) by XXREAL_0:2,A5;
rng (f*.o.n) c= {f.o_(n,1)}
proof
let z be object;
assume A7:z in rng (f*.o.n);
then consider x such that
A8:x in dom (f*.o.n) & (f*.o.n).x = z by FUNCT_1:def 3;
reconsider x as Nat by A8;
A9:dom (f*.o) = dom o by FOMODEL2:def 6;
n in dom (f*.o)
proof
assume not n in dom (f*.o);
then (f*.o).n={} by FUNCT_1:def 2;
hence thesis by A7;
end;
then A10: (f*.o.n) = f*(o.n) by A9, FOMODEL2:def 6;
then A11: (f*(o.n)).x = f.(o.n.x) & x in dom (o.n) by A8,FUNCT_1:11,12;
then 1<= x & x <= len (o.n) by FINSEQ_3:25;
then w = f.o_(n,x) & 1<= len (o.n) by XXREAL_0:2,A5;
then z = f.o_(n,1) by A5,A8,A11,A10;
hence thesis by TARSKI:def 1;
end;
hence thesis by A6,FINSEQ_3:25,ZFMISC_1:33;
end;
Lm7:for f be FinSequence
for o1,o2 be valued_reorganization of f st
rng (f*.o1.i) = rng (f*.o2.i)
holds
rng (o1.i) c= rng (o2.i)
proof
let f be FinSequence;
let o1,o2 be valued_reorganization of f such that
A1:rng (f*.o1.i) = rng (f*.o2.i);
len (f*.o1.i) = len (o1.i) by CARD_1:def 7;
then A2:dom (o1.i) = dom (f*.o1.i) by FINSEQ_3:29;
A3: len (f*.o2.i) = len (o2.i) by CARD_1:def 7;
A4:Values o1 = dom f & Values o2=dom f by Def7;
let y be object;
assume y in rng (o1.i);
then consider x be object such that
A5: x in dom (o1.i) & o1.i.x = y by FUNCT_1:def 3;
reconsider x as Nat by A5;
(f*.o1.i).x in rng (f*.o2.i) by A2, A5,FUNCT_1:def 3,A1;
then consider u be object such that
A6: u in dom (f*.o2.i) & (f*.o2.i).u = (f*.o1.i).x by FUNCT_1:def 3;
A7:(f*.o1)_(i,x) = f.o1_(i,x) by Th42;
A8:(f*.o2)_(i,u) = f.o2_(i,u) by Th42;
i in dom o1
proof
assume not i in dom o1;
then o1.i = {} by FUNCT_1:def 2;
hence thesis by A5;
end;
then consider j,w be object such that
A9: j in dom o2 & w in dom (o2.j) & o2.j.w = y by Th1,A5,A4;
A10:u in dom (o2.i) by A6,A3,FINSEQ_3:29;
f.o2_(i,u)=f.o2_(j,w) by A5,A9,A6,A7,A8;
then j=i by Def9,A10,A9;
hence thesis by A9,FUNCT_1:def 3;
end;
theorem
for f be FinSequence
for o1,o2 be valued_reorganization of f st
rng (f*.o1.i) = rng (f*.o2.i)
holds
rng (o1.i) = rng (o2.i) by Lm7;
theorem
for f be FinSequence,
g be complex-valued FinSequence
for o1,o2 be DoubleReorganization of dom g st
o1 is valued_reorganization of f &
o2 is valued_reorganization of f & rng (f*.o1.i) = rng (f*.o2.i)
holds
Sum (g*.o1).i =Sum (g*.o2).i
proof
let f be FinSequence,
g be complex-valued FinSequence;
let o1,o2 be DoubleReorganization of dom g such that
A1:o1 is valued_reorganization of f &
o2 is valued_reorganization of f & rng (f*.o1.i) = rng (f*.o2.i);
A2:rng (o1.i) = rng (o2.i) by A1,Lm7;
then consider h be Function such that
A3:dom h = dom (o1.i) & rng h=dom (o2.i) & h is one-to-one & (o2.i)*h=o1.i
by RFINSEQ:26,CLASSES1:77;
rng ((g*.o1).i) c= COMPLEX;
then reconsider g1=(g*.o1).i as FinSequence of COMPLEX by FINSEQ_1:def 4;
rng ((g*.o2).i) c= COMPLEX;
then reconsider g2=(g*.o2).i as FinSequence of COMPLEX by FINSEQ_1:def 4;
len (o1.i)=len (o2.i) by A2,FINSEQ_1:48;
then A4:dom (o1.i)=dom (o2.i) by FINSEQ_3:29;
A5: len (g*.o2.i) = len (o2.i) by CARD_1:def 7;
then dom g2 = dom (o2.i) by FINSEQ_3:29;
then reconsider h as Function of dom g2,dom g2 by A3,A4,FUNCT_2:1;
h is onto by A3,A5,FINSEQ_3:29,FUNCT_2:def 3;
then reconsider h as Permutation of dom g2 by A3;
A6: g1 = g*(o1.i) by Th41
.= (g*(o2.i))*h by A3,RELAT_1:36
.= g2*h by Th41;
thus Sum (g*.o1).i = Sum ((g*.o1).i) by Def8
.= addcomplex "**" g1 by RVSUM_1:def 11
.= addcomplex "**" g2 by A6,FINSOP_1:7
.= Sum ((g*.o2).i) by RVSUM_1:def 11
.= Sum (g*.o2).i by Def8;
end;