theorem Th12: :: RLAFFIN1:12

for V being RealLinearSpace
for A being Subset of V holds 0 * A c= {(0. V)}