let S be finite set ; :: thesis: for s, t being FinSequence of S holds

( s,t -are_prob_equivalent iff FDprobSEQ s = FDprobSEQ t )

let s, t be FinSequence of S; :: thesis: ( s,t -are_prob_equivalent iff FDprobSEQ s = FDprobSEQ t )

( s,t -are_prob_equivalent iff FDprobSEQ s = FDprobSEQ t )

let s, t be FinSequence of S; :: thesis: ( s,t -are_prob_equivalent iff FDprobSEQ s = FDprobSEQ t )

A1: now :: thesis: ( FDprobSEQ s = FDprobSEQ t implies s,t -are_prob_equivalent )

assume A2:
FDprobSEQ s = FDprobSEQ t
; :: thesis: s,t -are_prob_equivalent

for x being set holds FDprobability (x,t) = FDprobability (x,s)

end;for x being set holds FDprobability (x,t) = FDprobability (x,s)

proof

hence
s,t -are_prob_equivalent
; :: thesis: verum
let x be set ; :: thesis: FDprobability (x,t) = FDprobability (x,s)

end;per cases
( x in S or not x in S )
;

end;

suppose
x in S
; :: thesis: FDprobability (x,t) = FDprobability (x,s)

then
x in rng (canFS S)
by FUNCT_2:def 3;

then consider n being object such that

A3: n in dom (canFS S) and

A4: x = (canFS S) . n by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A3;

len (canFS S) = card S by FINSEQ_1:93;

then A5: n in Seg (card S) by A3, FINSEQ_1:def 3;

then A6: n in dom (FDprobSEQ t) by Def3;

n in dom (FDprobSEQ s) by A5, Def3;

hence FDprobability (x,s) = (FDprobSEQ s) . n by A4, Def3

.= FDprobability (x,t) by A2, A4, A6, Def3 ;

:: thesis: verum

end;then consider n being object such that

A3: n in dom (canFS S) and

A4: x = (canFS S) . n by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A3;

len (canFS S) = card S by FINSEQ_1:93;

then A5: n in Seg (card S) by A3, FINSEQ_1:def 3;

then A6: n in dom (FDprobSEQ t) by Def3;

n in dom (FDprobSEQ s) by A5, Def3;

hence FDprobability (x,s) = (FDprobSEQ s) . n by A4, Def3

.= FDprobability (x,t) by A2, A4, A6, Def3 ;

:: thesis: verum

suppose A7:
not x in S
; :: thesis: FDprobability (x,t) = FDprobability (x,s)

not x in rng t
by A7;

then rng t misses {x} by ZFMISC_1:50;

then A8: t " {x} = {} by RELAT_1:138;

not x in rng s by A7;

then rng s misses {x} by ZFMISC_1:50;

then s " {x} = {} by RELAT_1:138;

hence FDprobability (x,s) = 0

.= FDprobability (x,t) by A8 ;

:: thesis: verum

end;then rng t misses {x} by ZFMISC_1:50;

then A8: t " {x} = {} by RELAT_1:138;

not x in rng s by A7;

then rng s misses {x} by ZFMISC_1:50;

then s " {x} = {} by RELAT_1:138;

hence FDprobability (x,s) = 0

.= FDprobability (x,t) by A8 ;

:: thesis: verum

now :: thesis: ( s,t -are_prob_equivalent implies FDprobSEQ s = FDprobSEQ t )

hence
( s,t -are_prob_equivalent iff FDprobSEQ s = FDprobSEQ t )
by A1; :: thesis: verumassume A9:
s,t -are_prob_equivalent
; :: thesis: FDprobSEQ s = FDprobSEQ t

hence FDprobSEQ s = FDprobSEQ t by A10, Def3; :: thesis: verum

end;A10: now :: thesis: for n being Nat st n in dom (FDprobSEQ t) holds

(FDprobSEQ t) . n = FDprobability (((canFS S) . n),s)

dom (FDprobSEQ t) = Seg (card S)
by Def3;(FDprobSEQ t) . n = FDprobability (((canFS S) . n),s)

let n be Nat; :: thesis: ( n in dom (FDprobSEQ t) implies (FDprobSEQ t) . n = FDprobability (((canFS S) . n),s) )

assume n in dom (FDprobSEQ t) ; :: thesis: (FDprobSEQ t) . n = FDprobability (((canFS S) . n),s)

hence (FDprobSEQ t) . n = FDprobability (((canFS S) . n),t) by Def3

.= FDprobability (((canFS S) . n),s) by A9 ;

:: thesis: verum

end;assume n in dom (FDprobSEQ t) ; :: thesis: (FDprobSEQ t) . n = FDprobability (((canFS S) . n),s)

hence (FDprobSEQ t) . n = FDprobability (((canFS S) . n),t) by Def3

.= FDprobability (((canFS S) . n),s) by A9 ;

:: thesis: verum

hence FDprobSEQ s = FDprobSEQ t by A10, Def3; :: thesis: verum