let F be Field; :: thesis: for S being SymSp of F
for b, a 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 SymSp of F; :: thesis: for b, a being Element of S
for l being Element of F st not a _|_ & not l = 0. F holds
( not a _|_ & not l * a _|_ )
let b, a 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

consider k being Element of F such that
A4: k * l = 1. F by A2, VECTSP_1:def 20;
assume l * a _|_ ; :: thesis: contradiction
then b _|_ by Th12;
then b _|_ by Def1;
then b _|_ by A4, VECTSP_1:def 28, VECTSP_1:def 29;
then b _|_ by VECTSP_1:def 29;
hence contradiction by A1, Th12; :: thesis: verum

end;

now

consider k being Element of F such that
A5: k * l = 1. F by A2, VECTSP_1:def 20;
assume a _|_ ; :: thesis: contradiction
then a _|_ by Def1;
then a _|_ by A5, VECTSP_1:def 28, VECTSP_1:def 29;
hence contradiction by A1, VECTSP_1:def 29; :: thesis: verum

end;

hence ( not a _|_ & not l * a _|_ ) by A3; :: thesis: verum