theorem Th36: :: MATRIXR2:36

for D being non empty set
for n being Nat
for A being Matrix of n,D
for p being FinSequence of D
for i being Nat st p = A . i & i in Seg n holds
len p = n