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
consider m being Nat such that
A1: for x being object st x in rng M holds
ex p being FinSequence of K st
( x = p & len p = m ) by MATRIX_0:9;
let x be object ; :: 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 K such that
A3: x = p and
len p = m by A2, A1;
len p = n by A2, A3, MATRIX_0:def 2;
then p is Element of n -tuples_on the carrier of K by FINSEQ_2:92;
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