### The Mizar article:

### Properties of Partial Functions from a Domain to the Set of Real Numbers

**by****Jaroslaw Kotowicz, and****Yuji Sakai**

- Received March 15, 1993
Copyright (c) 1993 Association of Mizar Users

- MML identifier: RFUNCT_3
- [ MML identifier index ]

environ vocabulary SQUARE_1, ARYTM, ARYTM_1, ABSVALUE, FINSEQ_1, RELAT_1, FUNCT_1, BOOLE, PARTFUN1, ARYTM_3, SEQ_1, RFINSEQ, CARD_1, FUNCOP_1, BINOP_1, SUBSET_1, SETWISEO, RLVECT_1, FUNCT_3, TDGROUP, LIMFUNC1, FINSET_1, RCOMP_1, PROB_1, FINSEQ_2, RVSUM_1, VECTSP_1, RFUNCT_3; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, RELAT_1, FUNCT_1, FINSEQ_1, BINOP_1, CARD_1, REAL_1, NAT_1, ABSVALUE, FUNCOP_1, SETWISEO, FINSEQ_2, SQUARE_1, RELSET_1, PARTFUN1, FINSEQOP, SEQ_1, RFUNCT_1, FINSEQ_4, SETWOP_2, FINSET_1, RVSUM_1, RCOMP_1, PARTFUN2, LIMFUNC1, TOPREAL1, RFINSEQ; constructors MONOID_1, PROB_1, REAL_1, NAT_1, SETWISEO, FINSEQOP, RFUNCT_1, RCOMP_1, PARTFUN2, LIMFUNC1, TOPREAL1, RFINSEQ, FINSOP_1, FINSEQ_4, SEQ_1, SEQ_4, MEMBERED, XBOOLE_0; clusters FINSET_1, RFINSEQ, PRELAMB, RELSET_1, FINSEQ_2, XREAL_0, PARTFUN1, MONOID_1, NAT_1, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2, FINSEQ_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, BINOP_1, SETWISEO, RFINSEQ, XBOOLE_0; theorems FINSEQ_1, FINSEQ_2, REAL_1, REAL_2, NAT_1, FUNCT_1, AXIOMS, CARD_2, TARSKI, CARD_1, FINSET_1, LIMFUNC1, PARTFUN1, RCOMP_1, SQUARE_1, BINOP_1, FINSEQ_3, FUNCOP_1, RFUNCT_1, TOPREAL1, ZFMISC_1, SUBSET_1, RVSUM_1, ABSVALUE, RFINSEQ, AMI_1, RELAT_1, SEQ_1, FINSOP_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1; schemes NAT_1, FINSEQ_1, SEQ_1, MATRIX_2, BINOP_1; begin reserve n,m for Nat, r,s for Real, x,y for set; :: :: Nonnegative and Nonpositive Part of a Real Number :: definition let n,m be Nat; redefine func min(n,m)->Nat; coherence by FINSEQ_2:1; end; definition let r be real number; func max+ (r) -> Real equals :Def1: max(r,0); correctness by XREAL_0:def 1; func max- (r) -> Real equals :Def2: max(-r,0); correctness by XREAL_0:def 1; end; theorem Th1: for r be real number holds r = max+(r) - max-(r) proof let r be real number; now per cases; case A1: 0<=r; A2: max+(r) =max(0,r) by Def1 .= r by A1,SQUARE_1:def 2; A3: -r<=0 by A1,REAL_1:26,50; max-(r) = max(-r,0) by Def2 .= 0 by A3,SQUARE_1:def 2; hence thesis by A2; case A4: r<0; A5: max+(r) = max(r,0) by Def1 .= 0 by A4,SQUARE_1:def 2; A6: 0<-r by A4,REAL_1:66; A7: max-(r) = max(-r,0) by Def2 .= -r by A6,SQUARE_1:def 2; thus r = 0+-(-r) .= max+(r) - max-(r) by A5,A7,XCMPLX_0:def 8; end; hence thesis; end; theorem Th2: for r be real number holds abs(r) = max+(r) + max-(r) proof let r be real number; now per cases; case A1: 0<=r; A2: max+(r) =max(0,r) by Def1 .= r by A1,SQUARE_1:def 2; A3: -r<=0 by A1,REAL_1:26,50; max-(r) = max(-r,0) by Def2 .= 0 by A3,SQUARE_1:def 2; hence thesis by A1,A2,ABSVALUE:def 1; case A4: r<0; A5: max+(r) = max(r,0) by Def1 .= 0 by A4,SQUARE_1:def 2; A6: 0<-r by A4,REAL_1:66; max-(r) = max(-r,0) by Def2 .= -r by A6,SQUARE_1:def 2; hence abs(r) = max+(r) + max-(r) by A4,A5,ABSVALUE:def 1; end; hence thesis; end; theorem Th3: for r be real number holds 2*max+(r) = r + abs(r) proof let r be real number; thus r + abs(r) = max+(r) - max-(r) + abs(r) by Th1 .= max+(r) - max-(r) + (max+(r) + max-(r)) by Th2 .= 1*max+(r) + max+(r) by XCMPLX_1:28 .= (1+1)*max+(r) by XCMPLX_1:8 .= 2*max+(r); end; theorem Th4: for r,s be real number st 0<=r holds max+(r*s) = r*(max+ s) proof let r,s be real number; assume A1: 0<=r; A2: max+(r*s) = max(r*s,0) & max+ s = max(s,0) by Def1; now per cases; case A3: 0<=s; then 0<=r*s by A1,SQUARE_1:19; then max+(r*s) = r*s & r*(max+ s) = r*s by A2,A3,SQUARE_1:def 2; hence thesis; case A4: s<0; then A5: max+ s= 0 by A2,SQUARE_1:def 2; r*s<=0 by A1,A4,REAL_2:123; hence max+(r*s) = r*(max+ s) by A2,A5,SQUARE_1:def 2; end; hence thesis; end; theorem Th5: for r,s be real number holds max+(r+s) <= max+(r) + max+(s) proof let r,s be real number; A1: max+(r+s) = max(r+s,0) by Def1; A2: r<=max(r,0) & s<=max(s,0) & 0<=max(r,0) & 0<=max(s,0) by SQUARE_1:46; now per cases; case 0<=r+s; then max+(r+s) = r+s by A1,SQUARE_1:def 2; then max+(r+s)<= max(r,0) + max(s,0) by A2,REAL_1:55; then max+(r+s)<= max+(r) + max(s,0) by Def1; hence thesis by Def1; case r+s<0; then max+(r+s) = 0+0 by A1,SQUARE_1:def 2; then max+(r+s)<= max(r,0) + max(s,0) by A2,REAL_1:55; then max+(r+s)<= max+(r) + max(s,0) by Def1; hence thesis by Def1; end; hence thesis; end; theorem for r be real number holds 0 <= max+(r) & 0 <=max-(r) proof let r be real number; max+(r) = max(r,0) & max-(r) = max(-r,0) by Def1,Def2; hence thesis by SQUARE_1:46; end; theorem Th7: for r1,r2, s1,s2 be real number st r1<=s1 & r2<=s2 holds max(r1,r2) <= max(s1,s2) proof let r1,r2, s1,s2 be real number; assume A1: r1<=s1 & r2<=s2; s1<=max(s1,s2) & s2<=max(s1,s2) by SQUARE_1:46; then r1<=max(s1,s2) & r2<=max(s1,s2) by A1,AXIOMS:22; hence thesis by SQUARE_1:50; end; Lm1: 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; Lm2: for f be Function,x be set st not x in rng f holds f"{x}={} proof let f be Function,x be set; assume A1: not x in rng f; rng f misses {x} proof assume A2: rng f /\ {x} <> {}; consider y being Element of rng f /\ {x}; y in rng f & y in {x} by A2,XBOOLE_0:def 3; hence contradiction by A1,TARSKI:def 1; end; hence thesis by RELAT_1:173; end; begin :: :: Partial Functions from a Domain to the Set of Real Numbers :: theorem Th8: for D be non empty set, F be PartFunc of D,REAL, r,s be real number st r <> 0 holds F"{s/r} = (r(#)F)"{s} proof let D be non empty set, F be PartFunc of D,REAL, r,s be real number; assume A1: r <> 0; thus F"{s/r} c= (r(#)F)"{s} proof let x; assume A2: x in F"{s/r}; then reconsider d=x as Element of D; d in dom F & F.d in {s/r} by A2,FUNCT_1:def 13; then A3: d in dom(r(#)F) & F.d = s/r by SEQ_1:def 6,TARSKI:def 1; then r*F.d = s by A1,XCMPLX_1:88; then (r(#)F).d = s by A3,SEQ_1:def 6; then (r(#)F).d in {s} by TARSKI:def 1; hence thesis by A3,FUNCT_1:def 13; end; let x; assume A4: x in (r(#)F)"{s}; then reconsider d=x as Element of D; A5: d in dom(r(#)F) & (r(#)F).d in {s} by A4,FUNCT_1:def 13; then A6: d in dom F & (r(#)F).d = s by SEQ_1:def 6,TARSKI:def 1; then r*F.d = s by A5,SEQ_1:def 6; then F.d = s/r by A1,XCMPLX_1:90; then F.d in {s/r} by TARSKI:def 1; hence thesis by A6,FUNCT_1:def 13; end; theorem Th9: for D be non empty set, F be PartFunc of D,REAL holds (0(#)F)"{0} = dom F proof let D be non empty set, F be PartFunc of D,REAL; thus (0(#)F)"{0} c= dom F proof let x; assume A1: x in (0(#)F)"{0}; then reconsider d=x as Element of D; d in dom(0(#)F) & (0(#)F).d in {0} by A1,FUNCT_1:def 13; hence thesis by SEQ_1:def 6; end; let x; assume A2: x in dom F; then reconsider d=x as Element of D; A3: d in dom(0(#)F) by A2,SEQ_1:def 6; then (0(#)F).d = 0*(F.d) by SEQ_1:def 6 .= 0; then (0(#)F).d in {0} by TARSKI:def 1; hence thesis by A3,FUNCT_1:def 13; end; theorem Th10: for D be non empty set, F be PartFunc of D,REAL, r be Real st 0<r holds abs(F)"{r} = F"{-r,r} proof let D be non empty set, F be PartFunc of D,REAL, r; assume A1: 0<r; A2: dom abs(F) = dom F by SEQ_1:def 10; thus abs(F)"{r} c= F"{-r,r} proof let x; assume A3: x in abs(F)"{r}; then reconsider rr = x as Element of D; A4: rr in dom abs(F) & abs(F).rr in {r} by A3,FUNCT_1:def 13; then abs(F.rr) in {r} by SEQ_1:def 10; then A5: abs(F.rr) = r by TARSKI:def 1; now per cases; case 0<=F.rr; then F.rr = r by A5,ABSVALUE:def 1; then F.rr in {-r,r} by TARSKI:def 2; hence thesis by A2,A4,FUNCT_1:def 13; case F.rr<0; then -F.rr = r by A5,ABSVALUE:def 1; then F.rr in {-r,r} by TARSKI:def 2; hence thesis by A2,A4,FUNCT_1:def 13; end; hence thesis; end; let x; assume A6: x in F"{-r,r}; then reconsider rr = x as Element of D; A7: rr in dom F & F.rr in {-r,r} by A6,FUNCT_1:def 13; now per cases by A7,TARSKI:def 2; case F.rr = -r; then r = abs(-F.rr) by A1,ABSVALUE:def 1 .= abs(F.rr) by ABSVALUE:17 .= abs(F).rr by A2,A7,SEQ_1:def 10; then abs(F).rr in {r} by TARSKI:def 1; hence thesis by A2,A7,FUNCT_1:def 13; case F.rr = r; then r = abs(F.rr) by A1,ABSVALUE:def 1 .= abs(F).rr by A2,A7,SEQ_1:def 10; then abs(F).rr in {r} by TARSKI:def 1; hence thesis by A2,A7,FUNCT_1:def 13; end; hence thesis; end; theorem Th11: for D be non empty set, F be PartFunc of D,REAL holds abs(F)"{0} = F"{0} proof let D be non empty set, F be PartFunc of D,REAL; A1: dom abs(F) = dom F by SEQ_1:def 10; thus abs(F)"{0} c= F"{0} proof let x; assume A2: x in abs(F)"{0}; then reconsider r=x as Element of D; A3: r in dom abs(F) & abs(F).r in {0} by A2,FUNCT_1:def 13; then abs(F.r) in {0} by SEQ_1:def 10; then abs(F.r) = 0 by TARSKI:def 1; then F.r = 0 by ABSVALUE:7; then F.r in {0} by TARSKI:def 1; hence thesis by A1,A3,FUNCT_1:def 13; end; let x; assume A4: x in F"{0}; then reconsider r=x as Element of D; A5: r in dom F & F.r in {0} by A4,FUNCT_1:def 13; then F.r = 0 by TARSKI:def 1; then abs(F.r) = 0 by ABSVALUE:7; then abs(F).r = 0 by A1,A5,SEQ_1:def 10; then abs(F).r in {0} by TARSKI:def 1; hence thesis by A1,A5,FUNCT_1:def 13; end; theorem Th12: for D be non empty set, F be PartFunc of D,REAL, r be Real st r<0 holds abs(F)"{r} = {} proof let D be non empty set, F be PartFunc of D,REAL, r; assume A1: r<0; assume A2: abs(F)"{r} <> {}; consider x being Element of abs(F)"{r}; reconsider x as Element of D by A2,TARSKI:def 3; x in dom abs(F) & abs(F).x in {r} by A2,FUNCT_1:def 13; then abs(F.x) in {r} by SEQ_1:def 10; then abs(F.x) = r by TARSKI:def 1; hence contradiction by A1,ABSVALUE:5; end; theorem Th13: for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL, r be Real st r <> 0 holds F,G are_fiberwise_equipotent iff r(#)F, r(#)G are_fiberwise_equipotent proof let D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL, r; assume A1: r <> 0; A2: rng F c= REAL & rng G c= REAL & rng(r(#)F) c= REAL & rng(r(#)G) c= REAL; thus F,G are_fiberwise_equipotent implies r(#)F, r(#) G are_fiberwise_equipotent proof assume A3: F,G are_fiberwise_equipotent; now let x be Real; F"{x/r} = (r(#)F)"{x} & G"{x/r} = (r(#)G)"{x} by A1,Th8; hence Card((r(#)F)"{x}) = Card((r(#)G)"{x}) by A3,RFINSEQ:def 1; end; hence thesis by A2,RFINSEQ:5; end; assume A4: r(#)F, r(#)G are_fiberwise_equipotent; now let x be Real; A5: r*x/r = x by A1,XCMPLX_1:90; F"{r*x/r} = (r(#)F)"{r*x} & G"{r*x/r} = (r(#)G)"{r*x} by A1,Th8; hence Card(F"{x}) = Card(G"{x}) by A4,A5,RFINSEQ:def 1; end; hence thesis by A2,RFINSEQ:5; end; theorem for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL holds F,G are_fiberwise_equipotent iff -F, -G are_fiberwise_equipotent proof let D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL; -F = (-1)(#)F & -G = (-1)(#)G by RFUNCT_1:38; hence thesis by Th13; end; theorem for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL st F,G are_fiberwise_equipotent holds abs(F), abs(G) are_fiberwise_equipotent proof let D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL; assume A1: F,G are_fiberwise_equipotent; A2: rng abs(F) c= REAL & rng abs(G) c= REAL; now let r be Real; now per cases; case 0<r; then abs(F)"{r} = F"{-r,r} & abs(G)"{r} = G"{-r,r} by Th10; hence Card(abs(F)"{r}) = Card(abs(G)"{r}) by A1,RFINSEQ:4; case 0=r; then abs(F)"{r} = F"{r} & abs(G)"{r} = G"{r} by Th11; hence Card(abs(F)"{r}) = Card(abs(G)"{r}) by A1,RFINSEQ:4; case r<0; then abs(F)"{r} = {} & abs(G)"{r} = {} by Th12; hence Card(abs(F)"{r}) = Card(abs(G)"{r}); end; hence Card(abs(F)"{r}) = Card(abs(G)"{r}); end; hence thesis by A2,RFINSEQ:5; end; definition let X,Y be set; mode PartFunc-set of X,Y means :Def3: for x being Element of it holds x is PartFunc of X,Y; existence proof reconsider h={} as PartFunc of X,Y by PARTFUN1:56; take {h}; thus thesis by TARSKI:def 1; end; end; definition let X,Y be set; cluster non empty PartFunc-set of X,Y; existence proof reconsider h={} as PartFunc of X,Y by PARTFUN1:56; {h} is PartFunc-set of X,Y proof let x be Element of {h}; thus thesis by TARSKI:def 1; end; hence thesis; end; end; definition let X,Y be set; mode PFUNC_DOMAIN of X,Y is non empty PartFunc-set of X,Y; end; definition let X,Y be set; redefine func PFuncs(X,Y) -> PartFunc-set of X,Y; coherence proof for x be Element of PFuncs(X,Y) holds x is PartFunc of X,Y by PARTFUN1:121 ; hence thesis by Def3; end; let P be non empty PartFunc-set of X,Y; mode Element of P -> PartFunc of X,Y; coherence by Def3; end; definition let D,C be non empty set, X be Subset of D, c be Element of C; redefine func X --> c -> Element of PFuncs(D,C); coherence proof X --> c is PartFunc of D,C; hence thesis by PARTFUN1:119; end; end; definition let D be non empty set, F1,F2 be Element of PFuncs(D,REAL); redefine func F1+F2 -> Element of PFuncs(D,REAL); coherence by PARTFUN1:119; func F1-F2 -> Element of PFuncs(D,REAL); coherence by PARTFUN1:119; func F1(#)F2 -> Element of PFuncs(D,REAL); coherence by PARTFUN1:119; func F1/F2 -> Element of PFuncs(D,REAL); coherence by PARTFUN1:119; end; definition let D be non empty set, F be Element of PFuncs(D,REAL); redefine func abs(F) -> Element of PFuncs(D,REAL); coherence by PARTFUN1:119; func - F -> Element of PFuncs(D,REAL); coherence by PARTFUN1:119; func F^ -> Element of PFuncs(D,REAL); coherence by PARTFUN1:119; end; definition let D be non empty set, F be Element of PFuncs(D,REAL), r be real number; redefine func r(#)F -> Element of PFuncs(D,REAL); coherence by PARTFUN1:119; end; definition let D be non empty set; func addpfunc(D) -> BinOp of PFuncs(D,REAL) means :Def4: for F1,F2 be Element of PFuncs(D,REAL) holds it.(F1,F2) = F1 + F2; existence proof deffunc O(Element of PFuncs(D,REAL),Element of PFuncs(D,REAL))= $1 + $2; ex o being BinOp of PFuncs(D,REAL) st for a,b being Element of PFuncs(D,REAL) holds o.(a,b) = O(a,b) from BinOpLambda; hence thesis; end; uniqueness proof let o1,o2 be BinOp of PFuncs(D,REAL); assume that A1: for f1,f2 be Element of PFuncs(D,REAL) holds o1.(f1,f2) = f1 + f2 and A2: for f1,f2 be Element of PFuncs(D,REAL) holds o2.(f1,f2) = f1 + f2; now let f1,f2 be Element of PFuncs(D,REAL); o1.(f1,f2) = f1 + f2 & o2.(f1,f2) = f1 + f2 by A1,A2; hence o1.(f1,f2)=o2.(f1,f2); end; hence thesis by BINOP_1:2; end; end; theorem Th16: for D be non empty set holds addpfunc(D) is commutative proof let D be non empty set; let F1,F2 be Element of PFuncs(D,REAL); set o=addpfunc(D); thus o.(F1,F2) = F2+F1 by Def4 .= o.(F2,F1) by Def4; end; theorem Th17: for D be non empty set holds addpfunc(D) is associative proof let D be non empty set; let F1,F2,F3 be Element of PFuncs(D,REAL); set o=addpfunc(D); thus o.(F1,o.(F2,F3)) = o.(F1,F2+F3) by Def4 .= F1+(F2+F3) by Def4 .= F1+F2+F3 by RFUNCT_1:19 .= o.(F1,F2) + F3 by Def4 .= o.(o.(F1,F2),F3) by Def4; end; theorem Th18: for D be non empty set holds [#](D) --> (0 qua Real) is_a_unity_wrt addpfunc(D) proof let D be non empty set; set F = [#](D) --> (0 qua Real); A1: [#](D) = D by SUBSET_1:def 4; then A2: dom F = D by FUNCOP_1:19; A3: addpfunc(D) is commutative by Th16; now let G be Element of PFuncs(D,REAL); dom G /\ D = dom G by XBOOLE_1:28; then A4: dom(G+F) = dom G by A2,SEQ_1:def 3; now let d be Element of D; assume d in dom(G+F); hence (G+F).d = G.d+F.d by SEQ_1:def 3 .= G.d + 0 by A1,FUNCOP_1:13 .= G.d; end; then G+F = G by A4,PARTFUN1:34; hence addpfunc(D).(G,F) = G by Def4; end; hence thesis by A3,BINOP_1:13; end; theorem Th19: for D be non empty set holds the_unity_wrt addpfunc(D) = [#](D) --> (0 qua Real) proof let D be non empty set; [#](D) --> (0 qua Real) is_a_unity_wrt addpfunc(D) by Th18; hence thesis by BINOP_1:def 8; end; theorem Th20: for D be non empty set holds addpfunc(D) has_a_unity proof let D be non empty set; take [#](D) --> (0 qua Real); thus thesis by Th18; end; definition let D be non empty set, f be FinSequence of PFuncs(D,REAL); func Sum(f) -> Element of PFuncs(D,REAL) equals :Def5: (addpfunc(D)) $$ f; correctness; end; theorem Th21: for D be non empty set holds Sum(<*> PFuncs(D,REAL) ) = [#](D)-->(0 qua Real) proof let D be non empty set; set f=<*> PFuncs(D,REAL), o = addpfunc(D), o0 = [#](D) --> (0 qua Real); A1: o is commutative & o is associative & the_unity_wrt o = o0 & o has_a_unity by Th16,Th17,Th19,Th20; thus Sum f = addpfunc(D) $$ f by Def5 .= o0 by A1,FINSOP_1:11; end; theorem Th22: for D be non empty set, G be Element of PFuncs(D,REAL) holds Sum <*G*> = G proof let D be non empty set, G be Element of PFuncs(D,REAL); thus Sum <*G*> = addpfunc(D) $$ (<*G*>) by Def5 .= G by FINSOP_1:12; end; theorem Th23: for D be non empty set, f be FinSequence of PFuncs(D,REAL), G be Element of PFuncs(D,REAL) holds Sum(f^<*G*>) = Sum f + G proof let D be non empty set, f be FinSequence of PFuncs(D,REAL), G be Element of PFuncs(D,REAL); set o = addpfunc(D); A1: o is commutative & o is associative & o has_a_unity by Th16,Th17,Th20; thus Sum(f^<*G*>) = o $$ (f^<*G*>) by Def5 .= o.(o $$ f,G) by A1,FINSOP_1:5 .= o.(Sum f,G) by Def5 .= Sum f + G by Def4; end; theorem Th24: for D be non empty set, f1,f2 be FinSequence of PFuncs(D,REAL) holds Sum(f1^f2) = Sum f1 + Sum f2 proof let D be non empty set, f1,f2 be FinSequence of PFuncs(D,REAL); set o = addpfunc(D); A1: o is commutative & o is associative & o has_a_unity by Th16,Th17,Th20; thus Sum(f1^f2)= addpfunc(D) $$ (f1^f2) by Def5 .= addpfunc(D).(addpfunc(D) $$ f1,addpfunc(D) $$ f2) by A1,FINSOP_1:6 .= addpfunc(D).(Sum f1,addpfunc(D) $$ f2) by Def5 .= addpfunc(D).(Sum f1,Sum f2) by Def5 .= Sum f1 + Sum f2 by Def4; end; theorem for D be non empty set, f be FinSequence of PFuncs(D,REAL), G be Element of PFuncs(D,REAL) holds Sum(<*G*>^f) = G + Sum f proof let D be non empty set, f be FinSequence of PFuncs(D,REAL), G be Element of PFuncs(D,REAL); thus Sum(<*G*>^f) = Sum <*G*> + Sum f by Th24 .= G + Sum f by Th22; end; theorem Th26: for D be non empty set, G1,G2 be Element of PFuncs(D,REAL) holds Sum<*G1,G2*> = G1 + G2 proof let D be non empty set, G1,G2 be Element of PFuncs(D,REAL); thus Sum<*G1,G2*> = Sum(<*G1*>^<*G2*>) by FINSEQ_1:def 9 .= Sum<*G1*> + G2 by Th23 .= G1 + G2 by Th22; end; theorem for D be non empty set, G1,G2,G3 be Element of PFuncs(D,REAL) holds Sum<*G1,G2,G3*> = G1 + G2 + G3 proof let D be non empty set, G1,G2,G3 be Element of PFuncs(D,REAL); thus Sum<*G1,G2,G3*> = Sum(<*G1,G2*>^<*G3*>) by FINSEQ_1:60 .= Sum<*G1,G2*> + G3 by Th23 .= G1 + G2 + G3 by Th26; end; theorem for D be non empty set, f,g be FinSequence of PFuncs(D,REAL) st f,g are_fiberwise_equipotent holds Sum f = Sum g proof let D be non empty set; defpred P[Nat] means for f,g be FinSequence of PFuncs(D,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 PFuncs(D,REAL); assume f,g are_fiberwise_equipotent & len f = 0; then len g = 0 & f =<*>PFuncs(D,REAL) by FINSEQ_1:32,RFINSEQ:16; 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 PFuncs(D,REAL); assume A4: f,g are_fiberwise_equipotent & len f = n+1; then A5: rng f = rng g & len f = len g by RFINSEQ:1,16; 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; then reconsider a=f.(n+1) as Element of PFuncs(D,REAL) by FINSEQ_2:13; 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 RFINSEQ:21; 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,RFINSEQ:19; then A12: gm = (gm|m1) ^ <*a*> by A10,A11,RFINSEQ:20; 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,RFINSEQ:20; now let x; card(f"{x}) = card(g"{x}) by A4,RFINSEQ:def 1; 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 RFINSEQ:def 1; then Sum fn = Sum((g|m1)^gg) by A3,A15; hence Sum f = Sum((g|m1)^gg) + Sum <*a*> by A16,Th24 .= Sum(g|m1) + Sum gg+ Sum <*a*> by Th24 .= Sum(g|m1)+ Sum <*a*> + Sum gg by RFUNCT_1:19 .= Sum gm + Sum gg by A12,A14,Th24 .= Sum g by A8,Th24; end; A17: for n holds P[n] from Ind(A1,A2); let f,g be FinSequence of PFuncs(D,REAL); assume A18: f,g are_fiberwise_equipotent; len f = len f; hence Sum f = Sum g by A17,A18; end; definition let D be non empty set, f be FinSequence; func CHI(f,D) -> FinSequence of PFuncs(D,REAL) means :Def6: len it = len f & for n st n in dom it holds it.n = chi(f.n,D); existence proof deffunc F(Nat)= chi(f.$1,D); consider p be FinSequence such that A1: len p = len f and A2: for n st n in Seg len f holds p.n = F(n) from SeqLambda; rng p c= PFuncs(D,REAL) proof let x be set; assume x in rng p; then consider n such that A3: n in dom p & p.n = x by FINSEQ_2:11; n in Seg len f by A1,A3,FINSEQ_1:def 3; then x = chi(f.n,D) by A2,A3; hence x in PFuncs(D,REAL) by PARTFUN1:119; end; then reconsider p as FinSequence of PFuncs(D,REAL) by FINSEQ_1:def 4; take p; thus len p = len f by A1; let n; assume n in dom p; then n in Seg len f by A1,FINSEQ_1:def 3; hence p.n = chi(f.n,D) by A2; end; uniqueness proof let p1,p2 be FinSequence of PFuncs(D,REAL); assume that A4: len p1 = len f & for n st n in dom p1 holds p1.n = chi(f.n,D) and A5: len p2 = len f & for n st n in dom p2 holds p2.n = chi(f.n,D); now let n; A6: dom p1 = Seg len p1 & dom p2 = Seg len p2 by FINSEQ_1:def 3; assume n in Seg len p1; then p1.n = chi(f.n,D) & p2.n = chi(f.n,D) by A4,A5,A6; hence p1.n = p2.n; end; hence thesis by A4,A5,FINSEQ_2:10; end; end; definition let D be non empty set, f be FinSequence of PFuncs(D,REAL), R be FinSequence of REAL; func R (#) f -> FinSequence of PFuncs(D,REAL) means :Def7: len it = min(len R,len f) & for n st n in dom it for F be PartFunc of D,REAL, r st r = R.n & F = f.n holds it.n = r(#)F; existence proof set m = min(len R,len f); defpred P[Nat,set] means for F be PartFunc of D,REAL, r st r=R.$1 & F = f.$1 holds $2 = r(#)F; A1: m<=len R & m<=len f by SQUARE_1:35; A2: for n st n in Seg m ex x being Element of PFuncs(D,REAL) st P[n,x] proof let n; assume n in Seg m; then A3: 1<=n & n<=m by FINSEQ_1:3; then n<=len R & n<=len f by A1,AXIOMS:22; then n in dom R & n in dom f by A3,FINSEQ_3:27; then reconsider F=f.n as Element of PFuncs(D,REAL) by FINSEQ_2:13; reconsider r=R.n as Real; reconsider a= r(#)F as Element of PFuncs(D,REAL); take a; thus P[n,a]; end; consider p be FinSequence of PFuncs(D,REAL) such that A4: dom p = Seg m & for n st n in Seg m holds P[n,p.n] from SeqDEx(A2); take p; thus len p = m by A4,FINSEQ_1:def 3; let n; assume n in dom p; hence P[n,p.n] by A4; end; uniqueness proof let p1,p2 be FinSequence of PFuncs(D,REAL); set m = min(len R,len f); assume that A5: len p1 = m and A6: for n st n in dom p1 for F be PartFunc of D,REAL, r st r = R.n & F = f.n holds p1.n = r(#)F and A7: len p2 = m and A8: for n st n in dom p2 for F be PartFunc of D,REAL, r st r = R.n & F = f.n holds p2.n = r(#)F; A9: m<=len R & m<=len f by SQUARE_1:35; A10: dom p1 = Seg len p1 & dom p2 = Seg len p2 by FINSEQ_1:def 3; now let n; assume A11: n in Seg m; then A12: 1<=n & n<=m by FINSEQ_1:3; then n<=len R & n<=len f by A9,AXIOMS:22; then n in dom R & n in dom f by A12,FINSEQ_3:27; then reconsider F=f.n as Element of PFuncs(D,REAL) by FINSEQ_2:13; reconsider r=R.n as Real; p1.n=r(#)F & p2.n=r(#)F by A5,A6,A7,A8,A10,A11; hence p1.n = p2.n; end; hence thesis by A5,A7,FINSEQ_2:10; end; end; definition let D be non empty set, f be FinSequence of PFuncs(D,REAL), d be Element of D; func f#d -> FinSequence of REAL means :Def8: len it = len f & for n be Nat, G be Element of PFuncs(D,REAL) st n in dom it & f.n = G holds it.n = G.d; existence proof defpred P[Nat,set] means for G be Element of PFuncs(D,REAL) st f.$1=G holds $2=G.d; A1: for n st n in Seg len f ex x being Element of REAL st P[n,x] proof let n; assume n in Seg len f; then n in dom f by FINSEQ_1:def 3; then reconsider G=f.n as Element of PFuncs(D,REAL) by FINSEQ_2:13; take x=G.d; thus P[n,x]; end; consider p being FinSequence of REAL such that A2: dom p = Seg len f and A3: for n st n in Seg len f holds P[n,p.n] from SeqDEx(A1); take p; thus len p = len f by A2,FINSEQ_1:def 3; let n be Nat, G be Element of PFuncs(D,REAL); assume n in dom p & f.n = G; hence thesis by A2,A3; end; uniqueness proof let p1,p2 be FinSequence of REAL; assume that A4: len p1 = len f & for n be Nat, G be Element of PFuncs(D,REAL) st n in dom p1 & f.n = G holds p1.n = G.d and A5: len p2 = len f & for n be Nat, G be Element of PFuncs(D,REAL) st n in dom p2 & f.n = G holds p2.n = G.d; now let n; A6: dom p1=Seg len p1 & dom p2=Seg len p2 by FINSEQ_1:def 3; assume A7: n in Seg len p1; then n in dom f by A4,FINSEQ_1:def 3; then reconsider G = f.n as Element of PFuncs(D,REAL) by FINSEQ_2:13; p1.n = G.d & p2.n = G.d by A4,A5,A6,A7; hence p1.n = p2.n; end; hence thesis by A4,A5,FINSEQ_2:10; end; end; definition let D,C be non empty set, f be FinSequence of PFuncs(D,C), d be Element of D; pred d is_common_for_dom f means :Def9: for G be Element of PFuncs(D,C), n be Nat st n in dom f & f.n = G holds d in dom G; end; theorem Th29: for D,C be non empty set, f be FinSequence of PFuncs(D,C), d be Element of D, n be Nat st d is_common_for_dom f & n <> 0 holds d is_common_for_dom f|n proof let D1,D2 be non empty set, f be FinSequence of PFuncs(D1,D2), d1 be Element of D1, n; assume A1: d1 is_common_for_dom f & n<> 0; let G be Element of PFuncs(D1,D2), m; assume A2: m in dom (f|n) & (f|n).m = G; now per cases; case n>=len f; then f|n = f by Lm1; hence thesis by A1,A2,Def9; case A3: n<len f; then A4: dom f = Seg len f & dom(f|n) = Seg len(f|n) & len(f|n) = n by FINSEQ_1:def 3,TOPREAL1:3; 0<n by A1,NAT_1:19; then 0+1<=n by NAT_1:38; then n in dom f by A3,FINSEQ_3:27; then G = f.m & m in dom f by A2,A4,RFINSEQ:19; hence thesis by A1,Def9; end; hence thesis; end; theorem for D,C be non empty set, f be FinSequence of PFuncs(D,C), d be Element of D, n be Nat st d is_common_for_dom f holds d is_common_for_dom f /^ n proof let D1,D2 be non empty set, f be FinSequence of PFuncs(D1,D2), d1 be Element of D1, n; assume A1: d1 is_common_for_dom f; set fn = f /^ n; let G be Element of PFuncs(D1,D2), m; assume A2: m in dom fn & fn.m = G; now per cases; case len f<n; then fn = <*>PFuncs(D1,D2) by RFINSEQ:def 2; hence thesis by A2,FINSEQ_1:26; case n<=len f; then A3: dom f = Seg len f & dom fn = Seg len fn & len fn = len f - n & G= f.(m+n) by A2,FINSEQ_1:def 3,RFINSEQ:def 2; 1<=m & m<=len fn & m<=m+n by A2,FINSEQ_3:27,NAT_1:29; then 1<=m+n & m+n<=len f by A3,AXIOMS:22,REAL_1:84; then m+n in dom f by FINSEQ_3:27; hence thesis by A1,A3,Def9; end; hence thesis; end; theorem Th31: for D be non empty set, d be Element of D, f be FinSequence of PFuncs(D,REAL) st len f <> 0 holds d is_common_for_dom f iff d in dom Sum(f) proof let D be non empty set, d be Element of D; defpred P[Nat] means for f be FinSequence of PFuncs(D,REAL) st len f =$1 & len f <> 0 holds d is_common_for_dom f iff d in dom Sum(f); A1: P[0]; A2: for n st P[n] holds P[n+1] proof let n; assume A3: P[n]; let f be FinSequence of PFuncs(D,REAL); assume A4: len f = n+1 & len f <> 0; A5: dom f = Seg len f by FINSEQ_1:def 3; now per cases; case A6: n=0; then A7: 1 in dom f by A4,FINSEQ_3:27; then reconsider G = f.1 as Element of PFuncs(D,REAL) by FINSEQ_2:13; f=<*G*> by A4,A6,FINSEQ_1:57; then A8: Sum(f) = G by Th22; hence d is_common_for_dom f implies d in dom Sum(f) by A7,Def9; assume d in dom Sum(f); then for F be Element of PFuncs(D,REAL), m st m in dom f & f.m=F holds d in dom F by A4,A5,A6,A8,FINSEQ_1:4,TARSKI:def 1; hence d is_common_for_dom f by Def9; case A9: n <> 0; then 0<n by NAT_1:19; then A10: 0+1<=n by NAT_1:38; set fn = f|n; n<=n+1 by NAT_1:29; then A11: len fn = n & n in dom f by A4,A10,FINSEQ_3:27,TOPREAL1:3; 0<n+1 by NAT_1:19; then 0+1<=n+1 by NAT_1:38; then A12: n+1 in dom f by A4,FINSEQ_3:27; then reconsider G=f.(n+1) as Element of PFuncs(D,REAL) by FINSEQ_2:13; f = fn ^ <*G*> by A4,RFINSEQ:20; then A13: Sum(f) = Sum(fn) + G by Th23; thus d is_common_for_dom f implies d in dom Sum(f) proof assume A14: d is_common_for_dom f; then d is_common_for_dom fn by A9,Th29; then A15: d in dom Sum(fn) by A3,A9,A11; d in dom G by A12,A14,Def9; then d in dom(Sum(fn)) /\ dom G by A15,XBOOLE_0:def 3; hence d in dom(Sum(f)) by A13,SEQ_1:def 3; end; assume d in dom Sum(f); then A16: d in dom(Sum(fn)) /\ dom G by A13,SEQ_1:def 3; then d in dom(Sum(fn)) & d in dom G by XBOOLE_0:def 3; then A17: d is_common_for_dom fn by A3,A9,A11; now let F be Element of PFuncs(D,REAL), m; assume A18: m in dom f & f.m=F; then A19: 1<=m & m<=len f by FINSEQ_3:27; now per cases; case m=len f; hence d in dom F by A4,A16,A18,XBOOLE_0:def 3; case m<>len f; then m<len f by A19,REAL_1:def 5; then m<=n by A4,NAT_1:38; then A20: m in Seg n & dom fn = Seg len fn by A19,FINSEQ_1:3,def 3 ; then F = fn.m by A11,A18,RFINSEQ:19; hence d in dom F by A11,A17,A20,Def9; end; hence d in dom F; end; hence d is_common_for_dom f by Def9; end; hence thesis; end; A21: for n holds P[n] from Ind(A1,A2); let f be FinSequence of PFuncs(D,REAL); assume len f <> 0; hence thesis by A21; end; theorem Th32: for D be non empty set, f be FinSequence of PFuncs(D,REAL), d be Element of D, n be Nat holds (f|n)#d = (f#d)|n proof let D1 be non empty set, f be FinSequence of PFuncs(D1,REAL), d1 be Element of D1, n be Nat; A1: len(f#d1) = len f & len((f|n)#d1) = len(f|n) by Def8; now per cases; case A2: len f<=n; then f|n = f by Lm1; hence thesis by A1,A2,Lm1; case A3: n<len f; then A4: len(f|n) = n & len((f#d1)|n) = n by A1,TOPREAL1:3; A5: dom f = Seg len f & dom(f#d1) = Seg len(f#d1) & dom((f|n)#d1) = Seg len((f|n)#d1) by FINSEQ_1:def 3; now per cases; case n=0; then (f#d1)|n = <*>REAL & (f|n)#d1 = <*>REAL by A1,A4,FINSEQ_1:32; hence (f#d1)|n = (f|n)#d1; case n<>0; then 0<n by NAT_1:19; then 0+1<=n by NAT_1:38; then A6: n in dom f by A3,FINSEQ_3:27; now let m; assume A7: m in Seg len(f|n); then A8: ((f#d1)|n).m = (f#d1).m & m in dom (f#d1) by A1,A4,A5,A6,RFINSEQ:19; then reconsider G=f.m as Element of PFuncs(D1,REAL) by A1,A5,FINSEQ_2: 13; A9: ((f#d1)|n).m = G.d1 by A8,Def8; (f|n).m = G & m in dom f by A4,A6,A7,RFINSEQ:19; hence ((f#d1)|n).m = ((f|n)#d1).m by A1,A5,A7,A9,Def8; end; hence thesis by A1,A4,FINSEQ_2:10; end; hence thesis; end; hence thesis; end; theorem Th33: for D be non empty set, f be FinSequence, d be Element of D holds d is_common_for_dom CHI(f,D) proof let D be non empty set, f be FinSequence, d be Element of D; let G be Element of PFuncs(D,REAL), n; assume n in dom CHI(f,D) & CHI(f,D).n = G; then G = chi(f.n,D) by Def6; then dom G = D by RFUNCT_1:77; hence d in dom G; end; theorem Th34: for D be non empty set, d be Element of D, f be FinSequence of PFuncs(D,REAL), R be FinSequence of REAL st d is_common_for_dom f holds d is_common_for_dom R(#)f proof let D be non empty set, d be Element of D, f be FinSequence of PFuncs(D,REAL), R be FinSequence of REAL; assume A1: d is_common_for_dom f; let G be Element of PFuncs(D,REAL), n; assume A2: n in dom (R(#)f) & (R(#)f).n = G; set m = min(len R,len f); A3: m<=len R & m<=len f by SQUARE_1:35; len(R(#)f) = m by Def7; then A4: 1<=n & n<=m by A2,FINSEQ_3:27; then n<=len R & n<=len f by A3,AXIOMS:22; then A5: n in dom R & n in dom f by A4,FINSEQ_3:27; reconsider r=R.n as Real; reconsider F=f.n as Element of PFuncs(D,REAL) by A5,FINSEQ_2:13; A6: G=r(#)F by A2,Def7; d in dom F by A1,A5,Def9; hence d in dom G by A6,SEQ_1:def 6; end; theorem for D be non empty set, f be FinSequence, R be FinSequence of REAL, d be Element of D holds d is_common_for_dom R(#)CHI(f,D) proof let D be non empty set, f be FinSequence, R be FinSequence of REAL, d be Element of D; d is_common_for_dom CHI(f,D) by Th33; hence thesis by Th34; end; theorem for D be non empty set, d be Element of D, f be FinSequence of PFuncs(D,REAL) st d is_common_for_dom f holds (Sum(f)).d = Sum (f#d) proof let D be non empty set, d be Element of D; defpred P[Nat] means for f be FinSequence of PFuncs(D,REAL) st len f = $1 & d is_common_for_dom f holds (Sum(f)).d = Sum(f#d); A1: P[0] proof let f be FinSequence of PFuncs(D,REAL); A2: [#](D) = D by SUBSET_1:def 4; assume A3: len f = 0 & d is_common_for_dom f; then f=<*> PFuncs(D,REAL) by FINSEQ_1:32; then A4: (Sum(f)).d = ([#](D)-->(0 qua Real)).d by Th21 .= 0 by A2,FUNCOP_1:13; len(f#d)=0 by A3,Def8; hence (Sum(f)).d = Sum(f#d) by A4,FINSEQ_1:32,RVSUM_1:102; end; A5: for n st P[n] holds P[n+1] proof let n; assume A6: P[n]; let f be FinSequence of PFuncs(D,REAL); assume A7: len f = n+1 & d is_common_for_dom f; set fn = f|n; n<=n+1 by NAT_1:29; then A8: len fn = n by A7,TOPREAL1:3; A9: dom f = Seg len f & dom(f#d) = Seg len(f#d) & len (f#d)=len f by Def8,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 dom f by A7,FINSEQ_3:27; then reconsider G=f.(n+1) as Element of PFuncs(D,REAL) by FINSEQ_2:13; f = fn ^ <*G*> by A7,RFINSEQ:20; then A11: Sum f = Sum fn + G by Th23; A12: d in dom G by A7,A10,Def9; now per cases; case A13: n=0; then A14: f = <*G*> by A7,FINSEQ_1:57; A15: len(f#d) = 1 & len<*G.d*>=1 & dom(f#d)=dom(f#d) by A7,A13,Def8,FINSEQ_1:57; then A16: 1 in dom(f#d) by FINSEQ_3:27; now let m; assume m in Seg 1; then A17: m=1 by FINSEQ_1:4,TARSKI:def 1; hence (f#d).m=G.d by A13,A16,Def8 .=<*G.d*>.m by A17,FINSEQ_1:57; end; then A18: f#d = <*G.d*> by A15,FINSEQ_2:10; thus (Sum f).d = G.d by A14,Th22 .=Sum (f#d) by A18,RVSUM_1:103; case A19: n<>0; then A20: d is_common_for_dom fn by A7,Th29; then (Sum(fn)).d = Sum(fn#d) & d in dom(Sum(fn)) by A6,A8,A19,Th31; then d in dom(Sum(fn)) /\ dom G by A12,XBOOLE_0:def 3; then A21: d in dom(Sum(fn)+G) by SEQ_1:def 3; A22: (f#d).(n+1) =G.d by A9,A10,Def8; thus (Sum f).d = (Sum fn).d + G.d by A11,A21,SEQ_1:def 3 .= Sum(fn#d) + G.d by A6,A8,A20 .= Sum((f#d)|n) + G.d by Th32 .= Sum(((f#d)|n)^<*G.d*>) by RVSUM_1:104 .= Sum(f#d) by A7,A9,A22,RFINSEQ:20; end; hence thesis; end; A23: for n holds P[n] from Ind(A1,A5); let f be FinSequence of PFuncs(D,REAL); assume A24: d is_common_for_dom f; len f = len f; hence (Sum(f)).d = Sum(f#d) by A23,A24; end; definition let D be non empty set, F be PartFunc of D,REAL; func max+(F) -> PartFunc of D,REAL means :Def10: dom it = dom F & for d be Element of D st d in dom it holds it.d = max+(F.d); existence proof defpred P[set] means $1 in dom F; deffunc Q(set)=max+(F.$1); consider f be PartFunc of D,REAL such that A1: for d be Element of D holds d in dom f iff P[d] and A2: for d be Element of D st d in dom f holds f.d = Q(d) from LambdaPFD'; take f; thus dom f = dom F proof thus dom f c= dom F proof let x; assume x in dom f; hence thesis by A1; end; let x; assume x in dom F; hence thesis by A1; end; thus thesis by A2; end; uniqueness proof deffunc F(set)=max+(F.$1); for f,g being PartFunc of D,REAL st (dom f=dom F & for c be Element of D st c in dom f holds f.c = F(c)) & (dom g=dom F & for c be Element of D st c in dom g holds g.c = F(c)) holds f = g from UnPartFuncD'; hence thesis; end; func max-(F) -> PartFunc of D,REAL means :Def11: dom it = dom F & for d be Element of D st d in dom it holds it.d = max-(F.d); existence proof defpred P[set] means $1 in dom F; deffunc F(set)=max-(F.$1); consider f be PartFunc of D,REAL such that A3: for d be Element of D holds d in dom f iff P[d] and A4: for d be Element of D st d in dom f holds f.d =F(d) from LambdaPFD'; take f; thus dom f = dom F proof thus dom f c= dom F proof let x; assume x in dom f; hence thesis by A3; end; let x; assume x in dom F; hence thesis by A3; end; thus thesis by A4; end; uniqueness proof deffunc F(set)=max-(F.$1); for f,g being PartFunc of D,REAL st (dom f=dom F & for c be Element of D st c in dom f holds f.c = F(c)) & (dom g=dom F & for c be Element of D st c in dom g holds g.c = F(c)) holds f = g from UnPartFuncD'; hence thesis; end; end; theorem for D be non empty set, F be PartFunc of D,REAL holds F = max+(F) - max-(F) & abs(F) = max+(F) + max-(F) & 2 (#) max+(F) = F + abs(F) proof let D be non empty set, F be PartFunc of D,REAL; A1: dom max+(F) = dom F & dom max-(F) = dom F & dom abs(F) = dom F & dom(2(#)max+(F)) = dom max+(F) by Def10,Def11,SEQ_1:def 6,def 10; dom F = dom F /\ dom F; then A2: dom F = dom(max+(F) - max-(F)) & dom abs(F) = dom(max+(F) + max-(F)) & dom(2(#)max+(F)) = dom(F + abs(F)) by A1,SEQ_1:def 3,def 4; now let d be Element of D; assume A3: d in dom F; hence (max+(F) - max-(F)).d = max+(F).d - max-(F).d by A2,SEQ_1:def 4 .= max+(F.d) - max-(F).d by A1,A3,Def10 .= max+(F.d) - max-(F.d) by A1,A3,Def11 .= F.d by Th1; end; hence F = max+(F) - max-(F) by A2,PARTFUN1:34; now let d be Element of D; assume A4: d in dom abs(F); hence (max+(F) + max-(F)).d = max+(F).d + max-(F).d by A2,SEQ_1:def 3 .= max+(F.d) + max-(F).d by A1,A4,Def10 .= max+(F.d) + max-(F.d) by A1,A4,Def11 .= abs(F.d) by Th2 .= (abs(F)).d by A4,SEQ_1:def 10; end; hence abs(F) = max+(F) + max-(F) by A2,PARTFUN1:34; now let d be Element of D; assume A5: d in dom F; hence (2(#)max+(F)).d = 2*(max+(F).d) by A1,SEQ_1:def 6 .=2*max+(F.d) by A1,A5,Def10 .= F.d + abs(F.d) by Th3 .= F.d + (abs(F)).d by A1,A5,SEQ_1:def 10 .=(F+abs(F)).d by A1,A2,A5,SEQ_1:def 3; end; hence thesis by A1,A2,PARTFUN1:34; end; theorem Th38: for D be non empty set, F be PartFunc of D,REAL, r be Real st 0<r holds F"{r} = max+(F)"{r} proof let D be non empty set, F be PartFunc of D,REAL, r; assume A1: 0<r; A2: dom max+(F) = dom F by Def10; thus F"{r} c= max+(F)"{r} proof let x; assume A3: x in F"{r}; then reconsider d=x as Element of D; A4: d in dom F & F.d in {r} by A3,FUNCT_1:def 13; then A5: F.d = r by TARSKI:def 1; (max+(F)).d = max+(F.d) by A2,A4,Def10 .= max(F.d,0) by Def1 .= r by A1,A5,SQUARE_1:def 2; then (max+(F)).d in {r} by TARSKI:def 1; hence thesis by A2,A4,FUNCT_1:def 13; end; let x; assume A6: x in (max+ F)"{r}; then reconsider d=x as Element of D; A7: d in dom F & (max+ F).d in {r} by A2,A6,FUNCT_1:def 13; then A8: (max+ F).d = r by TARSKI:def 1; (max+ F).d = max+(F.d) by A2,A7,Def10 .= max(F.d,0) by Def1; then F.d = r by A1,A8,SQUARE_1:49; then F.d in {r} by TARSKI:def 1; hence thesis by A7,FUNCT_1:def 13; end; theorem Th39: for D be non empty set, F be PartFunc of D,REAL holds F"(left_closed_halfline(0)) = max+(F)"{0} proof let D be non empty set, F be PartFunc of D,REAL; set li = left_closed_halfline(0); A1: dom max+(F) = dom F by Def10; A2: li = {s : s<=0} by LIMFUNC1:def 1; thus F" li c= max+(F)"{0} proof let x; assume A3: x in F" li; then reconsider d=x as Element of D; A4: d in dom F & F.d in li by A3,FUNCT_1:def 13; then ex s st s=F.d & s<=0 by A2; then A5: max(F.d,0) = 0 by SQUARE_1:def 2; (max+(F)).d = max+(F.d) by A1,A4,Def10 .= max(F.d,0) by Def1; then (max+(F)).d in {0} by A5,TARSKI:def 1; hence thesis by A1,A4,FUNCT_1:def 13; end; let x; assume A6: x in (max+ F)"{0}; then reconsider d=x as Element of D; A7: d in dom F & (max+ F).d in {0} by A1,A6,FUNCT_1:def 13; then A8: (max+ F).d = 0 by TARSKI:def 1; (max+ F).d = max+(F.d) by A1,A7,Def10 .= max(F.d,0) by Def1; then F.d <= 0 by A8,SQUARE_1:def 2; then F.d in li by A2; hence thesis by A7,FUNCT_1:def 13; end; theorem Th40: for D be non empty set, F be PartFunc of D,REAL, d be Element of D st d in dom F holds 0<=(max+ F).d proof let D be non empty set, F be PartFunc of D,REAL, d be Element of D; assume A1: d in dom F; dom F = dom (max+ F) by Def10; then (max+ F).d = max+(F.d) by A1,Def10 .= max(F.d,0) by Def1; hence thesis by SQUARE_1:46; end; theorem Th41: for D be non empty set, F be PartFunc of D,REAL, r be Real st 0<r holds F"{-r} = max-(F)"{r} proof let D be non empty set, F be PartFunc of D,REAL, r; assume A1: 0<r; A2: dom max-(F) = dom F by Def11; thus F"{-r} c= max-(F)"{r} proof let x; assume A3: x in F"{-r}; then reconsider d=x as Element of D; A4: d in dom F & F.d in {-r} by A3,FUNCT_1:def 13; then A5: F.d = -r by TARSKI:def 1; (max-(F)).d = max-(F.d) by A2,A4,Def11 .= max(-F.d,0) by Def2 .= r by A1,A5,SQUARE_1:def 2; then (max-(F)).d in {r} by TARSKI:def 1; hence thesis by A2,A4,FUNCT_1:def 13; end; let x; assume A6: x in (max- F)"{r}; then reconsider d=x as Element of D; A7: d in dom F & (max- F).d in {r} by A2,A6,FUNCT_1:def 13; then A8: (max- F).d = r by TARSKI:def 1; (max- F).d = max-(F.d) by A2,A7,Def11 .= max(-F.d,0) by Def2; then -F.d = r by A1,A8,SQUARE_1:49; then F.d in {-r} by TARSKI:def 1; hence thesis by A7,FUNCT_1:def 13; end; theorem Th42: for D be non empty set, F be PartFunc of D,REAL holds F"(right_closed_halfline(0)) = max-(F)"{0} proof let D be non empty set, F be PartFunc of D,REAL; set li = right_closed_halfline(0); A1: dom max-(F) = dom F by Def11; A2: li = {s : 0<=s} by LIMFUNC1:def 2; thus F" li c= max-(F)"{0} proof let x; assume A3: x in F" li; then reconsider d=x as Element of D; A4: d in dom F & F.d in li by A3,FUNCT_1:def 13; then ex s st s=F.d & 0<=s by A2; then -F.d<=0 by REAL_1:26,50; then A5: max(-F.d,0) = 0 by SQUARE_1:def 2; (max-(F)).d = max-(F.d) by A1,A4,Def11 .= max(-F.d,0) by Def2; then (max-(F)).d in {0} by A5,TARSKI:def 1; hence thesis by A1,A4,FUNCT_1:def 13; end; let x; assume A6: x in (max- F)"{0}; then reconsider d=x as Element of D; A7: d in dom F & (max- F).d in {0} by A1,A6,FUNCT_1:def 13; then A8: (max- F).d = 0 by TARSKI:def 1; (max- F).d = max-(F.d) by A1,A7,Def11 .= max(-F.d,0) by Def2; then -F.d <= 0 by A8,SQUARE_1:def 2; then 0<=F.d by REAL_1:26,50; then F.d in li by A2; hence thesis by A7,FUNCT_1:def 13; end; theorem Th43: for D be non empty set, F be PartFunc of D,REAL, d be Element of D st d in dom F holds 0<=(max- F).d proof let D be non empty set, F be PartFunc of D,REAL, d be Element of D; assume A1: d in dom F; dom F = dom (max- F) by Def11; then (max- F).d = max-(F.d) by A1,Def11 .= max(-F.d,0) by Def2; hence thesis by SQUARE_1:46; end; theorem for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL st F,G are_fiberwise_equipotent holds max+(F), max+(G) are_fiberwise_equipotent proof let D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL; assume A1: F,G are_fiberwise_equipotent; A2: rng F c= REAL & rng G c= REAL & rng(max+ F) c= REAL & rng(max+ G) c= REAL ; A3: dom F = dom (max+ F) & dom G = dom (max+ G) by Def10; set li =left_closed_halfline(0); now let r; now per cases; case 0<r; then F"{r} = (max+ F)"{r} & G"{r} = (max+ G)"{r} by Th38; hence Card((max+ F)"{r}) = Card((max+ G)"{r}) by A1,A2,RFINSEQ:5; case A4: r=0; F" li = (max+ F)"{0} & G" li = (max+ G)"{0} by Th39; hence Card((max+ F)"{r}) = Card((max+ G)"{r}) by A1,A4,RFINSEQ:4; case A5: r<0; now assume r in rng(max+ F); then consider d be Element of D such that A6: d in dom(max+ F) & (max+ F).d = r by PARTFUN1:26; thus contradiction by A3,A5,A6,Th40; end; then A7: (max+ F)"{r} = {} by Lm2; now assume r in rng(max+ G); then consider c be Element of C such that A8: c in dom(max+ G) & (max+ G).c = r by PARTFUN1:26; thus contradiction by A3,A5,A8,Th40; end; hence Card(( max+F)"{r}) = Card(( max+ G)"{r}) by A7,Lm2; end; hence Card(( max+F)"{r}) = Card(( max+ G)"{r}); end; hence thesis by A2,RFINSEQ:5; end; theorem for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL st F,G are_fiberwise_equipotent holds max-(F), max-(G) are_fiberwise_equipotent proof let D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL; assume A1: F,G are_fiberwise_equipotent; A2: rng F c= REAL & rng G c= REAL & rng(max- F) c= REAL & rng(max- G) c= REAL ; A3: dom F = dom (max- F) & dom G = dom (max- G) by Def11; set li =right_closed_halfline(0); now let r; now per cases; case 0<r; then F"{-r} = (max- F)"{r} & G"{-r} = (max- G)"{r} by Th41; hence Card((max- F)"{r}) = Card((max- G)"{r}) by A1,A2,RFINSEQ:5; case A4: r=0; F" li = (max- F)"{0} & G" li = (max- G)"{0} by Th42; hence Card((max- F)"{r}) = Card((max- G)"{r}) by A1,A4,RFINSEQ:4; case A5: r<0; now assume r in rng(max- F); then consider d be Element of D such that A6: d in dom(max- F) & (max- F).d = r by PARTFUN1:26; thus contradiction by A3,A5,A6,Th43; end; then A7: (max- F)"{r} = {} by Lm2; now assume r in rng(max- G); then consider c be Element of C such that A8: c in dom(max- G) & (max- G).c = r by PARTFUN1:26; thus contradiction by A3,A5,A8,Th43; end; hence Card(( max-F)"{r}) = Card(( max- G)"{r}) by A7,Lm2; end; hence Card(( max-F)"{r}) = Card(( max- G)"{r}); end; hence thesis by A2,RFINSEQ:5; end; definition let A,B be set; cluster finite PartFunc of A,B; existence proof {} is finite & {} is PartFunc of A,B by PARTFUN1:56; hence thesis; end; end; definition let D be non empty set, F be finite PartFunc of D,REAL; cluster max+(F) -> finite; coherence proof dom F is finite; then dom(max+(F)) is finite by Def10; hence thesis by AMI_1:21; end; cluster max-(F) -> finite; coherence proof dom F is finite; then dom(max-(F)) is finite by Def11; hence thesis by AMI_1:21; end; end; theorem for D,C be non empty set, F be finite PartFunc of D,REAL, G be finite PartFunc of C,REAL st max+ F, max+ G are_fiberwise_equipotent & max- F, max- G are_fiberwise_equipotent holds F, G are_fiberwise_equipotent proof let D,C be non empty set, F be finite PartFunc of D,REAL, G be finite PartFunc of C,REAL; assume A1: max+ F, max+ G are_fiberwise_equipotent & max- F, max- G are_fiberwise_equipotent; A2: rng F c= REAL & rng G c= REAL & rng(max+ F) c= REAL & rng(max- F) c= REAL & rng(max+ G) c= REAL & rng(max- G) c= REAL; A3: dom F = dom(max+ F) & dom F = dom(max- F) & dom G = dom(max+ G) & dom G = dom(max- G) by Def10,Def11; set lh = left_closed_halfline(0), rh = right_closed_halfline(0), fp0 = (max+ F)"{0}, fm0 = (max- F)"{0}, gp0 = (max+ G)"{0}, gm0 = (max- G)"{0}; A4: lh /\ rh = [.0,0 .] by LIMFUNC1:19 .= {0} by RCOMP_1:14; A5: F"lh = fp0 & F"rh =fm0 & G"lh = gp0 & G"rh =gm0 by Th39,Th42; reconsider fp0,fm0,gp0,gm0 as finite set; card(fp0 \/ fm0) = card fp0 + card fm0 - card(fp0 /\ fm0) & card(gp0 \/ gm0) = card gp0 + card gm0 - card(gp0 /\ gm0) by CARD_2:64; then A6: card(fp0 /\ fm0) = card fp0 + card fm0 - card(fp0 \/ fm0) & card(gp0 /\ gm0) = card gp0 + card gm0 - card(gp0 \/ gm0) by XCMPLX_1:18; A7: lh \/ rh = REAL \ ].0,0 .[ by LIMFUNC1:25 .= REAL \ {} by RCOMP_1:12 .= REAL; then A8: fp0 \/ fm0 = F"(REAL) by A5,RELAT_1:175; F"(rng F) c= F"REAL by RELAT_1:178; then F"REAL c= dom F & dom F c= F"REAL by RELAT_1:167,169; then A9: fp0 \/ fm0 = dom F by A8,XBOOLE_0:def 10; A10: gp0 \/ gm0 = G"(lh \/ rh) by A5,RELAT_1:175; G"(rng G) c= G"REAL by RELAT_1:178; then G"REAL c= dom G & dom G c= G"REAL by RELAT_1:167,169; then A11: gp0 \/ gm0 = dom G by A7,A10,XBOOLE_0:def 10; now let r; A12: card fp0 = card gp0 & card fm0 = card gm0 by A1,RFINSEQ:9; now per cases; case 0<r; then F"{r} = (max+ F)"{r} & G"{r} = (max+ G)"{r} by Th38; hence card(F"{r}) = card(G"{r}) by A1,A2,RFINSEQ:11; case 0=r; then F"{r} = F"lh /\ F"rh & G"{r} = G"lh /\ G"rh by A4,FUNCT_1:137; hence card(F"{r}) = card(G"{r}) by A1,A3,A5,A6,A9,A11,A12,RFINSEQ:10; case r<0; then 0<-r & --r=r by REAL_1:66; then F"{r} = (max- F)"{-r} & G"{r} = (max- G)"{-r} by Th41; hence card(F"{r}) = card(G"{r}) by A1,A2,RFINSEQ:11; end; hence card(F"{r}) = card(G"{r}); end; hence thesis by A2,RFINSEQ:11; end; theorem Th47: for D be non empty set, F be PartFunc of D,REAL, X be set holds (max+ F)|X = max+ (F|X) proof let D be non empty set, F be PartFunc of D,REAL, X be set; A1: dom((max+ F)|X) = dom(max+ F) /\ X by FUNCT_1:68; A2: dom(max+ F) /\ X= dom F /\ X by Def10 .= dom(F|X) by FUNCT_1:68; A3: dom(F|X) = dom(max+ (F|X)) by Def10; now let d be Element of D; assume A4: d in dom((max+ F)|X); then A5: d in dom(max+ F) by A1,XBOOLE_0:def 3; thus ((max+ F)|X).d = (max+ F).d by A4,FUNCT_1:68 .=max+(F.d) by A5,Def10 .=max+((F|X).d) by A1,A2,A4,FUNCT_1:68 .=(max+ (F|X)).d by A1,A2,A3,A4,Def10; end; hence thesis by A1,A2,A3,PARTFUN1:34; end; theorem for D be non empty set, F be PartFunc of D,REAL, X be set holds (max- F)|X = max- (F|X) proof let D be non empty set, F be PartFunc of D,REAL, X be set; A1: dom((max- F)|X) = dom(max- F) /\ X by FUNCT_1:68; A2: dom(max- F) /\ X= dom F /\ X by Def11 .= dom(F|X) by FUNCT_1:68; A3: dom(F|X) = dom(max- (F|X)) by Def11; now let d be Element of D; assume A4: d in dom((max- F)|X); then A5: d in dom(max- F) by A1,XBOOLE_0:def 3; thus ((max- F)|X).d = (max- F).d by A4,FUNCT_1:68 .=max-(F.d) by A5,Def11 .=max-((F|X).d) by A1,A2,A4,FUNCT_1:68 .=(max- (F|X)).d by A1,A2,A3,A4,Def11; end; hence thesis by A1,A2,A3,PARTFUN1:34; end; theorem Th49: for D be non empty set, F be PartFunc of D,REAL st (for d be Element of D st d in dom F holds F.d>=0) holds max+ F = F proof let D be non empty set, F be PartFunc of D,REAL; assume A1: for d be Element of D st d in dom F holds F.d>=0; A2: dom(max+ F) = dom F by Def10; now let d be Element of D; assume A3: d in dom F; then A4: F.d>=0 by A1; thus (max+ F).d = max+(F.d) by A2,A3,Def10 .= max(0,F.d) by Def1 .= F.d by A4,SQUARE_1:def 2; end; hence thesis by A2,PARTFUN1:34; end; theorem for D be non empty set, F be PartFunc of D,REAL st (for d be Element of D st d in dom F holds F.d<=0) holds max- F = -F proof let D be non empty set, F be PartFunc of D,REAL; assume A1: for d be Element of D st d in dom F holds F.d<=0; A2: dom(max- F) = dom F by Def11; A3: dom F = dom(-F) by SEQ_1:def 7; now let d be Element of D; assume A4: d in dom F; then F.d<=0 by A1; then A5: 0<=-F.d by REAL_1:26,50; thus (max- F).d = max-(F.d) by A2,A4,Def11 .= max(0,-F.d) by Def2 .= -F.d by A5,SQUARE_1:def 2 .= (-F).d by A3,A4,SEQ_1:def 7; end; hence thesis by A2,A3,PARTFUN1:34; end; definition let D be non empty set, F be PartFunc of D,REAL, r be Real; func F - r -> PartFunc of D,REAL means :Def12: dom it = dom F & for d be Element of D st d in dom it holds it.d = F.d - r; existence proof defpred P[set] means $1 in dom F; deffunc F(set)=F.$1 - r; consider f be PartFunc of D,REAL such that A1: for d be Element of D holds d in dom f iff P[d] and A2: for d be Element of D st d in dom f holds f.d = F(d) from LambdaPFD'; take f; thus dom f = dom F proof thus dom f c= dom F proof let x; assume x in dom f; hence thesis by A1; end; let x; assume x in dom F; hence thesis by A1; end; thus thesis by A2; end; uniqueness proof deffunc F(set)=F.$1 - r; for f,g being PartFunc of D,REAL st (dom f=dom F & for c be Element of D st c in dom f holds f.c = F(c)) & (dom g=dom F & for c be Element of D st c in dom g holds g.c = F(c)) holds f = g from UnPartFuncD'; hence thesis; end; end; theorem Th51: for D be non empty set, F be PartFunc of D,REAL holds F - 0 = F proof let D be non empty set, F be PartFunc of D,REAL; A1: dom(F - 0) = dom F by Def12; now let d be Element of D; assume d in dom F; hence (F - 0).d = F.d - 0 by A1,Def12 .= F.d; end; hence thesis by A1,PARTFUN1:34; end; theorem for D be non empty set, F be PartFunc of D,REAL, r be Real, X be set holds (F|X) - r = (F-r)| X proof let D be non empty set, F be PartFunc of D,REAL, r be Real, X be set; A1: dom ((F|X) - r) = dom (F|X) by Def12 .= dom F /\ X by FUNCT_1:68; A2: dom F /\ X = dom(F-r) /\ X by Def12 .= dom((F-r)|X) by FUNCT_1:68; now let d be Element of D; assume A3: d in dom ((F|X) - r); then d in dom F by A1,XBOOLE_0:def 3; then A4: d in dom(F-r) by Def12; thus ((F|X) - r).d = (F|X).d - r by A3,Def12 .= F.d -r by A1,A3,FUNCT_1:71 .= (F-r).d by A4,Def12 .=((F-r)|X).d by A1,A2,A3,FUNCT_1:68; end; hence thesis by A1,A2,PARTFUN1:34; end; theorem Th53: for D be non empty set, F be PartFunc of D,REAL, r,s be Real holds F"{s+r} = (F-r)"{s} proof let D be non empty set, F be PartFunc of D,REAL, r,s; thus F"{s+r} c= (F-r)"{s} proof let x; assume A1: x in F"{s+r}; then reconsider d=x as Element of D; d in dom F & F.d in {s+r} by A1,FUNCT_1:def 13; then A2: d in dom(F-r) & F.d = s+r by Def12,TARSKI:def 1; then F.d - r = s by XCMPLX_1:26; then (F-r).d = s by A2,Def12; then (F-r).d in {s} by TARSKI:def 1; hence thesis by A2,FUNCT_1:def 13; end; let x; assume A3: x in (F-r)"{s}; then reconsider d=x as Element of D; A4: d in dom(F-r) & (F-r).d in {s} by A3,FUNCT_1:def 13; then A5: d in dom F & (F-r).d = s by Def12,TARSKI:def 1; then F.d -r= s by A4,Def12; then F.d = s+r by XCMPLX_1:27; then F.d in {s+r} by TARSKI:def 1; hence thesis by A5,FUNCT_1:def 13; end; theorem for D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL, r be Real holds F, G are_fiberwise_equipotent iff F-r ,G-r are_fiberwise_equipotent proof let D,C be non empty set, F be PartFunc of D,REAL, G be PartFunc of C,REAL, r be Real; A1: rng F c= REAL & rng G c= REAL & rng(F-r) c= REAL & rng(G-r) c= REAL; thus F, G are_fiberwise_equipotent implies F-r, G-r are_fiberwise_equipotent proof assume A2: F, G are_fiberwise_equipotent; now let s; thus Card ((F-r)"{s}) = Card(F"{s+r}) by Th53 .= Card(G"{s+r}) by A1,A2,RFINSEQ:5 .= Card((G-r)"{s}) by Th53; end; hence thesis by A1,RFINSEQ:5; end; assume A3: F-r, G-r are_fiberwise_equipotent; now let s; A4: s = s-r+r by XCMPLX_1:27; hence Card (F"{s}) = Card((F-r)"{s-r}) by Th53 .= Card((G- r)"{s-r}) by A1,A3,RFINSEQ:5 .= Card(G"{s}) by A4,Th53; end; hence thesis by A1,RFINSEQ:5; end; definition let F be PartFunc of REAL,REAL, X be set; pred F is_convex_on X means :Def13: X c= dom F & for p be Real st 0<=p & p<=1 holds for r,s be Real st r in X & s in X & p*r + (1-p)*s in X holds F.(p*r + (1-p)*s) <= p*F.r + (1-p)*F.s; end; theorem Th55: for a,b be Real, F be PartFunc of REAL,REAL holds F is_convex_on [.a,b.] iff [.a,b.] c= dom F & for p be Real st 0<=p & p<=1 holds for r,s be Real st r in [.a,b.] & s in [.a,b.] holds F.(p*r + (1-p)*s) <= p*F.r + (1-p)*F.s proof let a,b be Real, f be PartFunc of REAL,REAL; set ab = {r where r is Real: a<=r & r<=b}; A1: [.a,b.]= ab by RCOMP_1:def 1; thus f is_convex_on [.a,b.] implies [.a,b.] c= dom f & for p be Real st 0<=p & p<=1 holds for x,y be Real st x in [.a,b.] & y in [.a,b.] holds f.(p*x + (1-p)*y) <= p* f.x + (1-p)*f.y proof assume A2: f is_convex_on [.a,b.]; hence [.a,b.] c= dom f by Def13; let p be Real; assume A3: 0<=p & p<=1; then A4: 0<=1-p by SQUARE_1:12; let x,y be Real; assume A5: x in [.a,b.] & y in [.a,b.]; then A6: (ex r1 be Real st r1=x & a<=r1 & r1<=b) & ex r2 be Real st r2=y & a<=r2 & r2<=b by A1; then A7: p*a<=p*x & p*x<=p*b by A3,AXIOMS:25; A8: (1-p)*a<=(1-p)*y & (1-p)*y<=(1-p)*b by A4,A6,AXIOMS:25; p*a+(1-p)*a=p*a+(1*a-p*a) by XCMPLX_1:40 .=a by XCMPLX_1:27; then A9: a<=p*x+(1-p)*y by A7,A8,REAL_1:55; p*b+(1-p)*b=p*b+(1*b-p*b) by XCMPLX_1:40 .=b by XCMPLX_1:27; then p*x+(1-p)*y<=b by A7,A8,REAL_1:55; then p*x+(1-p)*y in ab by A9; hence thesis by A1,A2,A3,A5,Def13; end; assume A10: [.a,b.] c= dom f & for p be Real st 0<=p & p<=1 holds for x,y be Real st x in [.a,b.] & y in [.a,b.] holds f.(p*x + (1-p)*y) <= p* f.x + (1-p)*f.y; hence [.a,b.] c= dom f; let p be Real; assume A11: 0<=p & p<=1; let x,y be Real; assume x in [.a,b.] & y in [.a,b.] & p*x + (1-p)*y in [.a,b.]; hence thesis by A10,A11; end; theorem for a,b be Real, F be PartFunc of REAL,REAL holds F is_convex_on [.a,b.] iff [.a,b.] c= dom F & for x1,x2,x3 be Real st x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] & x1<x2 & x2<x3 holds (F.x1-F.x2)/(x1-x2)<=(F.x2-F.x3)/(x2-x3) proof let a,b be Real, f be PartFunc of REAL,REAL; thus f is_convex_on [.a,b.] implies [.a,b.] c= dom f & for x1,x2,x3 be Real st x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] & x1<x2 & x2<x3 holds (f.x1 - f.x2)/(x1 - x2) <= (f.x2 - f.x3)/(x2 - x3) proof assume A1: f is_convex_on [.a,b.]; hence [.a,b.] c= dom f by Def13; let x1,x2,x3 be Real; assume A2: x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] & x1<x2 & x2<x3; then A3: 0 < x3 - x2 & x2-x3<0 & 0 < x2 - x1 & x1-x2<0 by REAL_2:105,SQUARE_1:11; x1<x3 by A2,AXIOMS:22; then A4: x1-x3<0 & 0<>x1-x3 by REAL_2:105; set r = (x2-x3)/(x1-x3); A5: r + (x1-x2)/(x1-x3) = ((x1-x2) + (x2-x3))/(x1-x3) by XCMPLX_1:63 .= (x1-x3)/(x1-x3) by XCMPLX_1:39 .= 1 by A4,XCMPLX_1:60; then A6: r*x1 + (1-r)*x3=x1*((x2-x3)/(x1-x3))+x3*((x1-x2)/(x1-x3)) by XCMPLX_1:26 .= (x1*(x2-x3))/(x1-x3)+x3*((x1-x2)/(x1-x3)) by XCMPLX_1:75 .= (x1*(x2-x3))/(x1-x3)+(x3*(x1-x2))/(x1-x3) by XCMPLX_1:75 .= ((x2-x3)*x1+(x1-x2)*x3)/(x1-x3) by XCMPLX_1:63 .=((x2*x1-x3*x1)+(x1-x2)*x3)/(x1-x3) by XCMPLX_1:40 .=((x2*x1-x3*x1)+(x3*x1-x2*x3))/(x1-x3) by XCMPLX_1:40 .=(x2*x1-x2*x3)/(x1-x3) by XCMPLX_1:39 .=x2*(x1-x3)/(x1-x3) by XCMPLX_1:40 .=x2 by A4,XCMPLX_1:90; A7: 0<=r by A3,A4,REAL_2:127; A8: (x1-x2)/(x1-x3)>0 by A3,A4,REAL_2:127; A9: -(1-r)=-((x1-x2)/(x1-x3)) by A5,XCMPLX_1:26; A10: ((x1-x2)/(x1-x3))*(-1)<0 by A8,SQUARE_1:24; (-1)*((x1-x2)/(x1-x3))=-(1*((x1-x2)/(x1-x3))) by XCMPLX_1:175 .=-((x1-x2)/(x1-x3)); then A11: -1+r<=0 by A9,A10,XCMPLX_1:162; r=(1+-1)+r .=1+(-1+r) by XCMPLX_1:1; then A12: r<=1 by A11,REAL_2:174; r+(1-r)=1 by XCMPLX_1:27; then f.x2=(r+(1-r))*f.x2 .=r*f.x2+(1-r)*f.x2 by XCMPLX_1:8; then A13: r*f.x2+(1-r)*f.x2<=r*f.x1+(1-r)*f.x3 by A1,A2,A6,A7,A12,Def13; A14: r*(f.x2-f.x1)=r*f.x2 -r*f.x1 by XCMPLX_1:40; (1-r)*(f.x3-f.x2)=(1-r)*f.x3-(1-r)*f.x2 by XCMPLX_1:40; then r*(f.x2-f.x1)<=(1-r)*(f.x3-f.x2) by A13,A14,REAL_2:167; then A15: -((1-r)*(f.x3-f.x2))<=-(r*(f.x2-f.x1)) by REAL_1:50; (1-r)*(-(f.x3-f.x2))=-((1-r)*(f.x3-f.x2)) by XCMPLX_1:175; then A16: (1-r)*(-(f.x3-f.x2))<=r*(-(f.x2-f.x1)) by A15,XCMPLX_1:175; f.x2-f.x3=-(f.x3-f.x2) & f.x1-f.x2=-(f.x2-f.x1) by XCMPLX_1:143; then A17: (x1-x2)/(x1-x3)*(f.x2-f.x3)<=(x2-x3)/(x1-x3)*(f.x1-f.x2) by A5,A16,XCMPLX_1:26; (x1-x2)/(x1-x3)=(x1-x3)"*(x1-x2) by XCMPLX_0:def 9; then (x1-x3)"*(x1-x2)*(f.x2-f.x3)<=(x1-x3)"*(x2-x3)*(f.x1-f.x2) by A17,XCMPLX_0:def 9; then A18: (x1-x3)*((x1-x3)"*(x2-x3)*(f.x1-f.x2))<= (x1-x3)*((x1-x3)"*(x1-x2)*(f.x2-f.x3)) by A4,REAL_1:52; set u=(x2-x3)*(f.x1-f.x2); set v=(x1-x2)*(f.x2-f.x3); A19: (x1-x3)*((x1-x3)"*(x2-x3)*(f.x1-f.x2))=(x1-x3)*((x1-x3)"*u) by XCMPLX_1:4 .=((x1-x3)*(x1-x3)")*u by XCMPLX_1:4 .=1*u by A4,XCMPLX_0:def 7 .=u; (x1-x3)*((x1-x3)"*(x1-x2)*(f.x2-f.x3))=(x1-x3)*((x1-x3)"*v) by XCMPLX_1: 4 .=((x1-x3)*(x1-x3)")*v by XCMPLX_1:4 .=1*v by A4,XCMPLX_0:def 7 .=v; hence (f.x1-f.x2)/(x1-x2)<=(f.x2-f.x3)/(x2-x3) by A3,A18,A19,REAL_2:187; end; assume that A20: [.a,b.] c= dom f and A21: for x1,x2,x3 be Real st x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] & x1<x2 & x2<x3 holds (f.x1-f.x2)/(x1-x2)<=(f.x2-f.x3)/(x2-x3); now let p be Real; assume A22: 0<=p & p<=1; then A23: 0<=1-p by SQUARE_1:12; let x,y be Real; set r = p*x+(1-p)*y; A24: {s where s is Real: a<=s & s<=b} = [.a,b.] by RCOMP_1:def 1; A25: p*x+(1-p)*x = (p+(1-p))*x by XCMPLX_1:8 .= 1*x by XCMPLX_1:27 .= x; A26: p*y+(1-p)*y = (p+(1-p))*y by XCMPLX_1:8 .= 1*y by XCMPLX_1:27 .= y; A27: p*a+(1-p)*a = (p+(1-p))*a by XCMPLX_1:8 .= 1*a by XCMPLX_1:27 .= a; A28: p*b+(1-p)*b = (p+(1-p))*b by XCMPLX_1:8 .= 1*b by XCMPLX_1:27 .= b; assume A29: x in [.a,b.] & y in [.a,b.]; then (ex t be Real st t=x & a<=t & t<=b) & (ex t be Real st t=y & a<=t & t <=b) by A24; then p*a<=p*x & (1-p)*a<=(1-p)*y & p*x<=p*b & (1-p)*y<=(1-p)*b by A22,A23,AXIOMS:25; then a<=r & r<=b by A27,A28,REAL_1:55; then A30: r in [.a,b.] by A24; A31: r-y = p*x+((1-p)*y - 1*y) by XCMPLX_1:29 .= p*x+((1-p -1)*y) by XCMPLX_1:40 .= p*x+((1+-p -1)*y) by XCMPLX_0:def 8 .= p*x+(-p)*y by XCMPLX_1:26 .= p*x+-(p*y) by XCMPLX_1:175 .= p*x-p*y by XCMPLX_0:def 8 .= p*(x-y) by XCMPLX_1:40; A32: x-r = 1*x -p*x -(1-p)*y by XCMPLX_1:36 .= (1-p)*x -(1-p)*y by XCMPLX_1:40 .= (1-p)*(x-y) by XCMPLX_1:40; now per cases; case A33: x=y; then A34: p*x + (1-p)*y = (p+(1-p))*x by XCMPLX_1:8 .= 1*x by XCMPLX_1:27 .= x; p* f.x + (1-p)*f.y = (p + (1-p))*f.x by A33,XCMPLX_1:8 .= 1* f.x by XCMPLX_1:27 .= f.x; hence f.(p*x + (1-p)*y) <= p* f.x + (1-p)*f.y by A34; case A35: x<>y; now per cases; case p=0; hence f.(p*x + (1-p)*y) <= p* f.x + (1-p)*f.y; case A36: p<>0; now per cases; case p=1; hence f.(p*x + (1-p)*y) <= p* f.x + (1-p)*f.y; case p<>1; then p<1 by A22,REAL_1:def 5; then A37: 0<1-p by SQUARE_1:11; A38: f.r *p + f.r *(1-p) = f.r *(p+(1-p)) by XCMPLX_1:8 .= f.r *1 by XCMPLX_1:27 .= f.r; now per cases by A35,REAL_1:def 5; case A39: x<y; then p*x < p*y by A22,A36,REAL_1:70; then A40: r<y by A26,REAL_1:67; then A41: r-y<0 by REAL_2:105; (1-p)*x < (1-p)*y by A37,A39,REAL_1:70; then A42: x<r by A25,REAL_1:67; then A43: x-r<0 by REAL_2:105; A44: x-y<0 & x-y<>0 by A39,REAL_2:105; (f.x-f.r)/(x-r)<=(f.r-f.y)/(r-y) by A21,A29,A30,A40,A42; then (f.x-f.r)*(p*(x-y))<=(f.r-f.y)*((1-p)*(x-y)) by A31,A32,A41,A43,REAL_2:185; then (f.x-f.r)*p*(x-y)<=(f.r-f.y)*((1-p)*(x-y)) by XCMPLX_1:4; then (f.x-f.r)*p*(x-y)<=(f.r-f.y)*(1-p)*(x-y) by XCMPLX_1:4; then (f.x-f.r)*p*(x-y)/(x-y)>=(f.r-f.y)*(1-p)*(x-y)/(x-y) by A44,REAL_1:74; then (f.r-f.y)*(1-p)*(x-y)/(x-y)<=(f.x-f.r)*p by A44,XCMPLX_1:90; then (f.r-f.y)*(1-p)<=(f.x-f.r)*p by A44,XCMPLX_1:90; then f.r * (1-p) - f.y*(1-p) <= (f.x-f.r)*p by XCMPLX_1:40; then f.r *(1-p) - f.y*(1-p) <= f.x *p - f.r *p by XCMPLX_1:40; then f.r *p + (f.r *(1-p) - f.y*(1-p)) <= f.x *p by REAL_1:84; then f.r *p + f.r *(1-p) - f.y*(1-p) <= f.x *p by XCMPLX_1:29; hence f.r <= p*f.x + (1-p)*f.y by A38,REAL_1:86; case A45: y<x; then p*y < p*x by A22,A36,REAL_1:70; then A46: y<r by A26,REAL_1:67; then A47: y-r<0 by REAL_2:105; (1-p)*y < (1-p)*x by A37,A45,REAL_1:70; then A48: r<x by A25,REAL_1:67; then A49: r-x<0 by REAL_2:105; A50: y-x<0 & y-x <> 0 by A45,REAL_2:105; A51: y-r = 1*y -(1-p)*y -p*x by XCMPLX_1:36 .= (1 -(1-p))*y -p*x by XCMPLX_1:40 .= p*y -p*x by XCMPLX_1:18 .= p*(y -x) by XCMPLX_1:40; A52: r-x = (1-p)*y+(p*x -1*x) by XCMPLX_1:29 .= (1-p)*y+(p-1)*x by XCMPLX_1:40 .= (1-p)*y+(-(1-p))*x by XCMPLX_1:143 .= (1-p)*y+-((1-p)*x) by XCMPLX_1:175 .= (1-p)*y-(1-p)*x by XCMPLX_0:def 8 .= (1-p)*(y-x) by XCMPLX_1:40; (f.y-f.r)/(y-r)<=(f.r-f.x)/(r-x) by A21,A29,A30,A46,A48; then (f.y-f.r)*((1-p)*(y-x))<=(f.r-f.x)*(p*(y-x)) by A47,A49,A51,A52,REAL_2:185; then (f.y-f.r)*(1-p)*(y-x)<=(f.r-f.x)*(p*(y-x)) by XCMPLX_1:4; then (f.y-f.r)*(1-p)*(y-x)<=(f.r-f.x)*p*(y-x) by XCMPLX_1:4; then (f.y-f.r)*(1-p)*(y-x)/(y-x)>=(f.r-f.x)*p*(y-x)/(y-x) by A50,REAL_1:74; then (f.r-f.x)*p*(y-x)/(y-x)<=(f.y-f.r)*(1-p) by A50,XCMPLX_1:90; then (f.r-f.x)*p<=(f.y-f.r)*(1-p) by A50,XCMPLX_1:90; then f.r * p - f.x*p <= (f.y-f.r)*(1-p) by XCMPLX_1:40; then f.r *p - f.x *p <= f.y *(1-p) - f.r *(1-p) by XCMPLX_1:40; then f.r *p - f.x *p + f.r *(1-p) <= f.y *(1-p) by REAL_1:84; then f.r *p + f.r *(1-p) - f.x *p <= f.y *(1-p) by XCMPLX_1:29; hence f.r <= p*f.x + (1-p)*f.y by A38,REAL_1:86; end; hence f.(p*x + (1-p)*y) <= p* f.x + (1-p)*f.y; end; hence f.(p*x + (1-p)*y) <= p* f.x + (1-p)*f.y; end; hence f.(p*x + (1-p)*y) <= p* f.x + (1-p)*f.y; end; hence f.(p*x + (1-p)*y) <= p* f.x + (1-p)*f.y; end; hence thesis by A20,Th55; end; theorem for F be PartFunc of REAL,REAL, X,Y be set st F is_convex_on X & Y c= X holds F is_convex_on Y proof let F be PartFunc of REAL,REAL, X,Y be set; assume A1: F is_convex_on X & Y c= X; then X c= dom F by Def13; hence Y c= dom F by A1,XBOOLE_1:1; let p be Real; assume A2: 0<=p & p<=1; let x,y be Real; assume x in Y & y in Y & p*x+(1-p)*y in Y; hence thesis by A1,A2,Def13; end; theorem for F be PartFunc of REAL,REAL, X be set, r be Real holds F is_convex_on X iff F-r is_convex_on X proof let F be PartFunc of REAL,REAL, X be set, r; thus F is_convex_on X implies F-r is_convex_on X proof assume A1: F is_convex_on X; dom F = dom(F-r) by Def12; hence A2: X c= dom(F-r) by A1,Def13; let p be Real; assume A3: 0<=p & p<=1; let x,y be Real; assume A4: x in X & y in X & p*x + (1-p)*y in X; then F.(p*x+(1-p)*y) <= p*F.x + (1-p)*F.y by A1,A3,Def13; then A5: F.(p*x+(1-p)*y) - r <= p*F.x + (1-p)*F.y -r by REAL_1:49; p*F.x + (1-p)*F.y - r = p*F.x + (1-p)*F.y - 1*r .= p*F.x + (1-p)*F.y - (p+(1-p))*r by XCMPLX_1:27 .= p*F.x + (1-p)*F.y - (p*r+(1-p)*r) by XCMPLX_1:8 .= p*F.x + (1-p)*F.y - p*r -(1-p)*r by XCMPLX_1:36 .= p*F.x -p*r + (1-p)*F.y -(1-p)*r by XCMPLX_1:29 .= p*(F.x -r) + (1-p)*F.y - (1-p)*r by XCMPLX_1:40 .= p*(F.x -r) + ((1-p)*F.y - (1-p)*r) by XCMPLX_1:29 .= p*(F.x -r) + (1-p)*(F.y - r) by XCMPLX_1:40 .= p*(F-r).x + (1-p)*(F.y - r) by A2,A4,Def12 .= p*(F-r).x + (1-p)*(F-r).y by A2,A4,Def12; hence thesis by A2,A4,A5,Def12; end; assume A6: F-r is_convex_on X; A7: dom F = dom(F-r) by Def12; hence A8: X c= dom F by A6,Def13; let p be Real; assume A9: 0<=p & p<=1; let x,y be Real; assume A10: x in X & y in X & p*x + (1-p)*y in X; then (F-r).(p*x+(1-p)*y) <= p*(F-r).x + (1-p)*(F-r).y by A6,A9,Def13; then A11: F.(p*x+(1-p)*y) -r <= p*(F-r).x + (1-p)*(F-r).y by A7,A8,A10,Def12; p*(F-r).x + (1-p)*(F-r).y = p*(F-r).x + (1-p)*(F.y - r) by A7,A8,A10,Def12 .= p*(F.x -r)+ (1-p)*(F.y - r) by A7,A8,A10,Def12 .= p*(F.x - r) + ((1-p)*F.y - (1-p)*r) by XCMPLX_1:40 .= p*(F.x - r) + (1-p)*F.y - (1-p)*r by XCMPLX_1:29 .= p*F.x - p*r + (1-p)*F.y - (1-p)*r by XCMPLX_1:40 .= p* F.x + (1-p)*F.y - p*r - (1-p)*r by XCMPLX_1:29 .= p* F.x + (1-p)*F.y - (p*r + (1-p)*r) by XCMPLX_1:36 .= p*F.x + (1-p)*F.y - (p+(1-p))*r by XCMPLX_1:8 .= p*F.x + (1-p)*F.y - 1*r by XCMPLX_1:27 .= p*F.x + (1-p)*F.y - r; hence thesis by A11,REAL_1:54; end; theorem for F be PartFunc of REAL,REAL, X be set, r be Real st 0<r holds F is_convex_on X iff r(#)F is_convex_on X proof let F be PartFunc of REAL,REAL, X be set, r; assume A1: 0<r; A2: dom F = dom(r(#)F) by SEQ_1:def 6; thus F is_convex_on X implies r(#)F is_convex_on X proof assume A3: F is_convex_on X; then A4: X c= dom F by Def13; thus X c= dom(r(#)F) by A2,A3,Def13; let p be Real; assume A5: 0<=p & p<=1; let x,y be Real; assume A6: x in X & y in X & p*x+(1-p)*y in X; then F.(p*x+(1-p)*y)<=p*F.x + (1-p)*F.y by A3,A5,Def13; then r* F.(p*x+(1-p)*y)<=r*(p*F.x + (1-p)*F.y) by A1,AXIOMS:25; then (r(#)F).(p*x+(1-p)*y)<=r*(p*F.x + (1-p)*F.y) by A2,A4,A6,SEQ_1:def 6; then (r(#)F).(p*x+(1-p)*y)<=r*(p*F.x) + r*((1-p)*F.y) by XCMPLX_1:8; then (r(#)F).(p*x+(1-p)*y)<=r*p*F.x + r*((1-p)*F.y) by XCMPLX_1:4; then (r(#)F).(p*x+(1-p)*y)<=r*p*F.x + (1-p)*r*F.y by XCMPLX_1:4; then (r(#)F).(p*x+(1-p)*y)<=p*(r*F.x) + (1-p)*r*F.y by XCMPLX_1:4; then (r(#)F).(p*x+(1-p)*y)<=p*(r*F.x) + (1-p)*(r*F.y) by XCMPLX_1:4; then (r(#)F).(p*x+(1-p)*y)<=p*(r(#)F).x + (1-p)*(r*F.y) by A2,A4,A6,SEQ_1: def 6; hence thesis by A2,A4,A6,SEQ_1:def 6; end; assume A7: r(#)F is_convex_on X; then A8: X c= dom(r(#)F) by Def13; hence X c= dom F by SEQ_1:def 6; let p be Real; assume A9: 0<=p & p<=1; let x,y be Real; assume A10: x in X & y in X & p*x+(1-p)*y in X; then (r(#)F).(p*x+(1-p)*y)<=p*(r(#)F).x + (1-p)*(r(#)F).y by A7,A9,Def13; then r*F.(p*x+(1-p)*y)<=p*(r(#)F).x + (1-p)*(r(#)F).y by A8,A10,SEQ_1:def 6; then r*F.(p*x+(1-p)*y)<=p*(r*F.x) + (1-p)*(r(#)F).y by A8,A10,SEQ_1:def 6; then r*F.(p*x+(1-p)*y)<=p*(r*F.x) + (1-p)*(r*F.y) by A8,A10,SEQ_1:def 6; then r*F.(p*x+(1-p)*y)<=p*r*F.x + (1-p)*(r*F.y) by XCMPLX_1:4; then r*F.(p*x+(1-p)*y)<=r*p*F.x + (1-p)*r*F.y by XCMPLX_1:4; then r*F.(p*x+(1-p)*y)<=r*(p*F.x) + r*(1-p)*F.y by XCMPLX_1:4; then r*F.(p*x+(1-p)*y)<=r*(p*F.x) + r*((1-p)*F.y) by XCMPLX_1:4; then r*F.(p*x+(1-p)*y)<=r*(p*F.x + (1-p)*F.y) by XCMPLX_1:8; then r*F.(p*x+(1-p)*y)/r <= r*(p*F.x + (1-p)*F.y)/r by A1,REAL_1:73; then F.(p*x+(1-p)*y) <= r*(p*F.x + (1-p)*F.y)/r by A1,XCMPLX_1:90; hence thesis by A1,XCMPLX_1:90; end; theorem for F be PartFunc of REAL,REAL, X be set st X c= dom F holds 0(#) F is_convex_on X proof let F be PartFunc of REAL,REAL, X be set; assume A1: X c= dom F; A2: dom F = dom(0(#)F) by SEQ_1:def 6; thus X c= dom(0(#)F) by A1,SEQ_1:def 6; let p be Real; assume 0<=p & p<=1; let x,y be Real; assume A3: x in X & y in X & p*x + (1-p)*y in X; then A4: (0(#)F).(p*x+(1-p)*y) = 0* F.(p*x+(1-p)*y) by A1,A2,SEQ_1:def 6 .= 0; p*(0(#)F).x + (1-p)*(0(#)F).y = p*(0* F.x) + (1-p)*(0(#)F).y by A1,A2,A3,SEQ_1:def 6 .= p*0 + (1-p)*(0* F.y) by A1,A2,A3,SEQ_1:def 6 .= 0 + 0; hence thesis by A4; end; theorem for F,G be PartFunc of REAL,REAL, X be set st F is_convex_on X & G is_convex_on X holds F+G is_convex_on X proof let F,G be PartFunc of REAL,REAL, X be set; assume A1: F is_convex_on X & G is_convex_on X; A2: dom(F+G) = dom F /\ dom G by SEQ_1:def 3; X c= dom F & X c= dom G by A1,Def13; hence A3: X c= dom(F+G) by A2,XBOOLE_1:19; let p be Real; assume A4: 0<=p & p<=1; let x,y be Real; assume A5: x in X & y in X & p*x + (1-p)*y in X; then F.(p*x+(1-p)*y) <= p*F.x + (1-p)*F.y & G.(p*x+(1-p)*y) <= p*G.x + (1-p) *G.y by A1,A4,Def13; then F.(p*x+(1-p)*y) + G.(p*x+(1-p)*y) <= p*F.x + (1-p)*F.y + (p*G.x + (1-p) *G.y) by REAL_1:55; then A6: (F+G).(p*x+(1-p)*y) <= p*F.x + (1-p)*F.y + (p*G.x + (1-p)*G.y) by A3,A5,SEQ_1:def 3; p*F.x+(1-p)*F.y + (p*G.x+(1-p)*G.y) = (p*F.x+(1-p)*F.y) + p*G.x + (1-p)*G.y by XCMPLX_1:1 .= (p*F.x+p*G.x) + (1-p)*F.y + (1-p)*G.y by XCMPLX_1:1 .= p*(F.x+G.x) + (1-p)*F.y + (1-p)*G.y by XCMPLX_1:8 .= p*(F+G).x + (1-p)*F.y + (1-p)*G.y by A3,A5,SEQ_1:def 3 .= p*(F+G).x + ((1-p)*F.y + (1-p)*G.y) by XCMPLX_1:1 .= p*(F+G).x + (1-p)*(F.y + G.y) by XCMPLX_1:8; hence thesis by A3,A5,A6,SEQ_1:def 3; end; theorem Th62: for F be PartFunc of REAL,REAL, X be set, r be Real st F is_convex_on X holds max+(F-r) is_convex_on X proof let F be PartFunc of REAL,REAL, X be set, r; assume A1: F is_convex_on X; A2: dom F = dom(F-r) by Def12; A3: dom(max+(F-r)) = dom(F-r) by Def10; hence X c= dom(max+(F-r)) by A1,A2,Def13; let p be Real; assume A4: 0<=p & p<=1; let x,y be Real; assume A5: x in X & y in X & p*x+(1-p)*y in X; then F.(p*x+(1-p)*y) <= p*F.x + (1-p)*F.y by A1,A4,Def13; then F.(p*x+(1-p)*y) -r <= p*F.x + (1-p)*F.y -r by REAL_1:49; then max(F.(p*x+(1-p)*y) -r,0) <= max(p*F.x + (1-p)*F.y -r,0) by Th7; then max+(F.(p*x+(1-p)*y) -r) <= max(p*F.x + (1-p)*F.y -r,0) by Def1; then A6: max+(F.(p*x+(1-p)*y) -r) <= max+(p*F.x + (1-p)*F.y -r) by Def1; A7: X c= dom F by A1,Def13; A8: p*F.x + (1-p)*F.y - r = p*F.x + (1-p)*F.y - 1*r .= p*F.x + (1-p)*F.y - (p+(1-p))*r by XCMPLX_1:27 .= p*F.x + (1-p)*F.y - (p*r+(1-p)*r) by XCMPLX_1:8 .= p*F.x + (1-p)*F.y - p*r -(1-p)*r by XCMPLX_1:36 .= p*F.x -p*r + (1-p)*F.y -(1-p)*r by XCMPLX_1:29 .= p*(F.x -r) + (1-p)*F.y - (1-p)*r by XCMPLX_1:40 .= p*(F.x -r) + ((1-p)*F.y - (1-p)*r) by XCMPLX_1:29 .= p*(F.x -r) + (1-p)*(F.y - r) by XCMPLX_1:40 .= p*(F-r).x + (1-p)*(F.y - r) by A2,A5,A7,Def12 .= p*(F-r).x + (1-p)*(F-r).y by A2,A5,A7,Def12; A9: max+(p*(F-r).x + (1-p)*(F-r).y)<= max+(p*(F-r).x) + max+((1-p)*(F-r).y) by Th5; 0+p<=1 by A4; then 0<=1-p by REAL_1:84; then max+(p*(F-r).x)= p* (max+ ((F-r).x)) & max+((1-p)*(F-r).y) = (1-p)*(max+ ((F-r).y)) by A4,Th4; then max+(F.(p*x+(1-p)*y) -r) <= p*(max+ ((F-r).x)) + (1-p)*(max+ ((F-r).y)) by A6,A8,A9,AXIOMS:22; then max+ ((F-r).(p*x+(1-p)*y)) <= p*(max+ ((F-r).x)) + (1-p)*(max+ ((F-r).y )) by A2,A5,A7,Def12; then (max+ (F-r)).(p*x+(1-p)*y) <= p*(max+ ((F-r).x)) + (1-p)*(max+ ((F-r).y )) by A2,A3,A5,A7,Def10; then (max+ (F-r)).(p*x+(1-p)*y) <= p*(max+ (F-r)).x + (1-p)*(max+ ((F-r).y)) by A2,A3,A5,A7,Def10; hence thesis by A2,A3,A5,A7,Def10; end; theorem for F be PartFunc of REAL,REAL, X be set st F is_convex_on X holds max+ F is_convex_on X proof let F be PartFunc of REAL,REAL, X be set; assume F is_convex_on X; then max+(F - 0) is_convex_on X by Th62; hence thesis by Th51; end; theorem Th64: id [#](REAL) is_convex_on REAL proof set i = id [#](REAL); A1: [#](REAL) = REAL by SUBSET_1:def 4; hence REAL c= dom i by FUNCT_1:34; let p be Real; assume 0<=p & p<=1; let x,y be Real; assume x in REAL & y in REAL & p*x+(1-p)*y in REAL; i.x = x & i.y = y & i.(p*x+(1-p)*y) = p*x+(1-p)*y by A1,FUNCT_1:34; hence thesis; end; theorem for r be Real holds max+(id [#](REAL) - r) is_convex_on REAL by Th62,Th64; definition let D be non empty set, F be PartFunc of D,REAL, X be set; assume A1: dom(F|X) is finite; func FinS(F,X) -> non-increasing FinSequence of REAL means :Def14: F|X, it are_fiberwise_equipotent; existence proof set x = dom(F|X); consider b be FinSequence such that A2: F|x, b are_fiberwise_equipotent by A1,RFINSEQ:18; x = dom F /\ X by FUNCT_1:68; then A3: F|x = (F|dom F)|X by RELAT_1:100 .=F|X by RELAT_1:97; rng(F|x) c= rng F & rng F c= REAL & rng(F|x) = rng b by A2,FUNCT_1:76,RFINSEQ:1; then reconsider b as FinSequence of REAL by FINSEQ_1:def 4; consider a be non-increasing FinSequence of REAL such that A4: b,a are_fiberwise_equipotent by RFINSEQ:35; take a; thus thesis by A2,A3,A4,RFINSEQ:2; end; uniqueness proof let g1,g2 be non-increasing FinSequence of REAL; assume F|X, g1 are_fiberwise_equipotent & F|X,g2 are_fiberwise_equipotent; then g1,g2 are_fiberwise_equipotent by RFINSEQ:2; hence g1=g2 by RFINSEQ:36; end; end; theorem Th66: for D be non empty set, F be PartFunc of D,REAL, X be set st dom(F|X) is finite holds FinS(F,dom(F|X)) = FinS(F,X) proof let D be non empty set, F be PartFunc of D,REAL, X be set; assume A1: dom(F|X) is finite; then A2: FinS(F,X), F|X are_fiberwise_equipotent by Def14; F|(dom(F|X)) = F|(dom F /\ X) by FUNCT_1:68 .= (F|dom F)|X by RELAT_1:100 .= F|X by RELAT_1:97; hence thesis by A1,A2,Def14; end; theorem Th67: for D be non empty set, F be PartFunc of D,REAL, X be set st dom(F|X) is finite holds FinS(F|X,X) = FinS(F,X) proof let D be non empty set, F be PartFunc of D,REAL, X be set; assume A1: dom(F|X) is finite; then A2: FinS(F,X), F|X are_fiberwise_equipotent by Def14; (F|X)|X = F|X by RELAT_1:101; hence thesis by A1,A2,Def14; end; definition let D be non empty set; let F be PartFunc of D,REAL; let X be finite set; redefine func F|X -> finite PartFunc of D,REAL; coherence proof F|X is finite; hence thesis; end; end; theorem Th68: for D be non empty set, d be Element of D, X be set, F be PartFunc of D,REAL st X is finite & d in dom(F|X) holds FinS(F,X\{d})^<*F.d*>, F|X are_fiberwise_equipotent proof for D be non empty set, X be finite set, F be PartFunc of D,REAL, x be set st x in dom(F|X) holds FinS(F,X\{x})^<*F.x*>, F|X are_fiberwise_equipotent proof let D be non empty set, X be finite set, F be PartFunc of D,REAL, x; set Y = X \ {x}; assume A1: x in dom(F|X); dom(F|Y) is finite & Y is finite; then A2: F|Y, FinS(F,Y) are_fiberwise_equipotent by Def14; set A = FinS(F,Y)^<* F.x *>; x in dom F /\ X by A1,FUNCT_1:68; then x in X & x in dom F by XBOOLE_0:def 3; then A3: {x} c= X & {x} c= dom F by ZFMISC_1:37; now let y; A4: card((F|Y)"{y}) = card(FinS(F,Y)"{y}) by A2,RFINSEQ:def 1; A5: Y misses {x} by XBOOLE_1:79; A6: (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 A5,XBOOLE_0:def 7 .= {}; A7: (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 A3,XBOOLE_1:12 .= (F|X)"{y} by FUNCT_1:139; A8: dom(F|{x}) = {x} by A3,RELAT_1:91; A9: dom<*F.x*> = {1} by FINSEQ_1:4,55; now per cases; case A10: y=F.x; A11: (F|{x})"{y} c= {x} by A8,RELAT_1:167; {x} c= (F|{x})"{y} proof let z be set; assume A12: z in {x}; then z=x by TARSKI:def 1; then y=(F|{x}).z & y in {y} by A8,A10,A12,FUNCT_1:68,TARSKI:def 1; hence z in (F|{x})"{y} by A8,A12,FUNCT_1:def 13; end; then (F|{x})"{y} = {x} by A11,XBOOLE_0:def 10; then A13: card((F|{x})"{y}) = 1 by CARD_1:79; A14: <*F.x*>"{y} c= {1} by A9,RELAT_1:167; {1} c= <*F.x*>"{y} proof let z be set; assume A15: z in {1}; then z=1 by TARSKI:def 1; then y=<*F.x*>.z & y in {y} by A10,FINSEQ_1:57,TARSKI:def 1; hence z in <*F.x*>"{y} by A9,A15,FUNCT_1:def 13; end; then <*F.x*>"{y} = {1} by A14,XBOOLE_0:def 10; hence card((F|{x})"{y}) = card(<*F.x*>"{y}) by A13,CARD_1:79; case A16: y <> F.x; A17: now assume A18: (F|{x})"{y} <> {}; consider z be Element of (F|{x})"{y}; A19: z in {x} & (F|{x}).z in {y} by A8,A18,FUNCT_1:def 13; then z=x & (F|{x}).z=y by TARSKI:def 1; hence contradiction by A8,A16,A19,FUNCT_1:68; end; now assume A20: <*F.x*>"{y} <> {}; consider z be Element of <*F.x*>"{y}; z in {1} & <*F.x*>.z in {y} by A9,A20,FUNCT_1:def 13; then z=1 & <*F.x*>.z=y by TARSKI:def 1; hence contradiction by A16,FINSEQ_1:57; end; hence card((F|{x})"{y}) = card(<*F.x*>"{y}) by A17; end; hence card((F|X)"{y}) = card((F|Y)"{y}) + card(<*F.x*>"{y}) - card {} by A6,A7,CARD_2:64 .= card(A"{y}) by A4,CARD_1:78,FINSEQ_3:63; end; hence thesis by RFINSEQ:def 1; end; hence thesis; end; theorem Th69: for D be non empty set, d be Element of D, X be set, F be PartFunc of D,REAL st dom(F|X) is finite & d in dom(F|X) holds FinS(F,X\{d})^<*F.d*>, F|X are_fiberwise_equipotent proof let D be non empty set, d be Element of D, X be set, F be PartFunc of D,REAL; set dx = dom(F|X); assume A1: dx is finite & d in dx; A2: F|dx = F|(dom F /\ X) by FUNCT_1:68 .=(F|dom F)|X by RELAT_1:100 .=F|X by RELAT_1:97; set Y = X \ {d}, dy = dom(F|Y); A3: {d} c= dx & dy=dom F /\ Y & dx=dom F /\ X by A1,FUNCT_1:68,ZFMISC_1:37; A4: dy = dx \ {d} proof thus dy c= dx \ {d} proof let y; assume y in dy; then A5: y in dom F & y in X \ {d} by A3,XBOOLE_0:def 3; then A6: y in X & not y in {d} by XBOOLE_0:def 4; then y in dx by A3,A5,XBOOLE_0:def 3; hence thesis by A6,XBOOLE_0:def 4; end; let y; assume y in dx \{d}; then A7: y in dx & not y in {d} by XBOOLE_0:def 4; then A8: y in dom F & y in X by A3,XBOOLE_0:def 3; then y in Y by A7,XBOOLE_0:def 4; hence thesis by A3,A8,XBOOLE_0:def 3; end; then A9: dy is finite by A1,FINSET_1:16; FinS(F,dx\{d})^<*F.d*>, F|X are_fiberwise_equipotent by A1,A2,Th68; hence FinS(F,X\{d})^<*F.d*>, F|X are_fiberwise_equipotent by A4,A9,Th66; end; theorem Th70: for D be non empty set, F be PartFunc of D,REAL, X be set, Y being finite set st Y = dom(F|X) holds len FinS(F,X) = card Y proof let D be non empty set, F be PartFunc of D,REAL, X be set; let Y be finite set; assume A1: Y = dom(F|X); then reconsider fx = F|X as finite Function by AMI_1:21; A2: Y = dom fx by A1; A3: FinS(F,X), F|X are_fiberwise_equipotent by A1,Def14; reconsider fs = dom FinS(F,X) as finite set; A4: dom FinS(F,X) = Seg len FinS(F,X) by FINSEQ_1:def 3; thus card Y = card fs by A2,A3,RFINSEQ:10 .= len FinS(F,X) by A4,FINSEQ_1:78; end; theorem Th71: for D be non empty set, F be PartFunc of D,REAL holds FinS(F,{}) = <*>REAL proof let D be non empty set, F be PartFunc of D,REAL; dom(F|{}) = dom F /\ {} by FUNCT_1:68 .= {}; then len FinS(F,{}) = 0 by Th70,CARD_1:78; hence thesis by FINSEQ_1:32; end; theorem Th72: for D be non empty set, F be PartFunc of D,REAL, d be Element of D st d in dom F holds FinS(F,{d}) = <* F.d *> proof let D be non empty set, F be PartFunc of D,REAL, d be Element of D; assume d in dom F; then {d} c= dom F by ZFMISC_1:37; then A1: {d} = dom F /\ {d} by XBOOLE_1:28 .= dom(F|{d}) by FUNCT_1:68; then A2: len FinS(F,{d}) = card {d} by Th70 .= 1 by CARD_1:79; FinS(F,{d}), F|{d} are_fiberwise_equipotent by A1,Def14; then A3: rng FinS(F,{d}) = rng(F|{d}) by RFINSEQ:1; rng(F|{d}) = {F.d} proof thus rng(F|{d}) c= {F.d} proof let x; assume x in rng(F|{d}); then consider e be Element of D such that A4: e in dom(F|{d}) & (F|{d}).e = x by PARTFUN1:26; e=d by A1,A4,TARSKI:def 1; then x=F.d by A4,FUNCT_1:68; hence thesis by TARSKI:def 1; end; let x; assume x in {F.d}; then A5: x=F.d & d in dom(F|{d}) by A1,TARSKI:def 1; then x=(F|{d}).d by FUNCT_1:68; hence thesis by A5,FUNCT_1:def 5; end; hence thesis by A2,A3,FINSEQ_1:56; end; theorem Th73: for D be non empty set, F be PartFunc of D,REAL, X be set, d be Element of D st dom(F|X) is finite & d in dom(F|X) & FinS(F,X).(len FinS(F,X)) = F.d holds FinS(F,X) = FinS(F,X\{d}) ^ <*F.d*> proof let D be non empty set, F be PartFunc of D,REAL, X be set, d be Element of D; set dx = dom(F|X), fx = FinS(F,X), fy = FinS(F,X \{d}); assume A1: dx is finite & d in dx & fx.(len fx) = F.d; then A2: fx, F|X are_fiberwise_equipotent by Def14; then A3: rng fx = rng(F|X) by RFINSEQ:1; fy ^ <*F.d*>, F|X are_fiberwise_equipotent by A1,Th69; then A4: fx, fy^<*F.d*> are_fiberwise_equipotent by A2,RFINSEQ:2; rng fx <> {} by A1,A3,FUNCT_1:12; then fx <> {} by FINSEQ_1:27; then len fx <> 0 & 0<=len fx by FINSEQ_1:25,NAT_1:18; then 0+1<=len fx by NAT_1:38; then max(0,len fx -1) = len fx - 1 by FINSEQ_2:4; then reconsider n=len fx - 1 as Nat by FINSEQ_2:5; len fx = n+1 by XCMPLX_1:27; then A5: fx = fx|n ^ <*F.d*> by A1,RFINSEQ:20; then A6: fy, fx|n are_fiberwise_equipotent by A4,RFINSEQ:14; fx|n is non-increasing by RFINSEQ:33; hence thesis by A5,A6,RFINSEQ:36; end; defpred P[Nat] means for D be non empty set, F be PartFunc of D,REAL, X be set for Y be set, Z be finite set st Z = dom(F|Y) & dom(F|X) is finite & Y c= X & $1 = card Z & (for d1,d2 be Element of D st d1 in dom(F|Y) & d2 in dom(F|(X\Y)) holds F.d1>= F.d2) holds FinS(F,X) = FinS(F,Y) ^ FinS(F,X \ Y); Lm3: P[0] proof let D be non empty set, F be PartFunc of D,REAL, X be set; let Y be set; let Z be finite set such that A1: Z = dom(F|Y); assume A2: dom(F|X) is finite & Y c= X & 0 = card Z & for d1,d2 be Element of D st d1 in dom(F|Y) & d2 in dom(F|(X\Y)) holds F.d1>=F.d2; A3: dom(F|X) = dom F /\ X & dom(F|Y) = dom F /\ Y & dom(F|(X\Y))=dom F /\(X\Y) by FUNCT_1:68; A4: dom(F|Y) = {} by A1,A2,CARD_2:59; then A5: FinS(F,Y) = FinS(F,{}) by Th66 .= {} by Th71; dom(F|(X\Y)) = dom(F|X) \ {} by A3,A4,XBOOLE_1:50 .= dom(F|X); then FinS(F,X\Y) = FinS(F,dom(F|X)) by A2,Th66 .= FinS(F,X) by A2,Th66; hence thesis by A5,FINSEQ_1:47; end; Lm4: for n st P[n] holds P[n+1] proof let n; assume A1: P[n]; let D be non empty set, F be PartFunc of D,REAL, X be set; let Y be set; set dx = dom(F|X), dxy = dom(F|(X\Y)), fy = FinS(F,Y), fxy = FinS(F,X\Y); let dy be finite set such that A2: dy = dom(F|Y) & dom(F|X) is finite & Y c= X & n+1 = card dy & for d1,d2 be Element of D st d1 in dom(F|Y) & d2 in dxy holds F.d1>=F.d2; A3: X\Y c= X by XBOOLE_1:36; A4: dx = dom F /\ X & dy = dom F /\ Y & dxy = dom F /\ (X\Y) by A2,FUNCT_1:68; then dy c= dx & dxy c= dx by A2,A3,XBOOLE_1:26; then A5: dy is finite & dxy is finite by A2,FINSET_1:13; then A6: F|Y, fy are_fiberwise_equipotent & F|(X\Y) ,fxy are_fiberwise_equipotent by A2,Def14; then A7: rng fy = rng(F|Y) & rng fxy = rng(F|(X\Y)) by RFINSEQ:1; 1<=n+1 proof 0<n+1 by NAT_1:19; then 0+1<=n+1 by NAT_1:38; hence thesis; end; then A8: len fy = n+1 & 1<=n+1 by A2,Th70; then A9: len fy in dom fy by FINSEQ_3:27; then fy.(len fy) in rng fy by FUNCT_1:def 5; then consider d be Element of D such that A10: d in dy & (F|Y).d = fy.(len fy) by A2,A7,PARTFUN1:26; A11: F.d = fy.(len fy) by A2,A10,FUNCT_1:68; set Yd = Y \ {d}, dyd = dom(F|Yd), xyd = dom(F|(X \ Yd)); A12: {d} c= dy & dyd = dom F /\ Yd & xyd = dom F /\ (X \ Yd) & d in Y & d in dom F by A4,A10,FUNCT_1:68,XBOOLE_0:def 3,ZFMISC_1:37; A13: dyd = dy \ {d} proof thus dyd c= dy \ {d} proof let y; assume y in dyd; then A14: y in dom F & y in Y \ {d} by A12,XBOOLE_0:def 3; then A15: y in Y & not y in {d} by XBOOLE_0:def 4; then y in dy by A4,A14,XBOOLE_0:def 3; hence thesis by A15,XBOOLE_0:def 4; end; let y; assume y in dy \{d}; then A16: y in dy & not y in {d} by XBOOLE_0:def 4; then A17: y in dom F & y in Y by A4,XBOOLE_0:def 3; then y in Yd by A16,XBOOLE_0:def 4; hence thesis by A12,A17,XBOOLE_0:def 3; end; then reconsider dyd as finite set; A18: card dyd = card dy - card {d} by A12,A13,CARD_2:63 .= n+1-1 by A2,CARD_1:79 .= n by XCMPLX_1:26; Yd c= Y by XBOOLE_1:36; then A19: Yd c= X by A2,XBOOLE_1:1; A20: {d} c= X & {d} c= Y & {d} c= dom F by A2,A12,ZFMISC_1:37; A21: X \ Yd = (X\Y) \/ X /\ {d} by XBOOLE_1:52 .= (X\Y) \/ {d} by A20,XBOOLE_1:28; then A22: xyd = dxy \/ dom F /\ {d} by A4,A12,XBOOLE_1:23 .= dxy \/ {d} by A20,XBOOLE_1:28; now let d1,d2 be Element of D; assume A23: d1 in dyd & d2 in xyd; then A24: d1 in dy & not d1 in {d} by A13,XBOOLE_0:def 4; now per cases by A22,A23,XBOOLE_0:def 2; case d2 in dxy; hence F.d1>=F.d2 by A2,A24; case d2 in {d}; then A25: d2 = d & d1<>d by A24,TARSKI:def 1; (F|Y).d1 in rng(F|Y) by A2,A24,FUNCT_1:def 5; then F.d1 in rng(F|Y) by A2,A24,FUNCT_1:68; then consider m such that A26: m in dom fy & fy.m = F.d1 by A7,FINSEQ_2:11; A27: 1<=m & m<=len fy by A26,FINSEQ_3:27; now per cases; case m = len fy; hence F.d1>=F.d2 by A2,A10,A25,A26,FUNCT_1:68; case m<> len fy; then m<len fy by A27,REAL_1:def 5; hence F.d1>=F.d2 by A9,A11,A25,A26,RFINSEQ:32; end; hence F.d1>=F.d2; end; hence F.d1>=F.d2; end; then A28: FinS(F,X) = FinS(F,Yd) ^ FinS(F,X \ Yd) by A1,A2,A18,A19; A29: (X \ Yd) \ {d} = X \ (Yd \/ {d}) by XBOOLE_1:41 .= X \ (Y \/ {d}) by XBOOLE_1:39 .= X \ Y by A20,XBOOLE_1:12; A30: xyd is finite by A5,A22,FINSET_1:14; d in {d} by TARSKI:def 1; then d in (X\Yd) by A21,XBOOLE_0:def 2; then d in xyd by A12,XBOOLE_0:def 3; then A31: fxy ^ <*F.d*>, F|(X\Yd) are_fiberwise_equipotent by A29,A30,Th69; fxy ^ <*F.d*>, <*F.d*> ^ fxy are_fiberwise_equipotent by RFINSEQ:15; then A32: <*F.d*>^fxy, F|(X\Yd) are_fiberwise_equipotent by A31,RFINSEQ:2; FinS(F,X\Yd), F|(X\Yd) are_fiberwise_equipotent by A30,Def14; then A33: <*F.d*>^fxy, FinS(F,X\Yd) are_fiberwise_equipotent by A32,RFINSEQ :2; <*F.d*>^fxy is non-increasing proof let n; assume A34: n in dom(<*F.d*>^fxy) & n+1 in dom(<*F.d*>^fxy); set xfy = <*F.d*>^fxy; set r = xfy.n, s = xfy.(n+1); A35: len <*F.d*> = 1 & <*F.d*>. 1 = F.d by FINSEQ_1:57; A36: 1<=n & n<=len xfy & 1<=n+1 & n+1<=len xfy by A34,FINSEQ_3:27; then max(0,n-1)=n-1 by FINSEQ_2:4; then reconsider n1=n-1 as Nat by FINSEQ_2:5; len xfy = 1 + len fxy by A35,FINSEQ_1:35; then A37: len fxy = len xfy - 1 by XCMPLX_1:26; then A38: n1<=len fxy by A36,REAL_1:49; A39: n1+1 = n by XCMPLX_1:27; then n1+1<=len fxy & n<n+1 by A36,A37,NAT_1:38,REAL_1:84; then A40: n1+1 in dom fxy & 1<n+1 by A36,A39,AXIOMS:22,FINSEQ_3:27; then A41: xfy.(n+1) = fxy.(n+1-1) by A35,A36,FINSEQ_1:37 .= fxy.(n1+1) by A39,XCMPLX_1:26; fxy.(n1+1) in rng fxy by A40,FUNCT_1:def 5; then consider d1 be Element of D such that A42: d1 in dxy & (F|(X\Y)).d1 = fxy.(n1+1) by A7,PARTFUN1:26; A43: F.d1 = fxy.(n1+1) by A42,FUNCT_1:68; A44: F.d>=F.d1 by A2,A10,A42; now per cases; suppose n = 1; hence r>=s by A41,A43,A44,FINSEQ_1:58; suppose n <> 1; then A45: 1<n by A36,REAL_1:def 5; then A46: xfy.n = fxy.n1 by A35,A36,FINSEQ_1:37; 1+1<=n by A45,NAT_1:38; then 1<=n1 by REAL_1:84; then n1 in dom fxy by A38,FINSEQ_3:27; hence r>=s by A40,A41,A46,RFINSEQ:def 4; end; hence r>=s; end; then <*F.d*>^fxy = FinS(F,X\Yd) by A33,RFINSEQ:36; then A47: FinS(F,X) = FinS(F,Yd)^<*F.d*> ^ fxy by A28,FINSEQ_1:45; F|Y, FinS(F,Yd)^<*F.d*> are_fiberwise_equipotent by A2,A10,Th69; then A48: FinS(F,Yd)^<*F.d*>, fy are_fiberwise_equipotent by A6,RFINSEQ:2; A49: fy = fy|n ^ <*F.d*> by A8,A11,RFINSEQ:20; then A50: FinS(F,Yd), fy|n are_fiberwise_equipotent by A48,RFINSEQ:14; fy|n is non-increasing by RFINSEQ:33; hence thesis by A47,A49,A50,RFINSEQ:36; end; theorem for D be non empty set, F be PartFunc of D,REAL, X,Y be set st dom(F|X) is finite & Y c= X & (for d1,d2 be Element of D st d1 in dom(F|Y) & d2 in dom(F|(X\Y)) holds F.d1>=F.d2) holds FinS(F,X) = FinS(F,Y) ^ FinS(F,X \ Y) proof let D be non empty set, F be PartFunc of D,REAL, X be set; A1: for n holds P[n] from Ind(Lm3,Lm4); let Y be set; assume A2: dom(F|X) is finite & Y c= X & for d1,d2 be Element of D st d1 in dom(F|Y) & d2 in dom(F|(X\Y)) holds F.d1>=F.d2; then F|Y c= F|X by RELAT_1:104; then dom(F|Y) c= dom(F|X) by RELAT_1:25; then reconsider dFY = dom(F|Y) as finite set by A2,FINSET_1:13; card dFY = card dFY; hence thesis by A1,A2; end; theorem Th75: for D be non empty set, F be PartFunc of D,REAL, r be Real, X be set, d be Element of D st dom(F|X) is finite & d in dom(F|X) holds FinS(F-r,X).(len FinS(F-r,X)) = (F-r).d iff FinS(F,X).(len FinS(F,X)) = F.d proof let D be non empty set, F be PartFunc of D,REAL, r be Real, X be set, d be Element of D; set dx = dom(F|X), drx = dom((F-r)|X), frx = FinS(F-r,X), fx = FinS(F,X); assume A1: dx is finite & d in dx; then reconsider dx as finite set; A2: drx = dom(F-r) /\ X by FUNCT_1:68 .= dom F /\ X by Def12 .= dx by FUNCT_1:68; then A3: len frx = card dx & len fx = card dx by Th70; A4: dom frx = Seg len frx & dom fx = Seg len fx by FINSEQ_1:def 3; fx, F|X are_fiberwise_equipotent & frx, (F-r)|X are_fiberwise_equipotent by A2,Def14; then A5: rng fx = rng(F|X) & rng frx = rng((F-r)|X) by RFINSEQ:1; A6: drx = dom(F-r) /\ X & dx = dom F /\ X by FUNCT_1:68; then A7: d in dom(F-r) by A1,A2,XBOOLE_0:def 3; then A8: (F-r).d = F.d - r by Def12; A9: (F|X).d in rng(F|X) by A1,FUNCT_1:def 5; rng fx <> {} by A1,A5,FUNCT_1:12; then fx <> {} by FINSEQ_1:27; then len fx <> 0 & 0<=len fx by FINSEQ_1:25,NAT_1:18; then 0+1<=len fx by NAT_1:38; then A10: len fx in dom fx by FINSEQ_3:27; F.d in rng(F|X) by A1,A9,FUNCT_1:68; then consider n such that A11: n in dom fx & fx.n = F.d by A5,FINSEQ_2:11; A12: 1<=n & n<=len fx by A11,FINSEQ_3:27; thus frx.(len frx) = (F-r).d implies fx.(len fx) = F.d proof assume that A13: frx.(len frx) = (F-r).d and A14: fx.(len fx) <> F.d; fx.(len fx) in rng fx by A10,FUNCT_1:def 5; then consider d1 be Element of D such that A15: d1 in dx & (F|X).d1 = fx.(len fx) by A5,PARTFUN1:26; A16: F.d1 = fx.(len fx) by A15,FUNCT_1:68; A17: d1 in dom(F-r) by A2,A6,A15,XBOOLE_0:def 3; ((F-r)|X).d1 = (F-r).d1 by A2,A15,FUNCT_1:68 .= F.d1 - r by A17,Def12; then F.d1-r in rng((F-r)|X) by A2,A15,FUNCT_1:def 5; then consider m such that A18: m in dom frx & frx.m = F.d1-r by A5,FINSEQ_2:11; A19: 1<=m & m<=len frx by A18,FINSEQ_3:27; n<len fx by A11,A12,A14,REAL_1:def 5; then A20: F.d>=F.d1 by A10,A11,A16,RFINSEQ:32; now per cases; case len frx = m; then F.d1+-r=F.d-r by A8,A13,A18,XCMPLX_0:def 8; then F.d1+-r=F.d+-r by XCMPLX_0:def 8; hence contradiction by A14,A16,XCMPLX_1:2; case len frx <>m; then m<len frx by A19,REAL_1:def 5; then F.d1-r>=F.d-r by A3,A4,A8,A10,A13,A18,RFINSEQ:32; then F.d1>=F.d by REAL_1:54; hence contradiction by A14,A16,A20,AXIOMS:21; end; hence contradiction; end; assume that A21: fx.(len fx) = F.d and A22: frx.(len frx) <> (F-r).d; frx.(len frx) in rng frx by A3,A4,A10,FUNCT_1:def 5; then consider d1 be Element of D such that A23: d1 in drx & ((F-r)|X).d1 = frx.(len frx) by A5,PARTFUN1:26; A24: d1 in dom(F-r) by A6,A23,XBOOLE_0:def 3; A25: frx.(len frx) = (F-r).d1 by A23,FUNCT_1:68 .= F.d1 - r by A24,Def12; (F|X).d1 = F.d1 by A2,A23,FUNCT_1:68; then F.d1 in rng(F|X) by A2,A23,FUNCT_1:def 5; then consider m such that A26: m in dom fx & fx.m = F.d1 by A5,FINSEQ_2:11; A27: 1<=m & m<=len fx by A26,FINSEQ_3:27; ((F-r)|X).d in rng((F-r)|X) by A1,A2,FUNCT_1:def 5; then (F-r).d in rng((F-r)|X) by A1,A2,FUNCT_1:68; then consider n1 be Nat such that A28: n1 in dom frx & frx.n1 = F.d -r by A5,A8,FINSEQ_2:11; 1<=n1 & n1<=len frx by A28,FINSEQ_3:27; then n1<len frx by A8,A22,A28,REAL_1:def 5; then F.d-r>=F.d1-r by A3,A4,A10,A25,A28,RFINSEQ:32; then A29: F.d>=F.d1 by REAL_1:54; now per cases; case len fx = m; hence contradiction by A7,A21,A22,A25,A26,Def12; case len fx <> m; then m<len fx by A27,REAL_1:def 5; then F.d1>=F.d by A10,A21,A26,RFINSEQ:32; hence contradiction by A8,A22,A25,A29,AXIOMS:21; end; hence contradiction; end; theorem Th76: for D be non empty set, F be PartFunc of D,REAL, r be Real, X be set, Z being finite set st Z = dom(F|X) holds FinS(F-r, X) = FinS(F,X) - (card Z |->r) proof let D be non empty set, F be PartFunc of D,REAL, r be Real; let X be set; let G be finite set such that A1: G = dom(F|X); defpred P[Nat] means for X be set, G being finite set st G = dom(F|X) & $1= card(G) holds FinS(F-r, X) = FinS(F,X) - (card(G)|->r); A2: P[0] proof let X be set, G be finite set; assume A3: G = dom(F|X); assume 0=card(G); then A4: dom(F|X) = {} by A3,CARD_2:59; then FinS(F,X) = FinS(F,{}) by Th66 .= <*>REAL by Th71; then A5: FinS(F,X) - (card(G)|->r) = <*>REAL by RVSUM_1:49; dom((F-r)|X) = dom(F-r) /\ X by FUNCT_1:68 .=dom F /\ X by Def12 .=dom(F|X) by FUNCT_1:68; hence FinS(F-r,X) = FinS(F-r,{}) by A4,Th66 .= FinS(F,X) - (card(G)|->r) by A5,Th71; end; A6: for n st P[n] holds P[n+1] proof let n; assume A7: P[n]; let X be set, G be finite set; assume A8: G = dom(F|X); assume A9: n+1= card(G); A10: dom((F-r)|X) = dom(F-r) /\ X by FUNCT_1:68 .=dom F /\ X by Def12 .=dom(F|X) by FUNCT_1:68; then A11: FinS(F-r,X), (F-r)|X are_fiberwise_equipotent by A8,Def14; then A12: rng FinS(F-r,X) = rng((F-r)|X) by RFINSEQ:1; 0<n+1 by NAT_1:19; then A13: 0+1<=n+1 by NAT_1:38; set frx = FinS(F-r,X), fx = FinS(F,X); A14: len frx = card G & len fx = card G by A8,A10,Th70; then len frx in dom frx by A9,A13,FINSEQ_3:27; then frx.(len frx) in rng frx by FUNCT_1:def 5; then consider d be Element of D such that A15: d in dom((F-r)|X) & ((F-r)|X).d = frx.(len frx) by A12,PARTFUN1:26; (F-r).d = frx.(len frx) by A15,FUNCT_1:68; then A16: fx.(len fx) = F.d by A8,A10,A15,Th75; set Y = X \ {d}, dx = dom(F|X), dy = dom(F|Y), fry = FinS(F-r,Y), fy = FinS(F,Y), n1r = (n+1) |-> r, nr = n |-> r; fx = fy ^ <*F.d*> & fx = fx|n ^ <*F.d*> by A8,A9,A10,A14,A15,A16,Th73,RFINSEQ:20; then A17: fy = fx|n by FINSEQ_1:46; (F-r).d = frx.(len frx) by A15,FUNCT_1:68; then A18: frx = frx|n ^ <*(F-r).d*> by A9,A14,RFINSEQ:20; A19: frx|n is non-increasing by RFINSEQ:33; fry^<*(F-r).d*>, (F-r)|X are_fiberwise_equipotent by A8,A10,A15,Th69; then fry^<*(F-r).d*>, frx are_fiberwise_equipotent by A11,RFINSEQ:2; then fry, frx|n are_fiberwise_equipotent by A18,RFINSEQ:14; then A20: fry = frx|n by A19,RFINSEQ:36; A21: {d} c= dx & dy=dom F /\ Y & dx=dom F /\ X & dom((F-r)|X) = dom(F-r) /\ X by A10,A15,FUNCT_1:68,ZFMISC_1:37; A22: dy = dx \ {d} proof thus dy c= dx \ {d} proof let y; assume y in dy; then A23: y in dom F & y in X \ {d} by A21,XBOOLE_0:def 3; then A24: y in X & not y in {d} by XBOOLE_0:def 4; then y in dx by A21,A23,XBOOLE_0:def 3; hence thesis by A24,XBOOLE_0:def 4; end; let y; assume y in dx \{d}; then A25: y in dx & not y in {d} by XBOOLE_0:def 4; then A26: y in dom F & y in X by A21,XBOOLE_0:def 3; then y in Y by A25,XBOOLE_0:def 4; hence thesis by A21,A26,XBOOLE_0:def 3; end; then reconsider dx,dy as finite set by A8,FINSET_1:16; A27: card dy = card dx - card {d} by A21,A22,CARD_2:63 .= n+1-1 by A8,A9,CARD_1:79 .= n by XCMPLX_1:26; then A28: fry = fy - nr by A7; d in dom(F-r) by A15,A21,XBOOLE_0:def 3; then (F-r).d = F.d - r by Def12; then A29: <*(F-r).d*> = <*F.d*> - <*r*> by RVSUM_1:50; A30: len n1r = n+1 & len nr = n by FINSEQ_2:69; A31: len fx = n+1 & len fy = n by A8,A9,A27,Th70; A32: fx - n1r = diffreal.:(fx,n1r) & fy - nr = diffreal.:(fy,nr) by RVSUM_1:def 6; then A33: len (fx - n1r) = n+1 by A30,A31,FINSEQ_2:86; A34: len (fy - nr) = n by A30,A31,A32,FINSEQ_2:86; A35: len <*F.d*> =1 & len <*r*> = 1 & <*F.d*>.1=F.d & <*r*>.1=r & <*F.d*> - <*r*>=diffreal.: (<*F.d*>,<*r*>) by FINSEQ_1:57,RVSUM_1:def 6; then A36: len (<*F.d*> - <*r*>) = 1 by FINSEQ_2:86; then A37: len ((fy - nr)^(<*F.d*> - <*r*>)) = n+1 by A34,FINSEQ_1:35; A38: dom fx = Seg len fx by FINSEQ_1:def 3; A39: dom(<*F.d*> - <*r*>)=dom(<*F.d*> - <*r*>) & dom(fy - nr)=Seg len(fy - nr) & n+1 in Seg(n+1) by FINSEQ_1:6,def 3; A40: n<n+1 & 1 in Seg 1 by FINSEQ_1:3,NAT_1:38; then A41: 1 in dom(<*F.d*> - <*r*>) by A36,FINSEQ_1:def 3; now let m; assume A42: m in Seg(n+1); per cases; suppose A43: m=n+1; then A44: n1r.m = r by A39,FINSEQ_2:70; A45: m in dom (fx - n1r) by A33,A42,FINSEQ_1:def 3; ((fy - nr)^(<*F.d*> - <*r*>)).m = (<*F.d*> - <*r*>).(n+1-n) by A34,A37,A40,A43,FINSEQ_1:37 .= (<*F.d*> - <*r*>).1 by XCMPLX_1:26 .= F.d - r by A35,A41,RVSUM_1:47; hence (fx - n1r).m = ((fy - nr)^(<*F.d*> - <*r*>)).m by A16,A31,A43,A44,A45,RVSUM_1:47; suppose A46: m<>n+1; A47: 1<=m & m<=n+1 by A42,FINSEQ_1:3; then m<n+1 by A46,REAL_1:def 5; then A48: m<=n by NAT_1:38; then A49: m in Seg n by A47,FINSEQ_1:3; then A50: ((fy - nr)^(<*F.d*> - <*r*>)).m = (fy - nr).m by A34,A39,FINSEQ_1:def 7; A51: nr.m = r by A49,FINSEQ_2:70; 1<=n & n<=n+1 by A47,A48,AXIOMS:22,NAT_1:29; then n in Seg(n+1) by FINSEQ_1:3; then A52: (fx|n).m = fx.m & m in dom fx & n1r.m=r by A31,A38,A42,A49,FINSEQ_2:70,RFINSEQ:19; reconsider s=fx.m as Real; A53: m in dom(fx - n1r) by A33,A42,FINSEQ_1:def 3; m in dom(fy - nr) by A34,A49,FINSEQ_1:def 3; hence ((fy - nr)^(<*F.d*> - <*r*>)).m = s-r by A17,A50,A51,A52,RVSUM_1:47 .=(fx - n1r).m by A52,A53,RVSUM_1:47; end; hence thesis by A9,A18,A20,A28,A29,A33,A37,FINSEQ_2:10; end; for n holds P[n] from Ind(A2,A6); hence thesis by A1; end; theorem for D be non empty set, F be PartFunc of D,REAL, X be set st dom(F|X) is finite & (for d be Element of D st d in dom(F|X) holds F.d>=0) holds FinS(max+ F, X) = FinS(F, X) proof let D be non empty set, F be PartFunc of D,REAL, X be set; assume A1: dom(F|X) is finite & for d be Element of D st d in dom(F|X) holds F.d>=0; now let d be Element of D; assume d in dom(F|X); then F.d>=0 & (F|X).d=F.d by A1,FUNCT_1:68; hence (F|X).d>=0; end; then A2: (F|X) = max+ (F|X) by Th49 .= (max+ F)|X by Th47; hence FinS(F,X) = FinS((max+ F)|X,X) by A1,Th67 .= FinS(max+ F,X) by A1,A2,Th67; end; theorem for D be non empty set, F be PartFunc of D,REAL, X be set, r be Real, Z be finite set st Z = dom(F|X) & rng(F|X) = {r} holds FinS(F, X) = card(Z) |-> r proof let D be non empty set, F be PartFunc of D,REAL, X be set, r be Real; let dx be finite set such that A1: dx = dom(F|X); set fx = FinS(F,X); assume A2: rng(F|X) = {r}; F|X, fx are_fiberwise_equipotent by A1,Def14; then A3: rng fx = {r} by A2,RFINSEQ:1; len fx = card dx & dom fx = Seg len fx by A1,Th70,FINSEQ_1:def 3; then fx = Seg(card dx) --> r by A3,FUNCOP_1:15; hence thesis by FINSEQ_2:def 2; end; theorem Th79: for D be non empty set, F be PartFunc of D,REAL, X,Y be set st dom(F|(X \/ Y)) is finite & X misses Y holds FinS(F,X \/ Y), FinS(F,X) ^ FinS(F,Y) are_fiberwise_equipotent proof let D be non empty set, F be PartFunc of D,REAL, X,Y be set; assume A1: dom(F|(X \/ Y)) is finite; Y c= X \/ Y by XBOOLE_1:7; then F|Y c= F|(X \/ Y) by RELAT_1:104; then dom(F|Y) c= dom(F|(X \/ Y)) by RELAT_1:25; then reconsider dfy = dom(F|Y) as finite set by A1,FINSET_1:13; defpred P[Nat] means for Y be set, Z being finite set st Z = dom(F|Y) & dom(F|(X \/ Y)) is finite & X /\ Y = {} & $1 = card Z holds FinS(F,X \/ Y), FinS(F,X) ^ FinS(F,Y) are_fiberwise_equipotent; A2: P[0] proof let Y be set, Z be finite set; assume A3: Z = dom(F|Y) & dom(F|(X \/ Y)) is finite & X /\ Y = {} & 0 = card Z; A4: dom(F|(X \/ Y)) = dom F /\ (X \/ Y) by FUNCT_1:68 .= dom F /\ X \/ dom F /\ Y by XBOOLE_1:23 .= dom(F|X) \/ dom F /\ Y by FUNCT_1:68 .= dom(F|X) \/ dom(F|Y) by FUNCT_1:68; then dom(F|X) c= dom(F|(X \/ Y)) & dom(F|Y) c= dom(F|(X \/ Y)) by XBOOLE_1: 7 ; then A5: dom(F|X) is finite & dom(F|Y) is finite by A3,FINSET_1:13; A6: dom(F|Y) = {} by A3,CARD_2:59; then FinS(F,X \/ Y) = FinS(F,dom(F|X)) by A3,A4,Th66 .= FinS(F,X) by A5,Th66 .= FinS(F,X)^<*>REAL by FINSEQ_1:47 .= FinS(F,X)^FinS(F,dom(F|Y)) by A6,Th71 .= FinS(F,X)^ FinS(F,Y) by A3,Th66; hence thesis; end; A7: for n st P[n] holds P[n+1] proof let n; assume A8: P[n]; let Y be set, Z be finite set; assume A9: Z = dom(F|Y) & dom(F|(X \/ Y)) is finite & X /\ Y = {} & n+1 = card Z; A10: dom(F|(X \/ Y)) = dom F /\ (X \/ Y) by FUNCT_1:68 .= dom F /\ X \/ dom F /\ Y by XBOOLE_1:23 .= dom(F|X) \/ dom F /\ Y by FUNCT_1:68 .= dom(F|X) \/ dom(F|Y) by FUNCT_1:68; consider x being Element of dom(F|Y); reconsider x as Element of D by A9,CARD_1:47,TARSKI:def 3; set y1 = Y\{x}; A11: y1 c= Y by XBOOLE_1:36; then X \/ y1 c= X \/ Y by XBOOLE_1:13; then dom F /\(X \/ y1) c= dom F /\ (X \/ Y) by XBOOLE_1:27; then dom(F|(X \/ y1)) c= dom F /\ (X \/ Y) by FUNCT_1:68; then dom(F|(X \/ y1)) c= dom(F|(X \/ Y)) by FUNCT_1:68; then A12: dom(F|(X \/ y1)) is finite by A9,FINSET_1:13; X /\ y1 c= X /\ Y by A11,XBOOLE_1:27; then A13: X /\ y1 = {} by A9,XBOOLE_1:3; A14: {x} c= dom(F|Y) by A9,CARD_1:47,ZFMISC_1:37; A15: dom(F|y1) = dom F /\ y1 & dom(F|Y)= dom F /\ Y by FUNCT_1:68; A16: dom(F|y1) = dom(F|Y) \ {x} proof thus dom(F|y1) c= dom(F|Y) \ {x} proof let y; assume y in dom(F|y1); then A17: y in dom F & y in Y \ {x} by A15,XBOOLE_0:def 3; then A18: y in Y & not y in {x} by XBOOLE_0:def 4; then y in dom(F|Y) by A15,A17,XBOOLE_0:def 3; hence thesis by A18,XBOOLE_0:def 4; end; let y; assume y in dom(F|Y) \{x}; then A19: y in dom(F|Y) & not y in {x} by XBOOLE_0:def 4; then A20: y in dom F & y in Y by A15,XBOOLE_0:def 3; then y in y1 by A19,XBOOLE_0:def 4; hence thesis by A15,A20,XBOOLE_0:def 3; end; then reconsider dFy = dom(F|y1) as finite set by A9,FINSET_1:16; card dFy = n+1 - card {x} by A9,A14,A16,CARD_2:63 .= n+1-1 by CARD_1:79 .= n by XCMPLX_1:26; then FinS(F,X \/ y1), FinS(F,X) ^ FinS(F,y1) are_fiberwise_equipotent by A8,A12,A13; then FinS(F,X \/ y1) ^<*F.x*>, FinS(F,X) ^ FinS(F,y1) ^ <*F.x*> are_fiberwise_equipotent by RFINSEQ:14; then A21: FinS(F,X \/ y1) ^<*F.x*>, FinS(F,X) ^ (FinS(F,y1) ^ <*F.x*>) are_fiberwise_equipotent by FINSEQ_1:45; A22: FinS(F,y1)^<*F.x*>, F|Y are_fiberwise_equipotent by A9,Th69,CARD_1:47; FinS(F,Y), F|Y are_fiberwise_equipotent by A9,Def14; then FinS(F,y1)^<*F.x*>,FinS(F,Y) are_fiberwise_equipotent by A22,RFINSEQ:2 ; then A23: FinS(F,y1)^<*F.x*> ^ FinS(F,X), FinS(F,Y) ^ FinS(F,X) are_fiberwise_equipotent by RFINSEQ:14; A24: FinS(F,X)^(FinS(F,y1)^<*F.x*>),FinS(F,y1)^<*F.x*> ^ FinS(F,X) are_fiberwise_equipotent & FinS(F,Y) ^ FinS(F,X), FinS(F,X) ^ FinS(F,Y) are_fiberwise_equipotent by RFINSEQ:15; then FinS(F,X)^(FinS(F,y1)^<*F.x*>), FinS(F,Y)^FinS(F,X) are_fiberwise_equipotent by A23,RFINSEQ:2; then FinS(F,X)^(FinS(F,y1)^<*F.x*>), FinS(F,X)^FinS(F,Y) are_fiberwise_equipotent by A24,RFINSEQ:2; then A25: FinS(F,X \/ y1) ^<*F.x*>, FinS(F,X) ^ FinS(F,Y) are_fiberwise_equipotent by A21,RFINSEQ:2; now assume A26: x in X; x in Y by A9,A15,CARD_1:47,XBOOLE_0:def 3; hence contradiction by A9,A26,XBOOLE_0:def 3; end; then X \ {x} = X by ZFMISC_1:65; then A27: (X \/ Y) \ {x} = X \/ y1 by XBOOLE_1:42; x in dom(F|(X \/ Y)) by A9,A10,CARD_1:47,XBOOLE_0:def 2; then A28: FinS(F,X \/ y1)^<*F.x*>, F|(X \/ Y) are_fiberwise_equipotent by A9,A27,Th69; FinS(F,X \/ Y), F|(X \/ Y) are_fiberwise_equipotent by A9,Def14; then FinS(F,X \/ y1)^<*F.x*>, FinS(F,X \/ Y) are_fiberwise_equipotent by A28,RFINSEQ:2; hence thesis by A25,RFINSEQ:2; end; A29: for n holds P[n] from Ind(A2,A7); assume A30: X /\ Y = {}; card dfy = card dfy; hence thesis by A1,A29,A30; end; definition let D be non empty set, F be PartFunc of D,REAL, X be set; func Sum(F,X) -> Real equals :Def15: Sum(FinS(F,X)); correctness; end; theorem Th80: for D be non empty set, F be PartFunc of D,REAL, X be set, r be Real st dom(F|X) is finite holds Sum(r(#)F,X) = r * Sum(F,X) proof let D be non empty set, F be PartFunc of D,REAL, X be set, r be Real; assume A1: dom(F|X) is finite; then reconsider FX = F|X as finite Function by AMI_1:21; set x = dom(F|X); consider b be FinSequence such that A2: F|x, b are_fiberwise_equipotent by A1,RFINSEQ:18; x = dom F /\ X by FUNCT_1:68; then A3: F|x = (F|dom F)|X by RELAT_1:100 .=F|X by RELAT_1:97; rng(F|x) c= rng F & rng F c= REAL & rng(F|x) = rng b by A2,FUNCT_1:76,RFINSEQ:1; then reconsider b as FinSequence of REAL by FINSEQ_1:def 4; F|X, FinS(F,X) are_fiberwise_equipotent by A1,Def14; then b, FinS(F,X) are_fiberwise_equipotent by A2,A3,RFINSEQ:2; then A4: Sum b = Sum FinS(F,X) by RFINSEQ:22 .= Sum(F,X) by Def15; A5: dom((r(#)F)|X) = dom(r(#)F) /\ X by FUNCT_1:68 .= dom F /\ X by SEQ_1:def 6 .= dom(F|X) by FUNCT_1:68; A6: rng(r*b) c=REAL & rng((r(#)F)|X) c= REAL & rng b c=REAL & rng(F|X) c= REAL; A7: rng b = rng(F|X) by A2,A3,RFINSEQ:1; dom((r(#)F)|X) = dom(r(#)(F|X)) by RFUNCT_1:65 .= dom(F|X) by SEQ_1:def 6; then reconsider rFX = (r(#)F)|X as finite Function by A1,AMI_1:21; now let x be Real; r*b = (r multreal) * b by RVSUM_1:def 7; then A8: len(r*b) = len b by FINSEQ_2:37; now per cases; case A9: not x in rng(r*b); then A10: (r*b)"{x} = {} by Lm2; now assume x in rng((r(#)F)|X); then x in rng(r(#)(F|X)) by RFUNCT_1:65; then consider d be Element of D such that A11: d in dom(r(#)(F|X)) & (r(#)(F|X)).d = x by PARTFUN1:26; A12: x=r*(F|X).d & d in dom(F|X) by A11,SEQ_1:def 6; then (F|X).d in rng(F|X) by FUNCT_1:def 5; then consider n such that A13: n in dom b & b.n=(F|X).d by A7,FINSEQ_2:11; A14: n in dom (r*b) by A8,A13,FINSEQ_3:31; x=(r*b).n by A12,A13,RVSUM_1:66; hence contradiction by A9,A14,FUNCT_1:def 5; end; hence card((r*b)"{x}) = card(rFX"{x}) by A10,Lm2; case x in rng(r*b); then consider n such that A15: n in dom(r*b) & (r*b).n = x by FINSEQ_2:11; reconsider p=b.n as Real; A16: x = r*p by A15,RVSUM_1:66; now per cases; case A17: r=0; then A18: (r*b)"{x} = dom b by A16,RFINSEQ:38; dom(FX) =(r(#)(F|X))"{x} by A16,A17,Th9 .=((r(#)F)|X)"{x} by RFUNCT_1:65; hence card((r*b)"{x}) = card(rFX"{x}) by A2,A3,A18,RFINSEQ:10; case A19: r<>0; then A20: (r*b)"{x} = b"{x/r} by RFINSEQ:37; ((r(#)F)|X)"{x} = (r(#)(F|X))"{x} by RFUNCT_1:65 .= (FX)"{x/r} by A19,Th8; hence card((r*b)"{x}) = card(rFX"{x}) by A2,A3,A6,A20,RFINSEQ:11; end; hence card((r*b)"{x}) = card(rFX"{x}); end; hence card((r*b)"{x}) = card(rFX"{x}); end; then A21: r*b , (r(#)F)|X are_fiberwise_equipotent by A6,RFINSEQ:11; (r(#)F)|X, FinS(r(#)F,X) are_fiberwise_equipotent by A1,A5,Def14; then A22: r*b, FinS(r(#)F,X) are_fiberwise_equipotent by A21,RFINSEQ:2; thus Sum(r(#)F,X) = Sum FinS(r(#)F,X) by Def15 .= Sum(r*b) by A22,RFINSEQ:22 .= r* Sum(F,X) by A4,RVSUM_1:117; end; theorem Th81: for D be non empty set, F,G be PartFunc of D,REAL, X be set, Y being finite set st Y = dom(F|X) & dom(F|X) = dom(G|X) holds Sum(F+G,X) = Sum(F,X) + Sum(G,X) proof let D be non empty set; let F,G be PartFunc of D,REAL, X be set, Y be finite set such that A1: Y = dom(F|X); defpred P[Nat] means for F,G be PartFunc of D,REAL, X be set, Y being finite set st card(Y) = $1 & Y = dom(F|X) & dom(F|X) = dom(G|X) holds Sum(F+G,X) = Sum(F,X) + Sum(G,X); A2: P[0] proof let F,G be PartFunc of D,REAL, X be set, Y be finite set; assume A3: card(Y) = 0 & Y = dom(F|X) & dom(F|X) = dom(G|X); then dom(F|X) = {} & dom(G|X) = {} by CARD_2:59; then A4: rng(F|X) = {} & rng(G|X) = {} by RELAT_1:65; FinS(F,X), F|X are_fiberwise_equipotent by A3,Def14; then rng FinS(F,X) = {} by A4,RFINSEQ:1; then FinS(F,X) = <*> REAL by FINSEQ_1:27; then A5: Sum(F,X) = 0 by Def15,RVSUM_1:102; FinS(G,X), G|X are_fiberwise_equipotent by A3,Def14; then rng FinS(G,X) = {} by A4,RFINSEQ:1; then FinS(G,X) = <*> REAL by FINSEQ_1:27; then A6: Sum(F,X) + Sum(G,X) = 0+0 by A5,Def15,RVSUM_1:102; (F+G)|X = F|X + G|X by RFUNCT_1:60; then A7: dom((F+G)|X) = dom(F|X) /\ dom(G|X) by SEQ_1:def 3 .= {} by A3,CARD_2:59; then A8: rng ((F+G)|X) = {} & dom((F+G)|X) is finite by RELAT_1:65; FinS(F+G,X), (F+G)|X are_fiberwise_equipotent by A7,Def14; then rng FinS(F+G,X) = {} by A8,RFINSEQ:1; then FinS(F+G,X) = <*> REAL by FINSEQ_1:27; hence thesis by A6,Def15,RVSUM_1:102; end; A9: for n st P[n] holds P[n+1] proof let n; assume A10: P[n]; let F,G be PartFunc of D,REAL, X be set, dx be finite set; set gx = dom(G|X); assume A11: card(dx) = n+1 & dx = dom(F|X) & dom(F|X) = dom(G|X); consider x being Element of dx; reconsider x as Element of D by A11,CARD_1:47,TARSKI:def 3; set Y = X\{x}, dy = dom(F|Y), gy = dom(G|Y); A12: {x} c= dx & dy=dom F /\ Y & dx=dom F /\ X & gy= dom G /\ Y & gx=dom G /\ X by A11,CARD_1:47,FUNCT_1:68,ZFMISC_1:37; then A13: x in dom F & x in X & x in dom G by A11,CARD_1:47,XBOOLE_0:def 3; then {x} c= X & x in dom F /\ dom G by XBOOLE_0:def 3,ZFMISC_1:37; then A14: x in dom(F+G) by SEQ_1:def 3; then x in dom(F+G) /\ X by A13,XBOOLE_0:def 3; then A15: x in dom ((F+G)|X) by FUNCT_1:68; A16: dom((F+G)|X) = dom(F|X + G|X) by RFUNCT_1:60 .= dx /\ gx by A11,SEQ_1:def 3; A17: dy = dx \ {x} proof thus dy c= dx \ {x} proof let y; assume y in dy; then A18: y in dom F & y in X \ {x} by A12,XBOOLE_0:def 3; then A19: y in X & not y in {x} by XBOOLE_0:def 4; then y in dx by A12,A18,XBOOLE_0:def 3; hence thesis by A19,XBOOLE_0:def 4; end; let y; assume y in dx \{x}; then A20: y in dx & not y in {x} by XBOOLE_0:def 4; then A21: y in dom F & y in X by A12,XBOOLE_0:def 3; then y in Y by A20,XBOOLE_0:def 4; hence thesis by A12,A21,XBOOLE_0:def 3; end; then reconsider dy as finite set; A22: card(dy) = card(dx) - card {x} by A12,A17,CARD_2:63 .=n+1-1 by A11,CARD_1:79 .= n by XCMPLX_1:26; dy = gy proof thus dy c= gy proof let y; assume y in dy; then A23: y in dom F & y in Y by A12,XBOOLE_0:def 3; then y in X & not y in {x} by XBOOLE_0:def 4; then y in gx by A11,A12,A23,XBOOLE_0:def 3; then y in dom G by A12,XBOOLE_0:def 3; hence thesis by A12,A23,XBOOLE_0:def 3; end; let y; assume y in gy; then A24: y in dom G & y in Y by A12,XBOOLE_0:def 3; then y in X & not y in {x} by XBOOLE_0:def 4; then y in dx by A11,A12,A24,XBOOLE_0:def 3; then y in dom F by A12,XBOOLE_0:def 3; hence thesis by A12,A24,XBOOLE_0:def 3; end; then A25: Sum(F+G,Y) = Sum(F,Y) + Sum(G,Y) by A10,A22; A26: FinS(F,Y)^<*F.x*>, F|X are_fiberwise_equipotent by A11,Th69,CARD_1:47; FinS(F,X), F|X are_fiberwise_equipotent by A11,Def14; then A27: FinS(F,Y)^<*F.x*>, FinS(F,X) are_fiberwise_equipotent by A26,RFINSEQ:2; A28: Sum(F,X) = Sum(FinS(F,X)) by Def15 .= Sum (FinS(F,Y) ^ <*F.x*>) by A27,RFINSEQ:22 .= Sum FinS(F,Y) + F.x by RVSUM_1:104 .= Sum(F,Y) + F.x by Def15; A29: FinS(G,Y)^<*G.x*>, G|X are_fiberwise_equipotent by A11,Th69,CARD_1:47; FinS(G,X), G|X are_fiberwise_equipotent by A11,Def14; then A30: FinS(G,Y)^<*G.x*>, FinS(G,X) are_fiberwise_equipotent by A29,RFINSEQ:2; A31: FinS(F+G,Y)^<*(F+G).x*>, (F+G)|X are_fiberwise_equipotent by A15,A16,Th69; FinS(F+G,X), (F+G)|X are_fiberwise_equipotent by A16,Def14; then A32: FinS(F+G,Y) ^ <*(F+G).x*>, FinS(F+G,X) are_fiberwise_equipotent by A31,RFINSEQ:2; Sum(G,X) = Sum(FinS(G,X)) by Def15 .= Sum (FinS(G,Y)^<*G.x*>) by A30,RFINSEQ:22 .= Sum FinS(G,Y) + G.x by RVSUM_1:104 .= Sum(G,Y) + G.x by Def15; hence Sum(F,X)+ Sum(G,X) = Sum(F,Y) + F.x + Sum(G,Y) + G.x by A28,XCMPLX_1: 1 .= Sum(F+G,Y) + F.x + G.x by A25,XCMPLX_1:1 .= Sum FinS(F+G,Y) + F.x + G.x by Def15 .= Sum FinS(F+G,Y) + (F.x + G.x) by XCMPLX_1:1 .= Sum FinS(F+G,Y) + (F+G).x by A14,SEQ_1:def 3 .= Sum(FinS(F+G,Y)^<*(F+G).x*>) by RVSUM_1:104 .= Sum(FinS(F+G,X)) by A32,RFINSEQ:22 .= Sum(F+G,X) by Def15; end; A33: for n holds P[n] from Ind(A2,A9); assume A34: dom(F|X) = dom(G|X); card(Y)=card(Y); hence thesis by A1,A33,A34; end; theorem for D be non empty set, F,G be PartFunc of D,REAL, X be set st dom(F|X) is finite & dom(F|X) = dom(G|X) holds Sum(F-G,X) = Sum(F,X) - Sum (G,X) proof let D be non empty set, F,G be PartFunc of D,REAL, X be set; assume A1: dom(F|X) is finite & dom(F|X) = dom(G|X); A2: dom(((-1)(#)G)|X) = dom((-1)(#)G) /\ X by FUNCT_1:68 .= dom G /\ X by SEQ_1:def 6 .= dom(G|X) by FUNCT_1:68; F-G = F + -G by RFUNCT_1:40 .= F+(-1)(#)G by RFUNCT_1:38; hence Sum(F-G,X) = Sum(F,X) + Sum((-1)(#)G,X) by A1,A2,Th81 .= Sum(F,X) +(-1)* Sum(G,X) by A1,Th80 .= Sum(F,X) + - Sum(G,X) by XCMPLX_1:180 .= Sum(F,X) - Sum(G,X) by XCMPLX_0:def 8; end; theorem for D be non empty set, F be PartFunc of D,REAL, X be set, r be Real, Y being finite set st Y = dom(F|X) holds Sum(F-r,X) = Sum(F,X) - r*card(Y) proof let D be non empty set, F be PartFunc of D,REAL, X be set, r be Real; set fx = FinS(F,X); let Y be finite set; assume A1: Y = dom(F|X); set dr = card(Y) |-> r; A2: FinS(F-r,X) = fx - dr by A1,Th76; len fx = card(Y) & len dr = card(Y) by A1,Th70,FINSEQ_2:69; then reconsider xf = fx, rd = dr as Element of (card(Y))-tuples_on REAL by FINSEQ_2:110; thus Sum(F-r,X) = Sum (xf - rd) by A2,Def15 .= Sum xf - Sum rd by RVSUM_1:120 .= Sum fx - card(Y) * r by RVSUM_1:110 .= Sum(F,X) - r*card(Y) by Def15; end; theorem for D be non empty set, F be PartFunc of D,REAL holds Sum(F,{}) = 0 proof let D be non empty set, F be PartFunc of D,REAL; thus Sum(F,{}) = Sum FinS(F,{}) by Def15 .= 0 by Th71,RVSUM_1:102; end; theorem for D be non empty set, F be PartFunc of D,REAL, d be Element of D st d in dom F holds Sum(F,{d}) = F.d proof let D be non empty set, F be PartFunc of D,REAL, d be Element of D; assume A1: d in dom F; thus Sum(F,{d}) = Sum FinS(F,{d}) by Def15 .= Sum <*F.d*> by A1,Th72 .= F.d by RVSUM_1:103; end; theorem for D be non empty set, F be PartFunc of D,REAL, X,Y be set st dom(F|(X \/ Y)) is finite & X misses Y holds Sum(F, X \/ Y) = Sum(F,X) + Sum (F,Y) proof let D be non empty set, F be PartFunc of D,REAL, X,Y be set; assume dom(F|(X \/ Y)) is finite & X misses Y; then A1: FinS(F,X \/ Y), FinS(F,X) ^ FinS(F,Y) are_fiberwise_equipotent by Th79; thus Sum(F, X \/ Y) = Sum FinS(F,X \/ Y) by Def15 .= Sum (FinS(F,X) ^ FinS(F,Y)) by A1,RFINSEQ:22 .= Sum FinS(F,X) + Sum (FinS(F,Y)) by RVSUM_1:105 .= Sum(F,X) + Sum (FinS(F,Y)) by Def15 .= Sum(F,X) + Sum(F,Y) by Def15; end; theorem for D be non empty set, F be PartFunc of D,REAL, X,Y be set st dom(F|(X \/ Y)) is finite & dom(F|X) misses dom(F|Y) holds Sum(F, X \/ Y) = Sum(F,X) + Sum(F,Y) proof let D be non empty set, F be PartFunc of D,REAL, X,Y be set; assume A1: dom(F|(X \/ Y)) is finite & dom(F|X) misses dom(F|Y); A2: dom(F|(X \/ Y)) = dom F /\ (X \/ Y) by FUNCT_1:68 .= dom F /\ X \/ dom F /\ Y by XBOOLE_1:23 .= dom(F|X) \/ dom F /\ Y by FUNCT_1:68 .= dom(F|X) \/ dom(F|Y) by FUNCT_1:68; then dom(F|X) c= dom(F|(X \/ Y)) & dom(F|Y) c= dom(F|(X \/ Y)) by XBOOLE_1:7 ; then dom(F|X) is finite & dom(F|Y) is finite by A1,FINSET_1:13; then A3: FinS(F,X \/ Y) = FinS(F,dom(F|(X \/ Y))) & FinS(F,X) = FinS(F,dom(F| X)) & FinS(F,Y) = FinS(F,dom(F|Y)) by A1,Th66; dom(F| dom(F|(X \/ Y))) = dom F /\ dom(F|(X \/ Y)) by FUNCT_1:68 .= dom F /\ (dom F /\ (X \/ Y)) by FUNCT_1:68 .= dom F /\ dom F /\ (X \/ Y) by XBOOLE_1:16 .= dom(F|(X \/ Y)) by FUNCT_1:68; then A4: FinS(F,X \/ Y), FinS(F,X) ^ FinS(F,Y) are_fiberwise_equipotent by A1,A2,A3,Th79; thus Sum(F, X \/ Y) = Sum FinS(F,X \/ Y) by Def15 .= Sum (FinS(F,X) ^ FinS(F,Y)) by A4,RFINSEQ:22 .= Sum FinS(F,X) + Sum (FinS(F,Y)) by RVSUM_1:105 .= Sum(F,X) + Sum (FinS(F,Y)) by Def15 .= Sum(F,X) + Sum(F,Y) by Def15; end;

Back to top