let F be Field; :: thesis: for S being SymSp of F
for b, a, x being Element of S
for k, l being Element of F st not a _|_ & a _|_ & a _|_ holds
k = l
let S be SymSp of F; :: thesis: for b, a, x being Element of S
for k, l being Element of F st not a _|_ & a _|_ & a _|_ holds
k = l
let b, a, 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 )
assume that
A1: not a _|_ and
A2: ( a _|_ & a _|_ ) ; :: thesis: k = l
set 1F = 1_ F;
a _|_ by A2, Th23;
then a _|_ by VECTSP_1:59;
then a _|_ by VECTSP_1:def 26;
then a _|_ by VECTSP_1:41;
then a _|_ by VECTSP_1:def 19;
then a _|_ by VECTSP_1:def 26;
then a _|_ by Def1;
then A3: a _|_ by VECTSP_1:def 26;
assume not k = l ; :: thesis: contradiction
then k - l <> 0. F by RLVECT_1:35;
then a _|_ by A3, VECTSP_1:def 22;
hence contradiction by A1, VECTSP_1:def 26; :: thesis: verum