for F being Field
for S being OrtSp of F
for a, b being Element of S
for l being Element of F st not a _|_ & not l = 0. F holds
( not a _|_ & not l * a _|_ )