let S be non empty finite set ; :: thesis: for s being non empty FinSequence of S holds FDprobSEQ s is ProbFinS
let s be non empty FinSequence of S; :: thesis: FDprobSEQ s is ProbFinS
L0: Sum (FDprobSEQ s) = 1 by FREQDISTSUM;
for i being Element of NAT st i in dom (FDprobSEQ s) holds
(FDprobSEQ s) . i >= 0

proof

let i be Element of NAT ; :: thesis: ( i in dom (FDprobSEQ s) implies (FDprobSEQ s) . i >= 0 )
assume CAS: i in dom (FDprobSEQ s) ; :: thesis: (FDprobSEQ s) . i >= 0
(FDprobSEQ s) . i = FDprobability ((canFS S) . i),s by CAS, defFREQDIST;
hence (FDprobSEQ s) . i >= 0 ; :: thesis: verum

end;

hence FDprobSEQ s is ProbFinS by L0, MATRPROB:def 5; :: thesis: verum