let F be Field; :: thesis: for S being OrtSp of F

for a, b, x being Element of S

for k, l being Element of F st not a _|_ & a _|_ & a _|_ holds

k = l

let S be OrtSp of F; :: thesis: for a, b, x being Element of S

for k, l being Element of F st not a _|_ & a _|_ & a _|_ holds

k = l

let a, b, x be Element of S; :: thesis: for k, l being Element of F st not a _|_ & a _|_ & a _|_ holds

k = l

let k, l be Element of F; :: thesis: ( not a _|_ & a _|_ & a _|_ implies k = l )

set 1F = 1_ F;

assume that

A1: not a _|_ and

A2: ( a _|_ & a _|_ ) ; :: thesis: k = l

a _|_ by A2, Th7;

then a _|_ by VECTSP_1:14;

then a _|_ by VECTSP_1:def 16;

then a _|_ by VECTSP_1:9;

then a _|_ ;

then a _|_ by VECTSP_1:def 15;

then a _|_ by Def1;

then A3: a _|_ by VECTSP_1:def 16;

assume not k = l ; :: thesis: contradiction

then k - l <> 0. F by RLVECT_1:21;

then a _|_ by A3, VECTSP_1:def 10;

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

for a, b, x being Element of S

for k, l being Element of F st not a _|_ & a _|_ & a _|_ holds

k = l

let S be OrtSp of F; :: thesis: for a, b, x being Element of S

for k, l being Element of F st not a _|_ & a _|_ & a _|_ holds

k = l

let a, b, x be Element of S; :: thesis: for k, l being Element of F st not a _|_ & a _|_ & a _|_ holds

k = l

let k, l be Element of F; :: thesis: ( not a _|_ & a _|_ & a _|_ implies k = l )

set 1F = 1_ F;

assume that

A1: not a _|_ and

A2: ( a _|_ & a _|_ ) ; :: thesis: k = l

a _|_ by A2, Th7;

then a _|_ by VECTSP_1:14;

then a _|_ by VECTSP_1:def 16;

then a _|_ by VECTSP_1:9;

then a _|_ ;

then a _|_ by VECTSP_1:def 15;

then a _|_ by Def1;

then A3: a _|_ by VECTSP_1:def 16;

assume not k = l ; :: thesis: contradiction

then k - l <> 0. F by RLVECT_1:21;

then a _|_ by A3, VECTSP_1:def 10;

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