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