:: deftheorem Def6 defines FinSeq_log ENTROPY1:def 6 :
for a being Real
for p being FinSequence of REAL st p is nonnegative holds
for b₃ being FinSequence of REAL holds
( b₃ = FinSeq_log (a,p) iff ( len b₃ = len p & ( for k being Nat st k in dom b₃ holds
( ( p . k > 0 implies b₃ . k = log (a,(p . k)) ) & ( p . k = 0 implies b₃ . k = 0 ) ) ) ) );