for V being ComplexLinearSpace
for V1 being Subset of V holds
( V1 is linearly-closed iff ( V1 is add-closed & V1 is multi-closed ) ) ;