let F be Field; :: thesis: for S being OrtSp of F
for a being Element of S holds a _|_
let S be OrtSp of F; :: thesis: for a being Element of S holds a _|_
let a be Element of S; :: thesis: a _|_
set 0F = 0. F;
set 0V = 0. S;

A1: now

assume not a _|_ ; :: thesis: a _|_
then consider m being Element of F such that
A2: a _|_ by Def2;
a _|_ by A2, Def2;
hence a _|_ by VECTSP_1:14; :: thesis: verum

end;

now

assume a _|_ ; :: thesis: a _|_
then a _|_ by Def2;
hence a _|_ by VECTSP_1:14; :: thesis: verum

end;

hence a _|_ by A1; :: thesis: verum