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 :: thesis: ( not a _|_ implies a _|_ )

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

end;

now :: thesis: ( a _|_ implies a _|_ )

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

end;

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