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

per cases ( m = 0 or n = 0 or ( m > 0 & n > 0 ) ) ;

suppose A2: ( m = 0 or n = 0 ) ; :: thesis: (Segm (A,nt,mt1)) @ = ((Segm (A,nt,mt)) @) * f

len (Segm (A,nt,mt)) = n by MATRIX_0:def 2;
then width (Segm (A,nt,mt)) = 0 by A2, Th1, MATRIX_0:def 3;
then len ((Segm (A,nt,mt)) @) = 0 by MATRIX_0:def 6;
then A3: (Segm (A,nt,mt)) @ = {} ;
len (Segm (A,nt,mt1)) = n by MATRIX_0:def 2;
then width (Segm (A,nt,mt1)) = 0 by A2, Th1, MATRIX_0:def 3;
then len ((Segm (A,nt,mt1)) @) = 0 by MATRIX_0:def 6;
then (Segm (A,nt,mt1)) @ = {} ;
hence (Segm (A,nt,mt1)) @ = ((Segm (A,nt,mt)) @) * f by A3; :: thesis: verum

end;

suppose A4: ( m > 0 & n > 0 ) ; :: thesis: (Segm (A,nt,mt1)) @ = ((Segm (A,nt,mt)) @) * f

then A5: width (Segm (A,nt,mt1)) = m by Th1;
then A6: len ((Segm (A,nt,mt1)) @) = m by A4, MATRIX_0:54;
len (Segm (A,nt,mt1)) = n by A4, Th1;
then A7: width ((Segm (A,nt,mt1)) @) = n by A4, A5, MATRIX_0:54;
A8: width (Segm (A,nt,mt)) = m by A4, Th1;
len (Segm (A,nt,mt)) = n by A4, Th1;
then A9: width ((Segm (A,nt,mt)) @) = n by A4, A8, MATRIX_0:54;
len ((Segm (A,nt,mt)) @) = m by A4, A8, MATRIX_0:54;
then reconsider S9 = (Segm (A,nt,mt)) @ , S19 = (Segm (A,nt,mt1)) @ as Matrix of m,n,D by A4, A9, A7, A6, MATRIX_0:20;
set Sf = S9 * f;

now :: thesis: for i, j being Nat st [i,j] in Indices S19 holds
S19 * (i,j) = (S9 * f) * (i,j)

let i, j be Nat; :: thesis: ( [i,j] in Indices S19 implies S19 * (i,j) = (S9 * f) * (i,j) )
assume A10: [i,j] in Indices S19 ; :: thesis: S19 * (i,j) = (S9 * f) * (i,j)
A11: [j,i] in Indices (Segm (A,nt,mt1)) by A10, MATRIX_0:def 6;
then A12: S19 * (i,j) = (Segm (A,nt,mt1)) * (j,i) by MATRIX_0:def 6;
Indices S19 = [:(Seg m),(Seg n):] by A7, MATRIX_0:25;
then A13: i in Seg m by A10, ZFMISC_1:87;
Indices S19 = Indices S9 by MATRIX_0:26;
then consider k being Nat such that
A14: f . i = k and
A15: [k,j] in Indices S9 and
A16: (S9 * f) * (i,j) = S9 * (k,j) by A10, MATRIX11:37;
reconsider i9 = i, j9 = j, k9 = k as Element of NAT by ORDINAL1:def 12;
Seg m = dom mt1 by FINSEQ_2:124;
then mt1 . i9 = mt . (f . i) by A1, A13, FUNCT_1:12;
then A17: (Segm (A,nt,mt1)) * (j9,i9) = A * ((nt . j9),(mt . k9)) by A14, A11, Def1;
A18: [j,k] in Indices (Segm (A,nt,mt)) by A15, MATRIX_0:def 6;
then S9 * (k,j) = (Segm (A,nt,mt)) * (j,k) by MATRIX_0:def 6;
hence S19 * (i,j) = (S9 * f) * (i,j) by A16, A18, A12, A17, Def1; :: thesis: verum

end;

hence (Segm (A,nt,mt1)) @ = ((Segm (A,nt,mt)) @) * f by MATRIX_0:27; :: thesis: verum

end;

end;