let M be non 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 Element of 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 Element of 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 Element of 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 Element of 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:31;

now

let k be Element of 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:31;
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_2:18 ; :: thesis: verum

end;

hence ( len p = len M & ( for k being Element of 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 Element of 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:31;
A10: dom (Infor_FinSeq_of M) = dom M by A1, FINSEQ_3:31;

now

let k be Element of 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_2:18
.= Entropy (Line M,k) by A9, A11, Th53 ; :: thesis: verum

end;

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