:: deftheorem Def4 defines carr VECTSP_8:def 4 :
for F being Field
for VS being strict VectSp of F
for b₃ being Function of (Subspaces VS),(bool the carrier of VS) holds
( b₃ = carr VS iff for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
b₃ . h = the carrier of H );