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;

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 _|_ )

hence
a _|_
by A1; :: thesis: verumassume
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;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