:: deftheorem Def3 defines Len MATRIXJ1:def 3 :
for D being non empty set
for F being FinSequence_of_Matrix of D
for b₃ being FinSequence of NAT holds
( b₃ = Len F iff ( dom b₃ = dom F & ( for i being Nat st i in dom b₃ holds
b₃ . i = len (F . i) ) ) );