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 )

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)

proof

let x be set ; :: thesis: FDprobability (x,t) = FDprobability (x,s)

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

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;

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;

end;

end;

hence s,t -are_prob_equivalent ; :: thesis: verum

end;

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

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

A10: now :: thesis: for n being Nat st n in dom (FDprobSEQ t) holds
(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;

dom (FDprobSEQ t) = Seg (card S) by Def3;
hence FDprobSEQ s = FDprobSEQ t by A10, Def3; :: thesis: verum

end;

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