:: deftheorem Def1 defines Segm MATRIX13:def 1 :
for D being non empty set
for M being Matrix of D
for n, m being Nat
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for b₇ being Matrix of n,m,D holds
( b₇ = Segm (M,nt,mt) iff for i, j being Nat st [i,j] in Indices b₇ holds
b₇ * (i,j) = M * ((nt . i),(mt . j)) );