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

proof

consider m being Nat such that
A1: for x being set st x in rng M holds
ex p being FinSequence of st
( x = p & len p = m ) by MATRIX_1:9;
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 A2: x in rng M ; :: thesis: x in the carrier of (n -VectSp_over K)
consider p being FinSequence of such that
A3: x = p and
len p = m by A2, A1;
len p = n by A2, A3, MATRIX_1:def 3;
then p is Element of n -tuples_on the carrier of K 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 ; :: thesis: verum