let S be non empty finite set ; :: thesis: for D being EqSampleSpaces of S
for X being samplingRNG of D
for f being Function of S,BOOLEAN holds (Prob (f,X)) * (Prob X) = Prob ((f '&' (MembershipDecision X)),D)
let D be EqSampleSpaces of S; :: thesis: for X being samplingRNG of D
for f being Function of S,BOOLEAN holds (Prob (f,X)) * (Prob X) = Prob ((f '&' (MembershipDecision X)),D)
let X be samplingRNG of D; :: thesis: for f being Function of S,BOOLEAN holds (Prob (f,X)) * (Prob X) = Prob ((f '&' (MembershipDecision X)),D)
let f be Function of S,BOOLEAN; :: thesis: (Prob (f,X)) * (Prob X) = Prob ((f '&' (MembershipDecision X)),D)
set g = MembershipDecision X;
set Pc = Prob (f,X);
set Pp = Prob X;
consider s being Element of D, t being FinSequence of S, SD being Subset of (dom s) such that
A1: ( SD = s " X & t = extract (s,SD) & t in ConditionalSS X ) by Def14;
reconsider t = t as Element of ConditionalSS X by A1;
A2: len t = card SD by Th11, A1;
A3: rng t c= X

proof

assume not rng t c= X ; :: thesis: contradiction
then consider y being object such that
A4: ( y in rng t & not y in X ) by TARSKI:def 3;
consider x being object such that
A5: ( x in dom t & y = t . x ) by A4, FUNCT_1:def 3;
A6: dom t = Seg (card SD) by A2, FINSEQ_1:def 3;
reconsider x = x as Nat by A5;
set z = (canFS SD) . x;
A7: rng (canFS SD) c= SD by FINSEQ_1:def 4;
len (canFS SD) = card SD by FINSEQ_1:93;
then dom (canFS SD) = dom t by A6, FINSEQ_1:def 3;
then (canFS SD) . x in rng (canFS SD) by A5, FUNCT_1:3;
then ( (canFS SD) . x in dom s & s . ((canFS SD) . x) in X ) by A1, A7, FUNCT_1:def 7;
hence contradiction by A4, A5, Th11, A1; :: thesis: verum

end;

A8: SD = trueEVENT ((MembershipDecision X) * s) by Th37, A1;
A9: Prob X = Prob ((MembershipDecision X),s) by Def6
.= (len t) / (len s) by Th11, A1, A8 ;
Prob (f,X) = Prob (f,t) by Def6
.= (card (trueEVENT (f * t))) / (len t) ;
then A10: (Prob (f,X)) * (Prob X) = (((card (trueEVENT (f * t))) / (len t)) * (len t)) / (len s) by A9, XCMPLX_1:74
.= ((card (trueEVENT (f * t))) / ((len t) / (len t))) / (len s) by XCMPLX_1:82
.= ((card (trueEVENT (f * t))) / 1) / (len s) by XCMPLX_1:60
.= (card (trueEVENT (f * t))) / (len s) ;
A11: Prob ((f '&' (MembershipDecision X)),s) = (card ((trueEVENT (f * s)) /\ (trueEVENT ((MembershipDecision X) * s)))) / (len s) by Th25;
A12: t " (rng t) c= t " X by A3, RELAT_1:143;
t " (trueEVENT f) c= t " (rng t) by RELAT_1:135;
then (t " (trueEVENT f)) /\ (t " X) = t " (trueEVENT f) by A12, XBOOLE_1:1, XBOOLE_1:28;
then A13: t " ((trueEVENT f) /\ X) = t " (trueEVENT f) by FUNCT_1:68;
(trueEVENT f) /\ X c= X by XBOOLE_1:17;
then A14: card (s " ((trueEVENT f) /\ X)) = card (t " ((trueEVENT f) /\ X)) by Th34, A1
.= card (trueEVENT (f * t)) by Th14, A13 ;
card (trueEVENT (f * t)) = card ((s " (trueEVENT f)) /\ (s " X)) by A14, FUNCT_1:68
.= card ((trueEVENT (f * s)) /\ (trueEVENT ((MembershipDecision X) * s))) by A8, A1, Th14 ;
hence (Prob (f,X)) * (Prob X) = Prob ((f '&' (MembershipDecision X)),D) by Def6, A10, A11; :: thesis: verum