let M be m-nonnegative Matrix of REAL ; :: thesis: for M1 being Matrix of REAL holds
( M1 = Infor_FinSeq_of M iff ( len M1 = len M & width M1 = width M & ( for i, j being Element of NAT st [i,j] in Indices M1 holds
M1 * i,j = (M * i,j) * (log 2,(M * i,j)) ) ) )
let M1 be Matrix of REAL ; :: thesis: ( M1 = Infor_FinSeq_of M iff ( len M1 = len M & width M1 = width M & ( for i, j being Element of NAT st [i,j] in Indices M1 holds
M1 * i,j = (M * i,j) * (log 2,(M * i,j)) ) ) )
hereby :: thesis: ( len M1 = len M & width M1 = width M & ( for i, j being Element of NAT st [i,j] in Indices M1 holds
M1 * i,j = (M * i,j) * (log 2,(M * i,j)) ) implies M1 = Infor_FinSeq_of M )
assume A1:
M1 = Infor_FinSeq_of M
;
:: thesis: ( len M1 = len M & width M1 = width M & ( for i, j being Element of NAT st [i,j] in Indices M1 holds
M1 * i,j = (M * i,j) * (log 2,(M * i,j)) ) )then A2:
(
len M1 = len M &
width M1 = width M )
by Def8;
now let i,
j be
Element of
NAT ;
:: thesis: ( [i,j] in Indices M1 implies M1 * i,j = (M * i,j) * (log 2,(M * i,j)) )assume A3:
[i,j] in Indices M1
;
:: thesis: M1 * i,j = (M * i,j) * (log 2,(M * i,j))A4:
(
i in Seg (len M1) &
j in Seg (width M1) )
by A3, MATRPROB:12;
then A5:
i in dom M
by A2, FINSEQ_1:def 3;
then reconsider p =
Line M,
i as
nonnegative FinSequence of
REAL by Th19;
A6:
len p = width M
by MATRIX_1:def 8;
A7:
p . j = M * i,
j
by A2, A4, MATRIX_1:def 8;
len p = len (Infor_FinSeq_of p)
by Th47;
then A8:
j in dom (Infor_FinSeq_of p)
by A2, A4, A6, FINSEQ_1:def 3;
thus M1 * i,
j =
(Line M1,i) . j
by A4, MATRIX_1:def 8
.=
(Infor_FinSeq_of p) . j
by A1, A5, Th53
.=
(M * i,j) * (log 2,(M * i,j))
by A7, A8, Th47
;
:: thesis: verum end; hence
(
len M1 = len M &
width M1 = width M & ( for
i,
j being
Element of
NAT st
[i,j] in Indices M1 holds
M1 * i,
j = (M * i,j) * (log 2,(M * i,j)) ) )
by A1, Def8;
:: thesis: verum
end;
assume A9:
( len M1 = len M & width M1 = width M & ( for i, j being Element of NAT st [i,j] in Indices M1 holds
M1 * i,j = (M * i,j) * (log 2,(M * i,j)) ) )
; :: thesis: M1 = Infor_FinSeq_of M
then A10:
( dom M1 = dom M & Seg (width M1) = Seg (width M) )
by FINSEQ_3:31;
for k being Element of NAT st k in dom M1 holds
M1 . k = mlt (Line M,k),(FinSeq_log 2,(Line M,k))
proof
let k be
Element of
NAT ;
:: thesis: ( k in dom M1 implies M1 . k = mlt (Line M,k),(FinSeq_log 2,(Line M,k)) )
assume A11:
k in dom M1
;
:: thesis: M1 . k = mlt (Line M,k),(FinSeq_log 2,(Line M,k))
reconsider p =
Line M,
k as
nonnegative FinSequence of
REAL by A10, A11, Th19;
A12:
k in Seg (len M)
by A9, A11, FINSEQ_1:def 3;
A13:
(
len p = width M &
len (FinSeq_log 2,p) = len p )
by Def6, MATRIX_1:def 8;
then A14:
len (mlt p,(FinSeq_log 2,p)) = len p
by MATRPROB:30;
A15:
len (M1 . k) = width M1
by A11, GOBRD13:4;
then A16:
dom (M1 . k) = dom (mlt p,(FinSeq_log 2,p))
by A9, A13, A14, FINSEQ_3:31;
now let j be
Nat;
:: thesis: ( j in dom (M1 . k) implies (M1 . k) . b1 = (mlt p,(FinSeq_log 2,p)) . b1 )assume A17:
j in dom (M1 . k)
;
:: thesis: (M1 . k) . b1 = (mlt p,(FinSeq_log 2,p)) . b1A18:
j in NAT
by ORDINAL1:def 13;
A19:
j in Seg (width M)
by A9, A15, A17, FINSEQ_1:def 3;
then A20:
[k,j] in Indices M
by A12, MATRPROB:12;
A21:
[k,j] in Indices M1
by A11, A17, MATRPROB:13;
A22:
j in dom (FinSeq_log 2,p)
by A13, A19, FINSEQ_1:def 3;
A23:
(M1 . k) . j =
M1 * k,
j
by A18, A21, MATRPROB:14
.=
(M * k,j) * (log 2,(M * k,j))
by A9, A18, A21
;
A24:
p . j = M * k,
j
by A19, MATRIX_1:def 8;
A25:
(mlt p,(FinSeq_log 2,p)) . j =
(p . j) * ((FinSeq_log 2,p) . j)
by A16, A17, RVSUM_1:86
.=
(M * k,j) * ((FinSeq_log 2,p) . j)
by A19, MATRIX_1:def 8
;
end;
hence
M1 . k = mlt (Line M,k),
(FinSeq_log 2,(Line M,k))
by A16, FINSEQ_1:17;
:: thesis: verum
end;
hence
M1 = Infor_FinSeq_of M
by A9, Def8; :: thesis: verum