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 S = Segm A,nt,mt;
set S1 = Segm A,nt1,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) = [:(Seg n),(Seg (width (Segm A,nt1,mt))):] by MATRIX_1:26;
then A3: i in Seg n by A2, ZFMISC_1:106;
Indices (Segm A,nt1,mt) = Indices (Segm A,nt,mt) by MATRIX_1:27;
then consider k being Nat such that
A4: f . i = k and
A5: [k,j] in Indices (Segm A,nt,mt) and
A6: ((Segm A,nt,mt) * f) * i,j = (Segm A,nt,mt) * k,j by A2, MATRIX11:37;
reconsider i9 = i, j9 = j, k9 = k as Element of NAT by ORDINAL1:def 13;
Seg n = dom nt1 by FINSEQ_2:144;
then nt1 . i9 = nt . (f . i) by A1, A3, FUNCT_1:22;
hence (Segm A,nt1,mt) * i,j = A * (nt . k9),(mt . j9) by A2, A4, Def1
.= ((Segm A,nt,mt) * f) * i,j by A5, A6, Def1 ;
:: thesis: verum

end;

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