let D be non empty set ; :: thesis: for m, n being Nat
for A being Matrix of D
for nt1, nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for f being Function of (Seg n),(Seg n) st nt1 = nt * f holds
Segm A,nt1,mt = (Segm A,nt,mt) * f
let m, n be Nat; :: thesis: for A being Matrix of D
for nt1, nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for f being Function of (Seg n),(Seg n) st nt1 = nt * f holds
Segm A,nt1,mt = (Segm A,nt,mt) * f
let A be Matrix of D; :: thesis: for nt1, nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for f being Function of (Seg n),(Seg n) st nt1 = nt * f holds
Segm A,nt1,mt = (Segm A,nt,mt) * f
let nt1, nt be Element of n -tuples_on NAT ; :: thesis: for mt being Element of m -tuples_on NAT
for f being Function of (Seg n),(Seg n) st nt1 = nt * f holds
Segm A,nt1,mt = (Segm A,nt,mt) * f
let mt be Element of m -tuples_on NAT ; :: thesis: for f being Function of (Seg n),(Seg n) st nt1 = nt * f holds
Segm A,nt1,mt = (Segm A,nt,mt) * f
let f be Function of (Seg n),(Seg n); :: thesis: ( nt1 = nt * f implies Segm A,nt1,mt = (Segm A,nt,mt) * f )
assume A1: nt1 = nt * f ; :: thesis: Segm A,nt1,mt = (Segm A,nt,mt) * f
set S1 = Segm A,nt1,mt;
set S = Segm A,nt,mt;
set Sf = (Segm A,nt,mt) * f;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices (Segm A,nt1,mt) implies (Segm A,nt1,mt) * i,j = ((Segm A,nt,mt) * f) * i,j )
assume A2: [i,j] in Indices (Segm A,nt1,mt) ; :: thesis: (Segm A,nt1,mt) * i,j = ((Segm A,nt,mt) * f) * i,j
Indices (Segm A,nt1,mt) = Indices (Segm A,nt,mt) by MATRIX_1:27;
then consider k being Nat such that
A3: ( f . i = k & [k,j] in Indices (Segm A,nt,mt) & ((Segm A,nt,mt) * f) * i,j = (Segm A,nt,mt) * k,j ) by A2, MATRIX11:37;
reconsider i' = i, j' = j, k' = k as Element of NAT by ORDINAL1:def 13;
Indices (Segm A,nt1,mt) = [:(Seg n),(Seg (width (Segm A,nt1,mt))):] by MATRIX_1:26;
then ( i in Seg n & Seg n = dom nt1 ) by A2, FINSEQ_2:144, ZFMISC_1:106;
then nt1 . i' = nt . (f . i) by A1, FUNCT_1:22;
hence (Segm A,nt1,mt) * i,j = A * (nt . k'),(mt . j') by A2, A3, Def1
.= ((Segm A,nt,mt) * f) * i,j by A3, Def1 ;
:: thesis: verum

end;

hence Segm A,nt1,mt = (Segm A,nt,mt) * f by MATRIX_1:28; :: thesis: verum