set S = the VectSp of K;
take <* the VectSp of K*> ; :: thesis: for S being set st S in rng <* the VectSp of K*> holds
S is VectSp of K
let x be set ; :: thesis: ( x in rng <* the VectSp of K*> implies x is VectSp of K )
assume that
A1: x in rng <* the VectSp of K*> and
A2: x is not VectSp of K ; :: thesis: contradiction
x in { the VectSp of K} by A1, FINSEQ_1:38;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum