for n being Nat
for K being Field
for V being finite Subset of (n -VectSp_over K) ex M being Matrix of card V,n,K st
( M is without_repeated_line & lines M = V )