let F be Field; :: thesis: for V being VectSp of F
for W being Subspace of (Omega). V holds W is Subspace of V
let V be VectSp of F; :: thesis: for W being Subspace of (Omega). V holds W is Subspace of V
let W be Subspace of (Omega). V; :: thesis: W is Subspace of V
thus the carrier of W c= the carrier of V by VECTSP_4:def 2; :: according to VECTSP_4:def 2 :: thesis: ( 0. W = 0. V & the U5 of W = K112( the U5 of V, the carrier of W) & the lmult of W = K5( the lmult of V,[: the carrier of F, the carrier of W:]) )
thus 0. W = 0. ((Omega). V) by VECTSP_4:def 2
.= 0. V ; :: thesis: ( the U5 of W = K112( the U5 of V, the carrier of W) & the lmult of W = K5( the lmult of V,[: the carrier of F, the carrier of W:]) )
thus ( the U5 of W = K112( the U5 of V, the carrier of W) & the lmult of W = K5( the lmult of V,[: the carrier of F, the carrier of W:]) ) by VECTSP_4:def 2; :: thesis: verum