Copyright (c) 1993 Association of Mizar Users
environ
vocabulary RELAT_1, CARD_1, FUNCT_1, BOOLE, TARSKI, FUNCT_2, FINSET_1,
FINSEQ_1, ARYTM_1, SQUARE_1, RLVECT_1, PROB_1, ARYTM_3, VECTSP_1,
RFINSEQ;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, RELAT_1, FUNCT_1,
FUNCT_2, FINSEQ_1, CARD_1, REAL_1, NAT_1, SQUARE_1, SEQ_1, FINSEQ_4,
FINSET_1, RVSUM_1, TOPREAL1;
constructors WELLORD2, FINSEQOP, REAL_1, NAT_1, SQUARE_1, TOPREAL1, FINSEQ_4,
SEQ_1, MEMBERED, PARTFUN1, XBOOLE_0;
clusters FINSET_1, PRELAMB, FUNCT_1, RELSET_1, FINSEQ_1, FUNCT_2, NAT_1,
MEMBERED, ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0;
theorems AXIOMS, TARSKI, FINSEQ_1, FINSEQ_2, FINSEQ_3, REAL_1, NAT_1, FUNCT_1,
FUNCT_2, FINSET_1, CARD_1, CARD_2, SQUARE_1, TOPREAL1, RVSUM_1, WELLORD2,
ZFMISC_1, AMI_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1;
schemes NAT_1, FINSEQ_1, MATRIX_2, ZFREFLE1, COMPTS_1;
begin
reserve x,y for set,
n,m for Nat,
r,s for Real;
definition let F,G be Relation;
pred F,G are_fiberwise_equipotent means :Def1:
for x be set holds Card (F"{x}) = Card (G"{x});
reflexivity;
symmetry;
end;
Lm1:
for F be Function, x be set st not x in rng F holds F"{x} = {}
proof let F be Function,x; assume
A1: not x in rng F;
now assume
rng F meets {x};
then consider y being set such that
A2: y in rng F & y in {x} by XBOOLE_0:3;
thus contradiction by A1,A2,TARSKI:def 1;
end;
hence thesis by RELAT_1:173;
end;
theorem Th1:
for F,G be Function st F,G are_fiberwise_equipotent holds rng F = rng G
proof let F,G be Function; assume
A1: F,G are_fiberwise_equipotent;
thus rng F c= rng G
proof let x; assume that
A2: x in rng F and
A3: not x in rng G;
Card (F"{x}) = Card (G"{x}) by A1,Def1;
then A4: F"{x},G"{x} are_equipotent by CARD_1:21;
consider y such that
A5: y in dom F & F.y = x by A2,FUNCT_1:def 5;
A6: x in {x} by TARSKI:def 1;
G"{x} = {} by A3,Lm1;
then F"{x} = {} by A4,CARD_1:46;
hence contradiction by A5,A6,FUNCT_1:def 13;
end;
let x; assume that
A7: x in rng G and
A8: not x in rng F;
Card (G"{x}) = Card (F"{x}) by A1,Def1;
then A9: G"{x},F"{x} are_equipotent by CARD_1:21;
consider y such that
A10: y in dom G & G.y = x by A7,FUNCT_1:def 5;
A11: x in {x} by TARSKI:def 1;
F"{x} = {} by A8,Lm1;
then G"{x} = {} by A9,CARD_1:46;
hence contradiction by A10,A11,FUNCT_1:def 13;
end;
theorem
for F,G,H be Function
st F,G are_fiberwise_equipotent & F,H are_fiberwise_equipotent holds
G,H are_fiberwise_equipotent
proof let F,G,H be Function; assume
A1: F,G are_fiberwise_equipotent & F,H are_fiberwise_equipotent;
let x;
thus Card(G"{x}) = Card(F"{x}) by A1,Def1
.= Card(H"{x}) by A1,Def1;
end;
theorem Th3:
for F,G be Function holds
F,G are_fiberwise_equipotent
iff
ex H be Function st dom H = dom F & rng H = dom G & H is one-to-one & F = G*H
proof let F,G be Function;
thus F,G are_fiberwise_equipotent implies
ex H be Function st dom H = dom F & rng H = dom G & H is one-to-one & F = G*H
proof assume
A1: F,G are_fiberwise_equipotent;
defpred P[set,set] means $2 is Function &
for f be Function st $2 = f holds dom f = F"{$1} & rng f = G"{$1} &
f is one-to-one;
A2: for x st x in rng F ex y st P[x,y]
proof let x; assume x in rng F;
Card(F"{x}) = Card(G"{x}) by A1,Def1;
then F"{x},G"{x} are_equipotent by CARD_1:21;
then consider H be Function such that
A3: H is one-to-one & dom H = F"{x} & rng H = G"{x} by WELLORD2:def 4;
take H;
thus H is Function;
let g be Function; assume g = H;
hence thesis by A3;
end;
consider W be Function such that
A4: dom W = rng F & for x st x in rng F holds P[x,W.x]
from NonUniqFuncEx(A2);
defpred Q[set,set] means for H be Function st H = W.(F.$1) holds $2 = H.$1;
set df = dom F,
dg = dom G;
A5: for x st x in df ex y st y in dg & Q[x,y]
proof let x; assume
A6: x in df;
then A7: F.x in rng F by FUNCT_1:def 5;
then reconsider f = W.(F.x) as Function by A4;
A8: dom f = F"{F.x} & rng f = G"{F.x} & f is one-to-one by A4,A7;
take y = f.x;
F.x in {F.x} by TARSKI:def 1;
then x in F"{F.x} by A6,FUNCT_1:def 13;
then f.x in G"{F.x} by A8,FUNCT_1:def 5;
hence y in dg by FUNCT_1:def 13;
let g be Function;
assume g = W.(F.x);
hence thesis;
end;
consider IT be Function such that
A9: dom IT = df & rng IT c= dg & for x st x in df holds Q[x,IT.x]
from NonUniqBoundFuncEx(A5);
take IT;
thus dom IT = df by A9;
dom G c= rng IT
proof let x; assume
A10: x in dg;
then A11: G.x in rng G & rng F = rng G by A1,Th1,FUNCT_1:def 5;
then reconsider f = W.(G.x) as Function by A4;
A12: f is one-to-one & dom f = F"{G.x} & rng f = G"{G.x} by A4,A11;
G.x in {G.x} by TARSKI:def 1;
then x in rng f by A10,A12,FUNCT_1:def 13;
then consider z be set such that
A13: z in dom f & f.z = x by FUNCT_1:def 5;
A14: z in df & F.z in {G.x} by A12,A13,FUNCT_1:def 13;
then F.z = G.x by TARSKI:def 1;
then IT.z = x by A9,A13,A14;
hence thesis by A9,A14,FUNCT_1:def 5;
end;
hence rng IT = dg by A9,XBOOLE_0:def 10;
now let x,y; assume
A15: x in dom IT & y in dom IT & IT.x = IT.y;
then A16: F.x in rng F & F.y in rng F by A9,FUNCT_1:def 5;
then reconsider f1 = W.(F.x), f2 = W.(F.y) as Function by A4;
A17: IT.x = f1.x & IT.y = f2.y by A9,A15;
A18: dom f1 = F"{F.x} & rng f1 = G"{F.x} & f1 is one-to-one &
dom f2 = F"{F.y} & rng f2 = G"{F.y} & f2 is one-to-one by A4,A16;
F.x in {F.x} & F.y in {F.y} by TARSKI:def 1;
then A19: x in F"{F.x} & y in F"{F.y} by A9,A15,FUNCT_1:def 13;
then f1.x in rng f1 & f2.y in rng f2 by A18,FUNCT_1:def 5;
then f1.x in G"{F.x} /\ G"{F.y} by A15,A17,A18,XBOOLE_0:def 3;
then f1.x in G"({F.x} /\ {F.y}) by FUNCT_1:137;
then G.(f1.x) in {F.x} /\ {F.y} by FUNCT_1:def 13;
then G.(f1.x) in {F.x} & G.(f1.x) in {F.y} by XBOOLE_0:def 3;
then G.(f1.x) = F.x & G.(f1.x) = F.y by TARSKI:def 1;
hence x = y by A15,A17,A18,A19,FUNCT_1:def 8;
end;
hence IT is one-to-one by FUNCT_1:def 8;
A20: dom(G*IT) = df by A9,RELAT_1:46;
now let x; assume
A21: x in df;
then A22: F.x in rng F by FUNCT_1:def 5;
then reconsider f = W.(F.x) as Function by A4;
A23: f is one-to-one & dom f = F"{F.x} & rng f = G"{F.x} by A4,A22;
F.x in {F.x} by TARSKI:def 1;
then x in F"{F.x} by A21,FUNCT_1:def 13;
then f.x in G"{F.x} by A23,FUNCT_1:def 5;
then G.(f.x) in {F.x} by FUNCT_1:def 13;
then A24: G.(f.x) = F.x by TARSKI:def 1;
IT.x = f.x by A9,A21;
hence F.x = (G*IT).x by A9,A21,A24,FUNCT_1:23;
end;
hence F = G*IT by A20,FUNCT_1:9;
end;
given H be Function such that
A25: dom H = dom F & rng H = dom G & H is one-to-one & F = G*H;
let x;
set t = H|(F"{x});
A26: t is one-to-one by A25,FUNCT_1:84;
F"{x} c= dom F by RELAT_1:167;
then A27: dom t = F"{x} by A25,RELAT_1:91;
rng t = G"{x}
proof
thus rng t c= G"{x}
proof let z be set; assume
z in rng t;
then consider y such that
A28: y in dom t & t.y = z by FUNCT_1:def 5;
F.y in {x} by A27,A28,FUNCT_1:def 13;
then A29: F.y = x by TARSKI:def 1;
A30: z = H.y by A28,FUNCT_1:68;
dom t = dom H /\ F"{x} by FUNCT_1:68;
then A31: y in dom H by A28,XBOOLE_0:def 3;
then A32: z in dom G by A25,A30,FUNCT_1:def 5;
x = G.z by A25,A29,A30,A31,FUNCT_1:23;
then G.z in {x} by TARSKI:def 1;
hence thesis by A32,FUNCT_1:def 13;
end;
let z be set; assume
z in G"{x};
then A33: z in dom G & G.z in {x} by FUNCT_1:def 13;
then A34: G.z = x by TARSKI:def 1;
consider y such that
A35: y in dom H & H.y = z by A25,A33,FUNCT_1:def 5;
F.y = x by A25,A34,A35,FUNCT_1:23;
then F.y in {x} by TARSKI:def 1;
then A36: y in dom t by A25,A27,A35,FUNCT_1:def 13;
then t.y in rng t by FUNCT_1:def 5;
hence thesis by A35,A36,FUNCT_1:68;
end;
then F"{x},G"{x} are_equipotent by A26,A27,WELLORD2:def 4;
hence thesis by CARD_1:21;
end;
theorem Th4:
for F,G be Function holds
F,G are_fiberwise_equipotent iff for X be set holds Card (F"X) = Card (G"X)
proof let F,G be Function;
thus F,G are_fiberwise_equipotent implies
for X be set holds Card(F"X) = Card(G"X)
proof assume
F,G are_fiberwise_equipotent;
then consider H be Function such that
A1: dom H = dom F & rng H = dom G & H is one-to-one & F = G*H by Th3;
let X be set;
set t = H|(F"X);
A2: t is one-to-one by A1,FUNCT_1:84;
F"X c= dom F by RELAT_1:167;
then A3: dom t = F"X by A1,RELAT_1:91;
rng t = G"X
proof
thus rng t c= G"X
proof let z be set; assume
z in rng t;
then consider y such that
A4: y in dom t & t.y = z by FUNCT_1:def 5;
A5: F.y in X by A3,A4,FUNCT_1:def 13;
A6: z = H.y by A4,FUNCT_1:68;
dom t = dom H /\ F"X by FUNCT_1:68;
then A7: y in dom H by A4,XBOOLE_0:def 3;
then A8: z in dom G by A1,A6,FUNCT_1:def 5;
G.z in X by A1,A5,A6,A7,FUNCT_1:23;
hence thesis by A8,FUNCT_1:def 13;
end;
let z be set; assume
z in G"X;
then A9: z in dom G & G.z in X by FUNCT_1:def 13;
then consider y such that
A10: y in dom H & H.y = z by A1,FUNCT_1:def 5;
F.y in X by A1,A9,A10,FUNCT_1:23;
then A11: y in dom t by A1,A3,A10,FUNCT_1:def 13;
then t.y in rng t by FUNCT_1:def 5;
hence thesis by A10,A11,FUNCT_1:68;
end;
then F"X,G"X are_equipotent by A2,A3,WELLORD2:def 4;
hence thesis by CARD_1:21;
end;
assume for X be set holds Card(F"X) = Card(G"X);
hence for x holds Card(F"{x}) = Card(G"{x});
end;
theorem Th5:
for D be non empty set, F,G be Function st rng F c= D & rng G c= D holds
F,G are_fiberwise_equipotent
iff
for d be Element of D holds Card (F"{d}) = Card (G"{d})
proof let D be non empty set, F,G be Function;assume
A1: rng F c= D & rng G c= D;
thus F,G are_fiberwise_equipotent implies
for d be Element of D holds Card(F"{d}) = Card(G"{d}) by Def1;
assume A2: for d be Element of D holds Card(F"{d}) = Card(G"{d});
let x;
now per cases;
case not x in rng F;
then A3: F"{x} = {} by Lm1;
now assume A4: x in rng G;
then reconsider d = x as Element of D by A1;
Card(G"{d}) = Card(F"{d}) by A2;
then G"{d},F"{d} are_equipotent by CARD_1:21;
then A5: G"{x} = {} by A3,CARD_1:46;
consider y such that
A6: y in dom G & G.y = x by A4,FUNCT_1:def 5;
G.y in {x} by A6,TARSKI:def 1;
hence contradiction by A5,A6,FUNCT_1:def 13;
end;
hence thesis by A3,Lm1;
case x in rng F;
then reconsider d = x as Element of D by A1;
Card(F"{d}) = Card(G"{d}) by A2;
hence Card(F"{x}) = Card(G"{x});
end;
hence thesis;
end;
theorem Th6:
for F,G be Function st dom F = dom G holds
F,G are_fiberwise_equipotent iff ex P be Permutation of dom F st F = G*P
proof let F,G be Function; assume
A1: dom F = dom G;
thus F,G are_fiberwise_equipotent implies
ex P be Permutation of dom F st F = G*P
proof assume
F,G are_fiberwise_equipotent;
then consider I be Function such that
A2: dom I = dom F & rng I = dom G & I is one-to-one & F = G*I by Th3;
reconsider I as Function of dom F,dom F by A1,A2,FUNCT_2:4;
reconsider I as Permutation of dom F by A1,A2,FUNCT_2:83;
take I;
thus thesis by A2;
end; given P be Permutation of dom F such that
A3: F = G*P;
A4: rng P = dom F & P is one-to-one by FUNCT_2:def 3;
P is Function of dom F,dom F & dom F = {} implies dom F ={};
then dom P = dom F by FUNCT_2:def 1;
hence thesis by A1,A3,A4,Th3;
end;
theorem
for F,G be Function
st F,G are_fiberwise_equipotent holds Card (dom F) = Card (dom G)
proof let F,G be Function; assume
F,G are_fiberwise_equipotent;
then Card(F"(rng F)) = Card(G"(rng F)) & rng F = rng G by Th1,Th4;
hence Card(dom F) = Card(G"(rng G)) by RELAT_1:169
.= Card(dom G) by RELAT_1:169;
end;
definition let F be finite Function, A be set;
cluster F"A -> finite;
coherence
proof
dom F is finite & F"A c= dom F by RELAT_1:167;
hence thesis by FINSET_1:13;
end;
end;
canceled;
theorem
for F,G be finite Function holds
F,G are_fiberwise_equipotent iff for X be set holds card (F"X) = card (G"X)
by Th4;
theorem
for F,G be finite Function st
F,G are_fiberwise_equipotent holds card (dom F) = card (dom G)
proof let F,G be finite Function;
assume F,G are_fiberwise_equipotent;
then card(F"(rng F)) = card(G"(rng F)) & rng F = rng G by Th1,Th4;
hence card(dom F) = card(G"(rng G)) by RELAT_1:169
.= card(dom G) by RELAT_1:169;
end;
theorem
for D be non empty set, F,G be finite Function st rng F c= D & rng G c= D
holds F,G are_fiberwise_equipotent
iff
for d be Element of D holds card (F"{d}) = card (G"{d}) by Th5;
canceled;
theorem
for f,g be FinSequence holds
f,g are_fiberwise_equipotent iff for X be set holds card (f"X) = card (g"X)
by Th4;
theorem Th14:
for f,g,h be FinSequence holds
f,g are_fiberwise_equipotent iff f^h, g^h are_fiberwise_equipotent
proof let f,g,h be FinSequence;
thus f,g are_fiberwise_equipotent implies f^h, g^h are_fiberwise_equipotent
proof assume
A1: f,g are_fiberwise_equipotent;
now let y;
card (f"{y}) = card (g"{y}) by A1,Def1;
hence card ((f^h)"{y}) = card(g"{y}) + card(h"{y}) by FINSEQ_3:63
.= card((g^h)"{y}) by FINSEQ_3:63;
end;
hence thesis by Def1;
end; assume
A2: f^h,g^h are_fiberwise_equipotent;
now let x;
card((f^h)"{x}) = card(f"{x})+card(h"{x}) &
card((g^h)"{x}) = card(g"{x})+card(h"{x}) &
card((f^h)"{x}) = card((g^h)"{x}) by A2,Def1,FINSEQ_3:63;
hence card(f"{x}) = card(g"{x}) by XCMPLX_1:2;
end;
hence thesis by Def1;
end;
theorem
for f,g be FinSequence holds f^g, g^f are_fiberwise_equipotent
proof let f,g be FinSequence;
let y;
thus card((f^g)"{y}) = card(g"{y})+ card(f"{y}) by FINSEQ_3:63
.= card((g^f)"{y}) by FINSEQ_3:63;
end;
theorem Th16:
for f,g be FinSequence st
f,g are_fiberwise_equipotent holds len f = len g & dom f = dom g
proof let f,g be FinSequence;
A1: dom f = Seg len f & Seg len g = dom g by FINSEQ_1:def 3;
assume f,g are_fiberwise_equipotent;
then A2: card(f"(rng f)) = card(g"(rng f)) & rng f = rng g by Th1,Th4;
thus len f = card(Seg len f) by FINSEQ_1:78
.= card(g"(rng g)) by A1,A2,RELAT_1:169
.= card(Seg len g) by A1,RELAT_1:169
.= len g by FINSEQ_1:78;
hence thesis by A1;
end;
theorem
for f,g be FinSequence holds
f,g are_fiberwise_equipotent iff ex P be Permutation of dom g st f = g*P
proof let f,g be FinSequence;
thus f,g are_fiberwise_equipotent implies
ex P be Permutation of dom g st f = g*P
proof assume A1: f,g are_fiberwise_equipotent;
then dom f = dom g by Th16;
hence thesis by A1,Th6;
end;
given P be Permutation of dom g such that
A2: f = g*P;
(dom g = {} implies dom g = {}) & P is Function of dom g,dom g;
then dom P = dom g & rng P c= dom g by FUNCT_2:def 1,RELSET_1:12;
then dom f = dom g by A2,RELAT_1:46;
hence thesis by A2,Th6;
end;
definition let F be Function, X be finite set;
cluster F|X -> finite Function-like;
coherence
proof
dom(F|X) c= X by RELAT_1:87;
then dom(F|X) is finite by FINSET_1:13;
hence thesis by AMI_1:21;
end;
end;
defpred P[Nat] means
for X be finite set,F be Function st card(dom(F|X)) = $1
ex a be FinSequence st F|X, a are_fiberwise_equipotent;
Lm2: P[0]
proof let X be finite set, F be Function; assume
card(dom(F|X)) = 0;
then A1: dom(F|X) = {} by CARD_2:59;
take A = {};
A2: dom A = {} by FINSEQ_1:26;
let x;
(F|X)"{x} c= dom(F|X) & A"{x} c= dom A by RELAT_1:167;
then (F|X)"{x} = {} & A"{x} = {} by A1,A2,XBOOLE_1:3;
hence Card((F|X)"{x}) = Card(A"{x});
end;
Lm3: for n st P[n] holds P[n+1]
proof let n be Nat; assume
A1: P[n];
let X be finite set, F be Function;
reconsider dx = dom(F|X) as finite set;
assume
A2: card dom(F|X) = n+1;
then A3: dx <> {} by CARD_1:78;
consider x being Element of dx;
set Y = X\{x},
dy = dom(F|Y);
A4: {x} c= dx & dy = dom F /\ Y & dx = dom F /\ X
by A2,CARD_1:78,FUNCT_1:68,ZFMISC_1:37;
dy = dx \ {x}
proof
thus dy c= dx \ {x}
proof let y; assume y in dy;
then A5: y in dom F & y in X \ {x} by A4,XBOOLE_0:def 3;
then A6: y in X & not y in {x} by XBOOLE_0:def 4;
then y in dx by A4,A5,XBOOLE_0:def 3;
hence thesis by A6,XBOOLE_0:def 4;
end;
let y; assume y in dx \{x};
then A7: y in dx & not y in {x} by XBOOLE_0:def 4;
then A8: y in dom F & y in X by A4,XBOOLE_0:def 3;
then y in Y by A7,XBOOLE_0:def 4;
hence thesis by A4,A8,XBOOLE_0:def 3;
end;
then card(dom(F|Y)) = card dx - card {x} by A4,CARD_2:63
.= n+1-1 by A2,CARD_1:79
.= n by XCMPLX_1:26;
then consider a be FinSequence such that
A9: F|Y, a are_fiberwise_equipotent by A1;
take A = a^<* F.x *>;
x in dx by A3;
then x in dom F /\ X by FUNCT_1:68;
then x in X & x in dom F by XBOOLE_0:def 3;
then A10: {x} c= X & {x} c= dom F by ZFMISC_1:37;
now let y;
A11: card((F|Y)"{y}) = card(a"{y}) by A9,Def1;
A12: Y misses {x} by XBOOLE_1:79;
A13: (F|Y)"{y} /\ (F|{x})"{y} = Y /\ (F"{y}) /\ (F|{x})"{y} by FUNCT_1:139
.= Y /\ F"{y} /\ ({x} /\ F"{y}) by FUNCT_1:139
.= F"{y} /\ Y /\ {x} /\ F"{y} by XBOOLE_1:16
.= F"{y} /\ (Y /\ {x}) /\ F"{y} by XBOOLE_1:16
.= {} /\ F"{y} by A12,XBOOLE_0:def 7
.= {};
A14: (F|Y)"{y} \/ (F|{x})"{y} = (Y /\ F"{y}) \/ (F|{x})"{y} by FUNCT_1:139
.= (Y /\ F"{y}) \/ ({x} /\ F"{y}) by FUNCT_1:139
.= (Y \/ {x}) /\ F"{y} by XBOOLE_1:23
.= (X \/ {x}) /\ F"{y} by XBOOLE_1:39
.= X /\ F"{y} by A10,XBOOLE_1:12
.= (F|X)"{y} by FUNCT_1:139;
A15: dom(F|{x}) = {x} by A10,RELAT_1:91;
A16: dom<*F.x*> = {1} by FINSEQ_1:4,55;
reconsider FF = <*F.x*>"{y} as finite set;
now per cases;
case A17: y = F.x;
A18: (F|{x})"{y} c= {x} by A15,RELAT_1:167;
{x} c= (F|{x})"{y}
proof let z be set; assume A19: z in {x};
then z = x by TARSKI:def 1;
then y = (F|{x}).z & y in {y} by A15,A17,A19,FUNCT_1:68,TARSKI:def 1;
hence z in (F|{x})"{y} by A15,A19,FUNCT_1:def 13;
end;
then (F|{x})"{y} = {x} by A18,XBOOLE_0:def 10;
then A20: card((F|{x})"{y}) = 1 by CARD_1:79;
A21: <*F.x*>"{y} c= {1} by A16,RELAT_1:167;
{1} c= <*F.x*>"{y}
proof let z be set; assume A22: z in {1};
then z = 1 by TARSKI:def 1;
then y = <*F.x*>.z & y in {y} by A17,FINSEQ_1:57,TARSKI:def 1;
hence z in <*F.x*>"{y} by A16,A22,FUNCT_1:def 13;
end;
then <*F.x*>"{y} = {1} by A21,XBOOLE_0:def 10;
hence card((F|{x})"{y}) = card FF by A20,CARD_1:79;
case A23: y <> F.x;
A24: now assume
A25: (F|{x})"{y} <> {};
consider z being Element of (F|{x})"{y};
A26: z in {x} & (F|{x}).z in {y} by A15,A25,FUNCT_1:def 13;
then z = x & (F|{x}).z = y by TARSKI:def 1;
hence contradiction by A15,A23,A26,FUNCT_1:68;
end;
now assume
A27: <*F.x*>"{y} <> {};
consider z being Element of <*F.x*>"{y};
z in {1} & <*F.x*>.z in {y} by A16,A27,FUNCT_1:def 13;
then z = 1 & <*F.x*>.z = y by TARSKI:def 1;
hence contradiction by A23,FINSEQ_1:57;
end;
hence card((F|{x})"{y}) = card FF by A24;
end;
hence card((F|X)"{y}) = card((F|Y)"{y}) + card FF - card {}
by A13,A14,CARD_2:64
.= card(A"{y}) by A11,CARD_1:78,FINSEQ_3:63;
end;
hence thesis by Def1;
end;
theorem
for F be Function, X be finite set
ex f be FinSequence st F|X, f are_fiberwise_equipotent
proof let F be Function, X be finite set;
A1: for n holds P[n] from Ind(Lm2,Lm3);
card(dom(F|X)) = card(dom(F|X));
hence thesis by A1;
end;
definition let D be set,
f be FinSequence of D,
n be Nat;
func f /^ n -> FinSequence of D means :Def2:
len it = len f - n & for m be Nat st
m in dom it holds it.m = f.(m+n) if n<=len f
otherwise it = <*>D;
existence
proof
thus n<=len f implies ex p1 be FinSequence of D st
len p1 = len f - n & for m st m in dom p1 holds p1.m = f.(m+n)
proof assume n<=len f;
then max(0,len f - n) = len f - n by FINSEQ_2:4;
then reconsider k = len f - n as Nat by FINSEQ_2:5;
deffunc F(Nat)=f.($1+n);
consider p be FinSequence such that
A1: len p = k & for m st m in Seg k holds p.m = F(m) from SeqLambda;
A2: dom p = Seg len p & Seg len f = dom f & rng f c= D
by FINSEQ_1:def 3,def 4;
rng p c= rng f
proof let x; assume x in rng p;
then consider m such that
A3: m in dom p & p.m = x by FINSEQ_2:11;
m in Seg len p by A3,FINSEQ_1:def 3;
then A4: p.m = f.(m+n) by A1;
1<=m & m<=len p & m<=m+n by A3,FINSEQ_3:27,NAT_1:29;
then 1<=m+n & m+n<=len f by A1,AXIOMS:22,REAL_1:84;
then m+n in dom f by FINSEQ_3:27;
hence x in rng f by A3,A4,FUNCT_1:def 5;
end;
then rng p c= D by A2,XBOOLE_1:1;
then reconsider p as FinSequence of D by FINSEQ_1:def 4;
take p;
thus len p = len f - n by A1;
let m be Nat; assume m in dom p;
then m in Seg k by A1,FINSEQ_1:def 3;
hence p.m = f.(m+n) by A1;
end;
thus not n<=len f implies ex p1 be FinSequence of D st p1 = <*>D;
end;
uniqueness
proof let p1,p2 be FinSequence of D;
thus n<=len f &
(len p1 = len f - n & for m st m in dom p1 holds p1.m = f.(m+n)) &
(len p2 = len f - n & for m st m in dom p2 holds p2.m = f.(m+n)) implies
p1 = p2
proof assume that
n<=len f and
A5: len p1 = len f - n & for m st m in dom p1 holds p1.m = f.(m+n) and
A6: len p2 = len f - n & for m st m in dom p2 holds p2.m = f.(m+n);
A7: dom p1 = Seg len p1 & Seg len p2 = dom p2 by FINSEQ_1:def 3;
now let m; assume m in Seg len p1;
then p1.m = f.(m+n) & p2.m = f.(m+n) by A5,A6,A7;
hence p1.m = p2.m;
end;
hence p1 = p2 by A5,A6,FINSEQ_2:10;
end;
thus not n<=len f & p1 = <*>D & p2 = <*>D implies p1 = p2;
end;
consistency;
end;
Lm4:
for D be non empty set, f be FinSequence of D st len f<=n holds (f|n) = f
proof let D be non empty set,f be FinSequence of D; assume
A1: len f<=n;
A2: dom f = Seg len f & f|n = f|Seg n by FINSEQ_1:def 3,TOPREAL1:def 1;
then dom f c= Seg n by A1,FINSEQ_1:7;
hence (f|n) = f by A2,RELAT_1:97;
end;
theorem Th19:
for D be non empty set, f be FinSequence of D, n,m be Nat holds
n in dom f & m in Seg n implies (f|n).m = f.m & m in dom f
proof let D be non empty set,f be FinSequence of D, n,m; assume
A1: n in dom f & m in Seg n;
A2: dom f = Seg len f & f|n = f|Seg n by FINSEQ_1:def 3,TOPREAL1:def 1;
n<=len f by A1,FINSEQ_3:27;
then A3: Seg n c= dom f by A2,FINSEQ_1:7;
then Seg n = dom f /\ Seg n by XBOOLE_1:28
.= dom(f|n) by A2,FUNCT_1:68;
hence (f|n).m = f.m & m in dom f by A1,A2,A3,FUNCT_1:68;
end;
theorem Th20:
for D be non empty set, f be FinSequence of D, n be Nat, x be set st
len f = n+1 & x = f.(n+1) holds f = (f|n) ^ <*x*>
proof let D be non empty set, f be FinSequence of D, n,x; assume
A1: len f = n+1 & x = f.(n+1);
set fn = f|n;
A2: n<=n+1 by NAT_1:29;
then A3: len fn = n by A1,TOPREAL1:3;
then A4: len (fn^<*x*>) = n + len <*x*> by FINSEQ_1:35
.= len f by A1,FINSEQ_1:57;
now let m; assume m in Seg len f;
then A5: 1<=m & m<=len f by FINSEQ_1:3;
now per cases;
case m = len f;
hence f.m = (fn^<*x*>).m by A1,A3,FINSEQ_1:59;
case m <> len f;
then m<n+1 by A1,A5,REAL_1:def 5;
then A6: m<=n by NAT_1:38;
then A7: m in dom fn by A3,A5,FINSEQ_3:27;
1<=n by A5,A6,AXIOMS:22;
then A8:n in dom f by A1,A2,FINSEQ_3:27;
A9: Seg len fn = dom fn by FINSEQ_1:def 3;
thus (fn^<*x*>).m = fn.m by A7,FINSEQ_1:def 7
.= f.m by A3,A7,A8,A9,Th19;
end;
hence f.m = (fn^<*x*>).m;
end;
hence thesis by A4,FINSEQ_2:10;
end;
theorem Th21:
for D be non empty set, f be FinSequence of D, n be Nat holds (f|n)^(f/^n) = f
proof let D be non empty set, f be FinSequence of D,n;
set fn = f/^n;
now per cases;
case A1: len f<n;
then A2: f/^n = <*>D by Def2;
f|n = f by A1,Lm4;
hence (f|n) ^ (f/^n) = f by A2,FINSEQ_1:47;
case A3: n<=len f;
then A4: len fn = len f - n & for m st m in dom fn holds fn.m = f.(m+n) by
Def2;
A5: len (f|n) = n by A3,TOPREAL1:3;
then A6: len ((f|n)^(f/^n)) = n+(len f - n) by A4,FINSEQ_1:35
.= len f by XCMPLX_1:27;
A7: dom(f|n) = Seg n & dom f = dom f & dom fn = dom fn
by A5,FINSEQ_1:def 3;
now let m; assume m in Seg len f;
then A8: 1<=m & m<=len f by FINSEQ_1:3;
now per cases;
case m<=n;
then A9: m in Seg n & 1<=n by A8,AXIOMS:22,FINSEQ_1:3;
then A10: n in dom f by A3,FINSEQ_3:27;
thus ((f|n)^(f/^n)).m = (f|n).m by A7,A9,FINSEQ_1:def 7
.= f.m by A9,A10,Th19;
case A11: n<m;
then max(0,m-n) = m-n by FINSEQ_2:4;
then reconsider k = m-n as Nat by FINSEQ_2:5;
n+1<=m by A11,NAT_1:38;
then A12: 1<=k by REAL_1:84;
k<=len fn by A4,A8,REAL_1:49;
then A13: k in dom fn by A12,FINSEQ_3:27;
thus ((f|n) ^ (f/^n)).m = fn.k by A5,A6,A8,A11,FINSEQ_1:37
.= f.(k+n) by A3,A13,Def2
.= f.m by XCMPLX_1:27;
end;
hence ((f|n) ^ (f/^n)).m = f.m;
end;
hence (f|n) ^ (f/^n) = f by A6,FINSEQ_2:10;
end;
hence thesis;
end;
theorem
for R1,R2 be FinSequence of REAL
st R1,R2 are_fiberwise_equipotent holds Sum R1 = Sum R2
proof
defpred P[Nat] means
for f,g be FinSequence of REAL st f,g are_fiberwise_equipotent & len f = $1
holds Sum f = Sum g;
A1: P[0]
proof let f,g be FinSequence of REAL; assume
f,g are_fiberwise_equipotent & len f = 0;
then len g = 0 & f = <*>REAL by Th16,FINSEQ_1:32;
hence thesis by FINSEQ_1:32;
end;
A2: for n st P[n] holds P[n+1]
proof let n; assume
A3: P[n];
let f,g be FinSequence of REAL; assume
A4: f,g are_fiberwise_equipotent & len f = n+1;
then A5: rng f = rng g & len f = len g by Th1,Th16;
0<n+1 by NAT_1:19;
then 0+1<=n+1 by NAT_1:38;
then A6: n+1 in dom f by A4,FINSEQ_3:27;
set a = f.(n+1);
a in rng g by A5,A6,FUNCT_1:def 5;
then consider m such that
A7: m in dom g & g.m = a by FINSEQ_2:11;
A8: g = (g|m)^(g/^m) by Th21;
A9: 1<=m & m<=len g by A7,FINSEQ_3:27;
then max(0,m-1) = m-1 by FINSEQ_2:4;
then reconsider m1 = m-1 as Nat by FINSEQ_2:5;
set gg = g/^m,
gm = g|m;
A10: len gm = m by A9,TOPREAL1:3;
A11: m = m1+1 by XCMPLX_1:27;
m in Seg m by A9,FINSEQ_1:3;
then gm.m = a & m in dom g by A7,Th19;
then A12: gm = (gm|m1)^<*a*> by A10,A11,Th20;
m1<=m by A11,NAT_1:29;
then A13: Seg m1 c= Seg m by FINSEQ_1:7;
A14: gm|m1 = gm|(Seg m1) by TOPREAL1:def 1
.= (g|(Seg m))|(Seg m1) by TOPREAL1:def 1
.= g|((Seg m)/\(Seg m1)) by RELAT_1:100
.= g|(Seg m1) by A13,XBOOLE_1:28
.= g|m1 by TOPREAL1:def 1;
set fn = f|n;
n<=n+1 by NAT_1:29;
then A15: len fn = n by A4,TOPREAL1:3;
A16: f = fn ^ <*a*> by A4,Th20;
now let x;
card(f"{x}) = card(g"{x}) by A4,Def1;
then card(fn"{x}) + card(<*a*>"{x}) = card(((g|m1)^<*a*>^(g/^m))"{x})
by A8,A12,A14,A16,FINSEQ_3:63
.= card(((g|m1)^<*a*>)"{x}) + card((g/^m)"{x}) by FINSEQ_3:63
.= card((g|m1)"{x})+ card(<*a*>"{x}) + card((g/^m)"{x}) by FINSEQ_3:63
.= card((g|m1)"{x}) + card((g/^m)"{x})+ card(<*a*>"{x}) by XCMPLX_1:1
.= card(((g|m1)^(g/^m))"{x})+ card(<*a*>"{x}) by FINSEQ_3:63;
hence card(fn"{x}) = card(((g|m1)^(g/^m))"{x}) by XCMPLX_1:2;
end;
then fn, (g|m1)^(g/^m) are_fiberwise_equipotent by Def1;
then Sum fn = Sum((g|m1)^gg) by A3,A15;
hence Sum f = Sum((g|m1)^gg) + Sum <*a*> by A16,RVSUM_1:105
.= Sum(g|m1) + Sum gg+ Sum <*a*> by RVSUM_1:105
.= Sum(g|m1)+ Sum <*a*> + Sum gg by XCMPLX_1:1
.= Sum gm + Sum gg by A12,A14,RVSUM_1:105
.= Sum g by A8,RVSUM_1:105;
end;
A17: for n holds P[n] from Ind(A1,A2);
let R1,R2 be FinSequence of REAL; assume
A18: R1,R2 are_fiberwise_equipotent;
len R1 = len R1;
hence thesis by A17,A18;
end;
definition let R be FinSequence of REAL;
func MIM(R) -> FinSequence of REAL means :Def3:
len it = len R & it.(len it) = R.(len R) &
for n be Nat st 1 <= n & n <= len it - 1 holds it.n = (R.n) - (R.(n+1));
existence
proof
per cases;
suppose A1: len R = 0;
take a = R;
thus len a = len R & a.(len a) = R.(len R);
let n; assume 1<=n & n<=len a - 1;
hence a.n = R.n - R.(n+1) by A1,AXIOMS:22;
suppose len R <> 0;
then 0<len R by NAT_1:19;
then 0+1<=len R by NAT_1:38;
then max(0,len R -1) = len R - 1 by FINSEQ_2:4;
then reconsider l = len R -1 as Nat by FINSEQ_2:5;
set t = R.(len R);
defpred
P[Nat,set] means $2 = R.$1 - R.($1+1);
A2: for n st n in Seg l ex x be Real st P[n,x];
consider p be FinSequence of REAL such that
A3: dom p = Seg l & for n st n in Seg l holds P[n,p.n] from SeqDEx(A2);
take a = p^<*t*>;
thus A4: len a = len p + len <*t*> by FINSEQ_1:35
.= l+len <*t*> by A3,FINSEQ_1:def 3
.= l+1 by FINSEQ_1:56
.= len R by XCMPLX_1:27;
hence a.(len a) = a.(l+1) by XCMPLX_1:27
.= a.(len p +1) by A3,FINSEQ_1:def 3
.= R.(len R) by FINSEQ_1:59;
let n; assume
1<=n & n<=len a - 1;
then A5: n in Seg l by A4,FINSEQ_1:3;
then p.n = R.n - R.(n+1) by A3;
hence thesis by A3,A5,FINSEQ_1:def 7;
end;
uniqueness
proof let p1,p2 be FinSequence of REAL; assume that
A6: len p1 = len R & p1.(len p1) = R.(len R) and
A7: for n st 1<=n & n<=len p1 - 1 holds p1.n = R.n - R.(n+1) and
A8: len p2 = len R & p2.(len p2) = R.(len R) and
A9: for n st 1<=n & n<=len p2 - 1 holds p2.n = R.n - R.(n+1);
now let n;
assume n in Seg len R;
then A10: 1<=n & n<=len R by FINSEQ_1:3;
set r = R.n;
now per cases;
case n = len R; hence p1.n = p2.n by A6,A8;
case n <> len R; then n<len R & n<=n+1 by A10,NAT_1:29,REAL_1:def 5;
then A11: 1<=n+1 & n+1<=len R by A10,NAT_1:38;
set s = R.(n+1);
n<=len R - 1 by A11,REAL_1:84;
then p1.n = r-s & p2.n = r-s by A6,A7,A8,A9,A10;
hence p1.n = p2.n;
end;
hence p1.n = p2.n;
end;
hence thesis by A6,A8,FINSEQ_2:10;
end;
end;
theorem Th23:
for R be FinSequence of REAL, r be Real, n be Nat
st len R = n+2 & R.(n+1) = r holds MIM(R|(n+1)) = MIM(R)|n ^ <* r *>
proof let R be FinSequence of REAL, s,n; assume
A1: len R = n+2 & R.(n+1) = s;
set f1 = R|(n+1),
m1 = MIM(f1),
mf = MIM(R),
fn = mf|n;
A2: n+1+1 = n+(1+1) by XCMPLX_1:1;
then A3: n+1<=n+2 by NAT_1:29;
then A4: len f1 = n+1 by A1,TOPREAL1:3;
then A5: len MIM(f1) = n+1 & len mf = n+2 by A1,Def3;
A6: n<=n+2 by NAT_1:29;
then A7: len fn = n by A5,TOPREAL1:3;
then A8: len(fn^<*s*>) = n + len <*s*> by FINSEQ_1:35
.= n+1 by FINSEQ_1:57;
A9: dom m1 = Seg len m1 & Seg len f1 = dom f1 & Seg len mf = dom mf &
Seg len fn = dom fn & Seg len R = dom R by FINSEQ_1:def 3;
0<n+1 by NAT_1:19;
then 0+1<=n+1 by NAT_1:38;
then A10: n+1 in Seg(n+2) & n+1 in Seg(n+1) by A3,FINSEQ_1:3;
then f1.(n+1) = s by A1,A9,Th19;
then A11: m1.(n+1) = s by A4,A5,Def3;
now let m; assume
A12: m in Seg (n+1);
then A13: 1<=m & m<=n+1 by FINSEQ_1:3;
now per cases;
case m = n+1;
hence m1.m = (fn^<*s*>).m by A7,A11,FINSEQ_1:59;
case m <> n+1;
then A14: m<n+1 by A13,REAL_1:def 5;
then A15: m<=n by NAT_1:38;
then A16: m in Seg n by A13,FINSEQ_1:3;
1<=n by A13,A15,AXIOMS:22;
then n in Seg(n+2) by A6,FINSEQ_1:3;
then A17: fn.m = mf.m & m in dom mf by A5,A9,A16,Th19;
A18: len mf -1 = n+(1+1-1) by A5,XCMPLX_1:29
.= n+1;
set r1 = R.m;
A19: 1<=m+1 & m+1<=n+2 by A2,A13,AXIOMS:24,NAT_1:29;
set r2 = R.(m+1);
A20: r1 - r2 = fn.m by A13,A17,A18,Def3
.= (fn^<*s*>).m by A7,A9,A16,FINSEQ_1:def 7;
A21: len m1 -1 = n by A5,XCMPLX_1:26;
A22: f1.m = r1 by A1,A9,A10,A12,Th19;
m+1<=n+1 by A14,NAT_1:38;
then m+1 in Seg(n+1) by A19,FINSEQ_1:3;
then f1.(m+1) = r2 by A1,A9,A10,Th19;
hence m1.m = (fn^<*s*>).m by A13,A15,A20,A21,A22,Def3;
end;
hence m1.m = (fn^<*s*>).m;
end;
hence thesis by A5,A8,FINSEQ_2:10;
end;
theorem Th24:
for R be FinSequence of REAL, r,s be Real, n be Nat st
len R = n+2 & R.(n+1) = r & R.(n+2) = s holds MIM(R) = MIM(R)|n ^ <* r-s,s *>
proof let R be FinSequence of REAL, r,s,n;
set mf = MIM(R),
nf = mf|n; assume
A1: len R = n+2 & R.(n+1) = r & R.(n+2) = s;
then A2: len mf = n+2 by Def3;
A3: n+(1+1) = n+1+1 by XCMPLX_1:1;
then A4: n<=n+1 & n+1<=n+2 & n<=n+2 by NAT_1:29;
then A5: len nf = n by A2,TOPREAL1:3;
then len (nf^<* r-s,s *>) = n + len <* r-s,s *> by FINSEQ_1:35;
then A6: len(nf^<* r-s,s *>) = n+2 & <*r-s,s*>.1 = r-s & <*r-s,s*>.2 = s
by FINSEQ_1:61;
A7: n<n+2 by A4,NAT_1:38;
now let m; assume
m in Seg(n+2);
then A8: 1<=m & m<=n+2 by FINSEQ_1:3;
now per cases;
case A9: m = n+2;
hence mf.m = s by A1,A2,Def3
.= <* r-s,s *>.(n+2-n) by A6,XCMPLX_1:26
.= (nf ^ <* r-s,s *>).m by A5,A6,A7,A9,FINSEQ_1:37;
case m <> n+2;
then m<n+2 by A8,REAL_1:def 5;
then A10: m<=n+1 by A3,NAT_1:38;
A11: len mf - 1 = n+1 by A2,A3,XCMPLX_1:26;
now per cases;
case A12: m = n+1;
then A13: n<m by NAT_1:38;
thus mf.m = r - s by A1,A3,A8,A11,A12,Def3
.= <* r-s,s *>.(n+1-n) by A6,XCMPLX_1:26
.= (nf ^ <* r-s,s *>).m by A5,A6,A8,A12,A13,FINSEQ_1:37;
case m <> n+1; then m<n+1 by A10,REAL_1:def 5; then m<=n by NAT_1:38
;
then A14: m in Seg n & m<=m+1 & m+1<=n+1 & 1<=n
by A8,AXIOMS:22,24,FINSEQ_1:3,NAT_1:29;
then A15: n in Seg(n+2) by A4,FINSEQ_1:3;
A16: dom nf = Seg len nf & dom mf = Seg len mf by FINSEQ_1:def 3;
hence mf.m = nf.m by A2,A14,A15,Th19
.= (nf ^ <* r-s,s *>).m by A5,A14,A16,FINSEQ_1:def 7;
end;
hence mf.m = (nf ^ <* r-s,s *>).m;
end;
hence mf.m = (nf ^ <* r-s,s *>).m;
end;
hence thesis by A2,A6,FINSEQ_2:10;
end;
theorem Th25:
MIM( <*>REAL ) = <*>REAL
proof
set o = <*>REAL,
mo = MIM(o);
A1: len mo = len o & len o = 0 by Def3,FINSEQ_1:32;
for n st n in Seg 0 holds mo.n = o.n by FINSEQ_1:4;
hence thesis by A1,FINSEQ_2:10;
end;
theorem Th26:
for r be Real holds MIM(<*r*>) = <*r*>
proof let r be Real;
set f = <*r*>;
A1: len f = 1 & f.1 = r by FINSEQ_1:57;
then A2: len MIM(f) = 1 by Def3;
now let n; assume n in Seg 1;
then n = 1 by FINSEQ_1:4,TARSKI:def 1;
hence MIM(f).n = f.n by A1,A2,Def3;
end;
hence thesis by A1,A2,FINSEQ_2:10;
end;
theorem
for r,s be Real holds MIM(<*r,s*>) = <*r-s,s*>
proof let r,s be Real;
set f = <*r,s*>;
0+2 = 2 & 0+1 = 1 & len f = 2 & f.1 = r & f.2 = s by FINSEQ_1:61;
then A1: MIM(f) = MIM(f)|0 ^ <*r-s,s*> by Th24;
0<=len MIM(f) by NAT_1:18;
then len(MIM(f)|0) = 0 by TOPREAL1:3;
then MIM(f)|0 = {} by FINSEQ_1:25;
hence thesis by A1,FINSEQ_1:47;
end;
theorem
for R be FinSequence of REAL, n be Nat holds MIM(R) /^ n = MIM(R/^n)
proof let R be FinSequence of REAL,n;
set mf = MIM(R),
fn = R/^n,
mn = MIM(fn);
A1: len mf = len R & len mn = len fn by Def3;
now per cases;
case len R<n;
then mf /^ n = <*>REAL & fn = <*>REAL by A1,Def2;
hence mf /^ n = mn by Th25;
case A2: n<=len R;
then A3: len(mf/^n) = len R - n &
for m st m in dom(mf/^n) holds (mf/^n).m = mf.(m+n) by A1,Def2;
A4: len fn = len R - n &
for m st m in dom fn holds fn.m = R.(m+n) by A2,Def2;
A5: len mn = len fn by Def3;
A6: Seg len fn = dom fn & Seg len(mf/^n) = dom(mf/^n) by FINSEQ_1:def 3;
now let m; assume
A7: m in Seg len fn;
then A8: 1<=m & m<=len fn by FINSEQ_1:3;
m<=m+n by NAT_1:29;
then A9: 1<=m+n & m+n<=len R by A4,A8,AXIOMS:22,REAL_1:84;
set r1 = R.(m+n);
A10: fn.m = r1 by A2,A6,A7,Def2;
now per cases;
case A11: m = len fn;
then A12: m+n = len R by A4,XCMPLX_1:27;
thus (mf/^n).m = mf.(m+n) by A3,A4,A6,A7
.= r1 by A1,A12,Def3
.= mn.m by A5,A10,A11,Def3;
case m <> len fn;
then m<len fn by A8,REAL_1:def 5;
then A13: m+1<=len fn by NAT_1:38;
then A14: m+1+n<=len R & m<=m+1 & m+1<=m+1+n by A4,NAT_1:29,REAL_1:84;
set r2 = R.(m+1+n);
A15: m+1+n = m+n+1 by XCMPLX_1:1;
then A16: m+n<=len R - 1 & m<=len fn - 1 by A13,A14,REAL_1:84;
1<=m+1 by NAT_1:29;
then m+1 in dom fn by A13,FINSEQ_3:27;
then A17: fn.(m+1) = r2 by A2,Def2;
thus (mf/^n).m = mf.(m+n) by A3,A4,A6,A7
.= r1-r2 by A1,A9,A15,A16,Def3
.= mn.m by A1,A8,A10,A16,A17,Def3;
end;
hence (mf/^n).m = mn.m;
end;
hence thesis by A3,A4,A5,FINSEQ_2:10;
end;
hence thesis;
end;
theorem Th29:
for R be FinSequence of REAL st len R <> 0 holds Sum MIM(R) = R.1
proof let R be FinSequence of REAL;
defpred P[Nat] means
for R be FinSequence of REAL st len R <> 0 & len R = $1 holds Sum
MIM(R) = R.1;
A1: P[0];
A2: for n st P[n] holds P[n+1]
proof let n; assume
A3: P[n];
let R be FinSequence of REAL; assume
A4: len R <> 0 & len R = n+1;
now per cases;
case n = 0;
then A5: R = <*R.1*> by A4,FINSEQ_1:57;
then MIM(R) = R by Th26;
hence Sum MIM(R) = R.1 by A5,RVSUM_1:103;
case n <> 0;
then 0<n by NAT_1:19;
then 0+1<=n by NAT_1:38;
then max(0,n-1) = n-1 by FINSEQ_2:4;
then reconsider n1 = n-1 as Nat by FINSEQ_2:5;
A6: n1+2 = n1+(1+1)
.= n1+1+1 by XCMPLX_1:1;
then A7: n1+2 = len R by A4,XCMPLX_1:27;
A8: 0+1<=n1+1 & n1+1<=n1+2 by A6,NAT_1:29;
then A9: n1+1 in Seg(n1+2) by FINSEQ_1:3;
set r = R.(n1+1);
set s = R.(n1+2);
set f1 = R|(n1+1);
A10: n1+1 = n by XCMPLX_1:27;
A11: len f1 = n1+1 by A7,A8,TOPREAL1:3;
A12: Seg len R = dom R & 1 in Seg(n1+1) by A8,FINSEQ_1:3,def 3;
thus Sum MIM(R) = Sum((MIM(R)|n1) ^ <* r-s,s *>) by A7,Th24
.= Sum(MIM(R)|n1) + Sum(<* r-s,s *>) by RVSUM_1:105
.= Sum(MIM(R)|n1) + (r-s + s) by RVSUM_1:107
.= Sum(MIM(R)|n1) + r by XCMPLX_1:27
.= Sum((MIM(R)|n1) ^<*r*>) by RVSUM_1:104
.= Sum MIM(f1) by A7,Th23
.= f1.1 by A3,A10,A11
.= R.1 by A7,A9,A12,Th19;
end;
hence Sum MIM(R) = R.1;
end;
A13: for n holds P[n] from Ind(A1,A2);
assume len R <> 0;
hence thesis by A13;
end;
theorem
for R be FinSequence of REAL, n be Nat
st 1<=n & n<len R holds Sum MIM(R/^n) = R.(n+1)
proof let R be FinSequence of REAL,n; assume
A1: 1<=n & n<len R;
then n+1<=len R & n<=len R & n <> len R by NAT_1:38;
then A2: 1<=len R - n by REAL_1:84;
len(R/^n) = len R - n &
for m st m in dom(R/^n) holds (R/^n).m = R.(m+n) by A1,Def2;
then A3: 1 in dom(R/^n) & Seg len(R/^n) = dom(R/^n) & len(R/^n) <> 0
by A2,FINSEQ_1:def 3,FINSEQ_3:27;
hence Sum MIM(R/^n) = (R/^n).1 by Th29
.= R.(n+1) by A1,A3,Def2;
end;
definition let IT be FinSequence of REAL;
attr IT is non-increasing means :Def4:
for n be Nat st n in dom IT & n+1 in dom IT holds IT.n >= IT.(n+1);
end;
definition
cluster non-increasing FinSequence of REAL;
existence
proof
take f = <*>REAL;
let n; assume n in dom f & n+1 in dom f;
hence f.n>=f.(n+1) by FINSEQ_1:26;
end;
end;
theorem Th31:
for R be FinSequence of REAL
st len R = 0 or len R = 1 holds R is non-increasing
proof let R be FinSequence of REAL; assume
A1: len R = 0 or len R = 1;
now per cases by A1;
case len R = 0;
then R = <*>REAL by FINSEQ_1:32;
then for n st n in dom R & n+1 in dom R holds R.n>=R.(n+1) by FINSEQ_1:26;
hence thesis by Def4;
case len R = 1;
then A2: dom R = {1} by FINSEQ_1:4,def 3;
now let n; assume n in dom R & n+1 in dom R;
then n = 1 & n+1 = 1 by A2,TARSKI:def 1;
hence R.n>=R.(n+1);
end;
hence thesis by Def4;
end;
hence thesis;
end;
theorem Th32:
for R be FinSequence of REAL holds
R is non-increasing
iff
for n,m be Nat st n in dom R & m in dom R & n<m holds R.n>=R.m
proof let R be FinSequence of REAL;
thus R is non-increasing implies
for n,m st n in dom R & m in dom R & n<m holds R.n>=R.m
proof assume
A1: R is non-increasing;
defpred P[Nat] means $1 in dom R implies
for n st n in dom R & n<$1 holds R.n>=R.$1;
Seg len R = dom R by FINSEQ_1:def 3;
then A2: P[0] by FINSEQ_1:3;
A3: for m st P[m] holds P[m+1]
proof let m; assume
A4: P[m]; assume
A5: m+1 in dom R;
let n; assume
A6: n in dom R & n<m+1;
then A7: 1<=m+1 & m+1<=len R & 1<=n & n<=len R & n<=m & m<=m+1
by A5,FINSEQ_3:27,NAT_1:38;
then A8: 1<=m & m<=len R by AXIOMS:22;
then A9: m in dom R by FINSEQ_3:27;
set t = R.m, r = R.n, s = R.(m+1);
now per cases;
case n = m; hence r>=s by A1,A5,A6,Def4;
case n <> m;
then n<m by A7,REAL_1:def 5;
then A10: r>=t by A4,A6,A8,FINSEQ_3:27;
t>=s by A1,A5,A9,Def4;
hence r>=s by A10,AXIOMS:22;
end;
hence r>=s;
end;
for m holds P[m] from Ind(A2,A3);
hence thesis;
end; assume
A11: for n,m st n in dom R & m in dom R & n<m holds R.n>=R.m;
let n; assume
A12: n in dom R & n+1 in dom R;
n<n+1 by NAT_1:38;
hence thesis by A11,A12;
end;
theorem Th33:
for R be non-increasing FinSequence of REAL, n be Nat holds
R|n is non-increasing FinSequence of REAL
proof let f be non-increasing FinSequence of REAL, n;
set fn = f|n;
now per cases;
case A1: n = 0; then n<=len f by NAT_1:18;
then len fn = 0 by A1,TOPREAL1:3;
hence thesis by Th31;
case n <> 0;
then 0<n by NAT_1:19;
then A2: 0+1<=n by NAT_1:38;
now per cases;
case len f<=n; hence thesis by Lm4;
case n<len f;
then A3: n in dom f & len fn = n by A2,FINSEQ_3:27,TOPREAL1:3;
now let m; assume
A4: m in dom fn & m+1 in dom fn;
dom f = Seg len f & dom fn = Seg len fn by FINSEQ_1:def 3;
then f.m = fn.m & f.(m+1) = fn.(m+1) & m in dom f & m+1 in dom f
by A3,A4,Th19;
hence fn.m>=fn.(m+1) by Def4;
end;
hence thesis by Def4;
end;
hence thesis;
end;
hence thesis;
end;
theorem
for R be non-increasing FinSequence of REAL, n be Nat holds
R /^ n is non-increasing FinSequence of REAL
proof let f be non-increasing FinSequence of REAL, n;
set fn = f /^ n;
now let m; assume
A1: m in dom fn & m+1 in dom fn;
then A2: 1<=m & m<=len fn & 1<=m+1 & m+1<=len fn by FINSEQ_3:27;
A3: m+1+n = m+n+1 & m<=m+n & m+1<=m+1+n by NAT_1:29,XCMPLX_1:1;
then A4: 1<=m+n & 1<=m+n+1 & 1<=len fn by A2,AXIOMS:22;
set r = fn.m, s = fn.(m+1);
now per cases;
case n<=len f;
then A5: len fn = len f - n & r = f.(m+n) & s = f.(m+n+1) by A1,A3,Def2;
then m+n<=len f & m+n+1<=len f by A2,A3,REAL_1:84;
then m+n in dom f & m+n+1 in dom f by A4,FINSEQ_3:27;
hence r>=s by A5,Def4;
case len f<n;
then fn = <*>REAL by Def2;
hence r>=s by A1,FINSEQ_1:26;
end;
hence r>=s;
end;
hence thesis by Def4;
end;
Lm5:
for f,g be non-increasing FinSequence of REAL, n st
len f = n+1 & len f = len g & f,g are_fiberwise_equipotent holds
f.(len f) = g.(len g) & f|n, g|n are_fiberwise_equipotent
proof let f,g be non-increasing FinSequence of REAL, n; assume
A1: len f = n+1 & len f = len g & f,g are_fiberwise_equipotent;
0<n+1 by NAT_1:19;
then 0+1<=n+1 by NAT_1:38;
then A2: n+1 in dom f & n+1 in dom g by A1,FINSEQ_3:27;
set r = f.(n+1), s = g.(n+1);
A3: now assume A4: r <> s;
A5: rng f = rng g by A1,Th1;
now per cases by A4,REAL_1:def 5;
case A6: r>s;
s in rng f by A2,A5,FUNCT_1:def 5;
then consider m such that
A7: m in dom f & f.m = s by FINSEQ_2:11;
A8: 1<=m & m<=len f by A7,FINSEQ_3:27;
now per cases;
case m = len f;
hence contradiction by A1,A6,A7;
case m <> len f;
then m<n+1 by A1,A8,REAL_1:def 5;
hence contradiction by A2,A6,A7,Th32;
end;
hence contradiction;
case A9: r<s;
r in rng g by A2,A5,FUNCT_1:def 5;
then consider m such that
A10: m in dom g & g.m = r by FINSEQ_2:11;
A11: 1<=m & m<=len g by A10,FINSEQ_3:27;
now per cases;
case m = len g;
hence contradiction by A1,A9,A10;
case m <> len g;
then m<n+1 by A1,A11,REAL_1:def 5;
hence contradiction by A2,A9,A10,Th32;
end;
hence contradiction;
end;
hence contradiction;
end;
hence f.(len f) = g.(len g) by A1;
A12: f = (f|n)^<*r*> & g = (g|n)^<*r*> by A1,A3,Th20;
now let x;
card((f|n)"{x}) + card(<*r*>"{x}) = card (f"{x}) by A12,FINSEQ_3:63
.= card(g"{x}) by A1,Def1
.= card((g|n)"{x}) + card(<*r*>"{x}) by A12,FINSEQ_3:63;
hence card((f|n)"{x}) = card((g|n)"{x}) by XCMPLX_1:2;
end;
hence thesis by Def1;
end;
defpred P[Nat] means
for R be FinSequence of REAL st $1 = len R
ex b be non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent;
Lm6: P[0]
proof let R be FinSequence of REAL; assume
len R = 0;
then reconsider a = R as non-increasing FinSequence of REAL by Th31;
take a;
thus thesis;
end;
Lm7: for n st P[n] holds P[n+1]
proof let n; assume
A1: P[n];
let R be FinSequence of REAL; assume
A2: n+1 = len R;
then A3: dom R = Seg(n+1) by FINSEQ_1:def 3;
set fn = R|(Seg n);
A4: fn = R|n by TOPREAL1:def 1;
A5: dom fn = dom R /\ Seg n by FUNCT_1:68;
reconsider fn as FinSequence by FINSEQ_1:19;
rng fn c= rng R & rng R c= REAL by FINSEQ_1:def 4,FUNCT_1:76;
then rng fn c= REAL by XBOOLE_1:1;
then reconsider fn as FinSequence of REAL by FINSEQ_1:def 4;
n<=n+1 by NAT_1:29;
then Seg n c= Seg(n+1) by FINSEQ_1:7;
then dom fn = Seg n by A3,A5,XBOOLE_1:28;
then A6: len fn = n by FINSEQ_1:def 3;
then consider a be non-increasing FinSequence of REAL such that
A7: fn,a are_fiberwise_equipotent by A1;
A8: rng fn = rng a & len fn = len a by A7,Th1,Th16;
0<=n by NAT_1:18;
then 0+1<=n+1 by REAL_1:55;
then A9: n+1 in Seg(n+1) & Seg len a = dom a by FINSEQ_1:3,def 3;
set q = R.(n+1);
now per cases;
case A10: for t be Real st t in rng a holds q<=t;
set b = a^<*q*>;
A11: len b = n + len <*q*> by A6,A8,FINSEQ_1:35
.= n+1 by FINSEQ_1:56;
now let m; assume
m in dom b & m+1 in dom b;
then A12: 1<=m & m<=len b & 1<=m+1 & m+1<=len b by FINSEQ_3:27;
then m<=n+1-1 by A11,REAL_1:84;
then m<=n by XCMPLX_1:26;
then m in Seg n by A12,FINSEQ_1:3;
then A13: m in dom a by A6,A8,FINSEQ_1:def 3;
set r = b.m, s = b.(m+1);
A14: r = a.m & a.m in rng a by A13,FINSEQ_1:def 7,FUNCT_1:def 5;
now per cases;
case m+1 = len b;
then s = q by A6,A8,A11,FINSEQ_1:59;
hence r>=s by A10,A14;
case m+1 <> len b;
then m+1<len b by A12,REAL_1:def 5;
then m+1+1<=n+1 by A11,NAT_1:38;
then m+1<=n+1-1 by REAL_1:84;
then m+1<=n by XCMPLX_1:26;
then m+1 in Seg n by A12,FINSEQ_1:3;
then A15: m+1 in dom a by A6,A8,FINSEQ_1:def 3;
then a.(m+1) = s by FINSEQ_1:def 7;
hence r>=s by A13,A14,A15,Def4;
end;
hence r>=s;
end;
then reconsider b as non-increasing FinSequence of REAL by Def4;
take b;
fn^<*q*> = R by A2,A4,Th20;
hence R,b are_fiberwise_equipotent by A7,Th14;
case A16: ex t be Real st t in rng a & not q<=t;
defpred Q[Nat] means $1 in dom a & for r st r = a.$1 holds r<q;
A17: ex k be Nat st Q[k]
proof consider t be Real such that
A18: t in rng a & t<q by A16;
consider k be Nat such that
A19: k in dom a & a.k = t by A18,FINSEQ_2:11;
take k;
thus k in dom a by A19;
let r; assume r = a.k;
hence r<q by A18,A19;
end;
consider mi be Nat such that
A20: Q[mi] & for m st Q[m] holds mi <= m from Min(A17);
1<=mi by A20,FINSEQ_3:27;
then max(0,mi-1) = mi-1 by FINSEQ_2:4;
then reconsider k = mi-1 as Nat by FINSEQ_2:5;
set ak = a/^k,
b = (a|k)^<*q*>^ak;
mi<=mi+1 & mi<mi+1 by NAT_1:38;
then mi<=len a & k<=mi & k<mi by A20,FINSEQ_3:27,REAL_1:84;
then A21: k<=len a & k<len a by AXIOMS:22;
then A22: len(a|k) = k & len(a/^k) = len a - k & k+1<=len a
by Def2,NAT_1:38,TOPREAL1:3;
then A23: len((a|k)^<*q*>) = k+len <*q*> by FINSEQ_1:35
.= k+1 by FINSEQ_1:56;
A24: dom (a|k) = Seg len (a|k) & dom((a|k)^<*q*>) = Seg len((a|k)^<*q*>) &
dom(a/^k) = dom(a/^k) by FINSEQ_1:def 3;
A25: dom (a|k) c= dom((a|k)^<*q*>) by FINSEQ_1:39;
A26: 1<=len(a/^k) by A22,REAL_1:84;
A27: len b = k+1 + len(a/^k) by A23,FINSEQ_1:35;
now let m; assume
m in dom b & m+1 in dom b;
then A28: 1<=m & m<=len b & 1<=m+1 & m+1<=len b by FINSEQ_3:27;
set r = b.m, s = b.(m+1);
now per cases;
case A29: m+1<=k;
then A30: 1<=k & m<=k by A28,AXIOMS:22,NAT_1:38;
dom a = Seg len a by FINSEQ_1:def 3;
then A31: k in dom a & m in Seg k & m+1 in
Seg k by A21,A28,A29,A30,FINSEQ_1:3;
then A32: a.m = (a|k).m & a.(m+1) = (a|k).(m+1) & m in dom a & m+1 in
dom a
by Th19;
A33: b.m = ((a|k)^<*q*>).m by A22,A24,A25,A31,FINSEQ_1:def 7
.= a.m by A22,A24,A31,A32,FINSEQ_1:def 7;
A34: b.(m+1) = ((a|k)^<*q*>).(m+1) by A22,A24,A25,A31,FINSEQ_1:def 7
.= a.(m+1) by A22,A24,A31,A32,FINSEQ_1:def 7;
dom(a|k) c= dom((a|k)^(a/^k)) by FINSEQ_1:39;
then dom(a|k) c= dom a by Th21; hence r>=s by A22,A24,A31,A33,A34,Def4
;
case k<m+1;
then A35: k<=m by NAT_1:38;
now per cases;
case A36: k = m;
then A37: m in Seg k by A28,FINSEQ_1:3;
A38: k in dom a by A9,A21,A28,A36,FINSEQ_1:3;
then A39: a.m = (a|k).m & m in dom a by A37,Th19;
A40: b.m = ((a|k)^<*q*>).m by A22,A24,A25,A37,FINSEQ_1:def 7
.= a.m by A22,A24,A37,A39,FINSEQ_1:def 7;
m+1 in dom((a|k)^<*q*>) by A23,A24,A36,FINSEQ_1:6;
then A41: b.(m+1) = ((a|k)^<*q*>).(k+1) by A36,FINSEQ_1:def 7
.= q by A22,FINSEQ_1:59;
now assume s>r;
then for t be Real st t = a.k holds t<q by A36,A40,A41;
then mi<=k by A20,A38;
hence contradiction by SQUARE_1:29;
end;
hence r>=s;
case k <> m;
then k<m by A35,REAL_1:def 5;
then A42: k+1<=m by NAT_1:38;
then A43: k+1<m+1 by NAT_1:38;
max(0,m-(k+1)) = m-(k+1) by A42,FINSEQ_2:4;
then reconsider l = m-(k+1) as Nat by FINSEQ_2:5;
A44: l+1 = m+1-(k+1) by XCMPLX_1:29;
A45: 1<=l+1 & l+1<=l+1+k by NAT_1:29;
then l+1<=len b -(k+1) & 1<=l+1+k by A28,A44,AXIOMS:22,REAL_1:92;
then A46: l<=l+1 & l+1<=len(a/^k) & 1<=k+l+1
by A27,NAT_1:29,XCMPLX_1:26;
then A47: l+1 in dom(a/^k) & l<=len(a/^k) & k+(l+1)<=len a
by A22,A45,AXIOMS:22,FINSEQ_3:27,REAL_1:84;
then k+l+1<=len a & k+l<=k+l+1 by NAT_1:29,XCMPLX_1:1;
then A48: k+l+1 in dom a & k+l<=len a by A46,AXIOMS:22,FINSEQ_3:27;
now per cases;
case A49: k+1 = m;
then m in Seg (k+1) by A28,FINSEQ_1:3;
then A50: b.m = ((a|k)^<*q*>).(k+1) by A23,A24,A49,FINSEQ_1:def 7
.= q by A22,FINSEQ_1:59;
A51: 1 in dom(a/^k) by A26,FINSEQ_3:27;
b.(m+1) = (a/^k).(k+1+1 - (k+1)) by A23,A28,A43,A49,FINSEQ_1:37
.= (a/^k).1 by XCMPLX_1:26
.= a.(1+k) by A21,A51,Def2
.= a.mi by XCMPLX_1:27;
hence r>=s by A20,A50;
case k+1 <> m;
then A52: k+1<m by A42,REAL_1:def 5;
then k+1+1<=m & l<=l+k by NAT_1:29,38;
then A53: 1<=l & l<=k+l by REAL_1:84;
then A54: l in dom(a/^k) by A47,FINSEQ_3:27;
A55: b.m = (a/^k).l by A23,A28,A52,FINSEQ_1:37
.= a.(k+l) by A21,A54,Def2;
A56: b.(m+1) = (a/^k).(l+1) by A23,A28,A43,A44,FINSEQ_1:37
.= a.(l+1+k) by A21,A47,Def2
.= a.(k+l+1) by XCMPLX_1:1;
1<=k+l by A53,AXIOMS:22;
then k+l in dom a by A48,FINSEQ_3:27;
hence r>=s by A48,A55,A56,Def4;
end;
hence r>=s;
end;
hence r>=s;
end;
hence r>=s;
end;
then reconsider b as non-increasing FinSequence of REAL by Def4;
take b;
now let x;
A57: card(fn"{x}) = card(a"{x}) by A7,Def1;
thus card (b"{x}) = card (((a|k)^<*q*>)"{x}) + card(ak"{x})
by FINSEQ_3:63
.= card((a|k)"{x}) + card(<*q*>"{x}) + card(ak"{x}) by FINSEQ_3:63
.= card((a|k)"{x}) + card(ak"{x}) + card(<*q*>"{x}) by XCMPLX_1:1
.= card(((a|k)^ak)"{x}) + card(<*q*>"{x}) by FINSEQ_3:63
.= card(fn"{x}) + card(<*q*>"{x}) by A57,Th21
.= card((fn^<*q*>)"{x}) by FINSEQ_3:63
.= card(R"{x}) by A2,A4,Th20;
end;
hence R,b are_fiberwise_equipotent by Def1;
end;
hence thesis;
end;
theorem
for R be FinSequence of REAL
ex R1 be non-increasing FinSequence of REAL st R,R1 are_fiberwise_equipotent
proof let R be FinSequence of REAL;
A1: for n holds P[n] from Ind(Lm6,Lm7);
len R = len R;
hence thesis by A1;
end;
Lm8:
for n holds for g1,g2 be non-increasing FinSequence of REAL st
n = len g1 & g1,g2 are_fiberwise_equipotent holds g1 = g2
proof
defpred P[Nat] means
for g1,g2 be non-increasing FinSequence of REAL st $1 = len g1 &
g1,g2 are_fiberwise_equipotent holds g1 = g2;
A1: P[0]
proof
let g1,g2 be non-increasing FinSequence of REAL; assume that
A2: len g1 = 0 and
A3: g1,g2 are_fiberwise_equipotent;
len g2 = len g1 by A3,Th16;
then g1 = <*>REAL & g2 = <*>REAL by A2,FINSEQ_1:32;
hence thesis;
end;
A4: for n st P[n] holds P[n+1]
proof let n; assume
A5: P[n];
let g1,g2 be non-increasing FinSequence of REAL; assume that
A6: len g1 = n+1 and
A7: g1,g2 are_fiberwise_equipotent;
A8: len g2 = len g1 by A7,Th16;
then A9: g1.(len g1) = g2.(len g2) & g1|n, g2|n are_fiberwise_equipotent
by A6,A7,Lm5;
n<=len g1 by A6,NAT_1:29;
then A10: len(g1|n) = n & len(g2|n) = n by A8,TOPREAL1:3;
reconsider g1n = g1|n, g2n = g2|n as non-increasing FinSequence of REAL
by Th33;
set r = g1.(n+1);
A11: g1n = g2n by A5,A9,A10;
(g1|n)^<*r*> = g1 & (g2|n)^<*r*> = g2 by A6,A8,A9,Th20;
hence thesis by A11;
end;
thus for n holds P[n] from Ind(A1,A4);
end;
theorem
for R1,R2 be non-increasing FinSequence of REAL st
R1,R2 are_fiberwise_equipotent holds R1 = R2
proof let g1,g2 be non-increasing FinSequence of REAL; assume
A1: g1,g2 are_fiberwise_equipotent;
len g1 = len g1;
hence thesis by A1,Lm8;
end;
theorem
for R be FinSequence of REAL, r,s be Real st r <> 0 holds R"{s/r} = (r*R)"{s}
proof let R be FinSequence of REAL, r,s; assume
A1: r <> 0;
A2: r*R = (r multreal) * R by RVSUM_1:def 7;
A3: Seg len R = dom R & dom(r*R) = Seg len(r*R) by FINSEQ_1:def 3;
thus R"{s/r} c= (r*R)"{s}
proof let x; assume A4: x in R"{s/r};
then reconsider i = x as Nat;
A5: i in dom R & R.i in {s/r} by A4,FUNCT_1:def 13;
then A6: i in
Seg len(r*R) & R.i = s/r by A2,A3,FINSEQ_2:37,TARSKI:def 1;
A7:i in dom (r*R) by A2,A3,A5,FINSEQ_2:37;
r*(R.i) = s by A1,A6,XCMPLX_1:88;
then (r*R).i = s by RVSUM_1:66;
then (r*R).i in {s} by TARSKI:def 1;
hence thesis by A7,FUNCT_1:def 13;
end;
let x; assume A8: x in (r*R)"{s};
then reconsider i = x as Nat;
i in dom(r*R) & (r*R).i in {s} by A8,FUNCT_1:def 13;
then A9: i in dom R & (r*R).i = s by A2,A3,FINSEQ_2:37,TARSKI:def 1;
then r*R.i = s by RVSUM_1:66;
then R.i = s/r by A1,XCMPLX_1:90;
then R.i in {s/r} by TARSKI:def 1;
hence thesis by A9,FUNCT_1:def 13;
end;
theorem
for R be FinSequence of REAL holds (0*R)"{0} = dom R
proof let R be FinSequence of REAL;
0*R = ((0 qua Real) multreal) * R by RVSUM_1:def 7;
then A1: len(0*R) = len R by FINSEQ_2:37;
A2: dom R = Seg len R & Seg len(0*R) = dom(0*R) by FINSEQ_1:def 3;
hence (0*R)"{0} c= dom R by A1,RELAT_1:167;
let x; assume A3: x in dom R;
then reconsider i = x as Nat;
(0*R).i = 0*R.i by RVSUM_1:66
.= 0;
then (0*R).i in {0} by TARSKI:def 1;
hence thesis by A1,A2,A3,FUNCT_1:def 13;
end;