:: RFUNCT_3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let n, m be Nat;
:: original: min
redefine func min n,m -> Nat;
coherence
min n,m is Nat
by FINSEQ_2:1;
end;

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds r = (max+ r) - (max- r)
proof end;

theorem Th2: :: RFUNCT_3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds abs r = (max+ r) + (max- r)
proof end;

theorem Th3: :: RFUNCT_3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds 2 * (max+ r) = r + (abs r)
proof end;

theorem Th4: :: RFUNCT_3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, s being real number st 0 <= r holds
max+ (r * s) = r * (max+ s)
proof end;

theorem Th5: :: RFUNCT_3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, s being real number holds max+ (r + s) <= (max+ r) + (max+ s)
proof end;

theorem :: RFUNCT_3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number holds
( 0 <= max+ r & 0 <= max- r ) by SQUARE_1:46;

theorem Th7: :: RFUNCT_3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r1, r2, s1, s2 being real number st r1 <= s1 & r2 <= s2 holds
max r1,r2 <= max s1,s2
proof end;

Lm1: for n being Nat
for D being non empty set
for f being FinSequence of D st len f <= n holds
f | n = f
proof end;

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

theorem Th8: :: RFUNCT_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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}
proof end;

theorem Th9: :: RFUNCT_3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being PartFunc of D, REAL holds (0 (#) F) " {0} = dom F
proof end;

theorem Th10: :: RFUNCT_3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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}
proof end;

theorem Th11: :: RFUNCT_3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being PartFunc of D, REAL holds (abs F) " {0} = F " {0}
proof end;

theorem Th12: :: RFUNCT_3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being PartFunc of D, REAL
for r being Real st r < 0 holds
(abs F) " {r} = {}
proof end;

theorem Th13: :: RFUNCT_3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: RFUNCT_3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: RFUNCT_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

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
proof end;
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 PartFunc-set of X,Y;
existence
not for b1 being PartFunc-set of X,Y holds b1 is empty
proof 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 ;
:: original: PFuncs
redefine func PFuncs X,Y -> PartFunc-set of X,Y;
coherence
PFuncs X,Y is PartFunc-set of X,Y
proof end;
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 func X --> c -> Element of PFuncs D,C;
coherence
X --> c is Element of PFuncs D,C
proof end;
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 func F1 + F2 -> Element of PFuncs D,REAL ;
coherence
F1 + F2 is Element of PFuncs D,REAL
proof end;
:: original: -
redefine func F1 - F2 -> Element of PFuncs D,REAL ;
coherence
F1 - F2 is Element of PFuncs D,REAL
proof end;
:: original: (#)
redefine func F1 (#) F2 -> Element of PFuncs D,REAL ;
coherence
F1 (#) F2 is Element of PFuncs D,REAL
proof end;
:: original: /
redefine func F1 / F2 -> Element of PFuncs D,REAL ;
coherence
F1 / F2 is Element of PFuncs D,REAL
proof end;
end;

definition
let D be non empty set ;
let E be real-membered set ;
let F be Element of PFuncs D,E;
:: original: abs
redefine func abs F -> Element of PFuncs D,REAL ;
coherence
abs F is Element of PFuncs D,REAL
proof end;
:: original: -
redefine func - F -> Element of PFuncs D,REAL ;
coherence
- F is Element of PFuncs D,REAL
proof end;
:: original: ^
redefine func F ^ -> Element of PFuncs D,REAL ;
coherence
F ^ is Element of PFuncs D,REAL
proof end;
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 func r (#) F -> Element of PFuncs D,REAL ;
coherence
r (#) F is Element of PFuncs D,REAL
proof end;
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
proof end;
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 ) & ( for F1, F2 being Element of PFuncs D,REAL holds b2 . F1,F2 = F1 + F2 ) holds
b1 = b2
proof end;
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 Th16: :: RFUNCT_3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set holds addpfunc D is commutative
proof end;

theorem Th17: :: RFUNCT_3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set holds addpfunc D is associative
proof end;

theorem Th18: :: RFUNCT_3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set holds ([#] D) --> 0 is_a_unity_wrt addpfunc D
proof end;

theorem Th19: :: RFUNCT_3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set holds the_unity_wrt (addpfunc D) = ([#] D) --> 0
proof end;

theorem Th20: :: RFUNCT_3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set holds addpfunc D has_a_unity
proof end;

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 Th21: :: RFUNCT_3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set holds Sum (<*> (PFuncs D,REAL )) = ([#] D) --> 0
proof end;

theorem Th22: :: RFUNCT_3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for G being Element of PFuncs D,REAL holds Sum <*G*> = G by FINSOP_1:12;

theorem Th23: :: RFUNCT_3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th24: :: RFUNCT_3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f1, f2 being FinSequence of PFuncs D,REAL holds Sum (f1 ^ f2) = (Sum f1) + (Sum f2)
proof end;

theorem :: RFUNCT_3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th26: :: RFUNCT_3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for G1, G2 being Element of PFuncs D,REAL holds Sum <*G1,G2*> = G1 + G2
proof end;

theorem :: RFUNCT_3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for G1, G2, G3 being Element of PFuncs D,REAL holds Sum <*G1,G2,G3*> = (G1 + G2) + G3
proof end;

theorem :: RFUNCT_3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

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 & ( for n being 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 & ( for n being Nat st n in dom b1 holds
b1 . n = chi (f . n),D ) )
proof end;
uniqueness
for b1, b2 being FinSequence of PFuncs D,REAL st len b1 = len f & ( for n being Nat st n in dom b1 holds
b1 . n = chi (f . n),D ) & len b2 = len f & ( for n being Nat st n in dom b2 holds
b2 . n = chi (f . n),D ) holds
b1 = b2
proof end;
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 & ( for n being 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 ;
func R (#) f -> FinSequence of PFuncs D,REAL means :Def7: :: RFUNCT_3:def 7
( len it = min (len R),(len f) & ( for n being Nat st n in dom it holds
for F being PartFunc of D, REAL
for r being Real st r = R . n & 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) & ( for n being Nat st n in dom b1 holds
for F being PartFunc of D, REAL
for r being Real st r = R . n & F = f . n holds
b1 . n = r (#) F ) )
proof end;
uniqueness
for b1, b2 being FinSequence of PFuncs D,REAL st len b1 = min (len R),(len f) & ( for n being Nat st n in dom b1 holds
for F being PartFunc of D, REAL
for r being Real st r = R . n & F = f . n holds
b1 . n = r (#) F ) & len b2 = min (len R),(len f) & ( for n being Nat st n in dom b2 holds
for F being PartFunc of D, REAL
for r being Real st r = R . n & F = f . n holds
b2 . n = r (#) F ) holds
b1 = b2
proof end;
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) & ( for n being Nat st n in dom b4 holds
for F being PartFunc of D, REAL
for r being Real st r = R . n & 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;
func f # d -> FinSequence of REAL means :Def8: :: RFUNCT_3:def 8
( len it = len f & ( for n being Nat
for G being Element of PFuncs D,REAL st n in dom it & f . n = G holds
it . n = G . d ) );
existence
ex b1 being FinSequence of REAL st
( len b1 = len f & ( for n being Nat
for G being Element of PFuncs D,REAL st n in dom b1 & f . n = G holds
b1 . n = G . d ) )
proof end;
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len f & ( for n being Nat
for G being Element of PFuncs D,REAL st n in dom b1 & f . n = G holds
b1 . n = G . d ) & len b2 = len f & ( for n being Nat
for G being Element of PFuncs D,REAL st n in dom b2 & f . n = G holds
b2 . n = G . d ) holds
b1 = b2
proof end;
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 & ( for n being Nat
for G being Element of PFuncs D,REAL st n in dom b4 & f . n = G holds
b4 . n = G . d ) ) );

definition
let D, C be non empty set ;
let f be FinSequence of PFuncs D,C;
let d be Element of D;
pred d is_common_for_dom f means :Def9: :: RFUNCT_3:def 9
for G being Element of PFuncs D,C
for n being Nat st n in dom f & f . n = G holds
d in dom G;
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 G being Element of PFuncs D,C
for n being Nat st n in dom f & f . n = G holds
d in dom G );

theorem Th29: :: RFUNCT_3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, C being non empty set
for f being FinSequence of PFuncs D,C
for d being Element of D
for n being Nat st d is_common_for_dom f & n <> 0 holds
d is_common_for_dom f | n
proof end;

theorem :: RFUNCT_3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D, C being non empty set
for f being FinSequence of PFuncs D,C
for d being Element of D
for n being Nat st d is_common_for_dom f holds
d is_common_for_dom f /^ n
proof end;

theorem Th31: :: RFUNCT_3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem Th32: :: RFUNCT_3:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f being FinSequence of PFuncs D,REAL
for d being Element of D
for n being Nat holds (f | n) # d = (f # d) | n
proof end;

theorem Th33: :: RFUNCT_3:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th34: :: RFUNCT_3:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: RFUNCT_3:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: RFUNCT_3:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

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 & ( 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 & ( for d being Element of D st d in dom b1 holds
b1 . d = max+ (F . d) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of D, REAL st dom b1 = dom F & ( for d being Element of D st d in dom b1 holds
b1 . d = max+ (F . d) ) & dom b2 = dom F & ( for d being Element of D st d in dom b2 holds
b2 . d = max+ (F . d) ) holds
b1 = b2
proof end;
func max- F -> PartFunc of D, REAL means :Def11: :: RFUNCT_3:def 11
( dom it = dom F & ( 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 & ( for d being Element of D st d in dom b1 holds
b1 . d = max- (F . d) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of D, REAL st dom b1 = dom F & ( for d being Element of D st d in dom b1 holds
b1 . d = max- (F . d) ) & dom b2 = dom F & ( for d being Element of D st d in dom b2 holds
b2 . d = max- (F . d) ) holds
b1 = b2
proof end;
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 & ( 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 & ( for d being Element of D st d in dom b3 holds
b3 . d = max- (F . d) ) ) );

theorem :: RFUNCT_3:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being PartFunc of D, REAL holds
( F = (max+ F) - (max- F) & abs F = (max+ F) + (max- F) & 2 (#) (max+ F) = F + (abs F) )
proof end;

theorem Th38: :: RFUNCT_3:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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}
proof end;

theorem Th39: :: RFUNCT_3:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being PartFunc of D, REAL holds F " (left_closed_halfline 0) = (max+ F) " {0}
proof end;

theorem Th40: :: RFUNCT_3:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
0 <= (max+ F) . d
proof end;

theorem Th41: :: RFUNCT_3:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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}
proof end;

theorem Th42: :: RFUNCT_3:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being PartFunc of D, REAL holds F " (right_closed_halfline 0) = (max- F) " {0}
proof end;

theorem Th43: :: RFUNCT_3:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
0 <= (max- F) . d
proof end;

theorem :: RFUNCT_3:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: RFUNCT_3:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

registration
let A, B be set ;
cluster finite Relation of A,B;
existence
ex b1 being PartFunc of A,B st b1 is finite
proof end;
end;

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

theorem :: RFUNCT_3:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & max- F, max- G are_fiberwise_equipotent holds
F,G are_fiberwise_equipotent
proof end;

theorem Th47: :: RFUNCT_3:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being PartFunc of D, REAL
for X being set holds (max+ F) | X = max+ (F | X)
proof end;

theorem :: RFUNCT_3:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being PartFunc of D, REAL
for X being set holds (max- F) | X = max- (F | X)
proof end;

theorem Th49: :: RFUNCT_3:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: RFUNCT_3:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

definition
let D be non empty set ;
let F be PartFunc of D, REAL ;
let r be Real;
func F - r -> PartFunc of D, REAL means :Def12: :: RFUNCT_3:def 12
( dom it = dom F & ( for d being Element of D st d in dom it holds
it . d = (F . d) - r ) );
existence
ex b1 being PartFunc of D, REAL st
( dom b1 = dom F & ( for d being Element of D st d in dom b1 holds
b1 . d = (F . d) - r ) )
proof end;
uniqueness
for b1, b2 being PartFunc of D, REAL st dom b1 = dom F & ( for d being Element of D st d in dom b1 holds
b1 . d = (F . d) - r ) & dom b2 = dom F & ( for d being Element of D st d in dom b2 holds
b2 . d = (F . d) - r ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines - RFUNCT_3:def 12 :
for D being non empty set
for F being PartFunc of D, REAL
for r being Real
for b4 being PartFunc of D, REAL holds
( b4 = F - r iff ( dom b4 = dom F & ( for d being Element of D st d in dom b4 holds
b4 . d = (F . d) - r ) ) );

theorem Th51: :: RFUNCT_3:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being PartFunc of D, REAL holds F - 0 = F
proof end;

theorem :: RFUNCT_3:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th53: :: RFUNCT_3:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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}
proof end;

theorem :: RFUNCT_3:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let F be PartFunc of REAL , REAL ;
let X be set ;
pred F is_convex_on X means :Def13: :: RFUNCT_3:def 13
( X c= dom F & ( for p being Real st 0 <= p & p <= 1 holds
for r, s being 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;

:: deftheorem Def13 defines is_convex_on RFUNCT_3:def 13 :
for F being PartFunc of REAL , REAL
for X being set holds
( F is_convex_on X iff ( X c= dom F & ( for p being Real st 0 <= p & p <= 1 holds
for r, s being 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)) ) ) );

theorem Th55: :: RFUNCT_3:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & ( for p being Real st 0 <= p & p <= 1 holds
for r, s being 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 end;

theorem :: RFUNCT_3:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & ( for x1, x2, x3 being 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 end;

theorem :: RFUNCT_3:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being PartFunc of REAL , REAL
for X, Y being set st F is_convex_on X & Y c= X holds
F is_convex_on Y
proof end;

theorem :: RFUNCT_3:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: RFUNCT_3:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: RFUNCT_3:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being PartFunc of REAL , REAL
for X being set st X c= dom F holds
0 (#) F is_convex_on X
proof end;

theorem :: RFUNCT_3:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being PartFunc of REAL , REAL
for X being set st F is_convex_on X & G is_convex_on X holds
F + G is_convex_on X
proof end;

theorem Th62: :: RFUNCT_3:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: RFUNCT_3:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being PartFunc of REAL , REAL
for X being set st F is_convex_on X holds
max+ F is_convex_on X
proof end;

theorem Th64: :: RFUNCT_3:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
id ([#] REAL ) is_convex_on REAL
proof end;

theorem :: RFUNCT_3:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being Real holds max+ ((id ([#] REAL )) - r) is_convex_on REAL by Th62, Th64;

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 :Def14: :: RFUNCT_3:def 14
F | X,it are_fiberwise_equipotent ;
existence
ex b1 being non-increasing FinSequence of REAL st F | X,b1 are_fiberwise_equipotent
proof end;
uniqueness
for b1, b2 being non-increasing FinSequence of REAL st F | X,b1 are_fiberwise_equipotent & F | X,b2 are_fiberwise_equipotent holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines FinS RFUNCT_3:def 14 :
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 Th66: :: RFUNCT_3:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th67: :: RFUNCT_3:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

definition
let D be non empty set ;
let F be PartFunc of D, REAL ;
let X be finite set ;
:: original: |
redefine func F | X -> finite PartFunc of D, REAL ;
coherence
F | X is finite PartFunc of D, REAL
proof end;
end;

theorem Th68: :: RFUNCT_3:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & d in dom (F | X) holds
(FinS F,(X \ {d})) ^ <*(F . d)*>,F | X are_fiberwise_equipotent
proof end;

theorem Th69: :: RFUNCT_3:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & d in dom (F | X) holds
(FinS F,(X \ {d})) ^ <*(F . d)*>,F | X are_fiberwise_equipotent
proof end;

theorem Th70: :: RFUNCT_3:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th71: :: RFUNCT_3:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being PartFunc of D, REAL holds FinS F,{} = <*> REAL
proof end;

theorem Th72: :: RFUNCT_3:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)*>
proof end;

theorem Th73: :: RFUNCT_3:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & 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 end;

defpred S1[ 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) & dom (F | X) is finite & Y c= X & $1 = card Z & ( for d1, d2 being 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: S1[0]
proof end;

Lm4: for n being Nat st S1[n] holds
S1[n + 1]
proof end;

theorem :: RFUNCT_3:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being PartFunc of D, REAL
for X, Y being set st dom (F | X) is finite & Y c= X & ( for d1, d2 being 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 end;

theorem Th75: :: RFUNCT_3:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & 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 end;

theorem Th76: :: RFUNCT_3:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: RFUNCT_3:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being PartFunc of D, REAL
for X being set st dom (F | X) is finite & ( for d being Element of D st d in dom (F | X) holds
F . d >= 0 ) holds
FinS (max+ F),X = FinS F,X
proof end;

theorem :: RFUNCT_3:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) & rng (F | X) = {r} holds
FinS F,X = (card Z) |-> r
proof end;

theorem Th79: :: RFUNCT_3:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & X misses Y holds
FinS F,(X \/ Y),(FinS F,X) ^ (FinS F,Y) are_fiberwise_equipotent
proof end;

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 15
Sum (FinS F,X);
correctness
coherence
Sum (FinS F,X) is Real
;
;
end;

:: deftheorem defines Sum RFUNCT_3:def 15 :
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 Th80: :: RFUNCT_3:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th81: :: RFUNCT_3:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) & dom (F | X) = dom (G | X) holds
Sum (F + G),X = (Sum F,X) + (Sum G,X)
proof end;

theorem :: RFUNCT_3:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F, G being PartFunc of D, REAL
for X being 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 end;

theorem :: RFUNCT_3:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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))
proof end;

theorem :: RFUNCT_3:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for F being PartFunc of D, REAL holds Sum F,{} = 0 by Th71, RVSUM_1:102;

theorem :: RFUNCT_3:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: RFUNCT_3:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & X misses Y holds
Sum F,(X \/ Y) = (Sum F,X) + (Sum F,Y)
proof end;

theorem :: RFUNCT_3:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & dom (F | X) misses dom (F | Y) holds
Sum F,(X \/ Y) = (Sum F,X) + (Sum F,Y)
proof end;