A1: for i being Nat st i in dom (FDprobSEQ s) holds
(FDprobSEQ s) . i >= 0

proof

let i be 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 Th17;
hence FDprobSEQ s is ProbFinS by A1, MATRPROB:def 5; :: thesis: verum