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 S1 = Segm A,nt,mt1;
set S = Segm A,nt,mt;

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,mt1) = n & len (Segm A,nt,mt) = n ) by MATRIX_1:def 3;
then ( width (Segm A,nt,mt1) = 0 & width (Segm A,nt,mt) = 0 ) by A2, Th1, MATRIX_1:def 4;
then ( len ((Segm A,nt,mt1) @ ) = 0 & len ((Segm A,nt,mt) @ ) = 0 ) by MATRIX_1:def 7;
then ( (Segm A,nt,mt1) @ = {} & (Segm A,nt,mt) @ = {} ) ;
hence (Segm A,nt,mt1) @ = ((Segm A,nt,mt) @ ) * f ; :: thesis: verum

end;

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

then ( len (Segm A,nt,mt) = n & width (Segm A,nt,mt) = m & len (Segm A,nt,mt1) = n & width (Segm A,nt,mt1) = m ) by Th1;
then A4: ( width ((Segm A,nt,mt) @ ) = n & len ((Segm A,nt,mt) @ ) = m & width ((Segm A,nt,mt1) @ ) = n & len ((Segm A,nt,mt1) @ ) = m ) by A3, MATRIX_2:12;
then reconsider S' = (Segm A,nt,mt) @ , S1' = (Segm A,nt,mt1) @ as Matrix of m,n,D by A3, MATRIX_1:20;
set Sf = S' * f;

now

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

end;

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

end;

end;