let n, m be Nat; :: thesis: for D being non empty set
for F being Function of (Seg n),(Seg n)
for M being Matrix of n,m,D holds
( Indices M = Indices (M * F) & ( for i, j being Nat st [i,j] in Indices M holds
ex k being Nat st
( F . i = k & [k,j] in Indices M & (M * F) * (i,j) = M * (k,j) ) ) )
let D be non empty set ; :: thesis: for F being Function of (Seg n),(Seg n)
for M being Matrix of n,m,D holds
( Indices M = Indices (M * F) & ( for i, j being Nat st [i,j] in Indices M holds
ex k being Nat st
( F . i = k & [k,j] in Indices M & (M * F) * (i,j) = M * (k,j) ) ) )
let F be Function of (Seg n),(Seg n); :: thesis: for M being Matrix of n,m,D holds
( Indices M = Indices (M * F) & ( for i, j being Nat st [i,j] in Indices M holds
ex k being Nat st
( F . i = k & [k,j] in Indices M & (M * F) * (i,j) = M * (k,j) ) ) )
let M be Matrix of n,m,D; :: thesis: ( Indices M = Indices (M * F) & ( for i, j being Nat st [i,j] in Indices M holds
ex k being Nat st
( F . i = k & [k,j] in Indices M & (M * F) * (i,j) = M * (k,j) ) ) )
set Mp = M * F;
A1: dom F = Seg n by FUNCT_2:52;
A2: width M = width (M * F) by Def4;
len M = len (M * F) by Def4;
hence Indices M = Indices (M * F) by A2, MATRIX_4:55; :: thesis: for i, j being Nat st [i,j] in Indices M holds
ex k being Nat st
( F . i = k & [k,j] in Indices M & (M * F) * (i,j) = M * (k,j) )
let i, j be Nat; :: thesis: ( [i,j] in Indices M implies ex k being Nat st
( F . i = k & [k,j] in Indices M & (M * F) * (i,j) = M * (k,j) ) )
assume A3: [i,j] in Indices M ; :: thesis: ex k being Nat st
( F . i = k & [k,j] in Indices M & (M * F) * (i,j) = M * (k,j) )
Indices M = [:(Seg n),(Seg (width M)):] by MATRIX_0:25;
then i in Seg n by A3, ZFMISC_1:87;
then A4: F . i in rng F by A1, FUNCT_1:def 3;
A5: rng F c= Seg n by RELAT_1:def 19;
then F . i in Seg n by A4;
then reconsider k = F . i as Element of NAT ;
j in Seg (width M) by A3, ZFMISC_1:87;
then [k,j] in [:(Seg n),(Seg (width M)):] by A4, A5, ZFMISC_1:87;
then A6: [k,j] in Indices M by MATRIX_0:25;
(M * F) * (i,j) = M * (k,j) by A3, Def4;
hence ex k being Nat st
( F . i = k & [k,j] in Indices M & (M * F) * (i,j) = M * (k,j) ) by A6; :: thesis: verum