:: deftheorem Def4 defines Width MATRIXJ1:def 4 :
for D being non empty set
for F being FinSequence_of_Matrix of D
for b₃ being FinSequence of NAT holds
( b₃ = Width F iff ( dom b₃ = dom F & ( for i being Nat st i in dom b₃ holds
b₃ . i = width (F . i) ) ) );