for n being Nat
for K being Field
for M being V185(b₂) Matrix of n,K st the_rank_of M = n holds
lines M is Basis of (n -VectSp_over K)