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

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 A2, VECTSP_1:def 9;

assume l * a _|_ ; :: thesis: contradiction

then b _|_ by Th2;

then b _|_ by Def1;

then b _|_ by A4, VECTSP_1:def 16;

then b _|_ by VECTSP_1:def 17;

hence contradiction by A1, Th2; :: thesis: verum

end;A4: k * l = 1_ F by A2, VECTSP_1:def 9;

assume l * a _|_ ; :: thesis: contradiction

then b _|_ by Th2;

then b _|_ by Def1;

then b _|_ by A4, VECTSP_1:def 16;

then b _|_ by VECTSP_1:def 17;

hence contradiction by A1, Th2; :: thesis: verum

now :: thesis: not a _|_

hence
( not a _|_ & not l * a _|_ )
by A3; :: thesis: verumconsider k being Element of F such that

A5: k * l = 1_ F by A2, VECTSP_1:def 9;

assume a _|_ ; :: thesis: contradiction

then a _|_ by Def1;

then a _|_ by A5, VECTSP_1:def 16;

hence contradiction by A1, VECTSP_1:def 17; :: thesis: verum

end;A5: k * l = 1_ F by A2, VECTSP_1:def 9;

assume a _|_ ; :: thesis: contradiction

then a _|_ by Def1;

then a _|_ by A5, VECTSP_1:def 16;

hence contradiction by A1, VECTSP_1:def 17; :: thesis: verum