let M be empty-yielding Conditional_Probability Matrix of REAL; :: thesis: for p being FinSequence of REAL holds
( p = Entropy_of_Cond_Prob M iff ( len p = len M & ( for k being Nat st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) ) )
let p be FinSequence of REAL ; :: thesis: ( p = Entropy_of_Cond_Prob M iff ( len p = len M & ( for k being Nat st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) ) )
A1: len (Infor_FinSeq_of M) = len M by Def8;

hereby :: thesis: ( len p = len M & ( for k being Nat st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) implies p = Entropy_of_Cond_Prob M )

assume A2: p = Entropy_of_Cond_Prob M ; :: thesis: ( len p = len M & ( for k being Nat st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) )
then A3: len p = len M by Def11;
then A4: dom p = dom M by FINSEQ_3:29;

now :: thesis: for k being Nat st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k))

let k be Nat; :: thesis: ( k in dom p implies p . k = - (Sum ((Infor_FinSeq_of M) . k)) )
assume A5: k in dom p ; :: thesis: p . k = - (Sum ((Infor_FinSeq_of M) . k))
A6: k in dom (Infor_FinSeq_of M) by A1, A3, A5, FINSEQ_3:29;
thus p . k = Entropy (Line (M,k)) by A2, A5, Def11
.= - (Sum (Line ((Infor_FinSeq_of M),k))) by A4, A5, Th53
.= - (Sum ((Infor_FinSeq_of M) . k)) by A6, MATRIX_0:60 ; :: thesis: verum

end;

hence ( len p = len M & ( for k being Nat st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ) ) by A2, Def11; :: thesis: verum

end;

assume that
A7: len p = len M and
A8: for k being Nat st k in dom p holds
p . k = - (Sum ((Infor_FinSeq_of M) . k)) ; :: thesis: p = Entropy_of_Cond_Prob M
A9: dom p = dom M by A7, FINSEQ_3:29;
A10: dom (Infor_FinSeq_of M) = dom M by A1, FINSEQ_3:29;

now :: thesis: for k being Nat st k in dom p holds
p . k = Entropy (Line (M,k))

let k be Nat; :: thesis: ( k in dom p implies p . k = Entropy (Line (M,k)) )
assume A11: k in dom p ; :: thesis: p . k = Entropy (Line (M,k))
thus p . k = - (Sum ((Infor_FinSeq_of M) . k)) by A8, A11
.= - (Sum (Line ((Infor_FinSeq_of M),k))) by A10, A9, A11, MATRIX_0:60
.= Entropy (Line (M,k)) by A9, A11, Th53 ; :: thesis: verum

end;

hence p = Entropy_of_Cond_Prob M by A7, Def11; :: thesis: verum