let F be Field; :: thesis: for S being SymSp of F
for a being Element of S st (1_ F) + (1_ F) <> 0. F holds
a _|_
let S be SymSp of F; :: thesis: for a being Element of S st (1_ F) + (1_ F) <> 0. F holds
a _|_
let a be Element of S; :: thesis: ( (1_ F) + (1_ F) <> 0. F implies a _|_ )
set 1F = 1_ F;
assume A1: (1_ F) + (1_ F) <> 0. F ; :: thesis: a _|_

now :: thesis: ( a <> 0. S implies a _|_ )

assume a <> 0. S ; :: thesis: a _|_
then consider c being Element of S such that
A2: not a _|_ by Def1;
consider k being Element of F such that
A3: a _|_ by A2, Def1;
a + (- (k * c)) _|_ by A3, Th2;
then a + a _|_ by Def1;
then a + ((1_ F) * a) _|_ ;
then ((1_ F) * a) + ((1_ F) * a) _|_ ;
then ((1_ F) * a) + ((1_ F) * a) _|_ by VECTSP_1:14;
then ((1_ F) + (1_ F)) * a _|_ by VECTSP_1:def 15;
then ((1_ F) + (1_ F)) * a _|_ by VECTSP_1:def 16;
then ((1_ F) + (1_ F)) * a _|_ by VECTSP_1:9;
then ((1_ F) + (1_ F)) * a _|_ ;
then (- k) * c _|_ by Th2;
then (- k) * c _|_ by Def1;
then (- k) * c _|_ by A1, VECTSP_1:20;
then A4: a _|_ by Th2;
a _|_ by A3, VECTSP_1:21;
hence a _|_ by A4, Th4; :: thesis: verum

end;

hence a _|_ by Th1; :: thesis: verum