let F be Field; :: thesis: 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 _|_ )

let S be OrtSp of F; :: thesis: 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 _|_ )

let a, b be Element of S; :: thesis: for l being Element of F st not a _|_ & not l = 0. F holds
( not a _|_ & not l * a _|_ )

let l be Element of F; :: thesis: ( not a _|_ & not l = 0. F implies ( not a _|_ & not l * a _|_ ) )
set 1F = 1_ F;
assume that
A1: not a _|_ and
A2: not l = 0. F ; :: thesis: ( not a _|_ & not l * a _|_ )
A3: now :: thesis: not l * a _|_
consider k being Element of F such that
A4: k * l = 1_ F by ;
assume l * a _|_ ; :: thesis: contradiction
then b _|_ by Th2;
then b _|_ by Def1;
then b _|_ by ;
then b _|_ by VECTSP_1:def 17;
hence contradiction by A1, Th2; :: thesis: verum
end;
now :: thesis: not a _|_
consider k being Element of F such that
A5: k * l = 1_ F by ;
assume a _|_ ; :: thesis: contradiction
then a _|_ by Def1;
then a _|_ by ;
hence contradiction by A1, VECTSP_1:def 17; :: thesis: verum
end;
hence ( not a _|_ & not l * a _|_ ) by A3; :: thesis: verum