theorem Th34: :: MATRIX13:34

for D being non empty set
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