let Omega be non empty finite set ; :: thesis:
let P be Probability of Trivial-SigmaField Omega; :: thesis:
let Y be non empty finite Subset of Omega; :: thesis:
let f be Function of Omega,REAL; :: thesis:
set YN = Omega \ Y;
A1: ( dom ((Omega \ Y) --> 0) = Omega \ Y & rng ((Omega \ Y) --> 0) c= REAL ) by FUNCOP_1:13;
A2: dom (f +* ((Omega \ Y) --> 0)) = (dom f) \/ (dom ((Omega \ Y) --> 0)) by FUNCT_4:def 1
.= Omega \/ (Omega \ Y) by A1, FUNCT_2:def 1
.= Omega by XBOOLE_1:12 ;
rng (f +* ((Omega \ Y) --> 0)) c= REAL ;
then reconsider g = f +* ((Omega \ Y) --> 0) as Function of Omega,REAL by A2, FUNCT_2:2;
consider G being FinSequence of REAL , s being FinSequence of Omega such that
A3: ( len G = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom G holds
G . n = (g . (s . n)) * (P . {(s . n)}) ) & Integral ((P2M P),g) = Sum G ) by RANDOM_1:13;
reconsider g = g as Real-Valued-Random-Variable of (Trivial-SigmaField Omega) by RANDOM_1:29;
A4: dom g = Omega by FUNCT_2:def 1;
g is_integrable_on P by RANDOM_1:30;
then A5: g is_integrable_on P2M P by RANDOM_1:def 2;
A6: Y misses Omega \ Y by XBOOLE_1:79;
A7: Integral ((P2M P),(g | (Y \/ (Omega \ Y)))) = (Integral ((P2M P),(g | Y))) + (Integral ((P2M P),(g | (Omega \ Y)))) by A5, MESFUNC6:92, XBOOLE_1:79;
Y \/ (Omega \ Y) = Y \/ Omega by XBOOLE_1:39
.= Omega by XBOOLE_1:12 ;
then A8: g | (Y \/ (Omega \ Y)) = g ;
A9: g | Y = f | Y by A1, A6, FUNCT_4:72;
A10: dom (g | (Omega \ Y)) = Omega \ Y by A4, RELAT_1:62;
reconsider zz = 0 as R_eal by XXREAL_0:def 1;
A11: for x being object st x in dom (g | (Omega \ Y)) holds
(g | (Omega \ Y)) . x = 0

proof

let x be object ; :: thesis:
assume A12: x in dom (g | (Omega \ Y)) ; :: thesis:
then A13: ( x in Omega \ Y & (g | (Omega \ Y)) . x = g . x ) by A4, FUNCT_1:47, RELAT_1:62;
g . x = ((Omega \ Y) --> 0) . x by A12, A1, A10, FUNCT_4:13;
hence (g | (Omega \ Y)) . x = 0 by A13, FUNCOP_1:7; :: thesis:

end;

then Integral ((P2M P),(g | (Omega \ Y))) = zz * ((P2M P) . (Omega \ Y)) by A10, MESFUNC6:97
.= 0 ;
then A14: Integral ((P2M P),g) = Integral ((P2M P),(f | Y)) by A9, A7, A8, XXREAL_3:4;
set N1 = s " Y;
s is Function of (dom s),(rng s) by FUNCT_2:1;
then s " Y is finite Subset of (dom s) by FUNCT_2:39;
then reconsider N1 = s " Y as finite Subset of (Seg (len G)) by A3, FINSEQ_1:def 3;
rng (canFS N1) c= N1 by FINSEQ_1:def 4;
then rng (canFS N1) c= Seg (len G) by XBOOLE_1:1;
then A15: canFS N1 is FinSequence of Seg (len G) by FINSEQ_1:def 4;
dom s = Seg (len G) by A3, FINSEQ_1:def 3;
then A16: s is Function of (Seg (len G)),Omega by A3, FUNCT_2:1;
then reconsider t1 = s * (canFS N1) as FinSequence of Omega by A15, FINSEQ_2:32;
A17: rng t1 = s .: (rng (canFS N1)) by RELAT_1:127
.= s .: N1 by FUNCT_2:def 3
.= Y by A3, FUNCT_1:77 ;
set N2 = (Seg (len G)) \ N1;
reconsider N2 = (Seg (len G)) \ N1 as finite Subset of (Seg (len G)) by XBOOLE_1:36;
rng (canFS N2) c= N2 by FINSEQ_1:def 4;
then rng (canFS N2) c= Seg (len G) by XBOOLE_1:1;
then canFS N2 is FinSequence of Seg (len G) by FINSEQ_1:def 4;
then reconsider t2 = s * (canFS N2) as FinSequence of Omega by A16, FINSEQ_2:32;
reconsider t = t1 ^ t2 as FinSequence of Omega ;
A18: rng (canFS N1) = N1 by FUNCT_2:def 3;
A19: rng (canFS N2) = N2 by FUNCT_2:def 3;
A20: ( N1 is finite Subset of (dom s) & N2 is finite Subset of (dom s) ) by A3, FINSEQ_1:def 3;
then rng (s | N1) misses rng (s | N2) by Th1, A3, XBOOLE_1:79;
then rng t1 misses rng (s | N2) by A18, Th2, XBOOLE_1:63;
then A21: rng t1 misses rng t2 by A19, Th2, XBOOLE_1:63;
then A22: t is one-to-one by A3, FINSEQ_3:91;
len (canFS N1) = card N1 by FINSEQ_1:93;
then A23: dom (canFS N1) = Seg (card N1) by FINSEQ_1:def 3;
rng (canFS N1) is Subset of (dom s) by A20, FUNCT_2:def 3;
then dom t1 = Seg (card N1) by A23, RELAT_1:27;
then A24: len t1 = card N1 by FINSEQ_1:def 3;
len (canFS N2) = card N2 by FINSEQ_1:93;
then A25: dom (canFS N2) = Seg (card N2) by FINSEQ_1:def 3;
rng (canFS N2) is Subset of (dom s) by A20, FUNCT_2:def 3;
then dom t2 = Seg (card N2) by A25, RELAT_1:27;
then A26: len t2 = card N2 by FINSEQ_1:def 3;
A27: N1 \/ N2 = (Seg (len G)) \/ N1 by XBOOLE_1:39
.= Seg (len G) by XBOOLE_1:12
.= dom s by A3, FINSEQ_1:def 3 ;
dom t = Seg ((len t1) + (len t2)) by FINSEQ_1:def 7
.= Seg (card (N1 \/ N2)) by A24, A26, CARD_2:40, XBOOLE_1:79 ;
then A28: len t = card (N1 \/ N2) by FINSEQ_1:def 3;
then A29: len t = len s by A27, CARD_1:62;
A30: Seg (len s) = Seg (len t) by A28, A27, CARD_1:62;
A31: dom s = Seg (len s) by FINSEQ_1:def 3
.= dom t by A30, FINSEQ_1:def 3 ;
A32: card (dom t) = card Omega by A3, A29, CARD_1:62;
t is Function of (dom t),Omega by FINSEQ_2:26;
then t is onto by A22, A32, FINSEQ_4:63;
then rng s = rng t by A3, FUNCT_2:def 3;
then consider PN being Permutation of (dom s) such that
A33: ( t = s * PN & dom PN = dom s & rng PN = dom s ) by A3, A22, BHSP_5:1;
defpred S₁[ object , object ] means ( ( t . $1 in Y implies $2 = (f . (t . $1)) * (P . {(t . $1)}) ) & ( not t . $1 in Y implies $2 = (g . (t . $1)) * (P . {(t . $1)}) ) );

A34: now :: thesis:

let k be Nat; :: thesis:
assume k in Seg (card Omega) ; :: thesis:

now :: thesis:

per cases ;

suppose t . k in Y ; :: thesis:

hence ex x being Real st S₁[k,x] ; :: thesis:

end;

suppose not t . k in Y ; :: thesis:

hence ex x being Real st S₁[k,x] ; :: thesis:

end;

then consider x being Real such that
A35: S₁[k,x] ;
reconsider x = x as Element of REAL by XREAL_0:def 1;
take x = x; :: thesis:
thus S₁[k,x] by A35; :: thesis:

end;

consider F being FinSequence of REAL such that
A36: dom F = Seg (card Omega) and
A37: for n being Nat st n in Seg (card Omega) holds
S₁[n,F . n] from FINSEQ_1:sch 5(A34);
A38: dom s = Seg (len G) by A3, FINSEQ_1:def 3
.= dom G by FINSEQ_1:def 3 ;
then A39: dom (G * PN) = dom PN by A33, RELAT_1:27;
A40: dom F = dom s by A3, A36, FINSEQ_1:def 3;

now :: thesis:

let x be object ; :: thesis:
assume A41: x in dom F ; :: thesis:
then reconsider nx = x as Element of NAT ;
A42: nx in dom t by A41, A3, A36, A31, FINSEQ_1:def 3;
A43: t . nx = s . (PN . nx) by A33, A41, A40, A31, FUNCT_1:12;
PN . nx in dom G by A38, A42, A33, FUNCT_1:11;
then A44: G . (PN . nx) = (g . (s . (PN . nx))) * (P . {(s . (PN . nx))}) by A3;

now :: thesis:

per cases ;

suppose A45: t . nx in Y ; :: thesis:

hence F . nx = (f . (t . nx)) * (P . {(t . nx)}) by A37, A36, A41
.= ((f | Y) . (s . (PN . nx))) * (P . {(s . (PN . nx))}) by A43, A45, FUNCT_1:49
.= (g . (s . (PN . nx))) * (P . {(s . (PN . nx))}) by A45, A43, A9, FUNCT_1:49
.= (G * PN) . nx by A40, A41, A33, A44, FUNCT_1:13 ;
:: thesis:

end;

suppose not t . nx in Y ; :: thesis:

hence F . nx = (g . (s . (PN . nx))) * (P . {(s . (PN . nx))}) by A43, A37, A36, A41
.= (G * PN) . nx by A40, A41, A33, A44, FUNCT_1:13 ;
:: thesis:

end;

hence F . x = (G * PN) . x ; :: thesis:

end;

then F = G * PN by A33, A39, A40, FUNCT_1:2;
then A46: Sum G = Sum F by A38, FINSOP_1:7;
reconsider t1 = t1 as FinSequence of Y by A17, FINSEQ_1:def 4;
reconsider F1 = F | (len t1) as FinSequence of REAL ;
reconsider F2 = F /^ (len t1) as FinSequence of REAL ;
A47: F = F1 ^ F2 by RFINSEQ:8;
A48: len t1 = card Y by A17, A3, FINSEQ_4:62;
A49: len F = card Omega by A36, FINSEQ_1:def 3;
A50: len F = len t by A29, A3, A36, FINSEQ_1:def 3;
A51: len t = (len t1) + (len t2) by FINSEQ_1:22;
then A52: len t1 <= len t by NAT_1:11;
then A53: len F2 = (len F) - (len t1) by A50, RFINSEQ:def 1
.= len t2 by A51, A50 ;
then A54: dom F2 = Seg (len t2) by FINSEQ_1:def 3
.= dom ((len t2) |-> 0) by FUNCOP_1:13 ;

now :: thesis:

let m be Nat; :: thesis:
assume A55: m in dom F2 ; :: thesis:
then A56: m in Seg (len t2) by A53, FINSEQ_1:def 3;
then A57: m in dom t2 by FINSEQ_1:def 3;
A58: ( 1 <= m & m <= len t2 ) by A56, FINSEQ_1:1;
m <= m + (len t1) by NAT_1:11;
then ( 1 <= m + (len t1) & m + (len t1) <= len t ) by A51, A58, XREAL_1:6, XXREAL_0:2;
then A59: m + (len t1) in Seg (card Omega) by A3, A29;
A60: t . (m + (len t1)) = t2 . m by A57, FINSEQ_1:def 7;
A61: (rng t1) /\ (rng t2) = {} by A21, XBOOLE_0:def 7;
A62: t2 . m in rng t2 by A57, FUNCT_1:3;
then not t2 . m in rng t1 by A61, XBOOLE_0:def 4;
then A63: t2 . m in dom (g | (Omega \ Y)) by A10, A17, A62, XBOOLE_0:def 5;
then A64: g . (t2 . m) = (g | (Omega \ Y)) . (t2 . m) by FUNCT_1:47
.= 0 by A11, A63 ;
not t . (m + (len t1)) in Y by A17, A61, A62, A60, XBOOLE_0:def 4;
then A65: F . (m + (len t1)) = (g . (t . (m + (len t1)))) * (P . {(t . (m + (len t1)))}) by A37, A59
.= 0 by A64, A60 ;
thus F2 . m = F . (m + (len t1)) by A50, A52, A55, RFINSEQ:def 1
.= ((len t2) |-> 0) . m by A56, A65, FINSEQ_2:57 ; :: thesis:

end;

then A66: F2 = (len t2) |-> 0 by A54, FINSEQ_1:13;
Segm (card Y) c= Segm (card Omega) by CARD_1:11;
then A67: card Y <= card Omega by NAT_1:39;
A68: Sum F = (Sum F1) + (Sum F2) by A47, RVSUM_1:75
.= (Sum F1) + 0 by A66, RVSUM_1:81
.= Sum F1 ;
A69: len F1 = card Y by A49, A48, A67, FINSEQ_1:59;
for n being Nat st n in dom F1 holds
F1 . n = (f . (t1 . n)) * (P . {(t1 . n)})

proof

let n be Nat; :: thesis:
assume n in dom F1 ; :: thesis:
then A70: n in Seg (len t1) by A69, A48, FINSEQ_1:def 3;
then A71: n in dom t1 by FINSEQ_1:def 3;
then A72: t . n = t1 . n by FINSEQ_1:def 7;
then A73: t . n in Y by A17, A71, FUNCT_1:3;
A74: Seg (len t1) c= Seg (card Omega) by A48, A67, FINSEQ_1:5;
thus F1 . n = F . n by A70, FUNCT_1:49
.= (f . (t1 . n)) * (P . {(t1 . n)}) by A72, A74, A70, A37, A73 ; :: thesis:

end;

hence ex G being FinSequence of REAL ex s being FinSequence of Y st
( len G = card Y & s is one-to-one & rng s = Y & len s = card Y & ( for n being Nat st n in dom G holds
G . n = (f . (s . n)) * (P . {(s . n)}) ) & Integral ((P2M P),(f | Y)) = Sum G ) by A69, A48, A17, A68, A46, A3, A14; :: thesis: