let F be Field; :: thesis: for VS being strict VectSp of F
for H being strict Subspace of VS holds 0. VS in (carr VS) . H
let VS be strict VectSp of F; :: thesis: for H being strict Subspace of VS holds 0. VS in (carr VS) . H
let H be strict Subspace of VS; :: thesis: 0. VS in (carr VS) . H
H in Subspaces VS by VECTSP_5:def 3;
then A1: (carr VS) . H = the carrier of H by Def4;
0. H = 0. VS by VECTSP_4:11;
hence 0. VS in (carr VS) . H by A1; :: thesis: verum