:: deftheorem Def8 defines 1. MATRIXJ1:def 8 :
for K being Field
for f being FinSequence of NAT
for b₃ being FinSequence_of_Square-Matrix of K holds
( b₃ = 1. (K,f) iff ( dom b₃ = dom f & ( for i being Nat st i in dom b₃ holds
b₃ . i = 1. (K,(f . i)) ) ) );