let F be Field; :: thesis: for S being SymSp of F
for a, b being Element of S st b _|_ holds
a _|_
let S be SymSp of F; :: thesis: for a, b being Element of S st b _|_ holds
a _|_
let a, b be Element of S; :: thesis: ( b _|_ implies a _|_ )
set 0V = 0. S;
assume b _|_ ; :: thesis: a _|_
then A1: (0. S) + b _|_ by RLVECT_1:4;
b + a _|_ by Th1;
then a + (0. S) _|_ by A1, Def1;
hence a _|_ by RLVECT_1:4; :: thesis: verum