:: deftheorem Def5 defines Mx2FinS ENTROPY1:def 5 :
for D being non empty set
for M being Matrix of D
for b₃ being FinSequence of D holds
( ( len M = 0 implies ( b₃ = Mx2FinS M iff b₃ = {} ) ) & ( not len M = 0 implies ( b₃ = Mx2FinS M iff ex p being FinSequence of D * st
( b₃ = p . (len M) & len p = len M & p . 1 = M . 1 & ( for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) ) ) ) );