let F be Field; :: thesis: for S being SymSp 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 SymSp 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 )
assume that
A1: not a _|_ and
A2: ( a _|_ & a _|_ ) ; :: thesis: k = l
set 1F = 1_ F;
a _|_ by A2, Th11;
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; :: thesis: verum