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