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
A1: 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 i in dom (FDprobSEQ s) ; :: thesis: (FDprobSEQ s) . i >= 0
then (FDprobSEQ s) . i = FDprobability (((canFS S) . i),s) by Def3;
hence (FDprobSEQ s) . i >= 0 ; :: thesis: verum

end;

Sum (FDprobSEQ s) = 1 by Th20;
hence FDprobSEQ s is ProbFinS by A1, MATRPROB:def 5; :: thesis: verum