:: Properties of Partial Functions from a Domain to the Set of Real Numbers
:: by Jaros{\l}aw Kotowicz and Yuji Sakai
::
:: Received March 15, 1993
:: Copyright (c) 1993-2012 Association of Mizar Users


begin

definition
let r be real number ;
func max+ r ->  Real equals :: RFUNCT_3:def 1
 max (r,0);
correctness
coherence
max (r,0) is Real;
by XREAL_0:def_1;
func max- r ->  Real equals :: RFUNCT_3:def 2
 max ((- r),0);
correctness
coherence
max ((- r),0) is Real;
by XREAL_0:def_1;
end;

:: deftheorem  defines max+ RFUNCT_3:def_1_:_
 for r being real number holds max+ r = max (r,0);

:: deftheorem  defines max- RFUNCT_3:def_2_:_
 for r being real number holds max- r = max ((- r),0);

theorem Th1: :: RFUNCT_3:1
for r being real number holds r = (max+ r) - (max- r)
proofend;

theorem Th2: :: RFUNCT_3:2
for r being real number holds abs r = (max+ r) + (max- r)
proofend;

theorem Th3: :: RFUNCT_3:3
for r being real number holds 2 * (max+ r) = r + (abs r)
proofend;

theorem Th4: :: RFUNCT_3:4
for r, s being real number st 0 <= r holds
max+ (r * s) = r * (max+ s)
proofend;

theorem Th5: :: RFUNCT_3:5
for r, s being real number holds max+ (r + s) <= (max+ r) + (max+ s)
proofend;

Lm1:  for n being Element of NAT
for D being non empty set
for f being FinSequence of D st len f <= n holds
f | n = f
proofend;

Lm2:  for f being Function
for x being set st not x in rng f holds
f " {x} = {}
proofend;

begin

::
:: Partial Functions from a Domain to the Set of Real Numbers
::
theorem Th6: :: RFUNCT_3:6
for D being non empty set
for F being PartFunc of D,REAL
for r, s being real number st r <> 0 holds
F " {(s / r)} = (r (#) F) " {s}
proofend;

theorem Th7: :: RFUNCT_3:7
for D being non empty set
for F being PartFunc of D,REAL holds (0 (#) F) " {0} = dom F
proofend;

theorem Th8: :: RFUNCT_3:8
for D being non empty set
for F being PartFunc of D,REAL
for r being Real st 0 < r holds
(abs F) " {r} = F " {(- r),r}
proofend;

theorem Th9: :: RFUNCT_3:9
for D being non empty set
for F being PartFunc of D,REAL holds (abs F) " {0} = F " {0}
proofend;

theorem Th10: :: RFUNCT_3:10
for D being non empty set
for F being PartFunc of D,REAL
for r being Real st r < 0 holds
(abs F) " {r} = {}
proofend;

theorem Th11: :: RFUNCT_3:11
for D, C being non empty set
for F being PartFunc of D,REAL
for G being PartFunc of C,REAL
for r being Real st r <> 0 holds
( F,G are_fiberwise_equipotent iff r (#) F,r (#) G are_fiberwise_equipotent )
proofend;

theorem :: RFUNCT_3:12
for D, C being non empty set
for F being PartFunc of D,REAL
for G being PartFunc of C,REAL holds
( F,G are_fiberwise_equipotent iff - F, - G are_fiberwise_equipotent )
proofend;

theorem :: RFUNCT_3:13
for D, C being non empty set
for F being PartFunc of D,REAL
for G being PartFunc of C,REAL st F,G are_fiberwise_equipotent holds
abs F, abs G are_fiberwise_equipotent
proofend;

definition
let X, Y be set ;
mode PartFunc-set of X,Y ->  set  means :Def3: :: RFUNCT_3:def 3
 for x being Element of it holds x is PartFunc of X,Y;
existence
 ex b1 being set st
for x being Element of b1 holds x is PartFunc of X,Y
proofend;
end;

:: deftheorem Def3 defines PartFunc-set RFUNCT_3:def_3_:_
 for X, Y being set
for b3 being set holds
( b3 is PartFunc-set of X,Y iff for x being Element of b3 holds x is PartFunc of X,Y );

registration
let X, Y be set ;
cluster non empty for PartFunc-set of X,Y;
existence
 not for b1 being PartFunc-set of X,Y holds b1 is empty
proofend;
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 ;
:: original:PFuncs
redefine func PFuncs (X,Y) ->  PartFunc-set of X,Y;
coherence
 PFuncs (X,Y) is PartFunc-set of X,Y
proofend;
let P be non empty PartFunc-set of X,Y;
:: original:Element
redefine mode Element of P ->  PartFunc of X,Y;
coherence
 for b1 being Element of P holds b1 is PartFunc of X,Y by Def3;
end;

definition
let D, C be non empty set ;
let X be Subset of D;
let c be Element of C;
:: original:-->
redefine funcX --> c ->  Element of PFuncs (D,C);
coherence
 X --> c is Element of PFuncs (D,C)
proofend;
end;

:: awaryjne, A.T.
registration
let D be non empty set ;
let E be real-membered set ;
cluster  ->  real-valued for Element of PFuncs (D,E);
coherence
 for b1 being Element of PFuncs (D,E) holds b1 is real-valued ;
end;

definition
let D be non empty set ;
let E be real-membered set ;
let F1, F2 be Element of PFuncs (D,E);
:: original:+
redefine funcF1 + F2 ->  Element of PFuncs (D,REAL);
coherence
 F1 + F2 is Element of PFuncs (D,REAL)
proofend;
:: original:-
redefine funcF1 - F2 ->  Element of PFuncs (D,REAL);
coherence
 F1 - F2 is Element of PFuncs (D,REAL)
proofend;
:: original:(#)
redefine funcF1 (#) F2 ->  Element of PFuncs (D,REAL);
coherence
 F1 (#) F2 is Element of PFuncs (D,REAL)
proofend;
:: original:/
redefine funcF1 / F2 ->  Element of PFuncs (D,REAL);
coherence
 F1 / F2 is Element of PFuncs (D,REAL)
proofend;
end;

definition
let D be non empty set ;
let E be real-membered set ;
let F be Element of PFuncs (D,E);
:: original:|.
redefine func abs F ->  Element of PFuncs (D,REAL);
coherence
 |.F.| is Element of PFuncs (D,REAL)
proofend;
:: original:-
redefine func - F ->  Element of PFuncs (D,REAL);
coherence
 - F is Element of PFuncs (D,REAL)
proofend;
:: original:^
redefine funcF ^  ->  Element of PFuncs (D,REAL);
coherence
 F ^ is Element of PFuncs (D,REAL)
proofend;
end;

definition
let D be non empty set ;
let E be real-membered set ;
let F be Element of PFuncs (D,E);
let r be real number ;
:: original:(#)
redefine funcr (#) F ->  Element of PFuncs (D,REAL);
coherence
 r (#) F is Element of PFuncs (D,REAL)
proofend;
end;

definition
let D be non empty set ;
func addpfunc D ->  BinOp of (PFuncs (D,REAL)) means :Def4: :: RFUNCT_3:def 4
 for F1, F2 being Element of PFuncs (D,REAL) holds it . (F1,F2) = F1 + F2;
existence
 ex b1 being BinOp of (PFuncs (D,REAL)) st
for F1, F2 being Element of PFuncs (D,REAL) holds b1 . (F1,F2) = F1 + F2
proofend;
uniqueness
 for b1, b2 being BinOp of (PFuncs (D,REAL)) st ( for F1, F2 being Element of PFuncs (D,REAL) holds b1 . (F1,F2) = F1 + F2 ) &amp; ( for F1, F2 being Element of PFuncs (D,REAL) holds b2 . (F1,F2) = F1 + F2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines addpfunc RFUNCT_3:def_4_:_
 for D being non empty set
for b2 being BinOp of (PFuncs (D,REAL)) holds
( b2 = addpfunc D iff for F1, F2 being Element of PFuncs (D,REAL) holds b2 . (F1,F2) = F1 + F2 );

theorem Th14: :: RFUNCT_3:14
for D being non empty set holds addpfunc D is commutative
proofend;

theorem Th15: :: RFUNCT_3:15
for D being non empty set holds addpfunc D is associative
proofend;

theorem Th16: :: RFUNCT_3:16
for D being non empty set holds ([#] D) --> 0 is_a_unity_wrt addpfunc D
proofend;

theorem Th17: :: RFUNCT_3:17
for D being non empty set holds the_unity_wrt (addpfunc D) = ([#] D) --> 0
proofend;

theorem Th18: :: RFUNCT_3:18
for D being non empty set holds addpfunc D is having_a_unity
proofend;

definition
let D be non empty set ;
let f be FinSequence of PFuncs (D,REAL);
func Sum f ->  Element of PFuncs (D,REAL) equals :: RFUNCT_3:def 5
(addpfunc D) $$ f;
correctness
coherence
(addpfunc D) $$ f is Element of PFuncs (D,REAL);
;
end;

:: deftheorem  defines Sum RFUNCT_3:def_5_:_
 for D being non empty set
for f being FinSequence of PFuncs (D,REAL) holds Sum f = (addpfunc D) $$ f;

theorem Th19: :: RFUNCT_3:19
for D being non empty set holds Sum (<*> (PFuncs (D,REAL))) = ([#] D) --> 0
proofend;

theorem Th20: :: RFUNCT_3:20
for D being non empty set
for f being FinSequence of PFuncs (D,REAL)
for G being Element of PFuncs (D,REAL) holds Sum (f ^ <*G*>) = (Sum f) + G
proofend;

theorem Th21: :: RFUNCT_3:21
for D being non empty set
for f1, f2 being FinSequence of PFuncs (D,REAL) holds Sum (f1 ^ f2) = (Sum f1) + (Sum f2)
proofend;

theorem :: RFUNCT_3:22
for D being non empty set
for f being FinSequence of PFuncs (D,REAL)
for G being Element of PFuncs (D,REAL) holds Sum (<*G*> ^ f) = G + (Sum f)
proofend;

theorem Th23: :: RFUNCT_3:23
for D being non empty set
for G1, G2 being Element of PFuncs (D,REAL) holds Sum <*G1,G2*> = G1 + G2
proofend;

theorem :: RFUNCT_3:24
for D being non empty set
for G1, G2, G3 being Element of PFuncs (D,REAL) holds Sum <*G1,G2,G3*> = (G1 + G2) + G3
proofend;

theorem :: RFUNCT_3:25
for D being non empty set
for f, g being FinSequence of PFuncs (D,REAL) st f,g are_fiberwise_equipotent holds
Sum f = Sum g
proofend;

definition
let D be non empty set ;
let f be FinSequence;
func CHI (f,D) ->  FinSequence of PFuncs (D,REAL) means :Def6: :: RFUNCT_3:def 6
( len it = len f &amp; ( for n being Element of NAT st n in dom it holds
it . n = chi ((f . n),D) ) );
existence
 ex b1 being FinSequence of PFuncs (D,REAL) st
( len b1 = len f &amp; ( for n being Element of NAT st n in dom b1 holds
b1 . n = chi ((f . n),D) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of PFuncs (D,REAL) st len b1 = len f &amp; ( for n being Element of NAT st n in dom b1 holds
b1 . n = chi ((f . n),D) ) &amp; len b2 = len f &amp; ( for n being Element of NAT st n in dom b2 holds
b2 . n = chi ((f . n),D) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines CHI RFUNCT_3:def_6_:_
 for D being non empty set
for f being FinSequence
for b3 being FinSequence of PFuncs (D,REAL) holds
( b3 = CHI (f,D) iff ( len b3 = len f &amp; ( for n being Element of NAT st n in dom b3 holds
b3 . n = chi ((f . n),D) ) ) );

definition
let D be non empty set ;
let f be FinSequence of PFuncs (D,REAL);
let R be FinSequence of REAL ;
funcR (#) f ->  FinSequence of PFuncs (D,REAL) means :Def7: :: RFUNCT_3:def 7
( len it = min ((len R),(len f)) &amp; ( for n being Element of NAT st n in dom it holds
for F being PartFunc of D,REAL
for r being Real st r = R . n &amp; F = f . n holds
it . n = r (#) F ) );
existence
 ex b1 being FinSequence of PFuncs (D,REAL) st
( len b1 = min ((len R),(len f)) &amp; ( for n being Element of NAT st n in dom b1 holds
for F being PartFunc of D,REAL
for r being Real st r = R . n &amp; F = f . n holds
b1 . n = r (#) F ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of PFuncs (D,REAL) st len b1 = min ((len R),(len f)) &amp; ( for n being Element of NAT st n in dom b1 holds
for F being PartFunc of D,REAL
for r being Real st r = R . n &amp; F = f . n holds
b1 . n = r (#) F ) &amp; len b2 = min ((len R),(len f)) &amp; ( for n being Element of NAT st n in dom b2 holds
for F being PartFunc of D,REAL
for r being Real st r = R . n &amp; F = f . n holds
b2 . n = r (#) F ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines (#) RFUNCT_3:def_7_:_
 for D being non empty set
for f being FinSequence of PFuncs (D,REAL)
for R being FinSequence of REAL
for b4 being FinSequence of PFuncs (D,REAL) holds
( b4 = R (#) f iff ( len b4 = min ((len R),(len f)) &amp; ( for n being Element of NAT st n in dom b4 holds
for F being PartFunc of D,REAL
for r being Real st r = R . n &amp; F = f . n holds
b4 . n = r (#) F ) ) );

definition
let D be non empty set ;
let f be FinSequence of PFuncs (D,REAL);
let d be Element of D;
funcf # d ->  FinSequence of REAL  means :Def8: :: RFUNCT_3:def 8
( len it = len f &amp; ( for n being Element of NAT st n in dom it holds
it . n = (f . n) . d ) );
existence
 ex b1 being FinSequence of REAL st
( len b1 = len f &amp; ( for n being Element of NAT st n in dom b1 holds
b1 . n = (f . n) . d ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of REAL st len b1 = len f &amp; ( for n being Element of NAT st n in dom b1 holds
b1 . n = (f . n) . d ) &amp; len b2 = len f &amp; ( for n being Element of NAT st n in dom b2 holds
b2 . n = (f . n) . d ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines # RFUNCT_3:def_8_:_
 for D being non empty set
for f being FinSequence of PFuncs (D,REAL)
for d being Element of D
for b4 being FinSequence of REAL holds
( b4 = f # d iff ( len b4 = len f &amp; ( for n being Element of NAT st n in dom b4 holds
b4 . n = (f . n) . d ) ) );

definition
let D, C be non empty set ;
let f be FinSequence of PFuncs (D,C);
let d be Element of D;
predd is_common_for_dom f means :Def9: :: RFUNCT_3:def 9
 for n being Element of NAT st n in dom f holds
d in dom (f . n);
end;

:: deftheorem Def9 defines is_common_for_dom RFUNCT_3:def_9_:_
 for D, C being non empty set
for f being FinSequence of PFuncs (D,C)
for d being Element of D holds
( d is_common_for_dom f iff for n being Element of NAT st n in dom f holds
d in dom (f . n) );

theorem Th26: :: RFUNCT_3:26
for D, C being non empty set
for f being FinSequence of PFuncs (D,C)
for d being Element of D
for n being Element of NAT st d is_common_for_dom f &amp; n <> 0 holds
d is_common_for_dom f | n
proofend;

theorem :: RFUNCT_3:27
for D, C being non empty set
for f being FinSequence of PFuncs (D,C)
for d being Element of D
for n being Element of NAT st d is_common_for_dom f holds
d is_common_for_dom f /^ n
proofend;

theorem Th28: :: RFUNCT_3:28
for D being non empty set
for d being Element of D
for f being FinSequence of PFuncs (D,REAL) st len f <> 0 holds
( d is_common_for_dom f iff d in dom (Sum f) )
proofend;

theorem Th29: :: RFUNCT_3:29
for D being non empty set
for f being FinSequence of PFuncs (D,REAL)
for d being Element of D
for n being Element of NAT holds (f | n) # d = (f # d) | n
proofend;

theorem Th30: :: RFUNCT_3:30
for D being non empty set
for f being FinSequence
for d being Element of D holds d is_common_for_dom CHI (f,D)
proofend;

theorem Th31: :: RFUNCT_3:31
for D being non empty set
for d being Element of D
for f being FinSequence of PFuncs (D,REAL)
for R being FinSequence of REAL st d is_common_for_dom f holds
d is_common_for_dom R (#) f
proofend;

theorem :: RFUNCT_3:32
for D being non empty set
for f being FinSequence
for R being FinSequence of REAL
for d being Element of D holds d is_common_for_dom R (#) (CHI (f,D)) by Th30, Th31;

theorem :: RFUNCT_3:33
for D being non empty set
for d being Element of D
for f being FinSequence of PFuncs (D,REAL) st d is_common_for_dom f holds
(Sum f) . d = Sum (f # d)
proofend;

definition
let D be non empty set ;
let F be PartFunc of D,REAL;
func max+ F ->  PartFunc of D,REAL means :Def10: :: RFUNCT_3:def 10
( dom it = dom F &amp; ( for d being Element of D st d in dom it holds
it . d = max+ (F . d) ) );
existence
 ex b1 being PartFunc of D,REAL st
( dom b1 = dom F &amp; ( for d being Element of D st d in dom b1 holds
b1 . d = max+ (F . d) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of D,REAL st dom b1 = dom F &amp; ( for d being Element of D st d in dom b1 holds
b1 . d = max+ (F . d) ) &amp; dom b2 = dom F &amp; ( for d being Element of D st d in dom b2 holds
b2 . d = max+ (F . d) ) holds
b1 = b2
proofend;
func max- F ->  PartFunc of D,REAL means :Def11: :: RFUNCT_3:def 11
( dom it = dom F &amp; ( for d being Element of D st d in dom it holds
it . d = max- (F . d) ) );
existence
 ex b1 being PartFunc of D,REAL st
( dom b1 = dom F &amp; ( for d being Element of D st d in dom b1 holds
b1 . d = max- (F . d) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of D,REAL st dom b1 = dom F &amp; ( for d being Element of D st d in dom b1 holds
b1 . d = max- (F . d) ) &amp; dom b2 = dom F &amp; ( for d being Element of D st d in dom b2 holds
b2 . d = max- (F . d) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines max+ RFUNCT_3:def_10_:_
 for D being non empty set
for F, b3 being PartFunc of D,REAL holds
( b3 = max+ F iff ( dom b3 = dom F &amp; ( for d being Element of D st d in dom b3 holds
b3 . d = max+ (F . d) ) ) );

:: deftheorem Def11 defines max- RFUNCT_3:def_11_:_
 for D being non empty set
for F, b3 being PartFunc of D,REAL holds
( b3 = max- F iff ( dom b3 = dom F &amp; ( for d being Element of D st d in dom b3 holds
b3 . d = max- (F . d) ) ) );

theorem :: RFUNCT_3:34
for D being non empty set
for F being PartFunc of D,REAL holds
( F = (max+ F) - (max- F) &amp; abs F = (max+ F) + (max- F) &amp; 2 (#) (max+ F) = F + (abs F) )
proofend;

theorem Th35: :: RFUNCT_3:35
for D being non empty set
for F being PartFunc of D,REAL
for r being Real st 0 < r holds
F " {r} = (max+ F) " {r}
proofend;

theorem Th36: :: RFUNCT_3:36
for D being non empty set
for F being PartFunc of D,REAL holds F " (left_closed_halfline 0) = (max+ F) " {0}
proofend;

theorem Th37: :: RFUNCT_3:37
for D being non empty set
for F being PartFunc of D,REAL
for d being Element of D holds 0 <= (max+ F) . d
proofend;

theorem Th38: :: RFUNCT_3:38
for D being non empty set
for F being PartFunc of D,REAL
for r being Real st 0 < r holds
F " {(- r)} = (max- F) " {r}
proofend;

theorem Th39: :: RFUNCT_3:39
for D being non empty set
for F being PartFunc of D,REAL holds F " (right_closed_halfline 0) = (max- F) " {0}
proofend;

theorem Th40: :: RFUNCT_3:40
for D being non empty set
for F being PartFunc of D,REAL
for d being Element of D holds 0 <= (max- F) . d
proofend;

theorem :: RFUNCT_3:41
for D, C being non empty set
for F being PartFunc of D,REAL
for G being PartFunc of C,REAL st F,G are_fiberwise_equipotent holds
max+ F, max+ G are_fiberwise_equipotent
proofend;

theorem :: RFUNCT_3:42
for D, C being non empty set
for F being PartFunc of D,REAL
for G being PartFunc of C,REAL st F,G are_fiberwise_equipotent holds
max- F, max- G are_fiberwise_equipotent
proofend;

registration
let D be non empty set ;
let F be finite PartFunc of D,REAL;
cluster max+ F ->  finite ;
coherence
 max+ F is finite
proofend;
cluster max- F ->  finite ;
coherence
 max- F is finite
proofend;
end;

theorem :: RFUNCT_3:43
for D, C being non empty set
for F being finite PartFunc of D,REAL
for G being finite PartFunc of C,REAL st max+ F, max+ G are_fiberwise_equipotent &amp; max- F, max- G are_fiberwise_equipotent holds
F,G are_fiberwise_equipotent
proofend;

theorem Th44: :: RFUNCT_3:44
for D being non empty set
for F being PartFunc of D,REAL
for X being set holds (max+ F) | X = max+ (F | X)
proofend;

theorem :: RFUNCT_3:45
for D being non empty set
for F being PartFunc of D,REAL
for X being set holds (max- F) | X = max- (F | X)
proofend;

theorem Th46: :: RFUNCT_3:46
for D being non empty set
for F being PartFunc of D,REAL st ( for d being Element of D st d in dom F holds
F . d >= 0 ) holds
max+ F = F
proofend;

theorem :: RFUNCT_3:47
for D being non empty set
for F being PartFunc of D,REAL st ( for d being Element of D st d in dom F holds
F . d <= 0 ) holds
max- F = - F
proofend;

theorem Th48: :: RFUNCT_3:48
for D being non empty set
for F being PartFunc of D,REAL holds F - 0 = F
proofend;

theorem :: RFUNCT_3:49
for D being non empty set
for F being PartFunc of D,REAL
for r being Real
for X being set holds (F | X) - r = (F - r) | X
proofend;

theorem Th50: :: RFUNCT_3:50
for D being non empty set
for F being PartFunc of D,REAL
for r, s being Real holds F " {(s + r)} = (F - r) " {s}
proofend;

theorem :: RFUNCT_3:51
for D, C being non empty set
for F being PartFunc of D,REAL
for G being PartFunc of C,REAL
for r being Real holds
( F,G are_fiberwise_equipotent iff F - r,G - r are_fiberwise_equipotent )
proofend;

definition
let F be PartFunc of REAL,REAL;
let X be set ;
predF is_convex_on X means :Def12: :: RFUNCT_3:def 12
( X c= dom F &amp; ( for p being Real st 0 <= p &amp; p <= 1 holds
for r, s being Real st r in X &amp; s in X &amp; (p * r) + ((1 - p) * s) in X holds
F . ((p * r) + ((1 - p) * s)) <= (p * (F . r)) + ((1 - p) * (F . s)) ) );
end;

:: deftheorem Def12 defines is_convex_on RFUNCT_3:def_12_:_
 for F being PartFunc of REAL,REAL
for X being set holds
( F is_convex_on X iff ( X c= dom F &amp; ( for p being Real st 0 <= p &amp; p <= 1 holds
for r, s being Real st r in X &amp; s in X &amp; (p * r) + ((1 - p) * s) in X holds
F . ((p * r) + ((1 - p) * s)) <= (p * (F . r)) + ((1 - p) * (F . s)) ) ) );

theorem Th52: :: RFUNCT_3:52
for a, b being Real
for F being PartFunc of REAL,REAL holds
( F is_convex_on [.a,b.] iff ( [.a,b.] c= dom F &amp; ( for p being Real st 0 <= p &amp; p <= 1 holds
for r, s being Real st r in [.a,b.] &amp; s in [.a,b.] holds
F . ((p * r) + ((1 - p) * s)) <= (p * (F . r)) + ((1 - p) * (F . s)) ) ) )
proofend;

theorem :: RFUNCT_3:53
for a, b being Real
for F being PartFunc of REAL,REAL holds
( F is_convex_on [.a,b.] iff ( [.a,b.] c= dom F &amp; ( for x1, x2, x3 being Real st x1 in [.a,b.] &amp; x2 in [.a,b.] &amp; x3 in [.a,b.] &amp; x1 < x2 &amp; x2 < x3 holds
((F . x1) - (F . x2)) / (x1 - x2) <= ((F . x2) - (F . x3)) / (x2 - x3) ) ) )
proofend;

theorem :: RFUNCT_3:54
for F being PartFunc of REAL,REAL
for X, Y being set st F is_convex_on X &amp; Y c= X holds
F is_convex_on Y
proofend;

theorem :: RFUNCT_3:55
for F being PartFunc of REAL,REAL
for X being set
for r being Real holds
( F is_convex_on X iff F - r is_convex_on X )
proofend;

theorem :: RFUNCT_3:56
for F being PartFunc of REAL,REAL
for X being set
for r being Real st 0 < r holds
( F is_convex_on X iff r (#) F is_convex_on X )
proofend;

theorem :: RFUNCT_3:57
for F being PartFunc of REAL,REAL
for X being set st X c= dom F holds
0 (#) F is_convex_on X
proofend;

theorem :: RFUNCT_3:58
for F, G being PartFunc of REAL,REAL
for X being set st F is_convex_on X &amp; G is_convex_on X holds
F + G is_convex_on X
proofend;

theorem Th59: :: RFUNCT_3:59
for F being PartFunc of REAL,REAL
for X being set
for r being Real st F is_convex_on X holds
max+ (F - r) is_convex_on X
proofend;

theorem :: RFUNCT_3:60
for F being PartFunc of REAL,REAL
for X being set st F is_convex_on X holds
max+ F is_convex_on X
proofend;

theorem Th61: :: RFUNCT_3:61
id ([#] REAL) is_convex_on REAL
proofend;

theorem :: RFUNCT_3:62
for r being Real holds max+ ((id ([#] REAL)) - r) is_convex_on REAL by Th59, Th61;

definition
let D be non empty set ;
let F be PartFunc of D,REAL;
let X be set ;
assume A1: dom (F | X) is finite ;
func FinS (F,X) ->  non-increasing FinSequence of REAL  means :Def13: :: RFUNCT_3:def 13
F | X,it are_fiberwise_equipotent ;
existence
 ex b1 being non-increasing FinSequence of REAL st F | X,b1 are_fiberwise_equipotent
proofend;
uniqueness
 for b1, b2 being non-increasing FinSequence of REAL st F | X,b1 are_fiberwise_equipotent &amp; F | X,b2 are_fiberwise_equipotent holds
b1 = b2 by CLASSES1:76, RFINSEQ:23;
end;

:: deftheorem Def13 defines FinS RFUNCT_3:def_13_:_
 for D being non empty set
for F being PartFunc of D,REAL
for X being set st dom (F | X) is finite holds
for b4 being non-increasing FinSequence of REAL holds
( b4 = FinS (F,X) iff F | X,b4 are_fiberwise_equipotent );

theorem Th63: :: RFUNCT_3:63
for D being non empty set
for F being PartFunc of D,REAL
for X being set st dom (F | X) is finite holds
FinS (F,(dom (F | X))) = FinS (F,X)
proofend;

theorem Th64: :: RFUNCT_3:64
for D being non empty set
for F being PartFunc of D,REAL
for X being set st dom (F | X) is finite holds
FinS ((F | X),X) = FinS (F,X)
proofend;

theorem Th65: :: RFUNCT_3:65
for D being non empty set
for d being Element of D
for X being set
for F being PartFunc of D,REAL st X is finite &amp; d in dom (F | X) holds
(FinS (F,(X \ {d}))) ^ <*(F . d)*>,F | X are_fiberwise_equipotent
proofend;

theorem Th66: :: RFUNCT_3:66
for D being non empty set
for d being Element of D
for X being set
for F being PartFunc of D,REAL st dom (F | X) is finite &amp; d in dom (F | X) holds
(FinS (F,(X \ {d}))) ^ <*(F . d)*>,F | X are_fiberwise_equipotent
proofend;

theorem Th67: :: RFUNCT_3:67
for D being non empty set
for F being PartFunc of D,REAL
for X being set
for Y being finite set st Y = dom (F | X) holds
len (FinS (F,X)) = card Y
proofend;

theorem Th68: :: RFUNCT_3:68
for D being non empty set
for F being PartFunc of D,REAL holds FinS (F,{}) = <*> REAL
proofend;

theorem Th69: :: RFUNCT_3:69
for D being non empty set
for F being PartFunc of D,REAL
for d being Element of D st d in dom F holds
FinS (F,{d}) = <*(F . d)*>
proofend;

theorem Th70: :: RFUNCT_3:70
for D being non empty set
for F being PartFunc of D,REAL
for X being set
for d being Element of D st dom (F | X) is finite &amp; d in dom (F | X) &amp; (FinS (F,X)) . (len (FinS (F,X))) = F . d holds
FinS (F,X) = (FinS (F,(X \ {d}))) ^ <*(F . d)*>
proofend;

defpred S1[ Element of NAT ] means  for D being non empty set
for F being PartFunc of D,REAL
for X, Y being set
for Z being finite set st Z = dom (F | Y) &amp; dom (F | X) is finite &amp; Y c= X &amp; $1 = card Z &amp; ( for d1, d2 being Element of D st d1 in dom (F | Y) &amp; d2 in dom (F | (X \ Y)) holds
F . d1 >= F . d2 ) holds
FinS (F,X) = (FinS (F,Y)) ^ (FinS (F,(X \ Y)));

Lm3:  S1[ 0 ]
proofend;

Lm4:  for n being Element of NAT st S1[n] holds
S1[n + 1]
proofend;

theorem :: RFUNCT_3:71
for D being non empty set
for F being PartFunc of D,REAL
for X, Y being set st dom (F | X) is finite &amp; Y c= X &amp; ( for d1, d2 being Element of D st d1 in dom (F | Y) &amp; d2 in dom (F | (X \ Y)) holds
F . d1 >= F . d2 ) holds
FinS (F,X) = (FinS (F,Y)) ^ (FinS (F,(X \ Y)))
proofend;

theorem Th72: :: RFUNCT_3:72
for D being non empty set
for F being PartFunc of D,REAL
for r being Real
for X being set
for d being Element of D st dom (F | X) is finite &amp; 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 )
proofend;

theorem Th73: :: RFUNCT_3:73
for D being non empty set
for F being PartFunc of D,REAL
for r being Real
for X being set
for Z being finite set st Z = dom (F | X) holds
FinS ((F - r),X) = (FinS (F,X)) - ((card Z) |-> r)
proofend;

theorem :: RFUNCT_3:74
for D being non empty set
for F being PartFunc of D,REAL
for X being set st dom (F | X) is finite &amp; ( for d being Element of D st d in dom (F | X) holds
F . d >= 0 ) holds
FinS ((max+ F),X) = FinS (F,X)
proofend;

theorem :: RFUNCT_3:75
for D being non empty set
for F being PartFunc of D,REAL
for X being set
for r being Real
for Z being finite set st Z = dom (F | X) &amp; rng (F | X) = {r} holds
FinS (F,X) = (card Z) |-> r
proofend;

theorem Th76: :: RFUNCT_3:76
for D being non empty set
for F being PartFunc of D,REAL
for X, Y being set st dom (F | (X \/ Y)) is finite &amp; X misses Y holds
FinS (F,(X \/ Y)),(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent
proofend;

definition
let D be non empty set ;
let F be PartFunc of D,REAL;
let X be set ;
func Sum (F,X) ->  Real equals :: RFUNCT_3:def 14
 Sum (FinS (F,X));
correctness
coherence
Sum (FinS (F,X)) is Real;
;
end;

:: deftheorem  defines Sum RFUNCT_3:def_14_:_
 for D being non empty set
for F being PartFunc of D,REAL
for X being set holds Sum (F,X) = Sum (FinS (F,X));

theorem Th77: :: RFUNCT_3:77
for D being non empty set
for F being PartFunc of D,REAL
for X being set
for r being Real st dom (F | X) is finite holds
Sum ((r (#) F),X) = r * (Sum (F,X))
proofend;

theorem Th78: :: RFUNCT_3:78
for D being non empty set
for F, G being PartFunc of D,REAL
for X being set
for Y being finite set st Y = dom (F | X) &amp; dom (F | X) = dom (G | X) holds
Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X))
proofend;

theorem :: RFUNCT_3:79
for D being non empty set
for F, G being PartFunc of D,REAL
for X being set st dom (F | X) is finite &amp; dom (F | X) = dom (G | X) holds
Sum ((F - G),X) = (Sum (F,X)) - (Sum (G,X))
proofend;

theorem :: RFUNCT_3:80
for D being non empty set
for F being PartFunc of D,REAL
for X being set
for r being Real
for Y being finite set st Y = dom (F | X) holds
Sum ((F - r),X) = (Sum (F,X)) - (r * (card Y))
proofend;

theorem :: RFUNCT_3:81
for D being non empty set
for F being PartFunc of D,REAL holds Sum (F,{}) = 0 by Th68, RVSUM_1:72;

theorem :: RFUNCT_3:82
for D being non empty set
for F being PartFunc of D,REAL
for d being Element of D st d in dom F holds
Sum (F,{d}) = F . d
proofend;

theorem :: RFUNCT_3:83
for D being non empty set
for F being PartFunc of D,REAL
for X, Y being set st dom (F | (X \/ Y)) is finite &amp; X misses Y holds
Sum (F,(X \/ Y)) = (Sum (F,X)) + (Sum (F,Y))
proofend;

theorem :: RFUNCT_3:84
for D being non empty set
for F being PartFunc of D,REAL
for X, Y being set st dom (F | (X \/ Y)) is finite &amp; dom (F | X) misses dom (F | Y) holds
Sum (F,(X \/ Y)) = (Sum (F,X)) + (Sum (F,Y))
proofend;