let m, n be Nat; :: thesis: for K being Field
for M being Matrix of m,n,K holds rng M is Subset of (n -VectSp_over K)
let K be Field; :: thesis: for M being Matrix of m,n,K holds rng M is Subset of (n -VectSp_over K)
let M be Matrix of m,n,K; :: thesis: rng M is Subset of (n -VectSp_over K)
rng M c= the carrier of (n -VectSp_over K)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng M or x in the carrier of (n -VectSp_over K) )
assume A1: x in rng M ; :: thesis: x in the carrier of (n -VectSp_over K)
consider m being Nat such that
A2: for x being set st x in rng M holds
ex p being FinSequence of K st
( x = p & len p = m ) by MATRIX_1:9;
consider p being FinSequence of K such that
A3: ( x = p & len p = m ) by A1, A2;
len p = n by A1, A3, MATRIX_1:def 3;
then ( p is Element of n -tuples_on the carrier of K & not n -tuples_on the carrier of K is empty ) by FINSEQ_2:110;
then p in n -tuples_on the carrier of K ;
hence x in the carrier of (n -VectSp_over K) by A3, Th102; :: thesis: verum

end;

hence rng M is Subset of (n -VectSp_over K) ; :: thesis: verum