theorem Th10: :: MATRPROB:10

for D being set
for s being FinSequence holds
( s is Matrix of D iff ex n being Nat st
for i being Nat st i in dom s holds
ex p being FinSequence of D st
( s . i = p & len p = n ) )