let V be RealLinearSpace; :: thesis: for W being Subspace of V
for w being VECTOR of holds w is VECTOR of
let W be Subspace of V; :: thesis: for w being VECTOR of holds w is VECTOR of
let w be VECTOR of ; :: thesis: w is VECTOR of
w in V by Th17, RLVECT_1:3;
hence w is VECTOR of by STRUCT_0:def 5; :: thesis: verum