let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for V being VectSp of K
for V1 being Subspace of V
for W1 being Subspace of V1
for v being Vector of V st v in W1 holds
v is Vector of V1
let V be VectSp of K; :: thesis: for V1 being Subspace of V
for W1 being Subspace of V1
for v being Vector of V st v in W1 holds
v is Vector of V1
let V1 be Subspace of V; :: thesis: for W1 being Subspace of V1
for v being Vector of V st v in W1 holds
v is Vector of V1
let W1 be Subspace of V1; :: thesis: for v being Vector of V st v in W1 holds
v is Vector of V1
let v be Vector of V; :: thesis: ( v in W1 implies v is Vector of V1 )
assume v in W1 ; :: thesis: v is Vector of V1
then ( the carrier of W1 c= the carrier of V1 & v in the carrier of W1 ) by VECTSP_4:def 2;
hence v is Vector of V1 ; :: thesis: verum