:: deftheorem Def7 defines Det MATRIXJ1:def 7 :
for K being Field
for R being FinSequence_of_Square-Matrix of K
for b₃ being FinSequence of K holds
( b₃ = Det R iff ( dom b₃ = dom R & ( for i being Nat st i in dom b₃ holds
b₃ . i = Det (R . i) ) ) );