theorem Th33: :: MATRIX13:33

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