) = Seg len((a|k)^<*q*>) by FINSEQ_1:def 3; A33: dom (a|k) c= dom((a|k)^<*q*>) by FINSEQ_1:26; set ak = a/^k, b = (a|k)^<*q*>^ak; A34: dom (a|k) = Seg len (a|k) by FINSEQ_1:def 3; A35: len(a|k) = k by A29,A28,FINSEQ_1:59,XXREAL_0:2; then A36: len((a|k)^<*q*>) = k+len <*q*> by FINSEQ_1:22 .= k+1 by FINSEQ_1:39; then A37: len b = k+1 + len(a/^k) by FINSEQ_1:22; k+1<=len a by A27,FINSEQ_3:25; then A38: 1<=len(a/^k) by A31,XREAL_1:19; now let m; assume that A39: m in dom b and A40: m+1 in dom b; A41: 1<=m+1 by A40,FINSEQ_3:25; A42: m+1<=len b by A40,FINSEQ_3:25; set r = b.m, s = b.(m+1); A43: 1<=m by A39,FINSEQ_3:25; A44: m<=len b by A39,FINSEQ_3:25; now per cases; case A45: m+1<=k; dom(a|k) c= dom((a|k)^(a/^k)) by FINSEQ_1:26; then A46: dom(a|k) c= dom a by Th8; A47: dom a = Seg len a by FINSEQ_1:def 3; m<=k by A45,NAT_1:13; then A48: m in Seg k by A43,FINSEQ_1:1; 1<=k by A41,A45,XXREAL_0:2; then A49: k in dom a by A30,A47,FINSEQ_1:1; then A50: a.m = (a|k).m by A48,Th6; A51: m+1 in Seg k by A41,A45,FINSEQ_1:1; then A52: a.(m+1) = (a|k).(m+1) by A49,Th6; A53: b.(m+1) = ((a|k)^<*q*>).(m+1) by A35,A34,A33,A51,FINSEQ_1:def 7 .= a.(m+1) by A35,A34,A51,A52,FINSEQ_1:def 7; b.m = ((a|k)^<*q*>).m by A35,A34,A33,A48,FINSEQ_1:def 7 .= a.m by A35,A34,A48,A50,FINSEQ_1:def 7; hence r>=s by A35,A34,A48,A51,A53,A46,Def3; end; case k) by A36,A32,FINSEQ_1:4; then A56: b.(m+1) = ((a|k)^<*q*>).(k+1) by A55,FINSEQ_1:def 7 .= q by A35,FINSEQ_1:42; A57: m in Seg k by A43,A55,FINSEQ_1:1; A58: k in dom a by A9,A30,A43,A55,FINSEQ_1:1; then A59: a.m = (a|k).m by A57,Th6; A60: b.m = ((a|k)^<*q*>).m by A35,A34,A33,A57,FINSEQ_1:def 7 .= a.m by A35,A34,A57,A59,FINSEQ_1:def 7; now assume s>r; then for t be Real st t = a.k holds t =s; end; case k <> m; then k).(k+1) by A36,A32,A71,FINSEQ_1:def 7 .= q by A35,FINSEQ_1:42; A73: 1 in dom(a/^k) by A38,FINSEQ_3:25; b.(m+1) = (a/^k).(k+1+1 - (k+1)) by A36,A42,A62,A71, FINSEQ_1:24 .= a.mi by A30,A73,Def1; hence r>=s by A27,A72; end; case k+1 <> m; then A74: k+1 =s by A68,A78,A77,Def3; end; end; hence r>=s; end; end; hence r>=s; end; end; hence r>=s; end; then reconsider b as non-increasing FinSequence of REAL by Def3,RVSUM_1:145; take b; now let x be object; A79: card Coim(fn,x) = card Coim(a,x) by A7; thus card Coim(b,x) = card (((a|k)^<*q*>)"{x}) + card(ak"{x}) by FINSEQ_3:57 .= card((a|k)"{x}) + card(<*q*>"{x}) + card(ak"{x}) by FINSEQ_3:57 .= card((a|k)"{x}) + card(ak"{x}) + card(<*q*>"{x}) .= card(((a|k)^ak)"{x}) + card(<*q*>"{x}) by FINSEQ_3:57 .= card(fn"{x}) + card(<*q*>"{x}) by A79,Th8 .= card((fn^<*q*>)"{x}) by FINSEQ_3:57 .= card Coim(R,x) by A5,A2,Th7; end; hence R,b are_fiberwise_equipotent; end; end; hence thesis; end; theorem Th22: 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: len R = len R; for n holds P[n] from NAT_1:sch 2(Lm5,Lm6); hence thesis by A1; end; Lm7: 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: for n st P[n] holds P[n+1] proof let n; assume A2: P[n]; let g1,g2 be non-increasing FinSequence of REAL; set r = g1.(n+1); reconsider g1n = g1|n, g2n = g2|n as non-increasing FinSequence of REAL by Th20; assume that A3: len g1 = n+1 and A4: g1,g2 are_fiberwise_equipotent; A5: len g2 = len g1 by A4,Th3; then A6: g1.(len g1) = g2.(len g2) by A3,A4,Lm4; A7: (g1|n)^<*r*> = g1 by A3,Th7; len(g1|n) = n by A3,FINSEQ_1:59,NAT_1:11; then g1n = g2n by A2,A3,A4,A5,Lm4; hence thesis by A3,A5,A6,A7,Th7; end; A8: P[0] proof let g1,g2 be non-increasing FinSequence of REAL; assume len g1 = 0 & g1,g2 are_fiberwise_equipotent; then len g2 = len g1 & g1 = <*>REAL by Th3; hence thesis; end; thus for n holds P[n] from NAT_1:sch 2(A8,A1); 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; A1: len g1 = len g1; assume g1,g2 are_fiberwise_equipotent; hence thesis by A1,Lm7; end; theorem for R be FinSequence of REAL, r,s st r <> 0 holds R"{s/r} = (r *R)"{ s } proof let R be FinSequence of REAL, r,s; A1: Seg len R = dom R & dom(r*R) = Seg len(r*R) by FINSEQ_1:def 3; assume A2: r <> 0; thus R"{s/r} c= (r*R)"{s} proof let x be object; assume A3: x in R"{s/r}; then reconsider i = x as Element of NAT; R.i in {s/r} by A3,FUNCT_1:def 7; then R.i = s/r by TARSKI:def 1; then r*(R.i) = s by A2,XCMPLX_1:87; then (r*R).i = s by RVSUM_1:44; then A4: (r*R).i in {s} by TARSKI:def 1; i in dom R by A3,FUNCT_1:def 7; then i in dom (r*R) by A1,FINSEQ_2:33; hence thesis by A4,FUNCT_1:def 7; end; let x be object; assume A5: x in (r*R)"{s}; then reconsider i = x as Element of NAT; (r*R).i in {s} by A5,FUNCT_1:def 7; then (r*R).i = s by TARSKI:def 1; then r*R.i = s by RVSUM_1:44; then R.i = s/r by A2,XCMPLX_1:89; then A6: R.i in {s/r} by TARSKI:def 1; i in dom(r*R) by A5,FUNCT_1:def 7; then i in dom R by A1,FINSEQ_2:33; hence thesis by A6,FUNCT_1:def 7; end; theorem for R be FinSequence of REAL holds (0*R)"{0} = dom R proof let R be FinSequence of REAL; A1: Seg len(0*R) = dom(0*R) by FINSEQ_1:def 3; A2: len(0*R) = len R & dom R = Seg len R by FINSEQ_1:def 3,FINSEQ_2:33; hence (0*R)"{0} c= dom R by A1,RELAT_1:132; let x be object; assume A3: x in dom R; then reconsider i = x as Element of NAT; (0*R).i = 0*R.i by RVSUM_1:44 .= 0; then (0*R).i in {0} by TARSKI:def 1; hence thesis by A2,A1,A3,FUNCT_1:def 7; end; begin :: Addenda :: from VECTSP_9, 2006.01.06, A.T. reserve f, g for Function; theorem for f, g st rng f = rng g & f is one-to-one & g is one-to-one holds f,g are_fiberwise_equipotent proof let f, g be Function such that A1: rng f = rng g and A2: f is one-to-one and A3: g is one-to-one; let x be object; per cases; suppose A4: x in rng f; then card Coim(f,x) = 1 by A2,FINSEQ_4:73; hence thesis by A1,A3,A4,FINSEQ_4:73; end; suppose A5: not x in rng f; then card(f"{x}) = 0 by CARD_1:27,FUNCT_1:72; hence thesis by A1,A5,CARD_1:27,FUNCT_1:72; end; end; :: from REVROT_1, 2007.03.18, A.T. theorem for f being FinSequence holds f /^ len f = {} proof let f be FinSequence; len (f /^ len f) = len f - len f by Def1 .= 0; hence thesis; end; :: from SCMBSORT, 2007.07.26, A.T. theorem for f,g be Function,m,n be set st f.m=g.n & f.n=g.m & m in dom f & n in dom f & dom f = dom g & (for k be set st k<>m & k<>n & k in dom f holds f.k= g.k) holds f,g are_fiberwise_equipotent proof let f,g be Function,m,n be set; assume that A1: f.m=g.n and A2: f.n=g.m and A3: m in dom f and A4: n in dom f and A5: dom f = dom g and A6: for k be set st k<>m & k<>n & k in dom f holds f.k=g.k; set t=id dom f, nm=n .--> m,mn=m .--> n, p=t +* nm +* mn; A7: dom nm ={ n } by FUNCOP_1:13; A8: dom t = dom f; A9: rng t = dom (t") by FUNCT_1:33 .= dom f by A8,FUNCT_1:45; dom mn ={ m } by FUNCOP_1:13; then A10: dom p = dom (t +* nm) \/ {m} by FUNCT_4:def 1 .= dom t \/ {n} \/ {m} by A7,FUNCT_4:def 1 .= dom f \/ {n} \/ {m} .= dom f \/ {m} by A4,ZFMISC_1:40 .= dom f by A3,ZFMISC_1:40; A11: now let x be object; assume A12: x in dom f; then A13: (p*p).x=p.(p.x) by A10,FUNCT_1:13; per cases; suppose A14: x=m; hence (p*p).x=p.n by A13,FUNCT_4:89 .=x by A14,FUNCT_4:90; end; suppose A15: x<>m; now per cases; suppose A16: x=n; hence (p*p).x=p.m by A13,FUNCT_4:90 .=x by A16,FUNCT_4:89; end; suppose A17: x<>n; hence (p*p).x=p.(t.x) by A13,A15,FUNCT_4:91 .=p.x by A12,FUNCT_1:17 .=t.x by A15,A17,FUNCT_4:91 .=x by A12,FUNCT_1:17; end; end; hence (p*p).x=x; end; end; rng nm ={m} by FUNCOP_1:8; then rng t \/ rng nm =dom f by A3,ZFMISC_1:40; then A18: rng(t +* nm) \/ rng mn c= dom f \/ rng mn by FUNCT_4:17,XBOOLE_1:9; for z be object st z in rng(p*p) holds z in rng p by FUNCT_1:14; then A19: rng(p*p) c= rng p; A20: rng p c= rng(t +* nm) \/ rng mn by FUNCT_4:17; A21: rng mn ={n} by FUNCOP_1:8; then dom f \/ rng mn =dom p by A4,A10,ZFMISC_1:40; then A22: dom (p*p) =dom f by A10,A18,A20,RELAT_1:27,XBOOLE_1:1; then p*p=t by A11,FUNCT_1:17; then A23: p is one-to-one by A10,FUNCT_1:31; rng p c= dom f \/ rng mn by A18,A20; then A24: rng p c= dom p by A4,A10,A21,ZFMISC_1:40; then A25: dom (g*p) =dom f by A5,A10,RELAT_1:27; now let x be object; assume A26: x in dom f; then A27: (g*p).x=g.(p.x) by A25,FUNCT_1:12; per cases; suppose x=m; hence (g*p).x=f.x by A1,A27,FUNCT_4:89; end; suppose A28: x<>m; now per cases; suppose x=n; hence (g*p).x=f.x by A2,A27,FUNCT_4:90; end; suppose A29: x<>n; hence (g*p).x=g.(t.x) by A27,A28,FUNCT_4:91 .=g.x by A26,FUNCT_1:17 .=f.x by A6,A26,A28,A29; end; end; hence (g*p).x=f.x; end; end; then A30: f=g*p by A25,FUNCT_1:2; rng(p*p)=dom f by A9,A22,A11,FUNCT_1:17; then rng p = dom g by A5,A10,A24,A19; hence thesis by A10,A23,A30,CLASSES1:77; end; :: form BINARITH, 2008.08.20, A.T. theorem for f being FinSequence, k being Nat holds len (f/^k)=len f-'k proof let f be FinSequence,k be Nat; per cases; suppose A1: k<=len f; then len f-'k=len f-k by XREAL_1:233; hence thesis by A1,Def1; end; suppose A2: k>len f; then (f/^k)={} by Def1; then A3: len (f/^k)=0; len f-k<0 by A2,XREAL_1:49; hence thesis by A3,XREAL_0:def 2; end; end; :: from SCPQSORT, 2008.10.12, A.T. theorem Th30: :: RFINSEQ:17 for f,g be FinSequence,x be set st x in dom g & f,g are_fiberwise_equipotent holds ex y be set st y in dom g & f.x=g.y proof let f,g be FinSequence,x be set; assume that A1: x in dom g and A2: f,g are_fiberwise_equipotent; consider P be Permutation of dom g such that A3: f = g*P by A2,Th4; take y=P.x; thus y in dom g by A1,FUNCT_2:5; thus thesis by A1,A3,FUNCT_2:15; end; theorem Th31: for f,g,h be FinSequence holds f,g are_fiberwise_equipotent iff h^f, h^g are_fiberwise_equipotent proof let f,g,h be FinSequence; thus f,g are_fiberwise_equipotent implies h^f, h^g are_fiberwise_equipotent proof assume A1: f,g are_fiberwise_equipotent; now let y be object; card Coim(f,y) = card Coim(g,y) by A1; hence card Coim(h^f,y) = card(g"{y}) + card(h"{y}) by FINSEQ_3:57 .= card Coim(h^g,y) by FINSEQ_3:57; end; hence thesis; end; assume A2: h^f,h^g are_fiberwise_equipotent; now let x be object; A3: card Coim(h^f,x) = card Coim(f,x)+card(h"{x}) & card((h^g)"{x}) = card(g"{x} )+card(h"{x}) by FINSEQ_3:57; card Coim(h^f,x) = card Coim(h^g,x) by A2; hence card Coim(f,x) = card Coim(g,x) by A3; end; hence thesis; end; theorem for f,g be FinSequence,m,n,j be Nat st f,g are_fiberwise_equipotent & m<=n & n <= len f & (for i be Nat st 1<=i & i<=m holds f.i=g.i) & (for i be Nat st n m by XREAL_1:29; len s2=m+m2 by A5; then consider p2,q2 be FinSequence such that A21: len p2 = m and A22: len q2 = m2 and A23: s2 = p2^q2 by FINSEQ_2:22; A24: Seg m = dom p2 by A21,FINSEQ_1:def 3; len s1=m+m2 by A9; then consider p1,q1 be FinSequence such that A25: len p1 = m and A26: len q1 = m2 and A27: s1 = p1^q1 by FINSEQ_2:22; A28: f=p1^(q1^r1) by A11,A27,FINSEQ_1:32; A29: dom p1 = Seg m by A25,FINSEQ_1:def 3; A30: g=p2^(q2^r2) by A7,A23,FINSEQ_1:32; now let i be Nat; reconsider a = i as Nat; assume A31: i in dom p1; then A32: 1<= i & i <= m by A29,FINSEQ_1:1; thus p1.i=f.i by A28,A31,FINSEQ_1:def 7 .=g.a by A4,A32 .=p2.i by A30,A24,A29,A31,FINSEQ_1:def 7; end; then p1=p2 by A25,A21,FINSEQ_2:9; then A33: q1,q2 are_fiberwise_equipotent by A27,A23,A19,Th31; assume that A34: m0 by A34,A25,XREAL_1:50; then reconsider x=j-len p1 as Element of NAT by INT_1:3; A36: x <= n-len p1 by A35,XREAL_1:9; A37: Seg m2 = dom q2 by A22,FINSEQ_1:def 3; A38: 1+ 0<= x by A34,A25,INT_1:7,XREAL_1:50; then x in dom q2 by A25,A37,A36,FINSEQ_1:1; then consider y be set such that A39: y in dom q2 and A40: q1.x=q2.y by A33,Th30; reconsider y as Nat by A39; A41: len p2 + y in dom s2 by A23,A39,FINSEQ_1:28; reconsider k=len p2+y as Nat; take k; 1<=y by A37,A39,FINSEQ_1:1; then k>=len p2+1 by XREAL_1:6; hence m