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;
( len M = len (M * F) & width M = width (M * F) ) by Def4;
hence Indices M = Indices (M * F) by 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 A1: [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_1:26;
then A2: ( i in Seg n & j in Seg (width M) & dom F = Seg n ) by A1, FUNCT_2:67, ZFMISC_1:106;
then A3: ( F . i in rng F & rng F c= Seg n ) by FUNCT_1:def 5, RELAT_1:def 19;
then F . i in Seg n ;
then reconsider k = F . i as Element of NAT ;
( [k,j] in [:(Seg n),(Seg (width M)):] & Indices M = [:(Seg n),(Seg (width M)):] ) by A2, A3, MATRIX_1:26, ZFMISC_1:106;
then ( [k,j] in Indices M & (M * F) * i,j = M * k,j ) by A1, Def4;
hence ex k being Nat st
( F . i = k & [k,j] in Indices M & (M * F) * i,j = M * k,j ) ; :: thesis: verum