let D be non empty set ; :: thesis: for m, n being Nat
for A being Matrix of D
for nt, nt1 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 nt, nt1 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 nt, nt1 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 nt, nt1 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 :: thesis: for i, j being Nat st [i,j] in Indices (Segm (A,nt1,mt)) holds
(Segm (A,nt1,mt)) * (i,j) = ((Segm (A,nt,mt)) * f) * (i,j)

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_0:25;
then A3: i in Seg n by A2, ZFMISC_1:87;
Indices (Segm (A,nt1,mt)) = Indices (Segm (A,nt,mt)) by MATRIX_0:26;
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 12;
Seg n = dom nt1 by FINSEQ_2:124;
then nt1 . i9 = nt . (f . i) by A1, A3, FUNCT_1:12;
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_0:27; :: thesis: verum