let F be Field; :: thesis: for V, W being VectSp of F st (Omega). W is Subspace of V holds
W is Subspace of V
let V, W be VectSp of F; :: thesis: ( (Omega). W is Subspace of V implies W is Subspace of V )
assume A1: (Omega). W is Subspace of V ; :: thesis: W is Subspace of V
hence 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). W)
.= 0. V by A1, VECTSP_4:def 2 ; :: 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 A1, VECTSP_4:def 2; :: thesis: verum