let S be non empty finite set ; for D being EqSampleSpaces of S
for s, t being Element of D
for judgefunc being Function of S,BOOLEAN holds Prob (judgefunc,s) = Prob (judgefunc,t)
let D be EqSampleSpaces of S; for s, t being Element of D
for judgefunc being Function of S,BOOLEAN holds Prob (judgefunc,s) = Prob (judgefunc,t)
let s, t be Element of D; for judgefunc being Function of S,BOOLEAN holds Prob (judgefunc,s) = Prob (judgefunc,t)
let judgefunc be Function of S,BOOLEAN; Prob (judgefunc,s) = Prob (judgefunc,t)
consider A being Subset of (dom (freqSEQ s)) such that
A1:
( A = trueEVENT (judgefunc * (canFS S)) & card (trueEVENT (judgefunc * s)) = Sum (extract ((freqSEQ s),A)) )
by Th15;
consider B being Subset of (dom (freqSEQ t)) such that
A2:
( B = trueEVENT (judgefunc * (canFS S)) & card (trueEVENT (judgefunc * t)) = Sum (extract ((freqSEQ t),B)) )
by Th15;
consider v being FinSequence of S such that
A3:
D = Finseq-EQclass v
by DIST_1:def 6;
A c= dom (freqSEQ s)
;
then A4:
A c= Seg (card S)
by DIST_1:def 9;
then A5:
A c= dom (FDprobSEQ s)
by DIST_1:def 3;
reconsider A0 = A as Subset of (dom (FDprobSEQ s)) by A4, DIST_1:def 3;
reconsider A1 = A as Subset of (dom ((len s) (#) (FDprobSEQ s))) by A5, VALUED_1:def 5;
B c= dom (freqSEQ t)
;
then A6:
B c= Seg (card S)
by DIST_1:def 9;
then A7:
B c= dom (FDprobSEQ t)
by DIST_1:def 3;
reconsider B0 = B as Subset of (dom (FDprobSEQ t)) by A6, DIST_1:def 3;
reconsider B1 = B as Subset of (dom ((len t) (#) (FDprobSEQ t))) by A7, VALUED_1:def 5;
A8:
v,s -are_prob_equivalent
by A3, DIST_1:7;
v,t -are_prob_equivalent
by A3, DIST_1:7;
then A9:
FDprobSEQ s = FDprobSEQ t
by DIST_1:10, A8, DIST_1:6;
A10:
freqSEQ s = (len s) (#) (FDprobSEQ s)
by Th16;
A11:
freqSEQ t = (len t) (#) (FDprobSEQ t)
by Th16;
A12:
extract (((len s) * (FDprobSEQ s)),A1) = (len s) * (extract ((FDprobSEQ s),A0))
proof
len (extract (((len s) * (FDprobSEQ s)),A1)) = card A1
by Th11;
then A13:
dom (extract (((len s) * (FDprobSEQ s)),A1)) = Seg (card A)
by FINSEQ_1:def 3;
len (extract ((FDprobSEQ s),A0)) = card A0
by Th11;
then A14:
dom (extract (((len s) * (FDprobSEQ s)),A1)) = dom (extract ((FDprobSEQ s),A0))
by A13, FINSEQ_1:def 3;
for
c being
object st
c in dom (extract (((len s) * (FDprobSEQ s)),A1)) holds
(extract (((len s) * (FDprobSEQ s)),A1)) . c = (len s) * ((extract ((FDprobSEQ s),A0)) . c)
proof
let c be
object ;
( c in dom (extract (((len s) * (FDprobSEQ s)),A1)) implies (extract (((len s) * (FDprobSEQ s)),A1)) . c = (len s) * ((extract ((FDprobSEQ s),A0)) . c) )
assume A15:
c in dom (extract (((len s) * (FDprobSEQ s)),A1))
;
(extract (((len s) * (FDprobSEQ s)),A1)) . c = (len s) * ((extract ((FDprobSEQ s),A0)) . c)
then A16:
(extract (((len s) * (FDprobSEQ s)),A1)) . c =
((len s) * (FDprobSEQ s)) . ((canFS A1) . c)
by Th11
.=
(freqSEQ s) . ((canFS A) . c)
by DIST_1:14
;
len (canFS A) = card A
by FINSEQ_1:93;
then A17:
dom (canFS A) = Seg (card A)
by FINSEQ_1:def 3;
(canFS A) . c in rng (canFS A)
by A17, A15, A13, FUNCT_1:3;
then A18:
(canFS A) . c in A
by FUNCT_2:def 3;
(extract ((FDprobSEQ s),A0)) . c = (FDprobSEQ s) . ((canFS A) . c)
by Th11, A14, A15;
hence
(extract (((len s) * (FDprobSEQ s)),A1)) . c = (len s) * ((extract ((FDprobSEQ s),A0)) . c)
by A16, A18, DIST_1:def 9;
verum
end;
hence
extract (
((len s) * (FDprobSEQ s)),
A1)
= (len s) * (extract ((FDprobSEQ s),A0))
by A14, VALUED_1:def 5;
verum
end;
A19:
extract (((len t) * (FDprobSEQ t)),B1) = (len t) * (extract ((FDprobSEQ t),B0))
proof
len (extract (((len t) * (FDprobSEQ t)),B1)) = card B1
by Th11;
then A20:
dom (extract (((len t) * (FDprobSEQ t)),B1)) = Seg (card B)
by FINSEQ_1:def 3;
len (extract ((FDprobSEQ t),B0)) = card B0
by Th11;
then A21:
dom (extract (((len t) * (FDprobSEQ t)),B1)) = dom (extract ((FDprobSEQ t),B0))
by A20, FINSEQ_1:def 3;
for
c being
object st
c in dom (extract (((len t) * (FDprobSEQ t)),B1)) holds
(extract (((len t) * (FDprobSEQ t)),B1)) . c = (len t) * ((extract ((FDprobSEQ t),B0)) . c)
proof
let c be
object ;
( c in dom (extract (((len t) * (FDprobSEQ t)),B1)) implies (extract (((len t) * (FDprobSEQ t)),B1)) . c = (len t) * ((extract ((FDprobSEQ t),B0)) . c) )
assume A22:
c in dom (extract (((len t) * (FDprobSEQ t)),B1))
;
(extract (((len t) * (FDprobSEQ t)),B1)) . c = (len t) * ((extract ((FDprobSEQ t),B0)) . c)
then A23:
(extract (((len t) * (FDprobSEQ t)),B1)) . c =
((len t) * (FDprobSEQ t)) . ((canFS B1) . c)
by Th11
.=
(freqSEQ t) . ((canFS B) . c)
by DIST_1:14
;
len (canFS B) = card B
by FINSEQ_1:93;
then A24:
dom (canFS B) = Seg (card B)
by FINSEQ_1:def 3;
(canFS B) . c in rng (canFS B)
by A24, A22, A20, FUNCT_1:3;
then A25:
(canFS B) . c in B
by FUNCT_2:def 3;
(len t) * ((extract ((FDprobSEQ t),B0)) . c) =
(len t) * ((FDprobSEQ t) . ((canFS B) . c))
by Th11, A21, A22
.=
(freqSEQ t) . ((canFS B) . c)
by A25, DIST_1:def 9
;
hence
(extract (((len t) * (FDprobSEQ t)),B1)) . c = (len t) * ((extract ((FDprobSEQ t),B0)) . c)
by A23;
verum
end;
hence
extract (
((len t) * (FDprobSEQ t)),
B1)
= (len t) * (extract ((FDprobSEQ t),B0))
by A21, VALUED_1:def 5;
verum
end;
A26:
card (trueEVENT (judgefunc * s)) = (len s) * (Sum (extract ((FDprobSEQ s),A0)))
by A12, A1, A10, RVSUM_1:87;
A27:
card (trueEVENT (judgefunc * t)) = (len t) * (Sum (extract ((FDprobSEQ t),B0)))
by A19, A11, A2, RVSUM_1:87;
thus Prob (judgefunc,s) =
Sum (extract ((FDprobSEQ s),A0))
by A26, XCMPLX_1:89
.=
Prob (judgefunc,t)
by A27, A9, A1, A2, XCMPLX_1:89
; verum