let n be Nat; :: thesis: 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 )
let K be Field; :: thesis: 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 )
let V be finite Subset of (n -VectSp_over K); :: thesis: ex M being Matrix of card V,n,K st
( M is without_repeated_line & lines M = V )
set cV = card V;
card (Seg (card V)) = card V by FINSEQ_1:57;
then Seg (card V),V are_equipotent by CARD_1:5;
then consider m being Function such that
A1: m is one-to-one and
A2: dom m = Seg (card V) and
A3: rng m = V by WELLORD2:def 4;
reconsider M = m as FinSequence by A2, FINSEQ_1:def 2;

now :: thesis: for x being object st x in rng M holds
ex p being FinSequence of K st
( x = p & len p = n )

let x be object ; :: thesis: ( x in rng M implies ex p being FinSequence of K st
( x = p & len p = n ) )
assume x in rng M ; :: thesis: ex p being FinSequence of K st
( x = p & len p = n )
then reconsider p = x as Element of n -tuples_on the carrier of K by A3, Th102;
len p = n by CARD_1:def 7;
hence ex p being FinSequence of K st
( x = p & len p = n ) ; :: thesis: verum

end;

then reconsider M = M as Matrix of K by MATRIX_0:9;
A4: len M = card V by A2, FINSEQ_1:def 3;
the carrier of (n -VectSp_over K) = n -tuples_on the carrier of K by Th102;
then for p being FinSequence of K st p in rng M holds
len p = n by A3, CARD_1:def 7;
then M is Matrix of card V,n,K by A4, MATRIX_0:def 2;
hence ex M being Matrix of card V,n,K st
( M is without_repeated_line & lines M = V ) by A1, A3; :: thesis: verum