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