let R be non degenerated commutative Ring; :: thesis: for n being Nat holds Lin (Base (R,n)) = R ^* n
let n be Nat; :: thesis: Lin (Base (R,n)) = R ^* n
set V = Lin (Base (R,n));
set B = Base (R,n);
A: the carrier of (Lin (Base (R,n))) = { (Sum l) where l is Linear_Combination of Base (R,n) : verum } by VECTSP_7:def 2;
B: the carrier of (Lin (Base (R,n))) c= the carrier of (R ^* n) by VECTSP_4:def 2;

now :: thesis: for o being object st o in the carrier of (R ^* n) holds
o in the carrier of (Lin (Base (R,n)))

let o be object ; :: thesis: ( o in the carrier of (R ^* n) implies o in the carrier of (Lin (Base (R,n))) )
assume o in the carrier of (R ^* n) ; :: thesis: o in the carrier of (Lin (Base (R,n)))
then consider l being Linear_Combination of Base (R,n) such that
C: Sum l = o by lemspan1;
thus o in the carrier of (Lin (Base (R,n))) by C, A; :: thesis: verum

end;

then the carrier of (R ^* n) c= the carrier of (Lin (Base (R,n))) ;
hence Lin (Base (R,n)) = R ^* n by B, XBOOLE_0:def 10, VECTSP_4:31; :: thesis: verum