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;
ADRYN: ( dom ((Omega \ Y) --> 0 ) = Omega \ Y & rng ((Omega \ Y) --> 0 ) c= REAL ) by FUNCOP_1:19;
ADFRY: dom (f +* ((Omega \ Y) --> 0 )) = (dom f) \/ (dom ((Omega \ Y) --> 0 )) by FUNCT_4:def 1
.= Omega \/ (Omega \ Y) by FUNCT_2:def 1, ADRYN
.= 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 ADFRY, FUNCT_2:4;
consider G being FinSequence of REAL , s being FinSequence of Omega such that
P1: ( 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;
consider E being Element of Trivial-SigmaField Omega;
DD20a: dom g = Omega by FUNCT_2:def 1;
g is_integrable_on P by RANDOM_1:30;
then DD3: g is_integrable_on P2M P by RANDOM_1:def 3;
DD3a: Y misses Omega \ Y by XBOOLE_1:79;
DD4: Integral (P2M P),(g | (Y \/ (Omega \ Y))) = (Integral (P2M P),(g | Y)) + (Integral (P2M P),(g | (Omega \ Y))) by DD3, MESFUNC6:92, XBOOLE_1:79;
Y \/ (Omega \ Y) = Y \/ Omega by XBOOLE_1:39
.= Omega by XBOOLE_1:12 ;
then DD5: g | (Y \/ (Omega \ Y)) = g by FUNCT_2:40;
DD6: g | Y = f | Y by FUNCT_4:76, ADRYN, DD3a;
Q20: dom (g | (Omega \ Y)) = Omega \ Y by RELAT_1:91, DD20a;
Q20A: for x being set st x in dom (g | (Omega \ Y)) holds
(g | (Omega \ Y)) . x = 0

let x be set ; :: thesis:
assume AQ20aaa: x in dom (g | (Omega \ Y)) ; :: thesis:
then AQ20a: ( x in Omega \ Y & (g | (Omega \ Y)) . x = g . x ) by RELAT_1:91, DD20a, FUNCT_1:70;
g . x = ((Omega \ Y) --> 0 ) . x by FUNCT_4:14, AQ20aaa, ADRYN, Q20;
hence (g | (Omega \ Y)) . x = 0 by AQ20a, FUNCOP_1:13; :: thesis:

end;

then Integral (P2M P),(g | (Omega \ Y)) = (R_EAL 0 ) * ((P2M P) . (Omega \ Y)) by MESFUNC6:97, Q20
.= R_EAL 0 ;
then P2: Integral (P2M P),g = Integral (P2M P),(f | Y) by DD6, XXREAL_3:4, DD4, DD5;
set N1 = s " Y;
s is Function of (dom s),(rng s) by FUNCT_2:3;
then s " Y is finite Subset of (dom s) by FUNCT_2:47;
then reconsider N1 = s " Y as finite Subset of (Seg (len G)) by P1, 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 FSCANFS1: canFS N1 is FinSequence of Seg (len G) by FINSEQ_1:def 4;
dom s = Seg (len G) by FINSEQ_1:def 3, P1;
then SF0: s is Function of (Seg (len G)),Omega by FUNCT_2:3, P1;
then reconsider t1 = s * (canFS N1) as FinSequence of Omega by FINSEQ_2:36, FSCANFS1;
RNGT1C: rng t1 = s .: (rng (canFS N1)) by RELAT_1:160
.= s .: N1 by FUNCT_2:def 3
.= Y by P1, FUNCT_1:147 ;
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 SF0, FINSEQ_2:36;
reconsider t = t1 ^ t2 as FinSequence of Omega ;
MISS1P: rng (canFS N1) = N1 by FUNCT_2:def 3;
MISS2P: rng (canFS N2) = N2 by FUNCT_2:def 3;
CDT1: ( N1 is finite Subset of (dom s) & N2 is finite Subset of (dom s) ) by FINSEQ_1:def 3, P1;
then rng (s | N1) misses rng (s | N2) by TRNG01, P1, XBOOLE_1:79;
then rng t1 misses rng (s | N2) by XBOOLE_1:63, MISS1P, TRNG02;
then MISS3: rng t1 misses rng t2 by XBOOLE_1:63, MISS2P, TRNG02;
then P3: t is one-to-one by FINSEQ_3:98, P1;
len (canFS N1) = card N1 by UPROOTS:5;
then DD1: dom (canFS N1) = Seg (card N1) by FINSEQ_1:def 3;
rng (canFS N1) is Subset of (dom s) by CDT1, FUNCT_2:def 3;
then dom t1 = Seg (card N1) by DD1, RELAT_1:46;
then DD1L: len t1 = card N1 by FINSEQ_1:def 3;
len (canFS N2) = card N2 by UPROOTS:5;
then DD2: dom (canFS N2) = Seg (card N2) by FINSEQ_1:def 3;
rng (canFS N2) is Subset of (dom s) by CDT1, FUNCT_2:def 3;
then dom t2 = Seg (card N2) by DD2, RELAT_1:46;
then DD2L: len t2 = card N2 by FINSEQ_1:def 3;
DDD: N1 \/ N2 = (Seg (len G)) \/ N1 by XBOOLE_1:39
.= Seg (len G) by XBOOLE_1:12
.= dom s by FINSEQ_1:def 3, P1 ;
dom t = Seg ((len t1) + (len t2)) by FINSEQ_1:def 7
.= Seg (card (N1 \/ N2)) by CARD_2:53, XBOOLE_1:79, DD1L, DD2L ;
then DDDDZ: len t = card (N1 \/ N2) by FINSEQ_1:def 3;
then DDD0: len t = len s by CARD_1:104, DDD;
DDD1: Seg (len s) = Seg (len t) by DDDDZ, CARD_1:104, DDD;
P5: dom s = Seg (len s) by FINSEQ_1:def 3
.= dom t by FINSEQ_1:def 3, DDD1 ;
DDD2: card (dom t) = card Omega by P1, DDD0, CARD_1:104;
t is Function of (dom t),Omega by FINSEQ_2:30;
then rng s = rng t by P1, P3, FINSEQ_4:78, DDD2;
then consider PN being Permutation of (dom s) such that
P6: ( t = s * PN & dom PN = dom s & rng PN = dom s ) by BHSP_5:1, P1, P3;
defpred S₁[ set , set ] 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)}) ) );

P7A: now

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

now

per cases ;

suppose t . k in Y ; :: thesis:

hence ex x being Element of REAL st S₁[k,x] ; :: thesis:

end;

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

hence ex x being Element of REAL st S₁[k,x] ; :: thesis:

end;

hence ex x being Element of REAL st S₁[k,x] ; :: thesis:

end;

consider F being FinSequence of REAL such that
P7B: dom F = Seg (card Omega) and
P7C: for n being Nat st n in Seg (card Omega) holds
S₁[n,F . n] from FINSEQ_1:sch 5(P7A);
XV0: dom s = Seg (len G) by FINSEQ_1:def 3, P1
.= dom G by FINSEQ_1:def 3 ;
then XV2: dom (G * PN) = dom PN by RELAT_1:46, P6;
XV3: dom F = dom s by P1, FINSEQ_1:def 3, P7B;

now

let x be set ; :: thesis:
assume XV4: x in dom F ; :: thesis:
then reconsider nx = x as Element of NAT ;
YV1: nx in dom t by XV4, P1, FINSEQ_1:def 3, P7B, P5;
YV2: t . nx = s . (PN . nx) by P6, FUNCT_1:22, XV4, XV3, P5;
PN . nx in dom G by XV0, FUNCT_1:21, YV1, P6;
then YV5: G . (PN . nx) = (g . (s . (PN . nx))) * (P . {(s . (PN . nx))}) by P1;

now

per cases ;

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

hence F . nx = (f . (t . nx)) * (P . {(t . nx)}) by P7C, P7B, XV4
.= ((f | Y) . (s . (PN . nx))) * (P . {(s . (PN . nx))}) by YV2, C1, FUNCT_1:72
.= (g . (s . (PN . nx))) * (P . {(s . (PN . nx))}) by C1, YV2, FUNCT_1:72, DD6
.= (G * PN) . nx by FUNCT_1:23, XV3, XV4, P6, YV5 ;
:: thesis:

end;

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

hence F . nx = (g . (s . (PN . nx))) * (P . {(s . (PN . nx))}) by YV2, P7C, P7B, XV4
.= (G * PN) . nx by FUNCT_1:23, XV3, XV4, P6, YV5 ;
:: thesis:

end;

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

end;

then F = G * PN by P6, XV2, XV3, FUNCT_1:9;
then P9: Sum G = Sum F by XV0, FINSOP_1:8;
reconsider t1 = t1 as FinSequence of Y by RNGT1C, FINSEQ_1:def 4;
reconsider F1 = F | (len t1) as FinSequence of REAL ;
reconsider F2 = F /^ (len t1) as FinSequence of REAL ;
P10: F = F1 ^ F2 by RFINSEQ:21;
A2: len t1 = card Y by RNGT1C, FINSEQ_4:77, P1;
P98: len F = card Omega by P7B, FINSEQ_1:def 3;
P201: len F = len t by DDD0, P1, P7B, FINSEQ_1:def 3;
P200: len t = (len t1) + (len t2) by FINSEQ_1:35;
then P203: len t1 <= len t by NAT_1:11;
then P202: len F2 = (len F) - (len t1) by P201, RFINSEQ:def 2
.= len t2 by P200, P201 ;
then P205: dom F2 = Seg (len t2) by FINSEQ_1:def 3
.= dom ((len t2) |-> 0 ) by FUNCOP_1:19 ;

now

let m be Nat; :: thesis:
assume P300: m in dom F2 ; :: thesis:
then P302: m in Seg (len t2) by P202, FINSEQ_1:def 3;
then P303: m in dom t2 by FINSEQ_1:def 3;
LLL1: ( 1 <= m & m <= len t2 ) by P302, FINSEQ_1:3;
m <= m + (len t1) by NAT_1:11;
then ( 1 <= m + (len t1) & m + (len t1) <= len t ) by P200, XREAL_1:8, XXREAL_0:2, LLL1;
then YV20: m + (len t1) in Seg (card Omega) by P1, DDD0;
YV21: t . (m + (len t1)) = t2 . m by FINSEQ_1:def 7, P303;
MISS4: (rng t1) /\ (rng t2) = {} by XBOOLE_0:def 7, MISS3;
P305: t2 . m in rng t2 by FUNCT_1:12, P303;
then not t2 . m in rng t1 by MISS4, XBOOLE_0:def 4;
then P308: t2 . m in dom (g | (Omega \ Y)) by Q20, XBOOLE_0:def 5, RNGT1C, P305;
then P309: g . (t2 . m) = (g | (Omega \ Y)) . (t2 . m) by FUNCT_1:70
.= 0 by Q20A, P308 ;
not t . (m + (len t1)) in Y by RNGT1C, MISS4, XBOOLE_0:def 4, P305, YV21;
then C10: F . (m + (len t1)) = (g . (t . (m + (len t1)))) * (P . {(t . (m + (len t1)))}) by P7C, YV20
.= 0 by P309, YV21 ;
thus F2 . m = F . (m + (len t1)) by P201, P203, RFINSEQ:def 2, P300
.= ((len t2) |-> 0 ) . m by P302, FINSEQ_2:71, C10 ; :: thesis:

end;

then P11: F2 = (len t2) |-> 0 by P205, FINSEQ_1:17;
card Y c= card Omega by CARD_1:27;
then P101: card Y <= card Omega by NAT_1:40;
P12: Sum F = (Sum F1) + (Sum F2) by RVSUM_1:105, P10
.= (Sum F1) + 0 by P11, RVSUM_1:111
.= Sum F1 ;
A1: len F1 = card Y by FINSEQ_1:80, P98, A2, P101;
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 A43: n in Seg (len t1) by A1, A2, FINSEQ_1:def 3;
then A45: n in dom t1 by FINSEQ_1:def 3;
then A44: t . n = t1 . n by FINSEQ_1:def 7;
then A42: t . n in Y by RNGT1C, A45, FUNCT_1:12;
A77P: Seg (len t1) c= Seg (card Omega) by FINSEQ_1:7, A2, P101;
thus F1 . n = F . n by A43, FUNCT_1:72
.= (f . (t1 . n)) * (P . {(t1 . n)}) by A44, A77P, A43, P7C, A42 ; :: 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 A1, A2, RNGT1C, P12, P9, P1, P2; :: thesis: