let S be non empty 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

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 set such that
A3: n in dom (canFS S) and
A4: x = (canFS S) . n by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A3;
len (canFS S) = card S by UPROOTS:5;
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

A8: t " {x} = {}

proof

assume t " {x} <> {} ; :: thesis: contradiction
then consider y being set such that
A9: y in t " {x} by XBOOLE_0:def 1;
y in dom t by A9, FUNCT_1:def 13;
then t . y in rng t by FUNCT_1:12;
then A10: t . y in S ;
t . y in {x} by A9, FUNCT_1:def 13;
hence contradiction by A7, A10, TARSKI:def 1; :: thesis: verum

end;

s " {x} = {}

proof

assume s " {x} <> {} ; :: thesis: contradiction
then consider y being set such that
A11: y in s " {x} by XBOOLE_0:def 1;
y in dom s by A11, FUNCT_1:def 13;
then s . y in rng s by FUNCT_1:12;
then A12: s . y in S ;
s . y in {x} by A11, FUNCT_1:def 13;
hence contradiction by A7, A12, TARSKI:def 1; :: thesis: verum

end;

hence FDprobability x,s = 0
.= FDprobability x,t by A8 ;
:: thesis: verum

end;

end;

end;

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

end;

now

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

A14: now

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 A13, Def4 ;
:: thesis: verum

end;

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

end;

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