let S be non empty finite set ; :: thesis: 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; :: thesis: 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; :: thesis: for judgefunc being Function of S,BOOLEAN holds Prob (judgefunc,s) = Prob (judgefunc,t)
let judgefunc be Function of S,BOOLEAN; :: thesis: 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 ; :: thesis: ( 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)) ; :: thesis: (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; :: thesis: verum

end;

hence extract (((len s) * (FDprobSEQ s)),A1) = (len s) * (extract ((FDprobSEQ s),A0)) by A14, VALUED_1:def 5; :: thesis: 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 ; :: thesis: ( 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)) ; :: thesis: (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; :: thesis: verum

end;

hence extract (((len t) * (FDprobSEQ t)),B1) = (len t) * (extract ((FDprobSEQ t),B0)) by A21, VALUED_1:def 5; :: thesis: 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 ; :: thesis: verum