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

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

end;

now :: thesis: not a _|_

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

end;

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