let p be ProbFinS FinSequence of REAL ; :: thesis: for k being Nat st k in dom p & p . k = 1 holds
p has_onlyone_value_in k
let k be Nat; :: thesis: ( k in dom p & p . k = 1 implies p has_onlyone_value_in k )
assume that
A1: k in dom p and
A2: p . k = 1 ; :: thesis: p has_onlyone_value_in k
p . k = Sum p by A2, MATRPROB:def 5;
hence p has_onlyone_value_in k by A1, Th14; :: thesis: verum