let D be non empty set ; :: thesis: for n, m being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt1, mt 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 n, m be Nat; :: thesis: for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt1, mt 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 mt1, mt 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 mt1, mt 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 mt1, mt 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_1:def 3;
then width (Segm A,nt,mt) = 0 by A2, Th1, MATRIX_1:def 4;
then len ((Segm A,nt,mt) @ ) = 0 by MATRIX_1:def 7;
then A3: (Segm A,nt,mt) @ = {} ;
len (Segm A,nt,mt1) = n by MATRIX_1:def 3;
then width (Segm A,nt,mt1) = 0 by A2, Th1, MATRIX_1:def 4;
then len ((Segm A,nt,mt1) @ ) = 0 by MATRIX_1:def 7;
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_2:12;
len (Segm A,nt,mt1) = n by A4, Th1;
then A7: width ((Segm A,nt,mt1) @ ) = n by A4, A5, MATRIX_2:12;
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_2:12;
len ((Segm A,nt,mt) @ ) = m by A4, A8, MATRIX_2:12;
then reconsider S9 = (Segm A,nt,mt) @ , S19 = (Segm A,nt,mt1) @ as Matrix of m,n,D by A4, A9, A7, A6, MATRIX_1:20;
set Sf = S9 * f;

now

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_1:def 7;
then A12: S19 * i,j = (Segm A,nt,mt1) * j,i by MATRIX_1:def 7;
Indices S19 = [:(Seg m),(Seg n):] by A7, MATRIX_1:26;
then A13: i in Seg m by A10, ZFMISC_1:106;
Indices S19 = Indices S9 by MATRIX_1:27;
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 13;
Seg m = dom mt1 by FINSEQ_2:144;
then mt1 . i9 = mt . (f . i) by A1, A13, FUNCT_1:22;
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_1:def 7;
then S9 * k,j = (Segm A,nt,mt) * j,k by MATRIX_1:def 7;
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_1:28; :: thesis: verum

end;

end;