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 A1: ( not a _|_ & not l = 0. F ) ; :: thesis: ( not a _|_ & not l * a _|_ )

A2: now

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

end;

now

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

end;

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